From f15ee10bbb130d04852c2a87b1e260ffd58c36fe Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sun, 22 Jan 2023 08:16:44 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 77 ++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 62 insertions(+), 15 deletions(-) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index f16fb72..8dd89b4 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -308,7 +308,8 @@ Qed. (* 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 *) +(* modifier l'énoncé : ajouter le modulo = 2 ET la différence sur le 7ème + ET existence d'un palindrome 2 * - *) Lemma tm_step_palindromic_length_8 : forall (n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ (rev a) ++ tl @@ -687,12 +688,23 @@ reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H. remonter encore d'un cran et prouver la différence à ce stade, TFFT TFTF FTFT TFFT (µ de TF TT FF TF) pourquoi impossible ? FTFT TFTF FTFT TFTF (µ de FF TT FF TT) pourquoi impossible ? - TFT TFT FF TFT TFT + FTTFTFFT FTTFTF (pb avec le repeating_pattern de 8 ???) + TFT TFT FF TFT TFT (si on part sur 2 mod 8) + (idem en partant de la droite pour 6 mod 8) revoir l'énoncé en fonction + +Le lemme repeating_patterns se base sur les huit premiers termes de TM : +[False, True, True, False, True, False, False, True] + --> il y a une contradiction à chaque fois + + *) +Admitted. + + @@ -701,19 +713,6 @@ reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H. - -Lemma tm_step_factor4_1mod4 : forall (n' : nat) (w z y : list bool), - tm_step n' = w ++ z ++ y - -> length z = 4 -> length w mod 4 = 1 - -> exists (x : bool), firstn 2 z = [x;x]. -Lemma tm_step_factor4_3mod4 : forall (n' : nat) (w z y : list bool), - tm_step n' = w ++ z ++ y - -> length z = 4 -> length w mod 4 = 3 - -> exists (x : bool), skipn 2 z = [x;x]. - - - - (* si on a ensuite le bloc précédent identique aux deux premiers de a @@ -748,6 +747,54 @@ Lemma tm_step_factor4_3mod4 : forall (n' : nat) (w z y : list bool), F T | F T | T F ][ F T | T F | T F 4n (par examen des cinq premiers termes à gauche) + *) + + +Lemma tm_step_palindromic_length_12 : + forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ rev a ++ tl + -> 6 < length a + -> length (hd ++ a) mod 4 = 0. +Proof. + intros n hd a tl. intros H I. + assert (J: even (length (hd ++ a)) = true). + assert (0 < length a). + apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I. + apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I. + apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I. + assumption. generalize H0. generalize H. + apply tm_step_palindromic_even_center. + apply even_mod4 in J. destruct J. assumption. + + rewrite <- firstn_skipn with (l := a) (n := length a - 4) in H. + rewrite rev_app_distr in H. rewrite <- app_assoc in H. + rewrite app_assoc in H. + assert (length (skipn (length a - 4) a) = 4). rewrite skipn_length. + replace (length a) with ((length a - 4) + 4) at 1. rewrite Nat.add_comm. + rewrite Nat.add_sub. reflexivity. rewrite Nat.add_comm. + rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. reflexivity. + apply Nat.le_refl. apply Nat.lt_le_incl. + apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I. + assumption. + + pose (hd' := hd ++ firstn (length a - 4) a). fold hd' in H. + pose (a' := skipn (length a - 4) a). fold a' in H. + rewrite <- app_assoc in H. + pose (tl' := rev (firstn (length a - 4) a) ++ tl). fold tl' in H. + + assert (K: length (hd' ++ a') mod 4 = 0 + \/ last hd' false <> List.hd false tl'). + fold a' in H1. generalize H1. generalize H. + apply tm_step_palindromic_length_8. + destruct K. + + + + + + + + Lemma tm_step_proper_palindromic_center : forall (m n k i: nat) (hd a tl : list bool),