Update

src/thue_morse2.v

@@ -390,7 +390,61 @@ Proof.
     rewrite <- Nat.succ_lt_mono in H0.
     apply Nat.nlt_0_r in H0. contradiction H0.
 Qed.
- 
+
+
+Theorem tm_step_length_even : forall (n : nat),
+  0 < n -> even (length (tm_step n)) = true.
+Proof.
+  intro n. intro H.
+  rewrite tm_size_power2. destruct n. inversion H.
+  rewrite Nat.pow_succ_r'. rewrite Nat.even_mul. reflexivity.
+Qed.
+
+Theorem tm_step_not_nil_factor_even : forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ tl
+  -> 0 < length a
+  -> even (length a) = true
+  -> 0 < n.
+Proof.
+  intros n hd a tl. intros H I J.
+  assert (M: 1 < length (tm_step n)). rewrite H.
+  rewrite app_length. rewrite app_length.
+  assert (0 <= length hd). apply le_0_n.
+  assert (2 <= length a + length tl). rewrite <- Nat.add_0_r at 1.
+  apply Nat.add_le_mono. destruct a. inversion I.
+  destruct a. inversion J. simpl. apply le_n_S. apply le_n_S. apply le_0_n.
+  apply le_0_n. rewrite <- Nat.add_0_l at 1. rewrite <- Nat.le_succ_l.
+  rewrite plus_n_Sm. apply Nat.add_le_mono; assumption.
+  rewrite tm_size_power2 in M.
+  rewrite Nat.pow_lt_mono_r_iff with (a := 2). simpl. assumption.
+  apply Nat.lt_1_2.
+Qed.
+
+Theorem tm_step_tail_not_nil_prefix_odd : forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ tl
+  -> 0 < length a
+  -> odd (length hd) = true
+  -> even (length a) = true
+  -> nil <> tl.
+Proof.
+  intros n hd a tl. intros H I J K.
+  assert (L: 0 < n). generalize K. generalize I. generalize H.
+  apply tm_step_not_nil_factor_even.
+  assert (M: even (length (tm_step n)) = true). generalize L.
+  apply tm_step_length_even.
+  destruct tl. rewrite app_nil_r in H.
+  rewrite H in M. rewrite app_length in M.
+  rewrite Nat.even_add in M. rewrite K in M. rewrite <- Nat.negb_odd in M.
+  rewrite J in M. inversion M. apply nil_cons.
+Qed.
+
+
+
+
+
+
+
+
 
 Theorem tm_step_square_pos_even : forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ a ++ tl
@@ -407,23 +461,15 @@ Proof.
     rewrite H1. reflexivity.
 
     (* proof that tl is not nil *)
-    destruct tl. rewrite app_nil_r in H.
-    assert (length (tm_step n) = length (tm_step n)). reflexivity.
-    rewrite H in H2 at 2.
-    assert (even (length (tm_step n)) = even (length (tm_step n))). reflexivity.
-    rewrite H in H3 at 2. rewrite app_length in H3. rewrite app_length in H3.
-    rewrite Nat.even_add in H3.
-    rewrite Nat.even_add in H3.
-    rewrite H0 in H3. symmetry in H3.
-    rewrite <- Nat.negb_odd in H3. rewrite H1 in H3. simpl in H3.
-    rewrite tm_size_power2 in H3. destruct n.
-    assert (1 < length (hd ++ a ++ a)). rewrite app_length.
-    apply Nat.lt_lt_add_l. rewrite app_length.
-    rewrite <- Nat.le_succ_l in I. rewrite <- Nat.le_succ_l.
-    rewrite <- Nat.add_1_r. apply Nat.add_le_mono; assumption.
-    rewrite <- H2 in H4. apply Nat.lt_irrefl in H4. contradiction H4.
-    rewrite Nat.pow_succ_r' in H3. rewrite Nat.even_mul in H3.
-    simpl in H3. inversion H3.
+    assert (W: nil <> tl).
+    assert (even (length (a++a)) = true). rewrite app_length.
+    rewrite Nat.even_add. rewrite H0. reflexivity.
+    assert (0 < length (a ++ a)). rewrite <- Nat.add_0_r at 1.
+    rewrite app_length. apply Nat.add_lt_mono; assumption.
+    generalize H2. generalize H1. generalize H3.
+    replace (hd++a++a++tl) with (hd++(a++a)++tl) in H. generalize H.
+    apply tm_step_tail_not_nil_prefix_odd. rewrite <- app_assoc. reflexivity.
+    destruct tl. contradiction W. reflexivity.
 
     (* proof that a is not nil *)
     destruct a. inversion I.
@@ -495,3 +541,4 @@ Proof.
        grâce à tm_step_factor4_odd_prefix *)
 
     Admitted. 
+    (* TODO: revoir tm_step_cube4 *)