From b8b836fb53cd90d792c1d36f0d08f0c1a9e91663 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Thu, 26 Jan 2023 14:48:30 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 205 +++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 204 insertions(+), 1 deletion(-) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index e7059ae..2be88ed 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -1374,12 +1374,191 @@ Proof. 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 -> 0 < length a -> even (length a) = true - -> 11= 42. + -> tm_morphism (tm_step (pred n)) = + tm_morphism + (firstn (Nat.div2 (length hd)) (tm_step (pred n)) ++ + firstn (Nat.div2 (length a)) + (skipn (Nat.div2 (length hd)) (tm_step (pred n))) ++ + map negb + (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))). Proof. intros n hd a tl. intros H I J. destruct n. assert (length (tm_step 0) <= length (tm_step 0)). @@ -1401,9 +1580,33 @@ Proof. destruct (even (length hd)). reflexivity. inversion H0. rewrite <- tm_step_lemma in H. + assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))). generalize H1. generalize H. apply tm_morphism_app2. + assert (a ++ (rev a) ++ tl + = tm_morphism (skipn (Nat.div2 (length hd)) (tm_step n))). + generalize H1. generalize H. apply tm_morphism_app3. symmetry in H3. + + assert (a = tm_morphism (firstn (Nat.div2 (length a)) + (skipn (Nat.div2 (length hd)) (tm_step n)))). + generalize J. generalize H3. apply tm_morphism_app2. + + assert (tl = tm_morphism (skipn (Nat.div2 (length (a ++ (rev a)))) + (skipn (Nat.div2 (length hd)) (tm_step n)))). + assert (even (length (a ++ (rev a))) = true). rewrite app_length. + rewrite rev_length. rewrite Nat.even_add. rewrite J. reflexivity. + generalize H5. rewrite app_assoc in H3. generalize H3. + apply tm_morphism_app3. + + rewrite H2 in H. rewrite H4 in H. rewrite tm_morphism_rev in H. + rewrite H5 in H. rewrite <- tm_morphism_app in H. + rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. + + rewrite app_length in H. rewrite rev_length in H. + replace (Nat.div2 (length a + length a)) with (length a) in H. + rewrite <- pred_Sn. +