From c1dd9ca8fb42bc408cc83c232f6dcb1950317206 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Fri, 20 Jan 2023 09:56:23 +0100 Subject: [PATCH] Update --- src/thue_morse.v | 156 +++++++++++++++++++++++++--------------------- src/thue_morse3.v | 101 +++++++++++++++++++++++++++++- 2 files changed, 183 insertions(+), 74 deletions(-) diff --git a/src/thue_morse.v b/src/thue_morse.v index 5ca2592..2088564 100644 --- a/src/thue_morse.v +++ b/src/thue_morse.v @@ -1012,30 +1012,10 @@ Proof. Qed. -Lemma tm_step_factor4_odd_prefix : forall (n : nat) (hd a tl : list bool), - tm_step n = hd ++ a ++ tl - -> length a = 4 -> odd (length hd) = true - -> exists (x : bool) (u v : list bool), a = u ++ [x;x] ++ v. -Proof. - intros n hd a tl. intros H I J. - - assert (K: 1 = (length hd) mod 2). - apply Nat.mod_unique with (q := Nat.div2 (length hd)). apply Nat.lt_1_2. - replace (1) with (Nat.b2n (Nat.odd (length hd))) at 2. - apply Nat.div2_odd. rewrite J. reflexivity. - - assert (L: (length hd) mod (2*2) - = (length hd) mod 2 + 2 * (((length hd) / 2) mod 2)). - apply Nat.mod_mul_r; easy. rewrite <- K in L. - replace (2*2) with (4) in L. rewrite <- Nat.bit0_mod in L. - - assert (M: (length hd) mod 4 = 1 \/ (length hd) mod 4 = 3). rewrite L. - destruct (Nat.testbit (length hd / 2) 0) ; [right | left] ; reflexivity. - - assert (forall (n' : nat) (w z y : list bool), +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]). + -> exists (x : bool), firstn 2 z = [x;x]. intros n' w z y. intros G0 G1 G2. assert (U: 4 * (length w / 4) <= length w). apply Nat.mul_div_le. easy. @@ -1070,11 +1050,11 @@ Proof. rewrite nth_error_app1 in O. rewrite nth_error_app2 in O. rewrite Nat.sub_succ_l in O. rewrite Nat.sub_diag in O. rewrite nth_error_app1 in O. destruct O. - assert (nth_error z 0 = nth_error z 1). apply H0. reflexivity. - rewrite nth_error_nth' with (d := false) in H2. - rewrite nth_error_nth' with (d := false) in H2. - exists (nth 0 z false). inversion H2. - rewrite H4 at 2. + assert (nth_error z 0 = nth_error z 1). apply H. reflexivity. + rewrite nth_error_nth' with (d := false) in H1. + rewrite nth_error_nth' with (d := false) in H1. + exists (nth 0 z false). inversion H1. + rewrite H3 at 2. destruct z. inversion G1. destruct z. inversion G1. reflexivity. rewrite G1. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. rewrite G1. apply Nat.lt_0_succ. @@ -1085,53 +1065,87 @@ Proof. reflexivity. easy. assumption. rewrite Nat.add_succ_r. rewrite <- Nat.div_mod_eq. reflexivity. reflexivity. apply Nat.lt_1_2. reflexivity. +Qed. + +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]. +Proof. + intros n hd a tl. intros H I M. + assert ((length (hd ++ (firstn 2 a))) mod 4 = 1). + rewrite app_length. rewrite firstn_length. rewrite I. + rewrite <- Nat.add_mod_idemp_l. rewrite M. reflexivity. easy. + assert (tm_step (S n) = tm_step n ++ map negb (tm_step n)). + apply tm_build. rewrite H in H1. + assert (length ((skipn 2 a) + ++ (firstn 2 (tl ++ (map negb (hd ++ a ++ tl))))) = 4). + rewrite app_length. rewrite skipn_length. rewrite I. + rewrite firstn_length. rewrite app_length. rewrite <- H. + rewrite map_length. + assert (4 <= length tl + length (tm_step n)). + assert (Q: length a <= length (tm_step n)). rewrite H. + rewrite app_length. rewrite app_length. + rewrite Nat.add_assoc. rewrite Nat.add_shuffle0. + apply Nat.le_add_l. rewrite I in Q. + rewrite <- Nat.add_0_l at 1. apply Nat.add_le_mono. + apply Nat.le_0_l. assumption. rewrite Nat.min_l. reflexivity. + assert (2 <= 4). apply le_n_S. apply le_n_S. apply Nat.le_0_l. + generalize H2. generalize H3. apply Nat.le_trans. + replace ((hd ++ a ++ tl) ++ map negb (hd ++ a ++ tl)) + with ((hd ++ firstn 2 a) + ++ (skipn 2 a ++ firstn 2 (tl ++ map negb (hd ++ a ++ tl))) + ++ (skipn 2 (tl ++ map negb (hd ++ a ++ tl)))) in H1. + assert (exists (x : bool), + firstn 2 (skipn 2 a ++ firstn 2 (tl ++ map negb (hd ++ a ++ tl))) + = [x;x]). + generalize H0. generalize H2. generalize H1. apply tm_step_factor4_1mod4. + destruct H3. exists x. + rewrite <- H3. rewrite firstn_app. rewrite skipn_length. rewrite I. + replace (2 - (4 - 2)) with 0. rewrite firstn_O. + rewrite app_nil_r. + destruct a. inversion I. destruct a. inversion I. + destruct a. inversion I. destruct a. inversion I. + destruct a. reflexivity. inversion I. + reflexivity. + rewrite <- app_assoc. symmetry. rewrite <- app_assoc. + apply app_inv_head_iff. + rewrite <- app_assoc. symmetry. rewrite <- app_assoc. + rewrite firstn_skipn. + rewrite <- firstn_skipn with (n := 2) (l := a) at 4. + rewrite <- app_assoc. reflexivity. +Admitted. + + +Lemma tm_step_factor4_odd_prefix : forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ tl + -> length a = 4 -> odd (length hd) = true + -> exists (x : bool) (u v : list bool), a = u ++ [x;x] ++ v. +Proof. + intros n hd a tl. intros H I J. + + assert (K: 1 = (length hd) mod 2). + apply Nat.mod_unique with (q := Nat.div2 (length hd)). apply Nat.lt_1_2. + replace (1) with (Nat.b2n (Nat.odd (length hd))) at 2. + apply Nat.div2_odd. rewrite J. reflexivity. + + assert (L: (length hd) mod (2*2) + = (length hd) mod 2 + 2 * (((length hd) / 2) mod 2)). + apply Nat.mod_mul_r; easy. rewrite <- K in L. + replace (2*2) with (4) in L. rewrite <- Nat.bit0_mod in L. + + assert (M: (length hd) mod 4 = 1 \/ (length hd) mod 4 = 3). rewrite L. + destruct (Nat.testbit (length hd / 2) 0) ; [right | left] ; reflexivity. destruct M as [M | M]. - assert (exists (x : bool), firstn 2 a = [x;x]). - generalize M. generalize I. generalize H. apply H0. - destruct H1. exists x. exists nil. exists (skipn 2 a). - rewrite app_nil_l. rewrite <- H1. symmetry. apply firstn_skipn. - - assert ((length (hd ++ (firstn 2 a))) mod 4 = 1). - rewrite app_length. rewrite firstn_length. rewrite I. - rewrite <- Nat.add_mod_idemp_l. rewrite M. reflexivity. easy. - assert (tm_step (S n) = tm_step n ++ map negb (tm_step n)). - apply tm_build. rewrite H in H2. - assert (length ((skipn 2 a) - ++ (firstn 2 (tl ++ (map negb (hd ++ a ++ tl))))) = 4). - rewrite app_length. rewrite skipn_length. rewrite I. - rewrite firstn_length. rewrite app_length. rewrite <- H. - rewrite map_length. - assert (4 <= length tl + length (tm_step n)). - assert (Q: length a <= length (tm_step n)). rewrite H. - rewrite app_length. rewrite app_length. - rewrite Nat.add_assoc. rewrite Nat.add_shuffle0. - apply Nat.le_add_l. rewrite I in Q. - rewrite <- Nat.add_0_l at 1. apply Nat.add_le_mono. - apply Nat.le_0_l. assumption. rewrite Nat.min_l. reflexivity. - assert (2 <= 4). apply le_n_S. apply le_n_S. apply Nat.le_0_l. - generalize H3. generalize H4. apply Nat.le_trans. - replace ((hd ++ a ++ tl) ++ map negb (hd ++ a ++ tl)) - with ((hd ++ firstn 2 a) - ++ (skipn 2 a ++ firstn 2 (tl ++ map negb (hd ++ a ++ tl))) - ++ (skipn 2 (tl ++ map negb (hd ++ a ++ tl)))) in H2. - assert (exists (x : bool), - firstn 2 (skipn 2 a ++ firstn 2 (tl ++ map negb (hd ++ a ++ tl))) - = [x;x]). - generalize H1. generalize H3. generalize H2. apply H0. - destruct H4. exists x. exists (firstn 2 a). exists nil. - rewrite <- H4. rewrite firstn_app. rewrite skipn_length. rewrite I. - replace (2 - (4 - 2)) with 0. rewrite firstn_O. - rewrite app_nil_r. rewrite app_nil_r. - destruct a. inversion I. destruct a. inversion I. - destruct a. inversion I. destruct a. inversion I. - destruct a. reflexivity. inversion I. - reflexivity. - rewrite <- app_assoc. symmetry. rewrite <- app_assoc. - apply app_inv_head_iff. - rewrite <- app_assoc. symmetry. rewrite <- app_assoc. - rewrite firstn_skipn. - rewrite <- firstn_skipn with (n := 2) (l := a) at 4. - rewrite <- app_assoc. reflexivity. + generalize M. generalize I. generalize H. apply tm_step_factor4_1mod4. + destruct H0. exists x. exists nil. exists (skipn 2 a). + rewrite app_nil_l. rewrite <- H0. symmetry. apply firstn_skipn. + - assert (exists (x : bool), skipn 2 a = [x;x]). + generalize M. generalize I. generalize H. apply tm_step_factor4_3mod4. + destruct H0. exists x. exists (firstn 2 a). exists nil. + rewrite app_nil_r. rewrite <- H0. symmetry. apply firstn_skipn. - reflexivity. Qed. diff --git a/src/thue_morse3.v b/src/thue_morse3.v index 24a688f..094b4c5 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -280,6 +280,78 @@ Proof. Qed. +Lemma tm_step_palindromic_negb_center : + forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ map negb (rev a) ++ tl + -> 1 < length a + -> even (length (hd ++ a)) = true. +Proof. + intros n hd a tl. intros H I. + assert (J: a = firstn (length a - 2) a ++ skipn (length a - 2) a). + symmetry. apply firstn_skipn. rewrite J in H. + rewrite rev_app_distr in H. rewrite map_app in H. + rewrite <- app_assoc in H. rewrite <- app_assoc in H. + rewrite app_assoc in H. + replace ( skipn (length a - 2) a ++ + map negb (rev (skipn (length a - 2) a)) ++ + map negb (rev (firstn (length a - 2) a)) ++ tl ) + with ( ( skipn (length a - 2) a ++ + map negb (rev (skipn (length a - 2) a)) ) ++ + map negb (rev (firstn (length a - 2) a)) ++ tl ) in H. + + assert (length (skipn (length a - 2) a) = 2). rewrite skipn_length. + replace (length a) with (2 + (length a - 2)) at 1. rewrite Nat.add_sub. + reflexivity. rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. + rewrite Nat.sub_diag. reflexivity. easy. rewrite Nat.le_succ_l. + assumption. + + assert (length + (skipn (length a - 2) a ++ map negb (rev (skipn (length a - 2) a))) = 4). + rewrite app_length. rewrite map_length. rewrite rev_length. + rewrite H0. reflexivity. + + assert (K: {even (length (hd ++ firstn (length a - 2) a))=true} + + {~ even (length (hd ++ firstn (length a - 2) a))=true}). + apply bool_dec. destruct K. + rewrite J. rewrite app_assoc. rewrite app_length. rewrite Nat.even_add. + rewrite e. rewrite H0. reflexivity. apply not_true_is_false in n0. + + assert (exists (x : bool) (u v : list bool), + (skipn (length a - 2) a ++ map negb (rev (skipn (length a - 2) a))) + = u ++ [x;x] ++ v). + assert (odd (length (hd ++ firstn (length a - 2) a)) = true). + rewrite <- Nat.negb_even. rewrite n0. reflexivity. generalize H2. + generalize H1. generalize H. apply tm_step_factor4_odd_prefix. + + destruct H2. destruct H2. destruct H2. rewrite H2 in H1. + + destruct x0. + assert (skipn (length a - 2) a = [x;x]). + assert (length (skipn (length a - 2) a) = length ([x;x])). rewrite H0. + reflexivity. generalize H3. generalize H2. rewrite app_nil_l. + apply app_eq_length_head. rewrite H3 in H. + + TODO contradiction en H + + + + +Lemma tm_step_factor4_odd_prefix : forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ tl + -> length a = 4 -> odd (length hd) = true + -> exists (x : bool) (u v : list bool), a = u ++ [x;x] ++ v. + + + + pose (hd' := hd ++ firstn (length a - 2) a). + pose (tl' := map negb (rev (firstn (length a - 2) a)) ++ tl). + pose (a' := skipn (length a - 2) a). + fold hd' in H. fold tl' in H. fold a' in H. + replace (a' ++ map negb (rev a') ++ tl') + with ((a' ++ map negb (rev a')) ++ tl') in H. + assert (length pat = 4). + + (** In this notebook I call "proper palindrome" in the Thue-Morse sequence, any palindromic subsequence such that the middle (of the palindromic @@ -355,6 +427,8 @@ Proof. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. generalize H0. generalize H. apply tm_step_palindromic_even_center. + assert (H' := H). + (* proof that 0 < n *) destruct n. assert (length (tm_step 0) = length (tm_step 0)). reflexivity. @@ -421,7 +495,7 @@ Proof. (skipn (Nat.div2 (length hd)) (tm_step n)))). fold hd' in H. fold a' in H. fold tl' in H. - assert (length a' = 2^S (Nat.double m)). unfold a'. + assert (I': length a' = 2^S (Nat.double m)). unfold a'. rewrite firstn_length_le. rewrite I. rewrite Nat.double_S. rewrite Nat.pow_succ_r. rewrite Nat.div2_double. reflexivity. apply le_0_n. rewrite skipn_length. @@ -429,10 +503,29 @@ Proof. rewrite Nat.mul_comm. rewrite <- Nat.add_0_r at 1. replace 0 with (Nat.b2n (Nat.odd (length a))) at 2. rewrite <- Nat.div2_odd. rewrite Nat.mul_sub_distr_r. + replace (length (tm_step n) * 2) with (length (tm_step (S n))). + replace (Nat.div2 (length hd) * 2) with (length hd). + rewrite H'. rewrite app_length. rewrite Nat.add_sub_swap. + rewrite Nat.sub_diag. simpl. rewrite app_length. + rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_le_mono_l. + apply Nat.le_0_l. apply Nat.le_refl. + rewrite Nat.mul_comm. symmetry. rewrite <- Nat.add_0_r at 1. + replace 0 with (Nat.b2n (Nat.odd (length hd))) at 2. + rewrite <- Nat.div2_odd. reflexivity. + rewrite <- Nat.negb_even. rewrite L. reflexivity. + rewrite tm_build. rewrite app_length. rewrite Nat.mul_comm. + simpl. rewrite Nat.add_0_r. rewrite map_length. reflexivity. + rewrite <- Nat.negb_even. rewrite K. reflexivity. + apply Nat.lt_0_2. + + assert (K': even (length a') = true). rewrite I'. + rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity. + apply le_0_n. - re - + (* montrer que length (hd'++a') est pair à l'aide de +H : tm_step n = hd' ++ a' ++ map negb (rev a') ++ tl' + *) @@ -807,6 +900,8 @@ Proof. *) + (* TODO: reprendre tous les lemmes hd ++ a ++ rev a ++ tl + et trouver un équivalent pour hd ++ a ++ map negb (rev a) ++ tl *) (* TODO: les palindromes de longueur 16 sont centrés autour