Update

2023-01-10 18:04:42 +01:00 · 2023-01-10 18:04:42 +01:00 · 5a6a3dd60e
commit 5a6a3dd60e
parent 33e87e55b5
1 changed files with 234 additions and 11 deletions
--- a/src/thue_morse2.v
+++ b/src/thue_morse2.v
@ -8,21 +8,235 @@ Require Import Bool.
 Import ListNotations.


+Lemma tm_step_consecutive_identical :
+  forall (n : nat) (hd a tl : list bool) (b1 b2 : bool),
+  tm_step n = hd ++ (b1::b1::nil) ++ a ++ (b2::b2::nil) ++ tl
+  -> even (length a) = true.
+Proof.
+  intros n hd a tl b1 b2. intros H.
+  assert (I: even (length hd) = false).
+  assert (J: {even (length hd) = false} + { ~ (even (length hd)) = false}).
+  apply bool_dec. destruct J. assumption. apply not_false_is_true in n0.
+  rewrite app_assoc in H.
+  assert (K: count_occ Bool.bool_dec (hd ++ [b1;b1]) true
+           = count_occ Bool.bool_dec (hd ++ [b1;b1]) false).
+  assert (even (length (hd ++ [b1;b1])) = true).
+  rewrite app_length. rewrite Nat.even_add_even. assumption.
+  simpl. apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
+  generalize H0. generalize H. apply tm_step_count_occ.
+
+
+
+  destruct n.
+  - simpl in H. destruct hd. simpl in H. assert (b1 = false).
+    inversion H. rewrite H0 in H. inversion H. inversion H.
+    symmetry in H2. apply app_eq_nil in H2. destruct H2. inversion H2.
+  - rewrite <- tm_step_lemma in H.
+    assert (I: even (length hd) = false).
+    assert (J: {even (length hd) = false} + { ~ (even (length hd)) = false}).
+    apply bool_dec. destruct J. assumption. apply not_false_is_true in n0.
+
+
+
+Theorem tm_step_count_occ : forall (hd tl : list bool) (n : nat),
+  tm_step n = hd ++ tl -> even (length hd) = true
+  -> count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false.
+
+
+Lemma tm_step_square_size_3 : forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ a ++ tl -> length a = 3
+  -> a = true::false::true::nil \/ a = false::true::false::nil.
+Proof.
+  intros n hd a tl. intros H I.
+  destruct a.
+  - inversion I.
+  - destruct b.
+    + left. destruct a. inversion I. destruct b.
+      * assert (J: a = false::nil). destruct a. inversion I.
+        destruct b.
+        assert (K: tm_step n = hd ++ [true] ++ [true] ++ [true]
+                               ++ a ++ [true] ++ [true] ++ [true] ++ a ++ tl).
+        rewrite H. apply app_inv_head_iff.
+        replace (true::true::true::a) with ([true] ++ [true] ++ [true] ++ a).
+        rewrite <- app_assoc. apply app_inv_head_iff.
+        rewrite <- app_assoc. apply app_inv_head_iff.
+        rewrite <- app_assoc. apply app_inv_head_iff. apply app_inv_head_iff.
+        rewrite <- app_assoc. apply app_inv_head_iff.
+        rewrite <- app_assoc. apply app_inv_head_iff.
+        rewrite <- app_assoc. reflexivity. reflexivity.
+        apply tm_step_cubefree in K. contradiction K. reflexivity.
+        simpl. apply Nat.lt_0_1. simpl in I. apply Nat.succ_inj in I.
+        apply Nat.succ_inj in I. apply Nat.succ_inj in I.
+        rewrite length_zero_iff_nil in I. rewrite I. reflexivity.
+
+
+
+        rewrite app_assoc_reverse.
+        apply app_inv_head_iff.
+
+
+
+Theorem tm_step_cubefree : forall (n : nat) (hd a b tl : list bool),
+  tm_step n = hd ++ a ++ a ++ b ++ tl -> 0 < length a -> a <> b.
+
+
+
+Carré de taille 3 :
+  AABAAB   (impossible)
+  ABBABB    (impossible)
+  ABAABA    (OK)
+  BABBAB    
+
+
+Lemma xxx : forall (n k : nat) (hd pat tl : list bool),
+  tm_step n = hd ++ pat ++ tl
+  -> length pat <= 2^k
+  -> exists (hd2 tl2 : list bool), tm_step (S (S k)) = hd2 ++ pat ++ tl2.
+Proof.
+  intros n k hd pat tl. intros H I.
+  assert (exists (m : nat),
+    (m * 2^(S (S (S k))) <= length hd /\ length (hd++pat) < (S m) * 2^(S (S (S k))))).
+  induction n.
+  - simpl in H. exists 0. rewrite Nat.mul_0_l. rewrite Nat.mul_1_l.
+    split. apply Nat.le_0_l.
+    assert (J: length [false] = length (hd ++ pat ++ tl)).
+    rewrite H. reflexivity. simpl in J. rewrite app_assoc in J.
+    rewrite app_length in J.
+    assert (K: length (hd++pat) <= 1). destruct tl. simpl in J.
+    rewrite Nat.add_0_r in J. rewrite <- J. apply Nat.le_refl.
+    simpl in J. rewrite <- Nat.add_comm in J. symmetry in J.
+    rewrite <- Nat.add_1_l in J. rewrite <- Nat.add_0_r in J.
+    rewrite <- Nat.add_assoc in J. rewrite Nat.add_cancel_l in J.
+    apply Nat.eq_add_0 in J. destruct J. rewrite H1. apply Nat.le_0_1.
+    assert (L: 1 < 2^(S (S (S k)))).
+    rewrite <- Nat.le_succ_l. rewrite Nat.pow_succ_r'.
+    rewrite <- Nat.mul_1_r at 1. apply Nat.mul_le_mono_l.
+    rewrite Nat.le_succ_l.
+    rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+    generalize L. generalize K. apply Nat.le_lt_trans.
+  -
+
+
+    ABCDABCDABCD
+    -> prouver ensuite  length (hd3 ++ pat) < 5 * 2^k
+      ou   length (hd3) < 4 * 2^k
+
+  
+  soit le motif se trouve dans un bloc de 2 répété depuis l'origine,
+  soit il se trouve dans un bloc de 4 répété depuis l'origine
+
+
+
+
+
+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 xxx : forall (k : nat) (hd pat tl : list bool),
+  tm_step (S (S k)) = hd ++ pat ++ tl
+  -> length pat <= 2^k
+    -> (exists (hd2 tl2 : list bool),
+          map negb (tm_step (S (S k))) = hd2 ++ pat ++ tl2).
+Proof.
+  intros k hd pat tl. intros H I.
+  assert (length (hd++pat) <= 2^(S k)
+          \/ (length (hd++pat) > 2^(S k) /\ length (hd++pat) <= 3 * 2^k)
+          \/ length (hd++pat) > 3 * 2^k).
+  assert (length (hd++pat) <= 2^(S k) \/ 2^(S k) < length (hd++pat)).
+  apply Nat.le_gt_cases.
+  assert (length (hd++pat) <= 3*2^k \/ 3*2^k < length (hd++pat)).
+  apply Nat.le_gt_cases.
+  assert (2^(S k) < length (hd++pat) <-> 
+           ((length (hd++pat) > 2^(S k) /\ length (hd++pat) <= 3 * 2^k)
+           \/ 3 * 2^k < length (hd++pat))).
+  split. intro J.
+  destruct H1.
+  left. split. apply J. assumption.
+  right. assumption.
+  intro J. destruct J. destruct H2. apply H2.
+  assert (2^(S k) < 3 * 2^k). simpl. rewrite Nat.add_0_r.
+  rewrite <- Nat.add_lt_mono_l. rewrite <- Nat.add_0_r at 1.
+  rewrite <- Nat.add_lt_mono_l.
+  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+  generalize H2. generalize H3. apply Nat.lt_trans.
+  rewrite H2 in H0. apply H0.
+  destruct H0.
+  - assert (J: exists (tl3 : list bool), tm_step (S k) = hd ++ pat ++ tl3).
+    exists (firstn (2^(S k) - (length (hd++pat))) tl).
+    rewrite tm_build in H. rewrite <- firstn_app_2. rewrite <- firstn_app_2.
+    rewrite app_length. rewrite Nat.add_assoc.
+    rewrite Nat.add_comm. rewrite Nat.sub_add.
+    assert (firstn (2^(S k)) (hd++pat++tl) = firstn (2^(S k)) (hd++pat++tl)).
+    reflexivity. rewrite <- H in H1 at 1.
+    rewrite firstn_app in H1. rewrite tm_size_power2 in H1.
+    rewrite Nat.sub_diag in H1. rewrite firstn_O in H1.
+    rewrite app_nil_r in H1. rewrite <- tm_size_power2 in H1 at 1.
+    rewrite firstn_all in H1. assumption.
+    rewrite <- app_length. assumption.
+    rewrite tm_build. rewrite map_app.
+    rewrite map_map.
+    assert (forall l, map (fun x : bool => negb (negb x)) l = l).
+    intro. induction l. reflexivity.
+    simpl. rewrite IHl. rewrite negb_involutive. reflexivity.
+    rewrite H1. destruct J. rewrite H2.
+    exists (map negb (hd ++ pat ++ x) ++ hd). exists (x).
+    rewrite app_assoc. reflexivity.
+  - destruct H0. destruct H0.
+
+
+    left. assumption.
+  - destruct H0.
+    + destruct H0. right.
+
+
+
+
+
+
+    replace (tl)
+      with ((firstn (2^(S k) - (length (hd++pat))) tl)
+            ++ (skipn (2^(S k) - (length (hd++pat))) tl)) in H.
+
+    replace (tm_step (S k))
+      with (hd ++ pat ++ (firstn (2^(S k) - (length (hd++pat))) tl)) in H.
+    rewrite <- app_assoc in H. apply app_inv_head_iff in H.
+    rewrite <- app_assoc in H. apply app_inv_head_iff in H.
+    apply app_inv_head_iff in H.
+
+
+
+
+
+    rewrite tm_build. rewrite map_app. rewrite map_map.
+
+
+
+
+  right.
+  replace (length (tl ++ pat) > 2^(S k)) with (True).
+  apply Nat.le_gt_cases.
+
+






