Update

src/thue_morse3.v

@@ -2549,14 +2549,127 @@ Proof.
 
   destruct m. left.
   apply tm_step_palindrome_mod8 with (n := n) (tl := tl); assumption.
-  right. rewrite J. apply Nat.pow_le_mono_r. easy.
-  rewrite Nat.double_S. rewrite Nat.double_S.
+  right. rewrite J. rewrite Nat.double_S. rewrite Nat.double_S.
+  apply Nat.pow_le_mono_r. easy.
   rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono.
   rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono.
-  rewrite <- Nat.succ_le_mono. apply le_0_n.
+  rewrite <- Nat.succ_le_mono.
+  apply le_0_n.
 Qed.
 
 
+Theorem tm_step_palindromic_power2_odd :
+  forall (m n : nat) (hd a tl : list bool),
+    tm_step n = hd ++ a ++ (rev a) ++ tl
+    -> 6 < length a
+    -> length a = 2^(S (Nat.double m))
+    -> length (hd ++ a) mod (2 ^ (S (Nat.double m))) = 0.
+Proof.
+  intros m n hd a tl. intros H I J.
+  assert (E: length (hd ++ a) mod (2 ^ (S (Nat.double m))) = 0
+     \/ 2^5 <= length a).
+  generalize J. generalize I. generalize H.
+  apply tm_step_palindromic_power2_odd_beta.
+
+  generalize dependent hd.
+  generalize dependent a.
+  generalize dependent tl.
+  generalize dependent n.
+
+  induction m.
+  - intros n tl a I J hd H E. destruct E. assumption.
+    apply tm_step_palindromic_power2_odd_alpha with (n := n) (tl := tl).
+    assumption. assumption. assumption.
+    rewrite J in H0. rewrite <- Nat.pow_le_mono_r_iff in H0.
+    inversion H0. inversion H2.
+    apply Nat.lt_1_2.
+  - intros n tl a I J hd H E. assert (E' := E).
+    destruct E as [E0 | E1]. assumption.
+    rewrite tm_step_palindromic_power2_odd_alpha with (n := n) (tl := tl).
+    rewrite <- pred_Sn.
+
+    assert (W: (length a) mod 4 = 0).
+    rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J.
+    rewrite Nat.pow_succ_r in J.
+    rewrite Nat.mul_assoc in J.
+    replace (2*2) with 4 in J. rewrite J.
+    rewrite <- Nat.mul_mod_idemp_l. reflexivity.
+    easy. reflexivity. apply le_0_n. apply le_0_n.
+
+    assert (
+       hd = tm_morphism (tm_morphism (firstn (length hd / 4)
+             (tm_step (pred (pred n)))))
+       /\ a = tm_morphism (tm_morphism
+             (firstn (length a / 4) (skipn (length hd / 4)
+             (tm_step (pred (pred n))))))
+       /\ tl = tm_morphism (tm_morphism
+             (skipn (length hd / 4 + Nat.div2 (length a))
+               (tm_step (pred (pred n)))))).
+    generalize W. generalize I. generalize H.
+    apply tm_step_palindromic_even_morphism2.
+    destruct H0 as [K H0]. destruct H0 as [L M].
+
+    assert (V: 3 < n). generalize I. generalize H.
+    apply tm_step_palindromic_length_12_n.
+    destruct n. inversion V. destruct n. inversion V. inversion H1.
+
+    rewrite K in H. rewrite L in H. rewrite M in H.
+    rewrite tm_morphism_twice_rev in H.
+    rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
+    rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
+    rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
+    rewrite <- tm_step_lemma in H. rewrite <- tm_step_lemma in H.
+    rewrite <- tm_morphism_eq in H. rewrite <- tm_morphism_eq in H.
+    rewrite Nat.pred_succ in H. rewrite Nat.pred_succ in H.
+
+    pose (hd' := (firstn (length hd / 4) (tm_step n))).
+    pose (a' := (firstn (length a / 4) (skipn (length hd / 4) (tm_step n)))).
+    pose (tl' := (skipn (length hd / 4 + Nat.div2 (length a)) (tm_step n))).
+    fold hd' in H. fold a' in H. fold tl' in H.
+
+    rewrite Nat.pred_succ in K. rewrite Nat.pred_succ in K.
+    rewrite Nat.pred_succ in L. rewrite Nat.pred_succ in L.
+    fold hd' in K. fold a' in L.
+    assert (N: length a = length a). reflexivity. rewrite L in N at 2.
+    rewrite tm_morphism_length in N. rewrite tm_morphism_length in N.
+    rewrite Nat.mul_assoc in N. replace (2*2) with 4 in N.
+    assert (O: length hd = length hd). reflexivity. rewrite K in O at 2.
+    rewrite tm_morphism_length in O. rewrite tm_morphism_length in O.
+    rewrite Nat.mul_assoc in O. replace (2*2) with 4 in O.
+
+    rewrite app_length. rewrite N. rewrite O. rewrite <- Nat.mul_add_distr_l.
+    rewrite Nat.mul_comm. rewrite Nat.div_mul. rewrite <- app_length.
+
+    assert (Y: length a' = 2 ^ (S (Nat.double m))).
+    rewrite J in N. rewrite Nat.double_S in N.
+    rewrite Nat.pow_succ_r in N. rewrite Nat.pow_succ_r in N.
+    rewrite Nat.mul_assoc in N. replace (2*2) with 4 in N.
+    rewrite Nat.mul_cancel_l in N. rewrite N. reflexivity. easy. reflexivity.
+    apply le_0_n. apply le_0_n.
+
+    assert (Y': 6 < length a').
+    rewrite N in E1.
+    rewrite Nat.pow_succ_r in E1. rewrite Nat.pow_succ_r in E1.
+    rewrite Nat.mul_assoc in E1. replace (2*2) with 4 in E1.
+    rewrite <- Nat.mul_le_mono_pos_l in E1.
+    assert (6 < 2^3). simpl.
+    rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+    rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+    rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+    apply Nat.lt_0_succ. generalize E1. generalize H0.
+    apply Nat.lt_le_trans. apply Nat.lt_0_succ. reflexivity.
+    apply le_0_n. apply le_0_n.
+
+    apply IHm with (n := n) (tl := tl').
+    assumption. assumption. assumption.
+    generalize Y. generalize Y'. generalize H.
+    apply tm_step_palindromic_power2_odd_beta.
+    easy. reflexivity. reflexivity.
+    assumption. assumption. assumption.
+Qed.
+
+
+
 (*
 Lemma tm_step_proper_palindrome_center :
   forall (m n k : nat) (hd a tl : list bool),