Update

src/thue_morse2.v

@@ -263,7 +263,7 @@ Qed.
 
 Lemma tm_step_consecutive_identical_length' :
   forall (n : nat) (hd a tl : list bool),
-  tm_step n = hd ++ a ++ tl -> length a > 4
+  tm_step n = hd ++ a ++ tl -> 4 < length a
   -> exists (b c : list bool) (d : bool), a = b ++ [d;d] ++ c.
 Proof.
   intros n hd a tl. intros H I.
@@ -282,78 +282,36 @@ Proof.
 Qed.
 
 
-
-
-
-
-
-Lemma tm_step_consecutive_identical_length :
-  forall (n : nat) (hd a tl : list bool),
-  tm_step n = hd ++ a ++ tl -> length a = 5
-  -> exists (b c : list bool) (d : bool), a = b ++ [d;d] ++ c.
-
-
-
-Lemma tm_step_square_size_3 : forall (n : nat) (hd a tl : list bool),
-  tm_step n = hd ++ a ++ a ++ tl -> length a = 3
-  -> a = true::false::true::nil \/ a = false::true::false::nil.
+Lemma tm_step_odd_square : forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ a ++ tl -> odd (length a) = true -> length a < 4.
 Proof.
   intros n hd a tl. intros H I.
-  destruct a.
-  - inversion I.
-  - destruct b.
-    + left. destruct a. inversion I. destruct b.
-      * assert (J: a = false::nil). destruct a. inversion I.
-        destruct b.
-        assert (K: tm_step n = hd ++ [true] ++ [true] ++ [true]
-                               ++ a ++ [true] ++ [true] ++ [true] ++ a ++ tl).
-        rewrite H. apply app_inv_head_iff.
-        replace (true::true::true::a) with ([true] ++ [true] ++ [true] ++ a).
-        rewrite <- app_assoc. apply app_inv_head_iff.
-        rewrite <- app_assoc. apply app_inv_head_iff.
-        rewrite <- app_assoc. apply app_inv_head_iff. apply app_inv_head_iff.
-        rewrite <- app_assoc. apply app_inv_head_iff.
-        rewrite <- app_assoc. apply app_inv_head_iff.
-        rewrite <- app_assoc. reflexivity. reflexivity.
-        apply tm_step_cubefree in K. contradiction K. reflexivity.
-        simpl. apply Nat.lt_0_1. simpl in I. apply Nat.succ_inj in I.
-        apply Nat.succ_inj in I. apply Nat.succ_inj in I.
-        rewrite length_zero_iff_nil in I. rewrite I. reflexivity.
+  assert (J: 4 < length a \/ length a <= 4).
+  apply Nat.lt_ge_cases. destruct J.
+  assert (exists b c d, a = b ++ [d;d] ++ c).
+  generalize H0. generalize H. apply tm_step_consecutive_identical_length'.
+  destruct H1. destruct H1. destruct H1. rewrite H1 in H.
 
-        replace (hd ++ (true::true::a) ++ (true::true::a) ++ tl)
-          with (hd ++ (true::true::nil) ++ (a ++ (true::true::a) ++ tl)) in H.
-        apply tm_step_consecutive_identical in H.
-        rewrite J in H. simpl in H. inversion H.
+  replace (hd ++ (x ++ [x1; x1] ++ x0) ++ (x ++ [x1; x1] ++ x0) ++ tl)
+    with ((hd ++ x) ++ [x1;x1] ++ (x0++x) ++ [x1;x1] ++ (x0 ++ tl)) in H.
+  apply tm_step_consecutive_identical in H.
 
