Update

src/thue_morse3.v

@@ -2742,9 +2742,29 @@ Proof.
     assert (Nat.Even (S m) \/ Nat.Odd (S m)). apply Nat.Even_or_Odd.
     destruct H2.
     + assert (E := H2). apply Nat.Even_double in H2. rewrite <- H2 in H1.
+      (*
+      assert (length (hd ++ a ++ rev a) mod 2^(S m) = 2^m).
+      rewrite app_assoc. rewrite app_length.
+      rewrite <- Nat.add_mod_idemp_l. rewrite H1. rewrite rev_length.
+      rewrite I. rewrite Nat.mod_small_iff. simpl.
+      apply Nat.lt_add_pos_r. rewrite Nat.add_0_r.
+      rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+      apply Nat.pow_nonzero. easy. apply Nat.pow_nonzero. easy.
+      *)
+      (*
+      apply Nat.Even_double in H0.
+      *)
+
       (* montrer que sur les repeating patterns de taille 2^(S (S m))
          les deux valeurs centrales sont distinctes *)
       rewrite <- Nat.div_exact in H1.
+      (* on prouve que  (length (hd ++ a) / 2^(S m)) est nn nul *)
+      destruct (length (hd ++ a) / 2^(S m)).
+      rewrite Nat.mul_0_r in H1. rewrite app_length in H1.
+      apply Nat.eq_add_0 in H1. destruct H1. rewrite H3 in I.
+      symmetry in I. apply Nat.pow_nonzero in I. contradiction. easy.
+
+Abort.
 
 
 
@@ -2765,6 +2785,13 @@ Lemma tm_step_repeating_patterns2 :
   -> pat = tm_step m \/ pat = map negb (tm_step m).
 Proof.
 
+Nat.mul_mod_distr_l:
+  forall a b c : nat, b <> 0 -> c <> 0 -> (c * a) mod (c * b) = c * (a mod b)
+Nat.mul_mod_distr_r:
+  forall a b c : nat, b <> 0 -> c <> 0 -> (a * c) mod (b * c) = a mod b * c
+Nat.mod_mul_r:
+  forall a b c : nat,
+  b <> 0 -> c <> 0 -> a mod (b * c) = a mod b + b * ((a / b) mod c)
 
 
 

src/thue_morse4.v

@@ -693,6 +693,87 @@ Proof.
 Qed.
 
 
+Lemma tm_square_rev' :
+  forall (m n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ a ++ tl
+  -> length a = 2^m
+  -> a = rev a
+  -> even m = true.
+Proof.
+  intros m n hd a tl. intros H I J.
+
+  assert (0 < length a). rewrite I.
+  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+
+  assert (  (a = rev a /\ exists j,
+         length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j))
+     \/ (a = map negb (rev a) /\ exists j,
+         length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j)))).
+  generalize H0. generalize H. apply tm_step_square_rev.
+  destruct H1. destruct H1. destruct H2. destruct H2.
+  rewrite I in H2. apply Nat.pow_inj_r in H2. rewrite H2.
+  rewrite Nat.double_twice. rewrite Nat.even_mul. reflexivity. lia.
+  rewrite I in H2.
+
+  assert (Nat.log2 (2^m) = Nat.log2 (2^m)). reflexivity. rewrite H2 in H3 at 2.
+  rewrite Nat.log2_pow2 in H3.
+  rewrite Nat.log2_mul_pow2 in H3. replace (Nat.log2 3) with 1 in H3.
+  rewrite H3 in H2. rewrite Nat.add_succ_r in H2.
+  rewrite Nat.add_0_r in H2. rewrite Nat.pow_succ_r in H2.
+  rewrite Nat.mul_cancel_r in H2. inversion H2.
+  apply Nat.pow_nonzero. easy. lia. reflexivity. lia. lia. lia.
+
+  destruct H1. rewrite J in H1 at 1.
+  destruct a. inversion H0. simpl in H1.
+  rewrite map_app in H1. apply app_inj_tail in H1.
+  destruct H1. destruct b. inversion H3. inversion H3.
+Qed.
+
+
+Lemma xxx :
+  forall (m n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ a ++ tl
+  -> length a = 2^m
+  -> a = rev a
+  -> even m = true /\ length (hd ++ a) mod (2^(S m)) = 0.
+Proof.
+  intros m n hd a tl. intros H I J.
+
+  assert (0 < length a). rewrite I.
+  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+
+  assert (even m = true).
+  assert (  (a = rev a /\ exists j,
+         length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j))
+     \/ (a = map negb (rev a) /\ exists j,
+         length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j)))).
+  generalize H0. generalize H. apply tm_step_square_rev.
+  destruct H1. destruct H1. destruct H2. destruct H2.
+  rewrite I in H2. apply Nat.pow_inj_r in H2. rewrite H2.
+  rewrite Nat.double_twice. rewrite Nat.even_mul. reflexivity. lia.
+  rewrite I in H2.
 
 
 
+
+  assert (even (length (hd ++ a)) = true).
+  generalize H0. generalize H. apply tm_step_palindromic_even_center.
+
+
+
+
+
+  replace (List.hd false a) with (negb (List.hd false (rev a))).
+
+
+
+
+Theorem tm_step_square_rev :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ a ++ tl
+  -> 0 < length a
+  -> (  (a = rev a /\ exists j,
+         length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j))
+     \/ (a = map negb (rev a) /\ exists j,
+         length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j)))).
+Proof.