From ddedf950b664cae2146c3854aa71eb5c08ef2120 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sat, 14 Jan 2023 21:37:37 +0100 Subject: [PATCH] Update --- src/thue_morse2.v | 130 +++++++++++++++++++--------------------------- 1 file changed, 53 insertions(+), 77 deletions(-) diff --git a/src/thue_morse2.v b/src/thue_morse2.v index 3ff4cec..adae841 100644 --- a/src/thue_morse2.v +++ b/src/thue_morse2.v @@ -329,71 +329,6 @@ Qed. prefix being odd or even in front of a squared pattern. *) -Lemma tm_step_odd_prefix_square_3 : forall (n : nat) (hd a tl : list bool), - tm_step n = hd ++ a ++ a ++ tl - -> length a = 3 -> even (length hd) = false. -Proof. - intros n hd a tl. intros H I. - assert (J: Nat.even (length hd) || Nat.odd (length hd) = true). - apply Nat.orb_even_odd. apply orb_prop in J. destruct J. - assert (Z: a = [true;false;true] \/ a = [false;true;false]). - destruct a. inversion I. destruct a. inversion I. - destruct a. inversion I. destruct a. - - destruct b; destruct b0; destruct b1. - + replace ([true;true;true] ++ [true;true;true] ++ tl) - with ([true;true] ++ [true] ++ [true;true] ++ [true] ++ tl) in H. - apply tm_step_consecutive_identical' in H. inversion H. - reflexivity. - + replace ([true;true;false] ++ [true;true;false] ++ tl) - with ([true;true] ++ [false] ++ [true;true] ++ [false] ++ tl) in H. - apply tm_step_consecutive_identical' in H. inversion H. - reflexivity. - + left. reflexivity. - + replace (hd ++ [true;false;false] ++ [true;false;false] ++ tl) - with ((hd ++ [true]) ++ [false; false] ++ [true] ++ [false;false] ++ tl) in H. - apply tm_step_consecutive_identical' in H. inversion H. - rewrite <- app_assoc. reflexivity. - + replace (hd ++ [false;true;true] ++ [false;true;true] ++ tl) - with ((hd ++ [false]) ++ [true; true] ++ [false] ++ [true;true] ++ tl) in H. - apply tm_step_consecutive_identical' in H. inversion H. - rewrite <- app_assoc. reflexivity. - + right. reflexivity. - + replace ([false;false;true] ++ [false;false;true] ++ tl) - with ([false;false] ++ [true] ++ [false;false] ++ [true] ++ tl) in H. - apply tm_step_consecutive_identical' in H. inversion H. - reflexivity. - + replace ([false;false;false] ++ [false;false;false] ++ tl) - with ([false;false] ++ [false] ++ [false;false] ++ [false] ++ tl) in H. - apply tm_step_consecutive_identical' in H. inversion H. - reflexivity. - - inversion I. - - assert (K: count_occ Bool.bool_dec hd true - = count_occ Bool.bool_dec hd false). - generalize H0. generalize H. apply tm_step_count_occ. - destruct Z; rewrite H1 in H. - replace (hd ++ [true;false;true] ++ [true;false;true] ++ tl) - with ((hd ++ [true;false;true;true]) ++ [false;true] ++ tl) in H. - assert (even (length (hd ++ [true;false;true;true])) = true). - rewrite app_length. rewrite Nat.even_add. rewrite H0. reflexivity. - assert (M: count_occ Bool.bool_dec (hd ++ [true;false;true;true]) true - = count_occ Bool.bool_dec (hd ++ [true;false;true;true]) false). - generalize H2. generalize H. apply tm_step_count_occ. - rewrite count_occ_app in M. symmetry in M. rewrite count_occ_app in M. - rewrite K in M. rewrite Nat.add_cancel_l in M. inversion M. - rewrite <- app_assoc. reflexivity. - replace (hd ++ [false;true;false] ++ [false;true;false] ++ tl) - with ((hd ++ [false;true;false;false]) ++ [true;false] ++ tl) in H. - assert (even (length (hd ++ [false;true;false;false])) = true). - rewrite app_length. rewrite Nat.even_add. rewrite H0. reflexivity. - assert (M: count_occ Bool.bool_dec (hd ++ [false;true;false;false]) true - = count_occ Bool.bool_dec (hd ++ [false;true;false;false]) false). - generalize H2. generalize H. apply tm_step_count_occ. - rewrite count_occ_app in M. symmetry in M. rewrite count_occ_app in M. - rewrite K in M. rewrite Nat.add_cancel_l in M. inversion M. - rewrite <- app_assoc. reflexivity. - - rewrite <- Nat.negb_odd. rewrite H0. reflexivity. -Qed. - Lemma tm_step_odd_prefix_square : forall (n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> odd (length a) = true -> even (length hd) = false. @@ -401,18 +336,59 @@ Proof. intros n hd a tl. intros H I. assert (length a < 4). generalize I. generalize H. apply tm_step_odd_square. destruct a. inversion I. destruct a. - rewrite <- negb_true_iff. rewrite Nat.negb_even. - generalize H. apply tm_step_consecutive_identical. - destruct a. inversion I. - destruct a. - apply tm_step_odd_prefix_square_3 with (n := n) (a := [b;b0;b1]) (tl := tl). - assumption. reflexivity. - simpl in H0. - rewrite <- Nat.succ_lt_mono in H0. - rewrite <- Nat.succ_lt_mono in H0. - rewrite <- Nat.succ_lt_mono in H0. - rewrite <- Nat.succ_lt_mono in H0. - apply Nat.nlt_0_r in H0. contradiction H0. + - rewrite <- negb_true_iff. rewrite Nat.negb_even. + generalize H. apply tm_step_consecutive_identical. + - destruct a. inversion I. destruct a. + + assert (J: {b0 = b1} + {b0 <> b1}). apply bool_dec. destruct J. + rewrite e in H. + replace (hd ++ [b;b1;b1] ++ [b;b1;b1] ++ tl) + with ((hd ++ [b]) ++ [b1;b1] ++ [b] ++ [b1;b1] ++ tl) in H. + assert (K: even (length [b]) = true). generalize H. + apply tm_step_consecutive_identical'. inversion K. + rewrite <- app_assoc. reflexivity. + assert (J: {b = b0} + {b <> b0}). apply bool_dec. destruct J. + rewrite e in H. + replace (hd ++ [b0;b0;b1] ++ [b0;b0;b1] ++ tl) + with (hd ++ [b0;b0] ++ [b1] ++ [b0;b0] ++ [b1] ++ tl) in H. + assert (K: even (length [b1]) = true). generalize H. + apply tm_step_consecutive_identical'. inversion K. + reflexivity. + assert (J: {b = b1} + {b <> b1}). apply bool_dec. destruct J. + rewrite e in H. + + assert (J: Nat.even (length hd) || Nat.odd (length hd) = true). + apply Nat.orb_even_odd. apply orb_prop in J. destruct J. + assert (K: count_occ Bool.bool_dec hd true + = count_occ Bool.bool_dec hd false). + generalize H1. generalize H. apply tm_step_count_occ. + + assert (L: count_occ Bool.bool_dec (hd ++ [b1;b0;b1;b1]) true + = count_occ Bool.bool_dec (hd ++ [b1;b0;b1;b1]) false). + assert (M: even (length (hd ++ [b1;b0;b1;b1])) = true). + rewrite app_length. rewrite Nat.even_add. rewrite H1. reflexivity. + replace (hd ++ [b1;b0;b1] ++ [b1;b0;b1] ++ tl) + with ((hd ++ [b1;b0;b1;b1]) ++ [b0;b1] ++ tl) in H. + generalize M. generalize H. apply tm_step_count_occ. + rewrite <- app_assoc. reflexivity. + rewrite count_occ_app in L. symmetry in L. rewrite count_occ_app in L. + rewrite K in L. rewrite Nat.add_cancel_l in L. + + destruct b0; destruct b1; inversion L. + rewrite <- Nat.negb_odd. rewrite H1. reflexivity. + + destruct b; destruct b0; destruct b1. + contradiction n0. contradiction n2. contradiction n1. contradiction n2. + contradiction n0. reflexivity. + contradiction n0. contradiction n2. reflexivity. + contradiction n1. reflexivity. contradiction n0. reflexivity. + + simpl in H0. + rewrite <- Nat.succ_lt_mono in H0. + rewrite <- Nat.succ_lt_mono in H0. + rewrite <- Nat.succ_lt_mono in H0. + rewrite <- Nat.succ_lt_mono in H0. + apply Nat.nlt_0_r in H0. contradiction H0. Qed.