Update

src/thue_morse4.v

@@ -1444,3 +1444,82 @@ Proof.
     rewrite Nat.add_succ_l; rewrite Nat.add_0_l;
     rewrite Nat.pow_succ_r; lia || rewrite Nat.pow_succ_r; lia.
 Qed.
+
+Lemma tm_step_square_rev_even' :
+  forall (m n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ a ++ tl
+  -> length a = 2^m
+  -> a = rev a
+  -> length (hd ++ a) mod 2^(S m) = 0.
+Proof.
+  intros m n hd a tl. intros H I J.
+  assert (K: even m = true). generalize J. generalize I. generalize H.
+  apply tm_step_square_rev_even.
+  assert (length a = 2^m \/ length a = 3*2^m). left. assumption.
+  assert (K' := K). apply Nat.even_EvenT in K. apply Nat.EvenT_Even in K.
+  apply Nat.Even_double in K. rewrite K in H0.
+  assert (
+     skipn (length (hd ++ a) - 2^(S (Nat.log2 (length a)))) (hd ++ a)
+    = rev (firstn (2^S (Nat.log2 (length a))) (a ++ tl))
+      /\ 2^(S (Nat.log2 (length a))) <= length (hd ++ a)
+      /\ 2^(S (Nat.log2 (length a))) <= length (a ++ tl)).
+  generalize H0. generalize H. apply tm_step_square_even_rev'_alpha.
+  destruct H1. rewrite I in H1. rewrite Nat.log2_pow2 in H1.
+  rewrite I in H2. rewrite Nat.log2_pow2 in H2.
+
+  (* cas : length a = 1 *)
+  destruct m.
+  assert (0 < length a). rewrite I. apply Nat.lt_0_1.
+  assert (even (length (hd ++ a)) = true).
+  generalize H3. generalize H. apply tm_step_square_pos.
+  apply Nat.even_EvenT in H4. apply Nat.EvenT_Even in H4.
+  apply Nat.Even_double in H4. rewrite Nat.double_twice in H4.
+  rewrite H4. rewrite Nat.mul_comm. rewrite Nat.mod_mul.
+  reflexivity. easy.
+
+  rewrite app_assoc in H.
+  rewrite <- firstn_skipn with (l := hd ++ a)
+           (n := length (hd++a) - 2^(S (S m))) in H.
+  rewrite <- firstn_skipn with (l := a ++ tl) (n := 2^(S (S m))) in H.
+  rewrite <- app_assoc in H.
+
+  assert (firstn (2^(S (S m))) (a ++ tl) =
+    rev (skipn (length (hd ++ a) - 2 ^ (S (S m))) (hd ++ a))).
+  rewrite H1. rewrite rev_involutive. reflexivity. rewrite H3 in H.
+
+  destruct m. inversion K'.
+  assert (6 < length (skipn (length (hd ++ a) - 2 ^ S (S (S m))) (hd ++ a))).
+  rewrite skipn_length.
+  replace (length (hd++a)) with ((length (hd++a) - 2^(S (S (S m))))
+         + 2^(S (S (S m)))) at 1.
+  rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
+  rewrite Nat.add_0_l. rewrite Nat.pow_succ_r.
+  rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r.
+  rewrite Nat.mul_assoc. rewrite Nat.mul_assoc.
+
+  assert (8*1 <= 8*2^m). apply Nat.mul_le_mono_l.
+  apply Nat.le_succ_l.
+  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+  assert (6 < 8). lia. generalize H4. generalize H5.
+  apply Nat.lt_le_trans. lia. lia. lia. lia. lia.
+
+  assert (length (skipn (length (hd ++ a) - 2 ^ S (S (S m))) (hd ++ a))
+    = 2^(S (Nat.double (Nat.div2 (S (S m)))))).
+  rewrite skipn_length.
+  replace (length (hd++a))
+    with ((length (hd++a) - 2^(S (S (S m)))) + 2^(S (S (S m)))) at 1.
+  rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
+  rewrite K at 1. reflexivity. lia.
+  apply Nat.sub_add. destruct H2. assumption.
+
+  assert (length (
+    firstn (length (hd ++ a) - 2 ^ S (S (S m))) (hd ++ a) ++
+    skipn (length (hd ++ a) - 2 ^ S (S (S m))) (hd ++ a))
+    mod (2^ (S (Nat.double (Nat.div2 (S (S m)))))) = 0).
+  generalize H5. generalize H4. generalize H.
+  apply tm_step_palindromic_power2_odd.
+
+  rewrite firstn_skipn in H6. rewrite <- Nat.Even_double in H6.
+  assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT.
+  assumption. lia. lia.
+Qed.