Update

src/thue_morse.v

@@ -898,7 +898,7 @@ Proof.
 Qed.
 
 
-Lemma tm_step_pattern4_odd_prefix : forall (n : nat) (hd a tl : list bool),
+Lemma tm_step_factor4_odd_prefix : forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ tl
   -> length a = 4 -> odd (length hd) = true
   -> exists (x : bool) (u v : list bool), a = u ++ [x;x] ++ v.
@@ -1021,6 +1021,75 @@ Proof.
   - reflexivity.
 Qed.
 
+Lemma tm_step_consecutive_identical_length :
+  forall (n : nat) (hd a tl : list bool),
+  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.
+  assert (J: Nat.Even (length hd) \/ Nat.Odd (length hd)).
+  apply Nat.Even_or_Odd. destruct J as [J | J].
+
+  (* first case *)
+  replace (hd++a++tl)
+    with ((hd ++ (firstn 1 a)) ++ (skipn 1 (firstn 5 a))
+                               ++ ((skipn 5 a) ++ tl)) in H.
+
+  assert (length (skipn 1 (firstn 5 a)) = 4).
+  rewrite skipn_length. rewrite firstn_length.
+  rewrite <- Nat.le_succ_l in I. rewrite Nat.min_l.
+  reflexivity. assumption.
+
+  assert (odd (length (hd ++ firstn 1 a)) = true).
+  rewrite app_length. rewrite Nat.odd_add. rewrite <- Nat.negb_even.
+  apply Nat.Even_EvenT in J. apply Nat.EvenT_even in J. rewrite J.
+  rewrite firstn_length. rewrite Nat.min_l. reflexivity.
+  
+  apply Nat.lt_le_incl.
+  assert (1 < 4). rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
+  generalize I. generalize H1. apply Nat.lt_trans.
+
+  assert (exists (x : bool) (u v : list bool),
+    skipn 1 (firstn 5 a) = u ++ [x;x] ++ v).
+  generalize H1. generalize H0. generalize H. apply tm_step_factor4_odd_prefix.
+  destruct H2. destruct H2. destruct H2.
+  exists ((firstn 1 a) ++ x0). exists (x1 ++ (skipn 5 a)). exists x.
+  replace ((firstn 1 a ++ x0) ++ [x; x] ++ x1 ++ skipn 5 a)
+    with (firstn 1 a ++ (x0 ++ [x;x] ++ x1) ++ skipn 5 a). rewrite <- H2.
+  rewrite app_assoc. replace (firstn 1 a) with (firstn 1 (firstn 5 a)).
+  rewrite firstn_skipn. rewrite firstn_skipn. reflexivity.
+  rewrite firstn_firstn. reflexivity.
+  rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
+  reflexivity.
+  rewrite <- app_assoc. apply app_inv_head_iff.
+  replace (firstn 1 a) with (firstn 1 (firstn 5 a)).
+  rewrite app_assoc. rewrite firstn_skipn.
+  rewrite app_assoc. rewrite firstn_skipn.
+  reflexivity.
+  rewrite firstn_firstn. reflexivity.
+
+  (* second case *)
+  replace (hd++a++tl) with (hd ++ (firstn 4 a) ++ ((skipn 4 a) ++ tl)) in H.
+
+  assert (length (firstn 4 a) = 4). rewrite firstn_length.
+  rewrite <- Nat.le_succ_l in I. rewrite Nat.min_l.
+  reflexivity. assert (4 <= 5). apply Nat.le_succ_diag_r.
+  generalize I. generalize H0. apply Nat.le_trans.
+
+  apply Nat.Odd_OddT in J. apply Nat.OddT_odd in J.
+
+  assert (exists (x : bool) (u v : list bool), firstn 4 a = u ++ [x;x] ++ v).
+  generalize J. generalize H0. generalize H. apply tm_step_factor4_odd_prefix.
+  destruct H1. destruct H1. destruct H1.
+  exists x0. exists (x1++(skipn 4 a)). exists x.
+
+  replace (x0 ++ [x;x] ++ x1 ++ (skipn 4 a))
+  with ((x0++[x;x]++x1) ++ (skipn 4 a)).
+  rewrite <- H1. rewrite firstn_skipn. reflexivity.
+  rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
+  apply app_inv_head_iff.
+  rewrite app_assoc. rewrite firstn_skipn. reflexivity.
+Qed.
 
 
 (**

src/thue_morse2.v

@@ -91,76 +91,6 @@ Qed.
    All squared factors of odd length have length 1 or 3.
 *)
 
