Update

src/thue_morse.v

@@ -425,6 +425,15 @@ Proof.
     rewrite rev_involutive. reflexivity.
 Qed.
 
+Lemma tm_step_even_step : forall (n : nat),
+  rev (tm_step (Nat.double n)) = tm_step (Nat.double n).
+Proof.
+  intro n. induction n.
+  - reflexivity.
+  - rewrite Nat.double_S. rewrite <- tm_step_lemma. rewrite <- tm_step_lemma.
+    rewrite tm_morphism_twice_rev. rewrite IHn. reflexivity.
+Qed.
+
 Theorem tm_step_double_index : forall (n k : nat),
   nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k).
 Proof.

src/thue_morse2.v

@@ -1624,3 +1624,77 @@ Proof.
   simpl. rewrite Nat.add_0_r. reflexivity.
   left. assumption.
 Qed.
+
+Theorem tm_step_square_prefix_not_nil :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ a ++ tl -> 0 < length a -> hd <> nil.
+Proof.
+  intros n hd a tl. intros H I.
+
+  assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
+  destruct W. rewrite e in H. rewrite app_nil_l in H.
+  generalize dependent a.
+  generalize dependent tl.
+  induction n.
+  - intros tl a. intros H I.
+    destruct a. inversion I. inversion H.
+    assert (length (nil : list bool) = length (nil : list bool)).
+    reflexivity. rewrite H2 in H0 at 2. rewrite app_length in H0.
+    rewrite Nat.add_comm in H0. inversion H0.
+  - intros tl a. intros H I.
+    assert (hd <> nil
+      \/ exists a' tl', tm_step (pred (S n)) = a' ++ a' ++ tl' /\ 0 < length a').
+    generalize I. generalize H. replace (a++a++tl) with (hd ++ a ++ a ++ tl).
+    apply tm_step_square_prefix_not_nil0. rewrite e. reflexivity.
+    destruct H0. assumption. destruct H0. destruct H0.
+    rewrite <- pred_Sn in H0.
+    destruct H0.
+    generalize H1. generalize H0. apply IHn.
+  - assumption.
+Qed.
+
+Theorem tm_step_square_tail_not_nil :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ a ++ tl -> 0 < length a -> tl <> nil.
+Proof.
+  intros n hd a tl. intros H I.
+  assert (W: {tl=nil} + {~ tl=nil}). apply list_eq_dec. apply bool_dec.
+  destruct W. rewrite e in H. rewrite app_nil_r in H.
+
+  assert (X: n = 2 * Nat.div2 n + Nat.b2n (Nat.odd n)). apply Nat.div2_odd.
+  rewrite <- Nat.double_twice in X.
+
+  assert (Y: rev (hd ++ a ++ a) = rev (hd ++ a ++ a)). reflexivity.
+  rewrite <- H in Y at 1.
+  rewrite rev_app_distr in Y. rewrite rev_app_distr in Y.
+  rewrite <- app_assoc in Y. rewrite X in Y.
+
+  assert (Z : { odd n = true } + {~ odd n = true}). apply bool_dec.
+  destruct Z. rewrite e0 in Y. rewrite Nat.add_1_r in Y.
+  rewrite tm_step_odd_step in Y.
+
+  assert (map negb (rev a ++ rev a ++ rev hd)
+    = map negb (rev a ++ rev a ++ rev hd)). reflexivity.
+  rewrite <- Y in H0 at 1.
+
+  assert (forall l, map negb (map negb l) = l).
+  intro l. induction l. reflexivity. simpl. rewrite negb_involutive.
+  rewrite IHl. reflexivity. rewrite H1 in H0.
+
+  rewrite map_app in H0. rewrite map_app in H0.
+  rewrite <- app_nil_l in H0. 
+  assert ((nil : list bool) <> nil).
+  assert (0 < length (map negb (rev a))). rewrite map_length.
+  rewrite rev_length. assumption. generalize H2. generalize H0.
+  apply tm_step_square_prefix_not_nil. contradiction H2.
+  reflexivity.
+
+  apply not_true_is_false in n0. rewrite n0 in Y.
+  rewrite Nat.add_0_r in Y. rewrite tm_step_even_step in Y.
+  rewrite <- app_nil_l in Y. 
+  assert ((nil : list bool) <> nil).
+  assert (0 < length (rev a)). rewrite rev_length. assumption.
+  generalize H0. generalize Y.
+  apply tm_step_square_prefix_not_nil. contradiction H0.
+  reflexivity. assumption.
+Qed.