From 19990e26cb3f2454869d899bf69666ff4b4a3080 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 11 Jan 2023 00:16:29 +0100 Subject: [PATCH] Update --- src/thue_morse2.v | 171 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 171 insertions(+) diff --git a/src/thue_morse2.v b/src/thue_morse2.v index 75ad572..66fada2 100644 --- a/src/thue_morse2.v +++ b/src/thue_morse2.v @@ -79,6 +79,177 @@ Proof. Qed. +Lemma tm_step_factor5 : forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ tl -> length a = 5 + -> a <> [ true; false; true; false; true]. +Proof. + intros n hd a tl. intros H I. + + destruct n. + assert (length (tm_step 0) = length (tm_step 0)). reflexivity. + rewrite H in H0 at 2. simpl in H0. + rewrite app_length in H0. rewrite app_length in H0. + rewrite I in H0. rewrite Nat.add_shuffle3 in H0. + apply Nat.succ_inj in H0. inversion H0. + + assert (even (length (tm_step (S n))) = true). + rewrite tm_size_power2. rewrite Nat.pow_succ_r. apply Nat.even_mul. + apply Nat.le_0_l. + + assert (J: even (length hd) = negb (even (length tl))). + rewrite H in H0. rewrite app_length in H0. rewrite app_length in H0. + rewrite I in H0. rewrite Nat.even_add in H0. rewrite Nat.even_add in H0. + destruct (even (length hd)); destruct (even (length tl)). + inversion H0. reflexivity. reflexivity. inversion H0. + + assert (K: {a=[true; false; true; false; true]} + + {~ a=[ true; false; true; false; true]}). + apply list_eq_dec. apply bool_dec. destruct K. + + assert ({even (length hd) = true} + {even (length hd) <> true}). + apply bool_dec. destruct H1. + + (* case length hd is even *) + rewrite e0 in J. rewrite Nat.negb_even in J. + destruct tl. inversion J. + destruct b. + + assert (count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false). + generalize e0. generalize H. apply tm_step_count_occ. + + assert (count_occ Bool.bool_dec (hd ++ a ++ [true]) true + = count_occ Bool.bool_dec (hd ++ a ++ [true]) false). + assert (even (length (hd ++ a ++ [true])) = true). + rewrite app_length. rewrite app_length. + rewrite Nat.even_add. rewrite Nat.even_add. + rewrite e0. rewrite e. reflexivity. + replace (hd ++ a ++ true :: tl) with ((hd ++ a ++ [true]) ++ tl) in H. + generalize H2. generalize H. apply tm_step_count_occ. + rewrite <- app_assoc. apply app_inv_head_iff. + rewrite <- app_assoc. reflexivity. + + rewrite count_occ_app in H2. rewrite H1 in H2. + symmetry in H2. + rewrite count_occ_app in H2. rewrite Nat.add_cancel_l in H2. + + rewrite count_occ_app in H2. rewrite count_occ_app in H2. + rewrite e in H2. simpl in H2. inversion H2. + + replace (hd ++ a ++ false::tl) + with (hd ++ [true; false] ++ [true; false] ++ [true; false] ++ tl) in H. + apply tm_step_cubefree in H. contradiction H. reflexivity. + simpl. apply Nat.lt_0_2. + + rewrite e. reflexivity. + + (* case length hd is odd *) + apply not_true_is_false in n0. + rewrite app_removelast_last with (l := hd) (d := true) in H. + rewrite app_removelast_last with (l := hd) (d := true) in n0. + rewrite app_length in n0. simpl in n0. + rewrite Nat.add_1_r in n0. rewrite Nat.even_succ in n0. + rewrite <- Nat.negb_even in n0. rewrite negb_false_iff in n0. + + destruct (last hd true). + rewrite <- app_assoc in H. + assert (count_occ Bool.bool_dec (removelast hd) true + = count_occ Bool.bool_dec (removelast hd) false). + generalize n0. generalize H. apply tm_step_count_occ. + replace (removelast hd ++ [true] ++ a ++ tl) + with ((removelast hd ++ [true; true]) ++ [false;true;false;true] ++ tl) in H. + assert (count_occ Bool.bool_dec (removelast hd ++ [true;true]) true + = count_occ Bool.bool_dec (removelast hd ++ [true;true]) false). + assert (even (length (removelast hd ++ [true;true])) = true). + rewrite app_length. rewrite Nat.even_add_even. assumption. + apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity. + generalize H2. generalize H. apply tm_step_count_occ. + + rewrite count_occ_app in H2. rewrite count_occ_app in H2. + rewrite H1 in H2. rewrite Nat.add_cancel_l in H2. + simpl in H2. inversion H2. + + rewrite e. rewrite app_assoc_reverse. reflexivity. + + replace ((removelast hd ++ [false]) ++ a ++ tl) + with (removelast hd ++ [false; true] ++ [false; true] ++ [false;true] ++ tl) in H. + apply tm_step_cubefree in H. contradiction H. reflexivity. + simpl. apply Nat.lt_0_2. + + rewrite e. rewrite app_assoc_reverse. reflexivity. + + assert (length hd <> 0). destruct hd. inversion n0. + simpl. apply Nat.neq_succ_0. rewrite <- length_zero_iff_nil. assumption. + assert (length hd <> 0). destruct hd. inversion n0. + simpl. apply Nat.neq_succ_0. rewrite <- length_zero_iff_nil. assumption. + + assumption. +Qed. + +Lemma tm_step_factor5' : forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ tl -> length a = 5 + -> a <> [ false; true; false; true; false]. +Proof. + + + + + + + + + assert ({last (b :: hd) true = true} + {last (b :: hd) true <> true}). + apply bool_dec. + assert (last (b::hd) true = true). destruct H1. assumption. + apply not_true_is_false in n0. + + replace ((removelast (b :: hd) ++ [last (b :: hd) true]) ++ a ++ tl) + with ((removelast (b :: hd)) ++ [false;true] ++ [false;true] + ++ [false;true] ++ tl) in H. + apply tm_step_cubefree in H. contradiction H. reflexivity. + simpl. apply Nat.lt_0_2. + rewrite <- app_assoc. apply app_inv_head_iff. + rewrite n0. rewrite e. reflexivity. + rewrite H1 in H. + + + + +Lemma two_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. +Proof. + intros n hd a tl. intros H I. + destruct a. inversion I. destruct a. inversion I. + destruct a. inversion I. destruct a. inversion I. + destruct a. inversion I. + + assert (a = nil). simpl in I. + apply Nat.succ_inj in I. apply Nat.succ_inj 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. assumption. + rewrite H0. rewrite H0 in H. rewrite H0 in I. + + destruct b; destruct b0; destruct b1; destruct b2; destruct b3. + + exists nil. exists (true::true::true::nil). exists true. simpl. reflexivity. + exists nil. exists (true::true::false::nil). exists true. simpl. reflexivity. + exists nil. exists (true::false::true::nil). exists true. simpl. reflexivity. + exists nil. exists (true::false::false::nil). exists true. simpl. reflexivity. + exists nil. exists (false::true::true::nil). exists true. simpl. reflexivity. + exists nil. exists (false::true::false::nil). exists true. simpl. reflexivity. + exists nil. exists (false::false::true::nil). exists true. simpl. reflexivity. + exists nil. exists (false::false::false::nil). exists true. simpl. reflexivity. + + exists (true::false::nil). exists (true::nil). exists true. simpl. reflexivity. + exists (true::false::nil). exists (false::nil). exists true. simpl. reflexivity. + + + + + + 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.