Update

thue-morse.v

@@ -682,6 +682,8 @@ 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 Nat.
+Require Import Bool.
+
 Import ListNotations.
 
 Fixpoint tm_morphism (l:list bool) : list bool :=
@@ -713,7 +715,7 @@ Proof.
   induction l.
   - reflexivity.
   - simpl. rewrite IHl. replace (negb (negb a)) with (a).
-    reflexivity. rewrite Bool.negb_involutive. reflexivity.
+    reflexivity. rewrite negb_involutive. reflexivity.
 Qed.
 
 Lemma tm_morphism_concat : forall (l1 l2 : list bool),
@@ -734,7 +736,7 @@ Proof.
     rewrite IHl. rewrite tm_morphism_concat.
     rewrite <- app_assoc.
     replace (map negb [a]) with ([negb a]). simpl.
-    rewrite Bool.negb_involutive. reflexivity.
+    rewrite negb_involutive. reflexivity.
     reflexivity.
 Qed.
 
@@ -804,7 +806,7 @@ Proof.
     rewrite IHn. simpl tm_morphism. simpl tl.
     rewrite PeanoNat.Nat.even_succ.
     rewrite PeanoNat.Nat.odd_succ.
-    rewrite Bool.negb_involutive.
+    rewrite negb_involutive.
     reflexivity. reflexivity.
 Qed.
 
@@ -827,3 +829,97 @@ Proof.
     reflexivity.
 Qed.
 
+
+
+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]
+ *)
+
+(* 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 (
+         match Pos.lxor ind_b1 ind_b2 with
+         | N0 => BinNums.xH (* arbitrary, never used *)
+         | Npos(p)  => p
+         end)).
+Proof.
+  intros n l1 l2 b1 b2.
+  intros H.
+  induction l1.
+  - simpl. destruct n. discriminate.
+    rewrite app_nil_l in H. assert (I := H).
+    rewrite tm_step_head_2 in I. injection I.
+    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. 
+
+
+
+
+
+
+
+    destruct b1 in H.
+    + destruct b2 in H.
+      (* Case 1: b1 = true, b2 = true  (false)   *)
+      replace (l2) with (tl (tl (tm_step (S n)))) in H.
+      assert (J : tm_step (S n) = false :: true :: tl (tl (tm_step (S n)))).
+      apply tm_step_head_2. rewrite J in H. discriminate H. rewrite H. reflexivity.
+      (* Case 2: b1 = true, b2 = false  (false)   *)
+      replace (l2) with (tl (tl (tm_step (S n)))) in H.
+      assert (J : tm_step (S n) = false :: true :: tl (tl (tm_step (S n)))).
+      apply tm_step_head_2. rewrite J in H. discriminate H. rewrite H. reflexivity.
+    + destruct b2.
+      (* Case 3: b1 = false, b2 = true  (TRUE)   *)
+      discriminate.
+
+
+
+
+
+
+    inversion H.
+    discriminate tm_step_head_2.
+    rewrite <- tm_step_head_2 in H.
+    discriminate H.
+    discriminate tm_step_head_2.
+
+  - simpl. simpl. simpl in H.
+    destruct n in H. discriminate H.
+    replace (l2) with (tl (tl (tm_step (S n)))) in H.
+    specialize (H tm_step_head_2).
+    rewrite <- tm_step_head_2 in H.
+
+
+
+Lemma tm_step_head_2 : forall (n : nat),
+    tm_step (S n) = false :: true :: tl (tl (tm_step (S n))).