From e1238e51987cda70d9323dc0150cc1fb634e4625 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sat, 14 Jan 2023 20:04:32 +0100 Subject: [PATCH] Update --- src/thue_morse2.v | 42 +++++------------------------------------- 1 file changed, 5 insertions(+), 37 deletions(-) diff --git a/src/thue_morse2.v b/src/thue_morse2.v index 596c2f4..015ccf8 100644 --- a/src/thue_morse2.v +++ b/src/thue_morse2.v @@ -329,37 +329,6 @@ Qed. prefix being odd or even in front of a squared pattern. *) -Lemma tm_step_odd_prefix_square_1 : forall (n : nat) (hd a tl : list bool), - tm_step n = hd ++ a ++ a ++ tl - -> length a = 1 -> 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 (K: count_occ Bool.bool_dec hd true - = count_occ Bool.bool_dec hd false). - generalize H0. generalize H. apply tm_step_count_occ. - assert (L: even (length (hd ++ a ++ a)) = true). - rewrite app_length. rewrite app_length. rewrite I. - rewrite Nat.even_add_even. assumption. rewrite Nat.add_1_r. - apply Nat.EvenT_Even. apply Nat.even_EvenT. easy. - assert (M: count_occ Bool.bool_dec (hd ++ a ++ a) true - = count_occ Bool.bool_dec (hd ++ a ++ a) false). - generalize L. generalize H. - replace (hd ++ a ++ a ++ tl) with ((hd ++ a ++ a) ++ tl). - apply tm_step_count_occ. - rewrite <- app_assoc. apply app_inv_head_iff. - rewrite <- app_assoc. reflexivity. - 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. destruct a. - + inversion I. - + destruct b; simpl in I; apply Nat.succ_inj in I; - rewrite length_zero_iff_nil in I; rewrite I in M; - simpl in M; inversion M. - - rewrite <- Nat.negb_odd. rewrite H0. reflexivity. -Qed. - 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. @@ -430,12 +399,10 @@ Lemma tm_step_odd_prefix_square : forall (n : nat) (hd a tl : list bool), -> odd (length a) = true -> even (length hd) = false. 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. - apply tm_step_odd_prefix_square_1 with (n := n) (a := [b]) (tl := tl). - assumption. reflexivity. + 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. apply hd. destruct a. inversion I. destruct a. apply tm_step_odd_prefix_square_3 with (n := n) (a := [b;b0;b1]) (tl := tl). @@ -549,3 +516,4 @@ Proof. (* TODO: utiliser tm_step_odd_prefix_square pour le cas impair *) (* TODO: la taille du facteur divise la taille du préfixe ? *) +