-Lemma tm_step_consecutive_identical_length :
-  forall (n : nat) (hd a tl : list bool),
-  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.
-  assert (J: Nat.Even (length hd) \/ Nat.Odd (length hd)).
-  apply Nat.Even_or_Odd. destruct J as [J | J].
-
-  (* first case *)
-  replace (hd++a++tl)
-    with ((hd ++ (firstn 1 a)) ++ (skipn 1 (firstn 5 a))
-                               ++ ((skipn 5 a) ++ tl)) in H.
-
-  assert (length (skipn 1 (firstn 5 a)) = 4).
-  rewrite skipn_length. rewrite firstn_length.
-  rewrite <- Nat.le_succ_l in I. rewrite Nat.min_l.
-  reflexivity. assumption.
-
-  assert (odd (length (hd ++ firstn 1 a)) = true).
-  rewrite app_length. rewrite Nat.odd_add. rewrite <- Nat.negb_even.
-  apply Nat.Even_EvenT in J. apply Nat.EvenT_even in J. rewrite J.
-  rewrite firstn_length. rewrite Nat.min_l. reflexivity.
-  
-  apply Nat.lt_le_incl.
-  assert (1 < 4). rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
-  generalize I. generalize H1. apply Nat.lt_trans.
-
-  assert (exists (x : bool) (u v : list bool),
-    skipn 1 (firstn 5 a) = u ++ [x;x] ++ v).
-  generalize H1. generalize H0. generalize H. apply tm_step_pattern4_odd_prefix.
-  destruct H2. destruct H2. destruct H2.
-  exists ((firstn 1 a) ++ x0). exists (x1 ++ (skipn 5 a)). exists x.
-  replace ((firstn 1 a ++ x0) ++ [x; x] ++ x1 ++ skipn 5 a)
-    with (firstn 1 a ++ (x0 ++ [x;x] ++ x1) ++ skipn 5 a). rewrite <- H2.
-  rewrite app_assoc. replace (firstn 1 a) with (firstn 1 (firstn 5 a)).
-  rewrite firstn_skipn. rewrite firstn_skipn. reflexivity.
-  rewrite firstn_firstn. reflexivity.
-  rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
-  reflexivity.
-  rewrite <- app_assoc. apply app_inv_head_iff.
-  replace (firstn 1 a) with (firstn 1 (firstn 5 a)).
-  rewrite app_assoc. rewrite firstn_skipn.
-  rewrite app_assoc. rewrite firstn_skipn.
-  reflexivity.
-  rewrite firstn_firstn. reflexivity.
-
-  (* second case *)
-  replace (hd++a++tl) with (hd ++ (firstn 4 a) ++ ((skipn 4 a) ++ tl)) in H.
-
-  assert (length (firstn 4 a) = 4). rewrite firstn_length.
-  rewrite <- Nat.le_succ_l in I. rewrite Nat.min_l.
-  reflexivity. assert (4 <= 5). apply Nat.le_succ_diag_r.
-  generalize I. generalize H0. apply Nat.le_trans.
-
-  apply Nat.Odd_OddT in J. apply Nat.OddT_odd in J.
-
-  assert (exists (x : bool) (u v : list bool), firstn 4 a = u ++ [x;x] ++ v).
-  generalize J. generalize H0. generalize H. apply tm_step_pattern4_odd_prefix.
-  destruct H1. destruct H1. destruct H1.
-  exists x0. exists (x1++(skipn 4 a)). exists x.
-
-  replace (x0 ++ [x;x] ++ x1 ++ (skipn 4 a))
-  with ((x0++[x;x]++x1) ++ (skipn 4 a)).
-  rewrite <- H1. rewrite firstn_skipn. reflexivity.
-  rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
-  apply app_inv_head_iff.
-  rewrite app_assoc. rewrite firstn_skipn. reflexivity.
-Qed.
-
 Theorem 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.