Update

thue-morse.v

@@ -829,48 +829,60 @@ Proof.
     reflexivity.
 Qed.
 
+Lemma tm_step_consecutive_pow2 :
+  forall (n k : nat) (l1 l2 : list bool) (b1 b2 b1' b2': bool),
+  tm_step n = l1 ++ b1 :: b2 :: l2
+    -> 2^k > S (length l1)
+      -> 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').
+Proof.
+  intros n k l1 l2 b1 b2 b1' b2'.
+  intros.
+Admitted.
 
 
 Require Import BinPosDef.
 
-(* utiliser Pos.pred à partir de 2 *)
-(* donc théorème sur S (S n)   *)
-Compute let b := Pos.of_nat 6 in Pos.lxor b (Pos.pred b).
-Compute let b := Pos.of_nat 3 in Pos.pred b.
-Compute let b := Pos.of_nat 7 in
-   Pos.size_nat (
-     match Pos.lxor b (Pos.pred b) with
-     | N0 => BinNums.xH (* arbitrary, never used *)
-     | Npos(p)  => p
-     end).
 
-Compute tm_step 4.
-(*
-= [false; true; true; false; true; false; false; true; true; false;
-        false; true; false; true; true; false]
- *)
+(* Autre construction de la suite, ici n est le nombre de termes *)
+Fixpoint tm_bin (n: nat) : list bool :=
+  match n with
+  | 0 => nil
+  | S n' => let t := tm_bin n' in
+            let m := Pos.of_nat n' in
+              (xorb (hd false t)
+                (odd (Pos.size_nat
+         match Pos.lxor m (Pos.pred m) with
+         | N0 => BinNums.xH
+         | Npos(p)  => p
+         end))) :: t
+  end.
 
-(* on suppose que len est la longueur de la liste qui précède b0 et b1 *)
-Compute let mylen := 5 in
-  let ind_b1 := Pos.of_nat (S mylen) in (* index of b1 *)
-  let ind_b0 := Pos.pred ind_b1 in (* index of b0 *)
-   even (Pos.size_nat (
-     match Pos.lxor ind_b0 ind_b1 with
-     | N0 => BinNums.xH (* arbitrary, never used *)
-     | Npos(p)  => p
-     end)).
 
 Theorem tm_step_consecutive : forall (n : nat) (l1 l2 : list bool) (b1 b2 : bool),
   tm_step n = l1 ++ b1 :: b2 :: l2 ->
     (eqb b1 b2) = 
       let ind_b2 := Pos.of_nat (S (length l1)) in (* index of b2 *)
       let ind_b1 := Pos.pred ind_b2 in            (* index of b1 *)
-       even (Pos.size_nat (
+       even (Pos.size_nat
          match Pos.lxor ind_b1 ind_b2 with
-         | N0 => BinNums.xH (* arbitrary, never used *)
+         | N0 => BinNums.xH
          | Npos(p)  => p
-         end)).
+         end).
 Proof.
+  intros n l1 l2 b1 b2.
+  destruct n.
+  - simpl. intros H. induction l1.
+    + rewrite app_nil_l in H. discriminate.
+    + destruct l1. rewrite app_nil_l in IHl1. discriminate. discriminate.
+  - rewrite tm_build.
+Admitted.
+
+
+
+
+(*
   intros n l1 l2 b1 b2.
   intros H.
   induction l1.
@@ -880,8 +892,8 @@ Proof.
     assert (J: tl (tl (tm_morphism (tm_step n))) = l2).
     { replace (tm_morphism (tm_step n)) with (tm_step (S n)).
       rewrite H. reflexivity. reflexivity. }
-    rewrite J. intros. rewrite <- H1. rewrite <- H2. reflexivity.
-  - 
+    (* rewrite J *) intros. rewrite <- H1. rewrite <- H2. reflexivity.
+  - replace (S (length (a :: l1))) with (S (S (length l1))).
 
 
 
@@ -924,3 +936,4 @@ Proof.
 
 Lemma tm_step_head_2 : forall (n : nat),
     tm_step (S n) = false :: true :: tl (tl (tm_step (S n))).
+ *)