-        apply app_inv_head_iff. rewrite <- app_assoc_reverse.
-        apply app_inv_head_iff. reflexivity.
-      * destruct a. inversion I. simpl in I.
-        apply Nat.succ_inj in I. apply Nat.succ_inj in I.
-        apply Nat.succ_inj in I. apply length_zero_iff_nil in I.
-        destruct b. rewrite I. reflexivity.
-        rewrite I in H.
-        replace (hd ++ [true;false;false] ++ [true;false;false] ++ tl)
-          with ((hd ++ [true]) ++ [false;false] ++ [true] ++ [false;false] ++ tl) in H.
-        apply tm_step_consecutive_identical in H. simpl in H. inversion H.
-        rewrite app_assoc_reverse. apply app_inv_head_iff. reflexivity.
-    + right. destruct a. inversion I. destruct b.
-      * destruct a. inversion I. simpl in I.
-        apply Nat.succ_inj in I. apply Nat.succ_inj in I.
-        apply Nat.succ_inj in I. apply length_zero_iff_nil in I.
-        destruct b. rewrite I in H.
-        replace (hd ++ [false;true;true] ++ [false;true;true] ++ tl)
-          with ((hd ++ [false]) ++ [true;true] ++ [false] ++ [true;true] ++ tl) in H.
-        apply tm_step_consecutive_identical in H. simpl in H. inversion H.
-        rewrite app_assoc_reverse. apply app_inv_head_iff. reflexivity.
-        rewrite I. reflexivity.
-      * replace (hd ++ (false::false::a) ++ (false::false::a) ++ tl)
-          with (hd ++ (false::false::nil) ++ a ++ (false::false::nil) ++ (a ++ tl)) in H.
-        apply tm_step_consecutive_identical in H. simpl in H. inversion H.
-        simpl in I. apply Nat.succ_inj in I. apply Nat.succ_inj in I.
-        rewrite I in H. inversion H.
-        apply app_inv_head_iff.
-        rewrite <- app_assoc_reverse.
-        apply app_inv_head_iff. reflexivity.
+  assert (J: even (length (x0 ++ x)) = false).
+  rewrite H1 in I. rewrite app_length in I. rewrite app_length in I.
+  rewrite Nat.add_shuffle3 in I. rewrite Nat.add_comm in I.
+  rewrite Nat.odd_add_even in I.
+  rewrite app_length. rewrite Nat.add_comm. rewrite <- Nat.negb_odd.
+  rewrite I. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT.
+  reflexivity. rewrite H in J. inversion J.
+
+  rewrite <- app_assoc. apply app_inv_head_iff.
+  rewrite <- app_assoc. rewrite <- app_assoc. apply app_inv_head_iff.
+  rewrite <- app_assoc. apply app_inv_head_iff. apply app_inv_head_iff.
+  rewrite <- app_assoc. apply app_inv_head_iff.
+  reflexivity.
+
+  apply Nat.le_lteq in H0. destruct H0. assumption.
+  rewrite H0 in I. inversion I.
 Qed.
 
 
@@ -361,46 +319,6 @@ Qed.
 
 
 
-
-        destruct a. inversion I.
-        destruct b.
-        assert (K: tm_step n = hd ++ [false] ++ [true] ++ [true]
-                               ++ a ++ [true] ++ [true] ++ [true] ++ a ++ tl).
-        rewrite H. apply app_inv_head_iff.
-        replace (true::true::true::a) with ([true] ++ [true] ++ [true] ++ a).
-        rewrite <- app_assoc. apply app_inv_head_iff.
-        rewrite <- app_assoc. apply app_inv_head_iff.
-        rewrite <- app_assoc. apply app_inv_head_iff. apply app_inv_head_iff.
-        rewrite <- app_assoc. apply app_inv_head_iff.
-        rewrite <- app_assoc. apply app_inv_head_iff.
-        rewrite <- app_assoc. reflexivity. reflexivity.
-        apply tm_step_cubefree in K. contradiction K. reflexivity.
-        simpl. apply Nat.lt_0_1. simpl in I. apply Nat.succ_inj in I.
-        apply Nat.succ_inj in I. apply Nat.succ_inj in I.
-        rewrite length_zero_iff_nil in I. rewrite I. reflexivity.
-
-        replace (hd ++ (true::true::a) ++ (true::true::a) ++ tl)
-          with (hd ++ (true::true::nil) ++ (a ++ (true::true::a) ++ tl)) in H.
-        apply tm_step_consecutive_identical in H.
-        rewrite J in H. simpl in H. inversion H.
-
-        apply app_inv_head_iff. rewrite <- app_assoc_reverse.
-        apply app_inv_head_iff. reflexivity.
-
-
-
-Theorem tm_step_cubefree : forall (n : nat) (hd a b tl : list bool),
-  tm_step n = hd ++ a ++ a ++ b ++ tl -> 0 < length a -> a <> b.
-
-
-
-Carré de taille 3 :
-  AABAAB   (impossible)
-  ABBABB    (impossible)
-  ABAABA    (OK)
-  BABBAB    
-
-
 Lemma xxx : forall (n k : nat) (hd pat tl : list bool),
   tm_step n = hd ++ pat ++ tl
   -> length pat <= 2^k