From 8c7bd4940a6579ae5badb8302bca5b37ba6b3050 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sat, 11 Feb 2023 08:40:24 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 129 ---------------------------------------------- src/thue_morse4.v | 42 +++++++++++++++ 2 files changed, 42 insertions(+), 129 deletions(-) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index 439b27b..3235368 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -301,15 +301,6 @@ Proof. Qed. -(** - In this notebook I call "proper palindrome" in the Thue-Morse sequence, - any palindromic subsequence such that the middle (of the palindromic - subsequence) is not also the middle of a wider palindromic subsequence. - In ther words, a proper palindrome can not be enlarged by adding more - termes on both sides. -*) - - (* palidrome 2*4 : soit centré en 4n soit pas plus de 2*6 *) (* modifier l'énoncé : ajouter le modulo = 2 ET la différence sur le 7ème ET existence d'un palindrome 2 * - *) @@ -2707,123 +2698,3 @@ Proof. apply tm_step_palindromic_power2_odd with (n := n) (tl := tl). assumption. assumption. rewrite <- E'. assumption. 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. - (* - 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. - - - - -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. - -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) - - - - -(* -Theorem tm_step_palindrome_power2_reciprocal : - forall (m n k : nat) (hd tl : list bool), - tm_step n = hd ++ tl - -> length hd = S (Nat.double k) * 2^m - -> odd m = true - -> skipn ((length hd) - 2^m) hd = rev (firstn (2^m) tl). -Proof. - intros m n. - assert (A: odd m = true - -> (forall k hd tl, tm_step n = hd ++ tl - ->length hd = S (Nat.double k) * 2^m - -> skipn ((length hd) - 2^m) hd = rev (firstn (2^m) tl)) - -> (forall k hd tl, tm_step (S n) = hd ++ tl - -> length hd = S (Nat.double k) * 2^m - -> skipn ((length hd) - 2^m) hd = rev (firstn (2^m) tl))). - intros H I. - intros k hd tl. intros J K. - - rewrite tm_build in J. - *) - - -(* -Lemma tm_step_proper_palindrome_center : - forall (m n k : nat) (hd a tl : list bool), - tm_step n = hd ++ a ++ (rev a) ++ tl - -> 6 < length a - -> length a = 2^(Nat.double m) (* palindrome non propre *) - -> skipn (length hd - length a) hd = rev (firstn (length a) tl). -*) diff --git a/src/thue_morse4.v b/src/thue_morse4.v index 92f8b9d..927bb78 100644 --- a/src/thue_morse4.v +++ b/src/thue_morse4.v @@ -783,5 +783,47 @@ Proof. assert (even m = true). generalize J. generalize I. generalize H. apply tm_step_square_rev_even. + (* + TODO: voir s'il faut remplacer la dernière implication + par une équivalence + *) +Abort. + + + +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. +Abort.