From 3bc04f10caa7e6b8379c89c3e119d917921a1772 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Fri, 3 Feb 2023 18:45:46 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 119 ++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 116 insertions(+), 3 deletions(-) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index b7d32c0..d1c3f26 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -2549,14 +2549,127 @@ Proof. destruct m. left. apply tm_step_palindrome_mod8 with (n := n) (tl := tl); assumption. - right. rewrite J. apply Nat.pow_le_mono_r. easy. - rewrite Nat.double_S. rewrite Nat.double_S. + right. rewrite J. rewrite Nat.double_S. rewrite Nat.double_S. + apply Nat.pow_le_mono_r. easy. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. - rewrite <- Nat.succ_le_mono. apply le_0_n. + rewrite <- Nat.succ_le_mono. + apply le_0_n. Qed. +Theorem tm_step_palindromic_power2_odd : + forall (m n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ (rev a) ++ tl + -> 6 < length a + -> length a = 2^(S (Nat.double m)) + -> length (hd ++ a) mod (2 ^ (S (Nat.double m))) = 0. +Proof. + intros m n hd a tl. intros H I J. + assert (E: length (hd ++ a) mod (2 ^ (S (Nat.double m))) = 0 + \/ 2^5 <= length a). + generalize J. generalize I. generalize H. + apply tm_step_palindromic_power2_odd_beta. + + generalize dependent hd. + generalize dependent a. + generalize dependent tl. + generalize dependent n. + + induction m. + - intros n tl a I J hd H E. destruct E. assumption. + apply tm_step_palindromic_power2_odd_alpha with (n := n) (tl := tl). + assumption. assumption. assumption. + rewrite J in H0. rewrite <- Nat.pow_le_mono_r_iff in H0. + inversion H0. inversion H2. + apply Nat.lt_1_2. + - intros n tl a I J hd H E. assert (E' := E). + destruct E as [E0 | E1]. assumption. + rewrite tm_step_palindromic_power2_odd_alpha with (n := n) (tl := tl). + rewrite <- pred_Sn. + + assert (W: (length a) mod 4 = 0). + rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J. + rewrite Nat.pow_succ_r in J. + rewrite Nat.mul_assoc in J. + replace (2*2) with 4 in J. rewrite J. + rewrite <- Nat.mul_mod_idemp_l. reflexivity. + easy. reflexivity. apply le_0_n. apply le_0_n. + + assert ( + hd = tm_morphism (tm_morphism (firstn (length hd / 4) + (tm_step (pred (pred n))))) + /\ a = tm_morphism (tm_morphism + (firstn (length a / 4) (skipn (length hd / 4) + (tm_step (pred (pred n)))))) + /\ tl = tm_morphism (tm_morphism + (skipn (length hd / 4 + Nat.div2 (length a)) + (tm_step (pred (pred n)))))). + generalize W. generalize I. generalize H. + apply tm_step_palindromic_even_morphism2. + destruct H0 as [K H0]. destruct H0 as [L M]. + + assert (V: 3 < n). generalize I. generalize H. + apply tm_step_palindromic_length_12_n. + destruct n. inversion V. destruct n. inversion V. inversion H1. + + rewrite K in H. rewrite L in H. rewrite M in H. + rewrite tm_morphism_twice_rev in H. + rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. + rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. + rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. + rewrite <- tm_step_lemma in H. rewrite <- tm_step_lemma in H. + rewrite <- tm_morphism_eq in H. rewrite <- tm_morphism_eq in H. + rewrite Nat.pred_succ in H. rewrite Nat.pred_succ in H. + + pose (hd' := (firstn (length hd / 4) (tm_step n))). + pose (a' := (firstn (length a / 4) (skipn (length hd / 4) (tm_step n)))). + pose (tl' := (skipn (length hd / 4 + Nat.div2 (length a)) (tm_step n))). + fold hd' in H. fold a' in H. fold tl' in H. + + rewrite Nat.pred_succ in K. rewrite Nat.pred_succ in K. + rewrite Nat.pred_succ in L. rewrite Nat.pred_succ in L. + fold hd' in K. fold a' in L. + assert (N: length a = length a). reflexivity. rewrite L in N at 2. + rewrite tm_morphism_length in N. rewrite tm_morphism_length in N. + rewrite Nat.mul_assoc in N. replace (2*2) with 4 in N. + assert (O: length hd = length hd). reflexivity. rewrite K in O at 2. + rewrite tm_morphism_length in O. rewrite tm_morphism_length in O. + rewrite Nat.mul_assoc in O. replace (2*2) with 4 in O. + + rewrite app_length. rewrite N. rewrite O. rewrite <- Nat.mul_add_distr_l. + rewrite Nat.mul_comm. rewrite Nat.div_mul. rewrite <- app_length. + + assert (Y: length a' = 2 ^ (S (Nat.double m))). + rewrite J in N. rewrite Nat.double_S in N. + rewrite Nat.pow_succ_r in N. rewrite Nat.pow_succ_r in N. + rewrite Nat.mul_assoc in N. replace (2*2) with 4 in N. + rewrite Nat.mul_cancel_l in N. rewrite N. reflexivity. easy. reflexivity. + apply le_0_n. apply le_0_n. + + assert (Y': 6 < length a'). + rewrite N in E1. + rewrite Nat.pow_succ_r in E1. rewrite Nat.pow_succ_r in E1. + rewrite Nat.mul_assoc in E1. replace (2*2) with 4 in E1. + rewrite <- Nat.mul_le_mono_pos_l in E1. + assert (6 < 2^3). simpl. + rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. + rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. + rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. + apply Nat.lt_0_succ. generalize E1. generalize H0. + apply Nat.lt_le_trans. apply Nat.lt_0_succ. reflexivity. + apply le_0_n. apply le_0_n. + + apply IHm with (n := n) (tl := tl'). + assumption. assumption. assumption. + generalize Y. generalize Y'. generalize H. + apply tm_step_palindromic_power2_odd_beta. + easy. reflexivity. reflexivity. + assumption. assumption. assumption. +Qed. + + + (* Lemma tm_step_proper_palindrome_center : forall (m n k : nat) (hd a tl : list bool),