Update

src/thue_morse2.v

@@ -392,14 +392,7 @@ Proof.
 Qed.
 
 
-
-
-
-
-
-
-
-Theorem tm_step_square_pos_even : forall (n : nat) (hd a tl : list bool),
+Lemma tm_step_square_pos_even : forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ a ++ tl
   -> 0 < length a
   -> odd (length hd) = true
@@ -495,8 +488,7 @@ Proof.
 Qed.
 
 
-
-Theorem tm_step_square_pos_even' : forall (n : nat) (hd a tl : list bool),
+Lemma tm_step_square_pos_even' : forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ a ++ tl
   -> 0 < length a
   -> odd (length hd) = true
@@ -608,6 +600,136 @@ Proof.
 Qed.
 
 
+Lemma tm_step_square_pos_even'' : forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ a ++ tl
+  -> 0 < length a
+  -> odd (length hd) = true
+  -> even (length a) = true
+  -> exists (hd' a' tl' : list bool),
+     tm_step n = hd' ++ a' ++ a' ++ tl'
+     /\ odd (length hd') = true
+     /\ even (length a') = true
+     /\ length a' < length a.
+Proof.
+  intros n hd a tl. intros H I J K.
+
+  assert (L: exists (hd' a' tl' : list bool),
+     tm_step n = hd' ++ a' ++ a' ++ tl'
+     /\ length hd' = S (length hd) /\ length a' = length a).
+  generalize K. generalize J. generalize I. generalize H.
+  apply tm_step_square_pos_even.
+
+  assert (M: exists (hd' a' tl' : list bool),
+     tm_step n = hd' ++ a' ++ a' ++ tl'
+     /\ length hd' = Nat.pred (length hd) /\ length a' = length a).
+  generalize K. generalize J. generalize I. generalize H.
+  apply tm_step_square_pos_even'.
+
+  destruct L as [hd' L2]. destruct L2 as [a' L3]. destruct L3 as [tl' L].
+  destruct M as [hd'' M2]. destruct M2 as [a'' M3]. destruct M3 as [tl'' M].
+  destruct L as [L1 L2]. destruct L2 as [L2 L3].
+  destruct M as [M1 M2]. destruct M2 as [M2 M3].
+
+  assert (N: 0 < n).
+  generalize K. generalize I. generalize H. apply tm_step_not_nil_factor_even.
+  destruct n. inversion N.
+
+  assert (L4: even (length hd') = true). rewrite L2. rewrite Nat.even_succ.
+  assumption.
+  assert (M4: even (length hd'') = true). rewrite M2. rewrite Nat.even_pred.
+  assumption. destruct hd. inversion J. easy.
+
+  rewrite <- tm_step_lemma in L1.
+  assert (L5: hd' = tm_morphism (firstn (Nat.div2 (length hd')) (tm_step n))).
+  generalize L4. generalize L1. apply tm_morphism_app2.
+
+  rewrite <- tm_step_lemma in M1.
+  assert (M5: hd'' = tm_morphism (firstn (Nat.div2 (length hd'')) (tm_step n))).
+  generalize M4. generalize M1. apply tm_morphism_app2.
+  
+  assert (L6: a' ++ a' ++ tl'
+      = tm_morphism (skipn (Nat.div2 (length hd')) (tm_step n))).
+  generalize L4. generalize L1. apply tm_morphism_app3.
+  
+  assert (M6: a'' ++ a'' ++ tl''
+      = tm_morphism (skipn (Nat.div2 (length hd'')) (tm_step n))).
+  generalize M4. generalize M1. apply tm_morphism_app3.
+
+  assert (L7: even (length a') = true). rewrite L3. assumption.
+  assert (L8: a' = tm_morphism (firstn (Nat.div2 (length a'))
+         (skipn (Nat.div2 (length hd')) (tm_step n)))).
+  generalize L7. symmetry in L6. generalize L6. apply tm_morphism_app2.
+
+  assert (M7: even (length a'') = true). rewrite M3. assumption.
+  assert (M8: a'' = tm_morphism (firstn (Nat.div2 (length a''))
+         (skipn (Nat.div2 (length hd'')) (tm_step n)))).
+  generalize M7. symmetry in M6. generalize M6. apply tm_morphism_app2.
+
+  rewrite app_assoc in L6. symmetry in L6.
+  rewrite app_assoc in M6. symmetry in M6.
+
+  assert (L9: even (length (a' ++ a')) = true). rewrite app_length.
+  rewrite Nat.even_add. rewrite L7. reflexivity.
+
+  assert (M9: even (length (a'' ++ a'')) = true). rewrite app_length.
+  rewrite Nat.even_add. rewrite M7. reflexivity.
+
+  assert (L10: tl' = tm_morphism (skipn (Nat.div2 (length (a' ++ a')))
+       (skipn (Nat.div2 (length hd')) (tm_step n)))).
+  generalize L9. generalize L6. apply tm_morphism_app3.
+
+  assert (M10: tl'' = tm_morphism (skipn (Nat.div2 (length (a'' ++ a'')))
+       (skipn (Nat.div2 (length hd'')) (tm_step n)))).
+  generalize M9. generalize M6. apply tm_morphism_app3.
+
+  rewrite L5 in L1. rewrite L8 in L1. rewrite L10 in L1.
+  rewrite <- tm_morphism_app in L1. rewrite <- tm_morphism_app in L1.
+  rewrite <- tm_morphism_app in L1. rewrite <- tm_morphism_eq in L1.
+
+  rewrite M5 in M1. rewrite M8 in M1. rewrite M10 in M1.
+  rewrite <- tm_morphism_app in M1. rewrite <- tm_morphism_app in M1.
+  rewrite <- tm_morphism_app in M1. rewrite <- tm_morphism_eq in M1.
+
+  assert (Nat.Even (Nat.div2 (length hd')) \/ Nat.Odd (Nat.div2 (length hd'))).
+  apply Nat.Even_or_Odd. destruct H0.
+
+  (* case Nat.div2 (length hd'') has an odd length *)
+  - assert( odd (Nat.div2 (length hd'')) = true).
+    apply eq_S in M2. rewrite Nat.succ_pred_pos in M2.
+    apply eq_S in M2. rewrite <- L2 in M2. rewrite <- M2 in H0.
+
+
+
+  (*
+  assert (L9: a' ++ a' = a' ++ a'). reflexivity.
+  rewrite L8 in L9 at 4. rewrite L8 in L9 at 3.
+  rewrite <- tm_morphism_app in L9.
+
+  assert (M9: a'' ++ a'' = a'' ++ a''). reflexivity.
+  rewrite M8 in M9 at 4. rewrite M8 in M9 at 3.
+  rewrite <- tm_morphism_app in M9.
+   *)
+  
+
+
+
+
+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).
+
+
+
+
+
+
+
     (* TODO: utiliser tm_step_odd_prefix_square pour le cas impair *)
     (* TODO: la taille du facteur divise la taille du préfixe ? *)
     (* TODO : le cas de la taille 2 est un cas pair facile