From 76efd13e3e8a09cbd64abe42be5644b983ffe80a Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 11 Jan 2023 09:03:32 +0100 Subject: [PATCH] Update --- src/thue_morse2.v | 136 +++++++++------------------------------------- 1 file changed, 27 insertions(+), 109 deletions(-) diff --git a/src/thue_morse2.v b/src/thue_morse2.v index 5e17452..bd9c4f7 100644 --- a/src/thue_morse2.v +++ b/src/thue_morse2.v @@ -263,7 +263,7 @@ Qed. Lemma tm_step_consecutive_identical_length' : forall (n : nat) (hd a tl : list bool), - tm_step n = hd ++ a ++ tl -> length a > 4 + tm_step n = hd ++ a ++ tl -> 4 < length a -> exists (b c : list bool) (d : bool), a = b ++ [d;d] ++ c. Proof. intros n hd a tl. intros H I. @@ -282,78 +282,36 @@ Proof. Qed. - - - - - -Lemma tm_step_consecutive_identical_length : - forall (n : nat) (hd a tl : list bool), - tm_step n = hd ++ a ++ tl -> length a = 5 - -> exists (b c : list bool) (d : bool), a = b ++ [d;d] ++ c. - - - -Lemma tm_step_square_size_3 : forall (n : nat) (hd a tl : list bool), - tm_step n = hd ++ a ++ a ++ tl -> length a = 3 - -> a = true::false::true::nil \/ a = false::true::false::nil. +Lemma tm_step_odd_square : forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ a ++ tl -> odd (length a) = true -> length a < 4. Proof. intros n hd a tl. intros H I. - destruct a. - - inversion I. - - destruct b. - + left. destruct a. inversion I. destruct b. - * assert (J: a = false::nil). destruct a. inversion I. - destruct b. - assert (K: tm_step n = hd ++ [true] ++ [true] ++ [true] - ++ a ++ [true] ++ [true] ++ [true] ++ a ++ tl). - rewrite H. apply app_inv_head_iff. - replace (true::true::true::a) with ([true] ++ [true] ++ [true] ++ a). - rewrite <- app_assoc. apply app_inv_head_iff. - rewrite <- app_assoc. apply app_inv_head_iff. - rewrite <- app_assoc. apply app_inv_head_iff. apply app_inv_head_iff. - rewrite <- app_assoc. apply app_inv_head_iff. - rewrite <- app_assoc. apply app_inv_head_iff. - rewrite <- app_assoc. reflexivity. reflexivity. - apply tm_step_cubefree in K. contradiction K. reflexivity. - simpl. apply Nat.lt_0_1. simpl in I. apply Nat.succ_inj in I. - apply Nat.succ_inj in I. apply Nat.succ_inj in I. - rewrite length_zero_iff_nil in I. rewrite I. reflexivity. + assert (J: 4 < length a \/ length a <= 4). + apply Nat.lt_ge_cases. destruct J. + assert (exists b c d, a = b ++ [d;d] ++ c). + generalize H0. generalize H. apply tm_step_consecutive_identical_length'. + destruct H1. destruct H1. destruct H1. rewrite H1 in H. - replace (hd ++ (true::true::a) ++ (true::true::a) ++ tl) - with (hd ++ (true::true::nil) ++ (a ++ (true::true::a) ++ tl)) in H. - apply tm_step_consecutive_identical in H. - rewrite J in H. simpl in H. inversion H. + replace (hd ++ (x ++ [x1; x1] ++ x0) ++ (x ++ [x1; x1] ++ x0) ++ tl) + with ((hd ++ x) ++ [x1;x1] ++ (x0++x) ++ [x1;x1] ++ (x0 ++ tl)) in H. + apply tm_step_consecutive_identical in H. - apply app_inv_head_iff. rewrite <- app_assoc_reverse. - apply app_inv_head_iff. reflexivity. - * destruct a. inversion I. simpl in I. - apply Nat.succ_inj in I. apply Nat.succ_inj in I. - apply Nat.succ_inj in I. apply length_zero_iff_nil in I. - destruct b. rewrite I. reflexivity. - rewrite I in H. - 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. simpl in H. inversion H. - rewrite app_assoc_reverse. apply app_inv_head_iff. reflexivity. - + right. destruct a. inversion I. destruct b. - * destruct a. inversion I. simpl in I. - apply Nat.succ_inj in I. apply Nat.succ_inj in I. - apply Nat.succ_inj in I. apply length_zero_iff_nil in I. - destruct b. rewrite I in H. - 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. simpl in H. inversion H. - rewrite app_assoc_reverse. apply app_inv_head_iff. reflexivity. - rewrite I. reflexivity. - * replace (hd ++ (false::false::a) ++ (false::false::a) ++ tl) - with (hd ++ (false::false::nil) ++ a ++ (false::false::nil) ++ (a ++ tl)) in H. - apply tm_step_consecutive_identical in H. simpl in H. inversion H. - simpl in I. apply Nat.succ_inj in I. apply Nat.succ_inj in I. - rewrite I in H. inversion H. - apply app_inv_head_iff. - rewrite <- app_assoc_reverse. - apply app_inv_head_iff. reflexivity. + assert (J: even (length (x0 ++ x)) = false). + rewrite H1 in I. rewrite app_length in I. rewrite app_length in I. + rewrite Nat.add_shuffle3 in I. rewrite Nat.add_comm in I. + rewrite Nat.odd_add_even in I. + rewrite app_length. rewrite Nat.add_comm. rewrite <- Nat.negb_odd. + rewrite I. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT. + reflexivity. rewrite H in J. inversion J. + + rewrite <- app_assoc. apply app_inv_head_iff. + rewrite <- app_assoc. rewrite <- app_assoc. apply app_inv_head_iff. + rewrite <- app_assoc. apply app_inv_head_iff. apply app_inv_head_iff. + rewrite <- app_assoc. apply app_inv_head_iff. + reflexivity. + + apply Nat.le_lteq in H0. destruct H0. assumption. + rewrite H0 in I. inversion I. Qed. @@ -361,46 +319,6 @@ Qed. - - destruct a. inversion I. - destruct b. - assert (K: tm_step n = hd ++ [false] ++ [true] ++ [true] - ++ a ++ [true] ++ [true] ++ [true] ++ a ++ tl). - rewrite H. apply app_inv_head_iff. - replace (true::true::true::a) with ([true] ++ [true] ++ [true] ++ a). - rewrite <- app_assoc. apply app_inv_head_iff. - rewrite <- app_assoc. apply app_inv_head_iff. - rewrite <- app_assoc. apply app_inv_head_iff. apply app_inv_head_iff. - rewrite <- app_assoc. apply app_inv_head_iff. - rewrite <- app_assoc. apply app_inv_head_iff. - rewrite <- app_assoc. reflexivity. reflexivity. - apply tm_step_cubefree in K. contradiction K. reflexivity. - simpl. apply Nat.lt_0_1. simpl in I. apply Nat.succ_inj in I. - apply Nat.succ_inj in I. apply Nat.succ_inj in I. - rewrite length_zero_iff_nil in I. rewrite I. reflexivity. - - replace (hd ++ (true::true::a) ++ (true::true::a) ++ tl) - with (hd ++ (true::true::nil) ++ (a ++ (true::true::a) ++ tl)) in H. - apply tm_step_consecutive_identical in H. - rewrite J in H. simpl in H. inversion H. - - apply app_inv_head_iff. rewrite <- app_assoc_reverse. - apply app_inv_head_iff. reflexivity. - - - -Theorem tm_step_cubefree : forall (n : nat) (hd a b tl : list bool), - tm_step n = hd ++ a ++ a ++ b ++ tl -> 0 < length a -> a <> b. - - - -Carré de taille 3 : - AABAAB (impossible) - ABBABB (impossible) - ABAABA (OK) - BABBAB - - Lemma xxx : forall (n k : nat) (hd pat tl : list bool), tm_step n = hd ++ pat ++ tl -> length pat <= 2^k