Update

src/thue_morse3.v

@@ -2709,6 +2709,66 @@ Proof.
 Qed.
 
 
+Theorem tm_step_palindrome_power2' :
+  forall (m n : nat) (hd a tl : list bool),
+    tm_step n = hd ++ a ++ (rev a) ++ tl
+    -> length a = 2^m
+    -> 2 < m
+    -> length (hd ++ a) mod 2^ (Nat.double (Nat.div2 (S m))) = 2^ (pred (Nat.double (Nat.div2 (S m)))).
+Proof.
+  intros m n hd a tl. intros H I J.
+  assert (K: length (hd ++ a) mod 2^ (pred (Nat.double (Nat.div2 (S m)))) = 0).
+  generalize J. generalize I. generalize H. apply tm_step_palindrome_power2.
+  rewrite <- Nat.div_exact in K.
+  assert (L: Nat.Even 
+    (length (hd ++ a) / 2 ^ pred (Nat.double (Nat.div2 (S m))))
+    \/ Nat.Odd
+    (length (hd ++ a) / 2 ^ pred (Nat.double (Nat.div2 (S m))))).
+  apply Nat.Even_or_Odd.
+  destruct L.
+  - assert (length (hd ++ a) mod 2 ^ Nat.double (Nat.div2 (S m)) = 0).
+    rewrite K. apply Nat.Even_double in H0. symmetry in H0.
+    rewrite Nat.double_twice in H0. rewrite <- H0. rewrite Nat.mul_assoc.
+    rewrite Nat.mul_shuffle0. rewrite Nat.mul_comm. rewrite Nat.mul_assoc.
+    rewrite <- Nat.pow_succ_r. rewrite Nat.succ_pred_pos. rewrite Nat.mul_comm.
+    apply Nat.mod_mul. apply Nat.pow_nonzero. easy.
+    assert (Nat.Even (S m) \/ Nat.Odd (S m)). apply Nat.Even_or_Odd.
+    destruct H1.
+    apply Nat.Even_double in H1. rewrite <- H1. apply Nat.lt_0_succ.
+    apply Nat.Odd_double in H1. apply Nat.succ_inj in H1.
+    rewrite <- H1. apply Nat.lt_succ_l in J. apply Nat.lt_succ_l in J.
+    assumption. apply Nat.le_0_l.
+    (* on cherche une contradiction à partir de H1 *)
+    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.
+      (* montrer que sur les repeating patterns de taille 2^(S (S m))
+         les deux valeurs centrales sont distinctes *)
+      rewrite <- Nat.div_exact in H1.
+
+
+
+
+Lemma tm_step_repeating_patterns :
+  forall (n m i j : nat),
+  i < 2^m -> j < 2^m
+  -> forall k, k < 2^n -> nth_error (tm_step m) i
+                        = nth_error (tm_step m) j
+                      <-> nth_error (tm_step (m+n)) (k * 2^m + i)
+                        = nth_error (tm_step (m+n)) (k * 2^m + j).
+
+Lemma tm_step_repeating_patterns2 :
+  forall (n m : nat) (hd pat tl : list bool), 
+     tm_step n = hd ++ pat ++ tl
+  -> length pat = 2^m
+  -> length hd mod (2^m) = 0
+  -> pat = tm_step m \/ pat = map negb (tm_step m).
+Proof.
+
+
+
+
+
 (*
 Theorem tm_step_palindrome_power2_reciprocal :
   forall (m n k : nat) (hd tl : list bool),

src/thue_morse4.v

@@ -696,125 +696,3 @@ Qed.
 
 
 
-(*
-Lemma xxx :
-  forall (n : nat) (hd a tl : list bool),
-  tm_step n = hd ++ a ++ a ++ tl
-  -> 0 < length a
-  -> a = rev a \/ a = map negb (rev a).
-Proof.
-  intros n hd a tl. intros H I.
-
-  destruct n. assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
-  rewrite H in H0 at 2. rewrite app_length in H0. rewrite app_length in H0.
-  rewrite app_length in H0. rewrite Nat.add_comm in H0.
-  destruct a. inversion I. rewrite <- Nat.add_assoc in H0.
-  rewrite <- Nat.add_assoc in H0. simpl in H0. rewrite Nat.add_succ_r in H0.
-  apply Nat.succ_inj in H0. apply Nat.neq_0_succ in H0. contradiction.
-
-  assert (exists k j, length a = S (Nat.double k) * 2^j).
-  apply trailing_zeros; assumption. destruct H0. destruct H0.
-  assert (x = 0 \/ x = 1). generalize H0. generalize H.
-  apply tm_step_square_size.
-
-  generalize dependent n. generalize dependent hd. generalize dependent a.
-  generalize dependent tl. generalize dependent x.
-  induction x0; intros x K tl a J I hd n H.
-  - destruct K; rewrite H0 in I; destruct a.
-    inversion J. destruct a. left. reflexivity. inversion I.
-    inversion I. destruct a. inversion I. destruct a. inversion I.
-    destruct a.
-    assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1.
-    rewrite e. left. reflexivity.
-    assert ({b0=b1} + {~ b0=b1}). apply bool_dec. destruct H1.
-    rewrite e in H.
-    replace (hd ++ [b; b1; b1] ++ [b; b1; b1] ++ tl)
-      with ((hd ++ [b]) ++ [b1;b1] ++ [b] ++ [b1;b1] ++ tl) in H.
-    apply tm_step_consecutive_identical' in H. inversion H.
-    rewrite <- app_assoc. reflexivity.
-    assert (b = b0). destruct b; destruct b0; destruct b1;
-    reflexivity || contradiction n0 || contradiction n1; reflexivity.
-    rewrite H1 in H.
-    replace (hd ++ [b0; b0; b1] ++ [b0; b0; b1] ++ tl)
-      with (hd ++ [b0;b0] ++ [b1] ++ [b0;b0] ++ ([b1] ++ tl)) in H.
-    apply tm_step_consecutive_identical' in H. inversion H. reflexivity.
-    inversion I.
-  - assert (even (length a) = true).
-    rewrite Nat.mul_comm in I. rewrite Nat.pow_succ_r in I. rewrite I.
-    rewrite Nat.even_mul. rewrite Nat.even_mul. reflexivity.
-    apply Nat.le_0_l.
-    assert (even (length (hd ++ a)) = true).
-    generalize J. generalize H. apply tm_step_square_pos.
-    assert (even (length hd) = true).
-    rewrite app_length in H1. rewrite Nat.even_add in H1.
-    rewrite H0 in H1. destruct (Nat.even (length hd)). reflexivity.
-    inversion H1.
-
-
-
-    (se débarrasser du S x0 en I)
-    generalize H. generalize n. generalize hd. generalize I. generalize J.
-    apply IHx0.
-
-
-Lemma tm_step_morphism4 :
-  forall (n : nat) (hd a b tl : list bool),
-  tm_step (S n) = hd ++ a ++ b ++ tl
-  -> even (length hd) = true
-  -> even (length a) = true
-  -> even (length b) = true
-  -> tm_step (S n) = tm_morphism
-      (firstn (Nat.div2 (length hd)) (tm_step n) ++
-       firstn (Nat.div2 (length a))
-         (skipn (Nat.div2 (length hd)) (tm_step n)) ++
-       firstn (Nat.div2 (length b))
-         (skipn (Nat.div2 (length (hd ++ a))) (tm_step n)) ++
-       skipn (Nat.div2 (length (hd ++ a ++ b))) (tm_step n)).
- *)
-
-
-
-
-
-Lemma xxx :
-  forall (n : nat) (hd a tl : list bool),
-  tm_step n = hd ++ a ++ a ++ tl
-  -> a = rev a
-  -> 0 < length a
-  -> length a <= 4
-    \/ (exists m, length a = 2 ^ m /\
-        length (hd ++ a) mod 2 ^ pred (Nat.double (Nat.div2 (S m))) = 0)
-    \/ length a = 3 * 2^(pred (Nat.log2 (length a))).
-Proof.
-  intros n hd a tl. intros H I J.
-  destruct n. assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
-  rewrite H in H0 at 2. rewrite app_length in H0. rewrite app_length in H0.
-  rewrite app_length in H0. rewrite Nat.add_comm in H0.
-  destruct a. inversion J. rewrite <- Nat.add_assoc in H0.
-  rewrite <- Nat.add_assoc in H0. simpl in H0. rewrite Nat.add_succ_r in H0.
-  apply Nat.succ_inj in H0. apply Nat.neq_0_succ in H0. contradiction.
-
-  assert (exists k j, length a = S (Nat.double k) * 2^j).
-  apply trailing_zeros; assumption. destruct H0. destruct H0.
-  assert (x = 0 \/ x = 1). generalize H0. generalize H.
-  apply tm_step_square_size.
-
-  rewrite I in H at 2.
-
-  destruct H1; rewrite H1 in H0.
-  - rewrite Nat.mul_1_l in H0.
-    assert (length a <= 4 \/ 4 < length a). apply Nat.le_gt_cases.
-    destruct H2. left. assumption.
-    assert (2 < x0). destruct x0. rewrite H0 in H2. inversion H2.
-    inversion H4. destruct x0. rewrite H0 in H2. inversion H2.
-    inversion H4. inversion H6. destruct x0. rewrite H0 in H2.
-    inversion H2. inversion H4. inversion H6. inversion H8. inversion H10.
-    lia.
-    assert (length (hd ++ a) mod 2^(pred (Nat.double (Nat.div2 (S x0)))) = 0).
-    generalize H3. generalize H0. generalize H.
-    apply tm_step_palindrome_power2.
-    right. left. exists x0. split; assumption.
-  - right. right. rewrite H0. rewrite Nat.mul_cancel_l.
-    rewrite Nat.log2_mul_pow2. rewrite Nat.add_1_r.
-    rewrite Nat.pred_succ. reflexivity. lia. lia. lia.
-Qed.