Update

src/thue_morse3.v

@@ -1356,36 +1356,51 @@ Proof.
   apply Nat.le_add_l. rewrite Nat.add_comm. simpl. reflexivity.
 Qed.
 
-
-(* TODO: this theorem could be made more powerful with 2 < n *)
 Lemma tm_step_palindromic_length_12_n :
   forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ (rev a) ++ tl
-  -> length a > 6
-  -> 1 < n.
+  -> 6 < length a
+  -> 3 < n.
 Proof.
   intros n hd a tl. intros H W.
 
   assert (length (tm_step n) <= length (tm_step n)).
-  apply Nat.le_refl. rewrite H in H0 at 1.
-  rewrite app_length in H0. rewrite app_length in H0.
-  rewrite Nat.add_comm in H0. rewrite <- Nat.add_assoc in H0.
-  rewrite <- Nat.add_0_r in H0. apply Nat.le_le_add_le in H0.
-  rewrite tm_size_power2 in H0. destruct n. destruct a.
-  inversion W. destruct a. inversion W. inversion H2.
-  destruct a. inversion W. inversion H2. inversion H4.
-  inversion H0. inversion H2. destruct a. inversion W.
-  destruct a. inversion W. inversion H2. destruct a. inversion W.
-  inversion H2. inversion H4. destruct n. inversion H0. inversion H2.
-  inversion H4. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
-  apply le_0_n.
-Qed.
+  reflexivity. rewrite H in H0 at 1.
+  rewrite app_length in H0.
+
+  assert (length (a++ rev a ++ tl) <= length hd + length (a ++ rev a ++ tl)).
+  apply Nat.le_add_l.
+  
+  assert (length (a ++ rev a ++ tl) <= length (tm_step n)).
+  generalize H0. generalize H1. apply Nat.le_trans.
+
+  rewrite app_length in H2. rewrite app_length in H2. rewrite rev_length in H2.
+  rewrite Nat.add_comm in H2. rewrite Nat.add_shuffle0 in H2.
+
+  apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W.
+  assert (4+4 < length a + length a). generalize W. generalize W.
+  apply Nat.add_lt_mono.
+
+  assert (length a + length a <= length a + length a + length tl).
+  apply Nat.le_add_r.
+
+  assert (length a + length a <= length (tm_step n)).
+  generalize H2. generalize H4. apply Nat.le_trans.
+
+  assert (4 + 4 < length (tm_step n)). generalize H5. generalize H3.
+  apply Nat.lt_le_trans. rewrite tm_size_power2 in H6.
+  replace (4+4) with (2^3) in H6.
+
+  rewrite <- Nat.pow_lt_mono_r_iff in H6.
+  assumption.
+  apply Nat.lt_1_2. reflexivity.
+Admitted.  
 
 
 Theorem tm_step_palindromic_length_12_prefix :
   forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ (rev a) ++ tl
-  -> length a > 6
+  -> 6 < length a
   -> length a mod 4 = 0 <-> length hd mod 4 = 0.
 Proof.
   intros n hd a tl. intros H I. split; intro J;
@@ -1401,7 +1416,7 @@ Qed.
 Theorem tm_step_palindromic_length_12_prefix2 :
   forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ (rev a) ++ tl
-  -> length a > 6
+  -> 6 < length a
   -> length a mod 4 = 0 -> length tl mod 4 = 0.
 Proof.
   intros n hd a tl. intros H I J.
@@ -1411,8 +1426,9 @@ Proof.
   assert (L: length (hd ++ a ++ rev a ++ tl) mod 4 = 0).
   rewrite <- H. rewrite tm_size_power2.
 
-  assert (V: 1 < n). generalize I. generalize H.
+  assert (V: 3 < n). generalize I. generalize H.
   apply tm_step_palindromic_length_12_n.
+  apply Nat.lt_succ_l in V. apply Nat.lt_succ_l in V.
   destruct n. inversion V. destruct n. inversion V. inversion H1.
   rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r.
   rewrite Nat.mul_comm. rewrite <- Nat.mul_assoc.
@@ -1533,7 +1549,7 @@ Qed.
 Lemma tm_step_palindromic_even_morphism2 :
   forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ (rev a) ++ tl
-  -> length a > 6
+  -> 6 < length a
   -> (length a) mod 4 = 0
   -> hd = tm_morphism (tm_morphism (firstn (length hd / 4)
            (tm_step (pred (pred n)))))
@@ -1546,8 +1562,9 @@ Proof.
   apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W.
   assumption.
 
-  assert (V: 1 < n). generalize W. generalize H.
+  assert (V: 3 < n). generalize W. generalize H.
   apply tm_step_palindromic_length_12_n.
+  apply Nat.lt_succ_l in V. apply Nat.lt_succ_l in V.
   destruct n. inversion V.
 
   assert (J1: length hd mod 4 = 0). generalize J0. generalize W.