Update

src/thue_morse2.v

@@ -609,7 +609,8 @@ Lemma tm_step_square_pos_even'' : forall (n : nat) (hd a tl : list bool),
      tm_step n = hd' ++ a' ++ a' ++ tl'
      /\ odd (length hd') = true
      /\ even (length a') = true
-     /\ length a' < length a.
+     /\ length a' < length a
+     /\ 0 < length a'.
 Proof.
   intros n hd a tl. intros H I J K.
 
@@ -756,6 +757,8 @@ Proof.
       apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
       assumption.
 
+      split.
+
       rewrite firstn_length.
       assert (min (Nat.div2 (length a''))
         (length (skipn (Nat.div2 (length hd'')) (tm_step n)))
@@ -764,6 +767,32 @@ Proof.
       assert (Nat.div2 (length a'') < length a). rewrite M3.
       apply Nat.lt_div2. assumption.
       generalize H3. generalize H2. apply Nat.le_lt_trans.
+
+      rewrite firstn_length_le. rewrite M3.
+      rewrite Nat.mul_lt_mono_pos_l with (p := 2).
+      rewrite Nat.mul_0_r. rewrite <- Nat.double_twice.
+      rewrite <- Nat.Even_double. assumption.
+      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
+      apply Nat.lt_0_2.
+
+      rewrite skipn_length.
+      rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd'')).
+      rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
+      rewrite Nat.sub_diag. rewrite Nat.add_0_l.
+      rewrite Nat.mul_le_mono_pos_l with (p := 2).
+      rewrite tm_size_power2. rewrite Nat.mul_add_distr_l.
+      rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
+      rewrite <- Nat.Even_double. rewrite <- Nat.Even_double.
+      rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite M0.
+      rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1.
+      apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl.
+      reflexivity.
+      apply le_0_n.
+      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
+      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
+      apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
+      assumption.
+
     + (* case Nat.div2 (length hd') has an odd length *)
       exists (firstn (Nat.div2 (length hd')) (tm_step n)).
       exists (firstn (Nat.div2 (length a'))
@@ -812,6 +841,8 @@ Proof.
       apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
       assumption.
 
+      split.
+
       rewrite firstn_length.
       assert (min (Nat.div2 (length a'))
         (length (skipn (Nat.div2 (length hd')) (tm_step n)))
@@ -820,6 +851,31 @@ Proof.
       assert (Nat.div2 (length a') < length a). rewrite L3.
       apply Nat.lt_div2. assumption.
       generalize H3. generalize H2. apply Nat.le_lt_trans.
+
+      rewrite firstn_length_le. rewrite L3.
+      rewrite Nat.mul_lt_mono_pos_l with (p := 2).
+      rewrite Nat.mul_0_r. rewrite <- Nat.double_twice.
+      rewrite <- Nat.Even_double. assumption.
+      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
+      apply Nat.lt_0_2.
+
+      rewrite skipn_length.
+      rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd')).
+      rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
+      rewrite Nat.sub_diag. rewrite Nat.add_0_l.
+      rewrite Nat.mul_le_mono_pos_l with (p := 2).
+      rewrite tm_size_power2. rewrite Nat.mul_add_distr_l.
+      rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
+      rewrite <- Nat.Even_double. rewrite <- Nat.Even_double.
+      rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite L0.
+      rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1.
+      apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl.
+      reflexivity.
+      apply le_0_n.
+      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
+      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
+      apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
+      assumption.
   - (* second case, a'0 is odd and we are looking for an even prefix *)
     assert (Nat.Even (Nat.div2 (length hd')) \/ Nat.Odd (Nat.div2 (length hd'))).
     apply Nat.Even_or_Odd. destruct H0.
@@ -900,7 +956,6 @@ Proof.
 
       rewrite firstn_length_le in H2.
 
-
       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.
       rewrite <- Nat.Odd_div2 in H0. rewrite <- Nat.Even_div2 in H0.
@@ -908,7 +963,6 @@ Proof.
       apply Nat.Even_EvenT in H0. apply Nat.EvenT_even in H0.
       rewrite H0 in H2. inversion H2.
 
-
       apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
       apply Nat.OddT_Odd. apply Nat.odd_OddT. rewrite Nat.odd_succ.
       assumption.
@@ -920,7 +974,23 @@ Qed.
 
 
 
-    (* TODO: utiliser tm_step_odd_prefix_square pour le cas impair *)
+
+
+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
+     /\ 0 < length a'.
+
+
+
+
     (* TODO: la taille du facteur divise la taille du préfixe ? *)
     (* TODO : le cas de la taille 2 est un cas pair facile
        grâce à tm_step_factor4_odd_prefix *)