From 5b0894346ac3efc3f44ab3e53355309ffca806e7 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Thu, 26 Jan 2023 15:28:49 +0100 Subject: [PATCH] Update --- src/thue_morse.v | 166 ++++++++++++++++++++++++++++ src/thue_morse3.v | 272 +++++++++++++++++----------------------------- 2 files changed, 268 insertions(+), 170 deletions(-) diff --git a/src/thue_morse.v b/src/thue_morse.v index 7ccffdd..314ca28 100644 --- a/src/thue_morse.v +++ b/src/thue_morse.v @@ -1237,3 +1237,169 @@ Proof. apply app_inv_head_iff. rewrite app_assoc. rewrite firstn_skipn. reflexivity. Qed. + + +(** + Some more lemmas are added there as convenient tools for further + investigations; they have been added quite late, after many + following results were proved, but they are inserted here in + case some proofs are re-written later. +*) + +Lemma tm_step_morphism2 : + forall (n : nat) (hd tl : list bool), + tm_step (S n) = hd ++ tl + -> even (length hd) = true + -> tm_step (S n) = tm_morphism + (firstn (Nat.div2 (length hd)) (tm_step n) ++ + skipn (Nat.div2 (length hd)) (tm_step n)). +Proof. + intros n hd tl. intros H I. + assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))). + generalize I. generalize H. apply tm_morphism_app2. + assert (tl = tm_morphism (skipn (Nat.div2 (length hd)) (tm_step n))). + generalize I. generalize H. apply tm_morphism_app3. + rewrite H0 in H. rewrite H1 in H. rewrite <- tm_morphism_app in H. + assumption. +Qed. + + +Lemma tm_step_morphism3 : + forall (n : nat) (hd a tl : list bool), + tm_step (S n) = hd ++ a ++ tl + -> even (length hd) = true + -> even (length a) = true + -> tm_morphism (tm_step n) = tm_morphism + (firstn (Nat.div2 (length hd)) (tm_step n) ++ + firstn (Nat.div2 (length a)) + (skipn (Nat.div2 (length hd)) (tm_step n)) ++ + skipn (Nat.div2 (length hd + length a)) (tm_step n)). +Proof. + intros n hd a tl. intros H I J. rewrite <- tm_step_lemma in H. + assert (even (length (hd ++ a)) = true). rewrite app_length. + rewrite Nat.even_add. rewrite I. rewrite J. reflexivity. + rewrite app_assoc in H. + assert (hd ++ a = tm_morphism (firstn (Nat.div2 (length (hd ++ a))) + (tm_step n))). + generalize H0. generalize H. apply tm_morphism_app2. + assert (tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a))) + (tm_step n))). + generalize H0. generalize H. apply tm_morphism_app3. + rewrite <- app_assoc in H. + assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))). + generalize I. generalize H. apply tm_morphism_app2. + assert (a = tm_morphism (skipn (Nat.div2 (length hd)) + (firstn (Nat.div2 (length (hd ++ a))) (tm_step n)))). + generalize I. symmetry in H1. generalize H1. apply tm_morphism_app3. + rewrite skipn_firstn_comm in H4. + rewrite H3 in H. rewrite H4 in H. rewrite H2 in H. + rewrite app_length in H. + + rewrite <- tm_morphism_app in H. + rewrite <- tm_morphism_app in H. + + replace (Nat.div2 (length hd + length a)) + with ((length hd) / 2 + Nat.div2 (length a)) in H. + rewrite <- Nat.div2_div in H. rewrite Nat.add_sub_swap in H. + rewrite Nat.sub_diag in H. rewrite Nat.add_0_l in H. + + rewrite Nat.div2_div in H at 3. rewrite <- Nat.div_add in H. + rewrite Nat.mul_comm in H. + + replace (2 * Nat.div2 (length a)) + with (2 * Nat.div2 (length a) + Nat.b2n (Nat.odd (length a))) in H. + rewrite <- Nat.div2_odd in H. rewrite <- Nat.div2_div in H. + assumption. + + rewrite <- Nat.negb_even. rewrite J. + rewrite <- Nat.add_0_r. reflexivity. easy. + apply Nat.le_refl. + + replace (length a) with (Nat.div2 (length a) * 2) at 2. + rewrite <- Nat.div_add. rewrite <- Nat.div2_div. reflexivity. + easy. rewrite Nat.mul_comm. + + replace (2 * Nat.div2 (length a)) + with (2 * Nat.div2 (length a) + Nat.b2n (Nat.odd (length a))). + rewrite Nat.div2_odd. reflexivity. + rewrite <- Nat.negb_even. rewrite J. + rewrite <- Nat.add_0_r. reflexivity. +Qed. + + +Lemma tm_step_morphism4 : + forall (n : nat) (hd a b tl : list bool), + tm_step (S n) = hd ++ a ++ b ++ tl + -> even (length hd) = true + -> even (length a) = true + -> even (length b) = true + -> tm_step (S n) = tm_morphism + (firstn (Nat.div2 (length hd)) (tm_step n) ++ + firstn (Nat.div2 (length a)) + (skipn (Nat.div2 (length hd)) (tm_step n)) ++ + firstn (Nat.div2 (length b)) + (skipn (Nat.div2 (length (hd ++ a))) (tm_step n)) ++ + skipn (Nat.div2 (length (hd ++ a ++ b))) (tm_step n)). +Proof. + intros n hd a b tl. intros H I J K. + + assert (even (length (hd ++ a)) = true). + rewrite app_length. rewrite Nat.even_add. + rewrite I. rewrite J. reflexivity. + rewrite app_assoc in H. rewrite <- tm_step_lemma in H. + + assert (hd ++ a = tm_morphism (firstn (Nat.div2 (length (hd ++ a))) + (tm_step n))). + generalize H0. generalize H. apply tm_morphism_app2. + + assert (b ++ tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a))) + (tm_step n))). + generalize H0. generalize H. apply tm_morphism_app3. + + rewrite <- app_assoc in H. symmetry in H1. symmetry in H2. + assert (even (length (hd ++ a ++ b)) = true). + rewrite app_length. rewrite Nat.even_add. rewrite I. + rewrite app_length. rewrite Nat.even_add. rewrite J. rewrite K. + reflexivity. + + assert (tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a ++ b))) + (tm_step n))). + replace (hd ++ a ++ b ++ tl) with ((hd ++ a ++ b) ++ tl) in H. + generalize H3. generalize H. apply tm_morphism_app3. + rewrite <- app_assoc. rewrite <- app_assoc. reflexivity. + + assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))). + generalize I. generalize H. apply tm_morphism_app2. + + assert (a = tm_morphism (skipn (Nat.div2 (length hd)) + (firstn (Nat.div2 (length (hd ++ a))) (tm_step n)))). + generalize I. generalize H1. apply tm_morphism_app3. + + assert (b = tm_morphism (firstn (Nat.div2 (length b)) + (skipn (Nat.div2 (length (hd ++ a))) (tm_step n)))). + generalize K. generalize H2. apply tm_morphism_app2. + + rewrite skipn_firstn_comm in H6. rewrite app_length in H6. + + replace (Nat.div2 (length hd + length a)) + with ((length hd) / 2 + Nat.div2 (length a)) in H6. + rewrite <- Nat.div2_div in H6. rewrite Nat.add_sub_swap in H6. + rewrite Nat.sub_diag in H6. rewrite Nat.add_0_l in H6. + + rewrite H5 in H. rewrite H6 in H. rewrite H7 in H. rewrite H4 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. + assumption. + + apply Nat.le_refl. + rewrite <- Nat.div_add. rewrite <- Nat.div2_div. + rewrite Nat.mul_comm. + + replace (2 * Nat.div2 (length a)) + with (2 * Nat.div2 (length a) + Nat.b2n (Nat.odd (length a))). + rewrite <- Nat.div2_odd. reflexivity. + + rewrite <- Nat.negb_even. rewrite J. + rewrite <- Nat.add_0_r. reflexivity. + easy. +Qed. diff --git a/src/thue_morse3.v b/src/thue_morse3.v index 2be88ed..a75ed4a 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -1377,173 +1377,6 @@ Qed. -Lemma tm_step_morphism2 : - forall (n : nat) (hd tl : list bool), - tm_step (S n) = hd ++ tl - -> even (length hd) = true - -> tm_step (S n) = tm_morphism - (firstn (Nat.div2 (length hd)) (tm_step n) ++ - skipn (Nat.div2 (length hd)) (tm_step n)). -Proof. - intros n hd tl. intros H I. - assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))). - generalize I. generalize H. apply tm_morphism_app2. - assert (tl = tm_morphism (skipn (Nat.div2 (length hd)) (tm_step n))). - generalize I. generalize H. apply tm_morphism_app3. - rewrite H0 in H. rewrite H1 in H. rewrite <- tm_morphism_app in H. - assumption. -Qed. - - -Lemma tm_step_morphism3 : - forall (n : nat) (hd a tl : list bool), - tm_step (S n) = hd ++ a ++ tl - -> even (length hd) = true - -> even (length a) = true - -> tm_morphism (tm_step n) = tm_morphism - (firstn (Nat.div2 (length hd)) (tm_step n) ++ - firstn (Nat.div2 (length a)) - (skipn (Nat.div2 (length hd)) (tm_step n)) ++ - skipn (Nat.div2 (length hd + length a)) (tm_step n)). -Proof. - intros n hd a tl. intros H I J. rewrite <- tm_step_lemma in H. - assert (even (length (hd ++ a)) = true). rewrite app_length. - rewrite Nat.even_add. rewrite I. rewrite J. reflexivity. - rewrite app_assoc in H. - assert (hd ++ a = tm_morphism (firstn (Nat.div2 (length (hd ++ a))) - (tm_step n))). - generalize H0. generalize H. apply tm_morphism_app2. - assert (tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a))) - (tm_step n))). - generalize H0. generalize H. apply tm_morphism_app3. - rewrite <- app_assoc in H. - assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))). - generalize I. generalize H. apply tm_morphism_app2. - assert (a = tm_morphism (skipn (Nat.div2 (length hd)) - (firstn (Nat.div2 (length (hd ++ a))) (tm_step n)))). - generalize I. symmetry in H1. generalize H1. apply tm_morphism_app3. - rewrite skipn_firstn_comm in H4. - rewrite H3 in H. rewrite H4 in H. rewrite H2 in H. - rewrite app_length in H. - - rewrite <- tm_morphism_app in H. - rewrite <- tm_morphism_app in H. - - replace (Nat.div2 (length hd + length a)) - with ((length hd) / 2 + Nat.div2 (length a)) in H. - rewrite <- Nat.div2_div in H. rewrite Nat.add_sub_swap in H. - rewrite Nat.sub_diag in H. rewrite Nat.add_0_l in H. - - rewrite Nat.div2_div in H at 3. rewrite <- Nat.div_add in H. - rewrite Nat.mul_comm in H. - - replace (2 * Nat.div2 (length a)) - with (2 * Nat.div2 (length a) + Nat.b2n (Nat.odd (length a))) in H. - rewrite <- Nat.div2_odd in H. rewrite <- Nat.div2_div in H. - assumption. - - rewrite <- Nat.negb_even. rewrite J. - rewrite <- Nat.add_0_r. reflexivity. easy. - apply Nat.le_refl. - - replace (length a) with (Nat.div2 (length a) * 2) at 2. - rewrite <- Nat.div_add. rewrite <- Nat.div2_div. reflexivity. - easy. rewrite Nat.mul_comm. - - replace (2 * Nat.div2 (length a)) - with (2 * Nat.div2 (length a) + Nat.b2n (Nat.odd (length a))). - rewrite Nat.div2_odd. reflexivity. - rewrite <- Nat.negb_even. rewrite J. - rewrite <- Nat.add_0_r. reflexivity. -Qed. - - -Lemma tm_step_morphism4 : - forall (n : nat) (hd a b tl : list bool), - tm_step (S n) = hd ++ a ++ b ++ tl - -> even (length hd) = true - -> even (length a) = true - -> even (length b) = true - -> tm_step (S n) = tm_morphism - (firstn (Nat.div2 (length hd)) (tm_step n) ++ - firstn (Nat.div2 (length a)) - (skipn (Nat.div2 (length hd)) (tm_step n)) ++ - firstn (Nat.div2 (length b)) - (skipn (Nat.div2 (length (hd ++ a))) (tm_step n)) ++ - skipn (Nat.div2 (length (hd ++ a ++ b))) (tm_step n)). -Proof. - intros n hd a b tl. intros H I J K. - - assert (even (length (hd ++ a)) = true). - rewrite app_length. rewrite Nat.even_add. - rewrite I. rewrite J. reflexivity. - rewrite app_assoc in H. rewrite <- tm_step_lemma in H. - - assert (hd ++ a = tm_morphism (firstn (Nat.div2 (length (hd ++ a))) - (tm_step n))). - generalize H0. generalize H. apply tm_morphism_app2. - - assert (b ++ tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a))) - (tm_step n))). - generalize H0. generalize H. apply tm_morphism_app3. - - rewrite <- app_assoc in H. symmetry in H1. symmetry in H2. - assert (even (length (hd ++ a ++ b)) = true). - rewrite app_length. rewrite Nat.even_add. rewrite I. - rewrite app_length. rewrite Nat.even_add. rewrite J. rewrite K. - reflexivity. - - assert (tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a ++ b))) - (tm_step n))). - replace (hd ++ a ++ b ++ tl) with ((hd ++ a ++ b) ++ tl) in H. - generalize H3. generalize H. apply tm_morphism_app3. - rewrite <- app_assoc. rewrite <- app_assoc. reflexivity. - - assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))). - generalize I. generalize H. apply tm_morphism_app2. - - assert (a = tm_morphism (skipn (Nat.div2 (length hd)) - (firstn (Nat.div2 (length (hd ++ a))) (tm_step n)))). - generalize I. generalize H1. apply tm_morphism_app3. - - assert (b = tm_morphism (firstn (Nat.div2 (length b)) - (skipn (Nat.div2 (length (hd ++ a))) (tm_step n)))). - generalize K. generalize H2. apply tm_morphism_app2. - - rewrite skipn_firstn_comm in H6. rewrite app_length in H6. - - replace (Nat.div2 (length hd + length a)) - with ((length hd) / 2 + Nat.div2 (length a)) in H6. - rewrite <- Nat.div2_div in H6. rewrite Nat.add_sub_swap in H6. - rewrite Nat.sub_diag in H6. rewrite Nat.add_0_l in H6. - - rewrite H5 in H. rewrite H6 in H. rewrite H7 in H. rewrite H4 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. - assumption. - - apply Nat.le_refl. - rewrite <- Nat.div_add. rewrite <- Nat.div2_div. - rewrite Nat.mul_comm. - - replace (2 * Nat.div2 (length a)) - with (2 * Nat.div2 (length a) + Nat.b2n (Nat.odd (length a))). - rewrite <- Nat.div2_odd. reflexivity. - - rewrite <- Nat.negb_even. rewrite J. - rewrite <- Nat.add_0_r. reflexivity. - easy. -Qed. - - - - - - - - - - Lemma tm_step_palindromic_even_morphism1 : forall (n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ (rev a) ++ tl @@ -1558,9 +1391,11 @@ Lemma tm_step_palindromic_even_morphism1 : (rev (firstn (Nat.div2 (length a)) (skipn (Nat.div2 (length hd)) (tm_step (pred n))))) ++ - skipn (length a + Nat.div2 (length hd)) (tm_step (pred n))). + skipn (Nat.div2 (length hd) + length a) (tm_step (pred n))). Proof. - intros n hd a tl. intros H I J. + intros n hd a tl. intros H Z J. + + (* proof that n <> 0 *) destruct n. assert (length (tm_step 0) <= length (tm_step 0)). apply Nat.le_refl. rewrite H in H0 at 1. rewrite app_length in H0. rewrite app_length in H0. @@ -1570,7 +1405,104 @@ Proof. assert (K: 1 <= length a + (length tl + length hd)). rewrite Nat.le_succ_l. apply Nat.lt_lt_add_r. assumption. rewrite <- Nat.sub_0_le in K. rewrite K in H0. apply Nat.le_0_r in H0. - rewrite H0 in I. inversion I. + rewrite H0 in Z. inversion Z. + + assert (even (length (hd ++ a)) = true). generalize Z. generalize H. + apply tm_step_palindromic_even_center. + + assert (I: even (length hd) = true). rewrite app_length in H0. + rewrite Nat.even_add in H0. rewrite J in H0. + destruct (even (length hd)). reflexivity. inversion H0. + + assert (K: even (length (rev a)) = true). rewrite rev_length. assumption. + + rewrite app_assoc in H. rewrite <- tm_step_lemma in H. + + assert (hd ++ a = tm_morphism (firstn (Nat.div2 (length (hd ++ a))) + (tm_step n))). + generalize H0. generalize H. apply tm_morphism_app2. + + rewrite <- app_assoc in H. symmetry in H1. + assert (even (length (hd ++ a ++ (rev a))) = true). + rewrite app_length. rewrite Nat.even_add. rewrite I. + rewrite app_length. rewrite Nat.even_add. rewrite J. rewrite K. + reflexivity. + + assert (tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a ++ (rev a)))) + (tm_step n))). + replace (hd ++ a ++ (rev a) ++ tl) with ((hd ++ a ++ (rev a)) ++ tl) in H. + generalize H2. generalize H. apply tm_morphism_app3. + rewrite <- app_assoc. rewrite <- app_assoc. reflexivity. + + assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))). + generalize I. generalize H. apply tm_morphism_app2. + + assert (a = tm_morphism (skipn (Nat.div2 (length hd)) + (firstn (Nat.div2 (length (hd ++ a))) (tm_step n)))). + generalize I. generalize H1. apply tm_morphism_app3. + + rewrite skipn_firstn_comm in H5. rewrite app_length in H5. + + replace (Nat.div2 (length hd + length a)) + with ((length hd) / 2 + Nat.div2 (length a)) in H5. + rewrite <- Nat.div2_div in H5. rewrite Nat.add_sub_swap in H5. + rewrite Nat.sub_diag in H5. rewrite Nat.add_0_l in H5. + + rewrite H4 in H. rewrite H5 in H. rewrite H3 in H. + rewrite tm_morphism_rev 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 app_length in H. rewrite app_length in H. rewrite rev_length in H. + replace (length a + length a) with ((length a)*2) in H. + replace (Nat.div2 (length hd + length a * 2)) + with ((length hd + length a * 2) / 2) in H. + rewrite Nat.div_add in H. rewrite <- Nat.div2_div in H. + + assumption. easy. + rewrite Nat.div2_div. reflexivity. rewrite Nat.mul_comm. simpl. + rewrite Nat.add_0_r. reflexivity. + + apply Nat.le_refl. + rewrite <- Nat.div_add. rewrite <- Nat.div2_div. + rewrite Nat.mul_comm. + + rewrite Nat.div2_odd with (a := length a) at 2. + rewrite <- Nat.negb_even. rewrite J. simpl. + rewrite Nat.add_0_r. rewrite Nat.add_0_r. reflexivity. easy. +Qed. + + + + + + + + + + + + + + assert (tm_step (S n) = tm_morphism + (firstn (Nat.div2 (length hd)) (tm_step n) ++ + firstn (Nat.div2 (length a)) + (skipn (Nat.div2 (length hd)) (tm_step n)) ++ + firstn (Nat.div2 (length (rev a))) + (skipn (Nat.div2 (length (hd ++ a))) (tm_step n)) ++ + skipn (Nat.div2 (length (hd ++ a ++ (rev a)))) (tm_step n))). + assert (K : even (length (rev a)) = true). + rewrite rev_length. assumption. + generalize K. generalize J. generalize H1. generalize H. + apply tm_step_morphism4. rewrite rev_length in H2. + + rewrite <- pred_Sn. + + + + + + assert (even (length (hd ++ a)) = true). generalize I. generalize H. apply tm_step_palindromic_even_center.