Update

thue-morse.v

@@ -1319,13 +1319,65 @@ Proof.
 Qed.
 
 
-Theorem tm_step_cubefree : forall (n : nat) (hd a b tl : list bool),
-  tm_step n = hd ++ a ++ a ++ b ++ tl -> a <> b.
+Lemma tm_step_cube7 : forall (n : nat),
+     (exists (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ a ++ tl
+     /\ 0 < length a)
+  -> exists (hd2 b tl2 : list bool), tm_step 0 = hd2 ++ b ++ b ++ b ++ tl2
+     /\ 0 < length b.
 Proof.
-  intros n hd a b tl. intro H.
-  assert (I: a=b \/ a<>b). 
+  intros n. intro H.
+  induction n.
+  - destruct H. destruct H. destruct H. destruct H.
+    exists x. exists x0. exists x1. split; assumption.
+  - destruct H. destruct H. destruct H. destruct H.
+    assert (J: exists (hd2 b2 tl2 : list bool), tm_step (Nat.pred (S n)) = hd2 ++ b2 ++ b2 ++ b2 ++ tl2 /\ 0 < length b2).
+    generalize H0. generalize H. apply tm_step_cube6. rewrite Nat.pred_succ in J.
+    apply IHn. apply J.
+Qed.
 
 
+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.
+Proof.
+  intros n hd a b tl. intros H I.
+
+  assert (J: {a=b} + {~ a=b}). apply list_eq_dec. apply bool_dec.
+
+  destruct J. rewrite <- e in H.
+  assert (0 < n). generalize I. generalize H. apply tm_step_cube2.
+
+  induction n. apply Nat.lt_irrefl in H0. contradiction H0.
+  
+  assert (exists (hd2 b2 tl2 : list bool), tm_step (Nat.pred (S n)) = hd2 ++ b2 ++ b2 ++ b2 ++ tl2 /\ 0 < length b2).
+  generalize I. generalize H. apply tm_step_cube6. rewrite Nat.pred_succ in H1.
+  destruct H1. destruct H1. destruct H1. destruct H1.
+  rewrite <- e in IHn.
+
+
+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
+     /\ 0 < length b.
+
+
+
+
+  assert (J: (a = b) \/ (a <> b)). cbv. easy.
+
+  destruct J. assert (a=b). apply H0.
+
+  assert (0 < n). generalize I. generalize H
+
+Lemma tm_step_cube2 : forall (n : nat) (a hd tl: list bool),
+  tm_step n = hd ++ a ++ a ++ a ++ tl -> 0 < length a -> 0 < n.
+
+
+list_eq_dec:
+  forall [A : Type],
+  (forall x y : A, {x = y} + {x <> y}) ->
+  forall l l' : list A, {l = l'} + {l <> l'}
+