-(**
-   Under construction
-*)

 Lemma xxx : forall (n k : nat) (hd pat tl : list bool),
  tm_step n = hd ++ pat ++ tl
  -> length pat <= 2^k
  -> exists (hd2 tl2 : list bool),
-       tm_step (S k) = hd2 ++ pat ++ tl2 /\ length (hd2 ++ pat) < 3 * (2^k).
+       tm_step (S (S k)) = hd2 ++ pat ++ tl2 /\ length (hd2 ++ pat) < 3 * (2^k).
 Proof.
  intros n k hd pat tl. intros H I.

@ -32,10 +246,19 @@ Proof.
 L'inégalité finale doit être stricte, car si le motif fait exactement 2^k
 et se situe à la fin des 3 * (2^k) termes, il est aussi au début !

-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).
+
+
+Carré de taille 3 :
+  AABAAB   (impossible)
+  ABBABB    (impossible)
+  ABAABA    (OK)
+  BABBAB    
+
+
+T[2:6] : carré (répété) de taille 2   (mais aussi T[10:14])
+T[4:12] : carré (répété) de taille 4   (mais aussi T[20:28])
+T[8:24] : carré (répété) de taille 8    (mais aussi T[40:56])
+
+Termes de 11 à 17 (exclus) : carré (répété) de taille 3
+Termes de 22 à 34 (exclus) : carré (répété) de taille 6
+Termes de 44 à 68 (exclus) : carré (répété) de taille 12