Update

src/thue_morse3.v

@@ -308,7 +308,8 @@ Qed.
 
 
 (* palidrome 2*4 : soit centré en 4n soit pas plus de 2*6 *)
-(* modifier l'énoncé : ajouter le modulo = 2 ET la différence sur le 7ème *)
+(* modifier l'énoncé : ajouter le modulo = 2 ET la différence sur le 7ème
+      ET existence d'un palindrome 2 * - *)
 Lemma tm_step_palindromic_length_8 :
   forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ (rev a) ++ tl
@@ -687,12 +688,23 @@ reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H.
                    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 ?
-                     TFT TFT FF TFT TFT
+                  FTTFTFFT FTTFTF  (pb avec le repeating_pattern de 8 ???)
+                     TFT TFT FF TFT TFT (si on part sur 2 mod 8)
+                                        (idem en partant de la droite pour 6 mod 8)
                      revoir l'énoncé en fonction
+
+Le lemme repeating_patterns se base sur les huit premiers termes de TM :
+[False, True, True, False, True, False, False, True]
+  --> il y a une contradiction à chaque fois
+
+
   *)
 
 
 
+Admitted.
+
+
 
 
                   
@@ -701,19 +713,6 @@ reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H.
 
 
 
-
-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
 
 
@@ -748,6 +747,54 @@ Lemma tm_step_factor4_3mod4 : forall (n' : nat) (w z y : list bool),
       F T | F T | T F ][ F T | T F | T F
                       4n   (par examen des cinq premiers termes à gauche)
 
+   *)
+
+
+Lemma tm_step_palindromic_length_12 :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ rev a ++ tl
+  -> 6 < length a
+  -> length (hd ++ a) mod 4 = 0.
+Proof.
+  intros n hd a tl. intros H I.
+  assert (J: even (length (hd ++ a)) = true).
+  assert (0 < length a).
+  apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
+  apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
+  apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
+  assumption. generalize H0. generalize H.
+  apply tm_step_palindromic_even_center.
+  apply even_mod4 in J. destruct J. assumption.
+
+  rewrite <- firstn_skipn with (l := a) (n := length a - 4) in H.
+  rewrite rev_app_distr in H. rewrite <- app_assoc in H.
+  rewrite app_assoc in H.
+  assert (length (skipn (length a - 4) a) = 4). rewrite skipn_length.
+  replace (length a) with ((length a - 4) + 4) at 1. rewrite Nat.add_comm.
+  rewrite Nat.add_sub. reflexivity. rewrite Nat.add_comm.
+  rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. reflexivity.
+  apply Nat.le_refl. apply Nat.lt_le_incl.
+  apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
+  assumption.
+
+  pose (hd' := hd ++ firstn (length a - 4) a). fold hd' in H.
+  pose (a' := skipn (length a - 4) a). fold a' in H.
+  rewrite <- app_assoc in H.
+  pose (tl' := rev (firstn (length a - 4) a) ++ tl). fold tl' in H.
+
+  assert (K: length (hd' ++ a') mod 4 = 0
+                \/ last hd' false <> List.hd false tl').
+  fold a' in H1. generalize H1. generalize H.
+  apply tm_step_palindromic_length_8.
+  destruct K.
+
+
+
+
+
+
+
+
 
 Lemma tm_step_proper_palindromic_center :
   forall (m n k i: nat) (hd a tl : list bool),