Update

thue-morse.v

@@ -849,7 +849,22 @@ Proof.
 Qed.
 
 
-
+Lemma tm_morphism_app3 : forall (l hd tl : list bool),
+  tm_morphism l = hd ++ tl
+  -> even (length hd) = true
+  -> tl = tm_morphism (skipn (Nat.div2 (length hd)) l).
+Proof.
+  intros l hd tl. intros H I.
+  assert (J: hd = tm_morphism (firstn (Nat.div2 (length hd)) l)).
+  generalize I. generalize H. apply tm_morphism_app2.
+  assert (K: l = (firstn (Nat.div2 (length hd)) l) ++ (skipn (Nat.div2 (length hd)) l)).
+  symmetry. apply firstn_skipn.
+  assert (L: tm_morphism l = (tm_morphism (firstn (Nat.div2 (length hd)) l))
+                          ++ (tm_morphism (skipn (Nat.div2 (length hd)) l))).
+  rewrite K at 1. apply tm_morphism_app.
+  rewrite H in L. rewrite <- J in L.
+  rewrite app_inv_head_iff in L. assumption.
+Qed.
 
 
 (*
@@ -1216,6 +1231,28 @@ Proof.
 Qed.
 
 
+Lemma tm_step_cube6 : forall (n : nat) (a hd tl: list bool),
+  tm_step n = hd ++ a ++ a ++ a ++ tl
+  -> 0 < length a
+  -> exists (hd2 b tl2 : list bool), tm_step (Nat.pred n) = hd2 ++ b ++ b ++ b ++ tl2.
+Proof.
+  intros n a hd tl. intros H I.
+  assert(J: exists (hd2 b tl2 : list bool), tm_step n = hd2 ++ b ++ b ++ b ++ tl2
+                         /\ length a = length b
+                         /\ even (length hd2) = true).
+  generalize I. generalize H. apply tm_step_cube5.
+  destruct J as [ hd2 J0]. destruct J0 as [ b J1]. destruct J1 as [ tl2 J2].
+  destruct J2 as [J3 J4]. destruct J4 as [J5 J6].
+  assert (J: even (length b) = true). generalize J3. apply tm_step_cube1.
+  
+  assert (K: 0 < n). generalize I. generalize H. apply tm_step_cube2.
+  destruct n.
+  - apply Nat.lt_irrefl in K. contradiction K.
+  - rewrite <- tm_step_lemma in J3.
+    assert (L: hd2 = tm_morphism (firstn (Nat.div2 (length hd2)) (tm_step n))).
+    generalize J6. generalize J3. apply tm_morphism_app2.
+    assert (M: b ++ b ++ b ++ tl2 = tm_morphism (skipn (Nat.div2 (length hd2)) (tm_step n))).
+    generalize J6. generalize J3. apply tm_morphism_app3.
 
 
 
@@ -1223,6 +1260,19 @@ Qed.
 
 
 
+
+Lemma tm_morphism_app2 : forall (l hd tl : list bool),
+  tm_morphism l = hd ++ tl
+  -> even (length hd) = true
+  -> hd = tm_morphism (firstn (Nat.div2 (length hd)) l).
+
+Lemma tm_morphism_app3 : forall (l hd tl : list bool),
+  tm_morphism l = hd ++ tl
+  -> even (length hd) = true
+  -> tl = tm_morphism (skipn (Nat.div2 (length hd)) l).
+
+
+
 Prouver que si un cube existe de taille k, il existe aussi un cube
 de même taille précédé par un préfixe de taille pair (par décalage éventuel de 1)