From 837884e8087d86426df3d498c1be6bdac594395e Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 1 Feb 2023 16:39:17 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 287 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 287 insertions(+) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index 6d4af5d..3a6986e 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -1893,6 +1893,292 @@ Qed. +Lemma xxx : + forall (m n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ (rev a) ++ tl + -> 6 < length a + -> length a = 2^(Nat.double m) + -> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0 + \/ 64 <= length a. +Proof. + intros m n hd a tl. intros H I J. + + destruct m. rewrite J in I. inversion I. inversion H1. + destruct m. rewrite J in I. inversion I. inversion H1. + inversion H3. inversion H5. inversion H7. + + destruct m. left. + + assert (W: length a mod 4 = 0). rewrite J. reflexivity. + + 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. + + replace (2^ pred (Nat.double 2)) with (4*2). + rewrite app_length. rewrite N. rewrite O. + rewrite <- Nat.mul_add_distr_l. rewrite Nat.mul_mod_distr_l. + rewrite Nat.mul_eq_0. right. rewrite <- app_length. + + assert (U: even (length (hd' ++ a')) = true). + assert (0 < length a'). + apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I. + rewrite N in I. + rewrite <- Nat.mul_1_r in I at 1. + rewrite <- Nat.mul_lt_mono_pos_l in I. + apply Nat.lt_succ_l in I. assumption. apply Nat.lt_0_succ. + generalize H0. generalize H. apply tm_step_palindromic_even_center. + + replace (length (hd' ++ a')) + with (2 * Nat.div2 (length (hd' ++ a')) + + Nat.b2n (Nat.odd (length (hd' ++ a')))). + rewrite <- Nat.negb_even. rewrite U. rewrite Nat.add_0_r. + rewrite Nat.mul_mod. reflexivity. easy. symmetry. apply Nat.div2_odd. + easy. easy. reflexivity. reflexivity. reflexivity. + + right. rewrite J. rewrite Nat.double_S. rewrite Nat.double_S. + rewrite Nat.double_S. rewrite Nat.pow_succ_r. + rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. + rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. + rewrite Nat.pow_succ_r. rewrite Nat.mul_assoc. + rewrite Nat.mul_assoc. rewrite Nat.mul_assoc. + rewrite Nat.mul_assoc. rewrite Nat.mul_assoc. + + replace (2*2*2*2*2*2) with 64. rewrite <- Nat.mul_1_r at 1. + rewrite <- Nat.mul_le_mono_pos_l. rewrite Nat.le_succ_l. + rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. + apply Nat.lt_0_succ. reflexivity. + apply le_0_n. apply le_0_n. apply le_0_n. + apply le_0_n. apply le_0_n. apply le_0_n. +Qed. + + + + + + + destruct m. left. + + assert (K: length a mod 4 = 0). rewrite J. reflexivity. + assert (L: length hd mod 4 = 0). + generalize K. generalize I. generalize H. + apply tm_step_palindromic_length_12_prefix. + + assert (M: 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 K. generalize I. generalize H. + apply tm_step_palindromic_even_morphism2. + + destruct M as [N O]. destruct O as [O P]. + rewrite N in H. rewrite O in H. rewrite P 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. + *) + + pose (hd' := (firstn (length hd / 4) (tm_step (pred (pred n))))). + pose (a' := (firstn (length a / 4) (skipn (length hd / 4) (tm_step (pred (pred n)))))). + pose (tl' := (skipn (length hd / 4 + Nat.div2 (length a)) (tm_step (pred (pred n))))). + fold hd' in H. fold a' in H. fold tl' in H. + + +Lemma tm_step_palindromic_power2_even : + forall (m n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ (rev a) ++ tl + -> 6 < length a + -> length a = 2^(Nat.double m) + -> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0 + <-> (length (hd ++ a) / 4) mod (2^(pred (Nat.double (pred m)))) = 0. +Proof. + intros m n hd a tl. intros H I J. + + + + + +Lemma xxx : + forall m : nat, + (forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ (rev a) ++ tl + -> 6 < length a + -> length a = 2^(Nat.double m) + -> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0) + -> (forall (n' : nat) (hd' a' tl' : list bool), + tm_step n' = hd' ++ a' ++ (rev a') ++ tl' + -> 6 < length a' + -> length a' = 2^(Nat.double (S m)) + -> length (hd' ++ a') mod (2 ^ (pred (Nat.double (S m)))) = 0). +Proof. + intro m. intro IH. + intros n hd a tl. intros H I J. + rewrite tm_step_palindromic_power2_even with (n := n) (tl := tl). + rewrite <- pred_Sn. + + destruct m. rewrite J in I. inversion I. inversion H1. + inversion H3. inversion H5. inversion H7. + + assert (W: (length a) mod 4 = 0). + rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J. + rewrite Nat.double_S 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 <- app_length. + rewrite Nat.mul_comm. rewrite Nat.div_mul. + apply IH with (n := n) (tl := tl'). assumption. + + + + + + + + replace (2^ pred (Nat.double 2)) with (4*2). + rewrite app_length. rewrite N. rewrite O. + rewrite <- Nat.mul_add_distr_l. rewrite Nat.mul_mod_distr_l. + rewrite Nat.mul_eq_0. right. rewrite <- app_length. + + assert (U: even (length (hd' ++ a')) = true). + assert (0 < length a'). + apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I. + rewrite N in I. + rewrite <- Nat.mul_1_r in I at 1. + rewrite <- Nat.mul_lt_mono_pos_l in I. + apply Nat.lt_succ_l in I. assumption. apply Nat.lt_0_succ. + generalize H0. generalize H. apply tm_step_palindromic_even_center. + + + + +Lemma tm_step_palindromic_even_morphism2 : + forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ (rev a) ++ tl + -> 6 < length a + -> (length a) mod 4 = 0 + -> 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))))). + + + rewrite Nat.double_S. + replace (pred (S (S (Nat.double m)))) with (S (S (pred (Nat.double m)))). + rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. rewrite Nat.mul_assoc. + replace (2*2) with 4. + +Lemma tm_step_palindromic_power2_even : + forall (m n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ (rev a) ++ tl + -> 6 < length a + -> length a = 2^(Nat.double m) + -> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0 + <-> (length (hd ++ a) / 4) mod (2^(pred (Nat.double (pred m)))) = 0. + + + +Lemma tm_step_palindromic_power2_even : + forall (m n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ (rev a) ++ tl + -> 6 < length a + -> length a = 2^(Nat.double m) + -> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0 + + + + Lemma xxx : forall (m n k : nat) (hd a tl : list bool), @@ -2048,6 +2334,7 @@ Proof. rewrite app_length. rewrite N. rewrite O. rewrite <- Nat.mul_add_distr_l. rewrite Nat.mul_mod_distr_l. rewrite Nat.mul_eq_0. right. rewrite <- app_length. + apply IHm. Lemma tm_step_palindromic_power2_even :