diff --git a/src/thue_morse2.v b/src/thue_morse2.v index bd9c4f7..fc063eb 100644 --- a/src/thue_morse2.v +++ b/src/thue_morse2.v @@ -8,6 +8,12 @@ Require Import Bool. Import ListNotations. +(** + The following lemma, while not of truly general use, is + used in several proofs and has therefore its own dedicated + section here. +*) + 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 @@ -79,6 +85,11 @@ Proof. Qed. +(** + The following lemmas and theorems are all related to + squares of odd length in the Thue-Morse sequence. +*) + Lemma tm_step_factor5 : forall (n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ tl -> length a = 5 -> a <> [ true; false; true; false; true]. @@ -282,7 +293,7 @@ Proof. Qed. -Lemma tm_step_odd_square : forall (n : nat) (hd a tl : list bool), +Theorem tm_step_odd_square : forall (n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> odd (length a) = true -> length a < 4. Proof. intros n hd a tl. intros H I. @@ -316,144 +327,9 @@ Qed. - - - -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. +(** + New section +*) @@ -461,19 +337,7 @@ Proof. - - -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 /\ length (hd2 ++ pat) < 3 * (2^k). -Proof. - intros n k hd pat tl. intros H I. - - - - +(* 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 ! @@ -493,3 +357,4 @@ 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 + *)