Update

thue-morse.v

@@ -683,7 +683,6 @@ A010060  Thue-Morse sequence: let A_k denote the first 2^k terms; then A_0 = 0 a
 Require Import Coq.Lists.List.
 Require Import PeanoNat.
 Require Import Nat.
-Require Import Nat.
 Require Import Bool.
 
 Import ListNotations.
@@ -1042,51 +1041,64 @@ Proof.
 Qed.
 
 
-
-
-
-
-
-
-
-Lemma tm_step_consecutive_power2 :
-  forall (n k : nat) (l1 l2 : list bool) (b1 b2 b1' b2': bool),
-  tm_step n = l1 ++ b1 :: b2 :: l2
-  -> 2^k >= S (S (length l1)) (* TODO: remplacer par inégalité stricte plus jolie *)
-      -> nth_error (tm_step n) (length l1 + 2^k) = Some b1'
-        -> nth_error (tm_step n) (S (length l1) + 2^k) = Some b2'
-          -> (eqb b1 b2) = (eqb b1' b2').
+Lemma tm_step_repunit : forall (n : nat),
+  nth_error (tm_step n) (2^n - 1) = Some (odd n).
 Proof.
-  intros n k l1 l2 b1 b2 b1' b2'.
-  intros.
-  (* on doit travailler sur tm_step (S k) et remarquer que b1 et b2 sont
-     dans la première moitié *)
-  (* on commence donc déjà par tm_step k pou rmontrer la présence dedans *)
-  assert (2^k < 2^n). {
-      assert (I: nth_error (tm_step n) (length l1 + 2^k) <> None).
-      rewrite H1. easy.
-      rewrite nth_error_Some in I. rewrite tm_size_power2 in I.
-      assert (2^k <= length l1 + 2^k).
-      apply Nat.le_add_l. generalize I. generalize H3. apply Nat.le_lt_trans.
-    }
+  intros n.
+  rewrite nth_error_nth' with (d := false).
+  replace (tm_step n) with (rev (rev (tm_step n))).
+  rewrite rev_nth. rewrite rev_length.
+  rewrite tm_size_power2. rewrite <- Nat.sub_succ_l.
+  rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
+  rewrite Nat.sub_diag. rewrite tm_step_end_1.
+  simpl. reflexivity.
 
-  assert (k < n). { generalize H3. apply Nat.pow_lt_mono_r_iff. 
-    apply Nat.lt_succ_diag_r. }
+  rewrite Nat.le_succ_l. induction n. simpl. apply Nat.lt_0_1.
+  rewrite Nat.mul_lt_mono_pos_r with (p := 2) in IHn.
+  simpl in IHn. rewrite Nat.mul_comm in IHn.
+  rewrite <- Nat.pow_succ_r in IHn. apply IHn.
+  apply Nat.le_0_l. apply Nat.lt_0_2.
 
-    (* montrer que l1 ++ b1 :: b2 :: nil appartient à tm_step k *)
+  rewrite rev_length. rewrite tm_size_power2.
+  rewrite Nat.sub_1_r. apply Nat.lt_pred_l.
+  apply Nat.pow_nonzero. easy.
+
+  rewrite rev_involutive. reflexivity.
+  rewrite tm_size_power2.
+  rewrite Nat.sub_1_r. apply Nat.lt_pred_l.
+  apply Nat.pow_nonzero. easy.
+Qed.
+
+  Nat.mul_lt_mono_neg_r: forall p n m : nat, p < 0 -> n < m <-> m * p < n * p
+
+
+  induction n. simpl. easy. simpl.
+
+
+Nat.le_succ_l: forall n m : nat, S n <= m <-> n < m
+  Nat.le_trans: forall n m p : nat, n <= m -> m <= p -> n <= p
+Nat.pow_nonzero: forall a b : nat, a <> 0 -> a ^ b <> 0
+
+
+rev_nth:
+  forall [A : Type] (l : list A) (d : A) [n : nat],
+  n < length l -> nth n (rev l) d = nth (length l - S n) l d
+
+nth_error_nth:
+  forall [A : Type] (l : list A) (n : nat) [x : A] (d : A),
+  nth_error l n = Some x -> nth n l d = x
+nth_error_nth':
+  forall [A : Type] (l : list A) [n : nat] (d : A),
+  n < length l -> nth_error l n = Some (nth n l d)
+
+Lemma tm_step_end_1 : forall (n : nat),
+  rev (tm_step n) = odd n :: tl (rev (tm_step n)).
 
 
 
-
-
-
-
-  assert (I: exists (l3 : list bool), tm_step k = l1 ++ b1 :: b2 :: l3).
-  { 
-    }
-Admitted.
-
-
+last_length:
+  forall [A : Type] (l : list A) (a : A),
+  length (l ++ a :: nil) = S (length l)
 
 
 
@@ -1096,6 +1108,7 @@ Require Import BinPosDef.
 
 (* Autre construction de la suite, ici n est le nombre de termes *)
 (* la construction se fait à l'envers *)
+(*
 Fixpoint tm_bin_rev (n: nat) : list bool :=
   match n with
   | 0 => nil
@@ -1107,6 +1120,7 @@ Fixpoint tm_bin_rev (n: nat) : list bool :=
                 | Npos(p)  => p
                 end))) :: t
   end.
+*)
 
 Fixpoint tm_bin (n: nat) : list bool :=
   match n with
@@ -1125,6 +1139,15 @@ Proof.
 Admitted.
 
 
+
+
+Déclagae vers la droite de k zéros pour un Bins :
+Pos.iter xO xH 3.   (ici k = 3)
+  --> on ajoute 3 zéros à gauche
+
+
+
+
 Theorem tm_step_consecutive : forall (n : nat) (l1 l2 : list bool) (b1 b2 : bool),
   tm_step n = l1 ++ b1 :: b2 :: l2 ->
     (eqb b1 b2) =