Update

src/thue_morse.v

@@ -113,6 +113,22 @@ Proof.
   assumption.
 Qed.
 
+Lemma even_mod4 : forall n : nat,
+  even n = true -> n mod 4 = 0 \/ n mod 4 = 2.
+Proof.
+  intro n. intro H.
+  assert (K: 0 = n mod 2).
+  apply Nat.mod_unique with (q := Nat.div2 n). apply Nat.lt_0_2.
+  replace (0) with (Nat.b2n (Nat.odd n)) at 2.
+  apply Nat.div2_odd. rewrite <- Nat.negb_even. rewrite H. reflexivity.
+  assert (L: n mod (2*2) = n mod 2 + 2 * ((n / 2) mod 2)).
+  apply Nat.mod_mul_r; easy. rewrite <- K in L.
+  replace (2*2) with (4) in L. rewrite <- Nat.bit0_mod in L.
+  rewrite L.
+  destruct (Nat.testbit (n / 2) 0) ; [right | left] ; reflexivity.
+  reflexivity.
+Qed.
+
 Lemma odd_mod4 : forall n : nat,
   odd n = true -> n mod 4 = 1 \/ n mod 4 = 3.
 Proof.
@@ -120,7 +136,7 @@ Proof.
   assert (K: 1 = n mod 2).
   apply Nat.mod_unique with (q := Nat.div2 n). apply Nat.lt_1_2.
   replace (1) with (Nat.b2n (Nat.odd n)) at 2.
-  apply Nat.div2_odd. rewrite H.  reflexivity.
+  apply Nat.div2_odd. rewrite H. reflexivity.
   assert (L: n mod (2*2) = n mod 2 + 2 * ((n / 2) mod 2)).
   apply Nat.mod_mul_r; easy. rewrite <- K in L.
   replace (2*2) with (4) in L. rewrite <- Nat.bit0_mod in L.

src/thue_morse3.v

@@ -313,8 +313,7 @@ Lemma tm_step_palindromic_length_8 :
   forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ (rev a) ++ tl
   -> length a = 4
-  -> length (hd ++ a) mod 4 = 2
-       \/ (length (hd ++ a) mod 4 = 0 /\ last hd false <> List.hd false tl).
+  -> length (hd ++ a) mod 4 = 0 \/ last hd false <> List.hd false tl.
 Proof.
   intros n hd a tl. intros H I.
 
@@ -323,6 +322,9 @@ Proof.
   assert (0 < length a). rewrite I. apply Nat.lt_0_succ. generalize H0.
   generalize H. apply tm_step_palindromic_even_center.
 
+  assert (M: length (hd ++ a) mod 4 = 0 \/ length (hd ++ a) mod 4 = 2).
+  generalize P. apply even_mod4.
+
   (* proof that length hd is even *)
   assert (Q: even (length hd) = true). rewrite app_length in P.
   rewrite Nat.even_add_even in P. assumption. rewrite I.
@@ -441,15 +443,90 @@ Proof.
   apply tm_step_cubefree in H. contradiction H. reflexivity.
   apply Nat.lt_0_1. reflexivity.
 
+  (* à ce stade on a F T | T F || F T T F
+        trois cas :
+              (??? T) | F T T F || F T T F | ???   impossible à gauche
+                (T F) | F T T F || F T T F | (F T)  cube
+                (T F) | F T T F || F T T F | (T F)   OK, diff + impossible à droite
+   *)
+  rewrite app_removelast_last with (l := b3::hd) (d := false) in H.
+  rewrite <- app_assoc in H.
+  assert ({last (b3::hd) false=b1} + {~ last (b3::hd) false=b1}).
+  apply bool_dec. destruct H1. rewrite e0 in H.
+  (* un cas à étudier 
+                (??? T) | F T T F || F T T F | ???   impossible à gauche
+  *)
+  destruct M. left. assumption. (* ici on postule le modulo = 2 *)
+
+  rewrite app_removelast_last with (l := b3::hd) (d := false) in Q.
+  rewrite last_length in Q. rewrite Nat.even_succ in Q. apply odd_mod4 in Q.
+  rewrite app_removelast_last with (l := b3::hd) (d := false) in H1.
+  destruct Q.
+  assert (exists x, firstn 2 [b1;b;b1;b1] = [x;x]). generalize H2.
+  assert (length [b1;b;b1;b1] = 4). reflexivity. generalize H3.
+  replace (
+    removelast (b3 :: hd) ++
+    [b1] ++ b :: b1 :: b1 :: b2 :: b2 :: b1 :: b1 :: b :: b4 :: tl )
+    with (
+    removelast (b3 :: hd) ++ [b1;b;b1;b1]
+      ++ (b2 :: b2 :: b1 :: b1 :: b :: b4 :: tl )) in H.
+  generalize H. apply tm_step_factor4_1mod4. reflexivity.
+  destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
+  contradiction n1. reflexivity.
+
+  rewrite app_length in H1. rewrite app_length in H1.
+  rewrite <- Nat.add_assoc in H1. rewrite <- Nat.add_mod_idemp_l in H1.
+  rewrite H2 in H1. inversion H1. easy. easy. easy.
+
+  (* Deux cas
+                (T F) | F T T F || F T T F | (F T)  cube
+                (T F) | F T T F || F T T F | (T F)  impossible à droite
+  *)
+  assert ({b4=b1} + {~ b4=b1}). apply bool_dec. destruct H1. rewrite e0 in H.
+     (* un sous-cas :
+                (T F) | F T T F || F T T F | (T F)  impossible à droite
+      *)
 
 
-  (* à ce stade on a F T | T F || F T T F *)
 
 
 
 
 
 
+  (* sinon, sur la base de    T F T F || F T F T
+        quatre cas :
+                (F T) | T F T F || F T F T | (F T)     diff + impossible à droite
+                (F T) | T F T F || F T F T | (T F)     4n+2    a/rev a/a possible ?
+     empiriquement : n'apparaît jamais
+                   remonter encore d'un cran et prouver la différence à ce stade,
+                TFFT TFTF FTFT TFFT (µ de TF TT FF TF) pourquoi impossible ?
+                FTFT TFTF FTFT TFTF (µ de FF TT FF TT) pourquoi impossible ?
+                     revoir l'énoncé en fonction
+                (T F) | T F T F || F T F T | (F T)     cube
+                (T F) | T F T F || F T F T | (T F)     diff + impossible à gauche
+
+
+   *)
+                  
+
+
+
+
+
+
+Lemma tm_step_factor4_1mod4 : forall (n' : nat) (w z y : list bool),
+    tm_step n' = w ++ z ++ y
+    -> length z = 4 -> length w mod 4 = 1
+    -> exists (x : bool), firstn 2 z = [x;x].
+Lemma tm_step_factor4_3mod4 : forall (n' : nat) (w z y : list bool),
+    tm_step n' = w ++ z ++ y
+    -> length z = 4 -> length w mod 4 = 3
+    -> exists (x : bool), skipn 2 z = [x;x].
+
+
+
+
   (* si on a ensuite le bloc précédent identique aux deux premiers de a