From 94e65475a3242bceca8d824be38aec2f719b7517 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sun, 15 Jan 2023 16:12:10 +0100 Subject: [PATCH] Update --- src/thue_morse.v | 448 ------------------------------------------- src/thue_morse2.v | 471 +++++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 466 insertions(+), 453 deletions(-) diff --git a/src/thue_morse.v b/src/thue_morse.v index 91906ab..3e94398 100644 --- a/src/thue_morse.v +++ b/src/thue_morse.v @@ -1179,451 +1179,3 @@ Proof. apply app_inv_head_iff. rewrite app_assoc. rewrite firstn_skipn. reflexivity. Qed. - - -(** - The following lemmas and theorems are related to the sequence being - cubefree. Only the final theorem is of general interest; all other - lemmas are defined for the very specific purpose of being used in the - final proof. -*) - -Lemma tm_step_cube1 : forall (n : nat) (a hd tl: list bool), - tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length a) = true. -Proof. - intros n a hd tl. intro H. - assert (Nat.Even (length hd) \/ Nat.Odd (length hd)). apply Nat.Even_or_Odd. - assert (Nat.Even (length a) \/ Nat.Odd (length a)). apply Nat.Even_or_Odd. - - destruct H1. - - apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption. - - destruct H0. - assert (count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false). - assert (Nat.even (length hd) = true). - apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption. - generalize H2. generalize H. apply tm_step_count_occ. - - assert (I := H). replace (hd++a++a++a++tl) with ((hd++a++a)++(a++tl)) in I. - assert (count_occ Bool.bool_dec (hd++a++a) true = count_occ Bool.bool_dec (hd++a++a) false). - assert (even (length (hd++a++a)) = true). - rewrite app_length. rewrite Nat.even_add_even. - apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption. - - rewrite app_length. replace (length a) with (1*(length a)). - rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_r. - rewrite <- Nat.add_0_l. apply Nat.EvenT_Even. - apply Nat.even_EvenT. - rewrite Nat.even_add_mul_2. reflexivity. - apply Nat.mul_1_l. - generalize H3. generalize I. apply tm_step_count_occ. - - rewrite count_occ_app in H3. symmetry in H3. - rewrite count_occ_app in H3. rewrite H2 in H3. - rewrite Nat.add_cancel_l in H3. - - rewrite count_occ_app in H3. rewrite count_occ_app in H3. - replace (count_occ bool_dec a false) with (1*(count_occ bool_dec a false)) in H3. - replace (count_occ bool_dec a true) with (1*(count_occ bool_dec a true)) in H3. - rewrite <- Nat.mul_add_distr_r in H3. rewrite <- Nat.mul_add_distr_r in H3. - rewrite Nat.mul_cancel_l in H3. apply count_occ_bool_list2 in H3. - assumption. easy. apply Nat.mul_1_l. apply Nat.mul_1_l. - rewrite app_assoc_reverse. rewrite app_inv_head_iff. - apply app_assoc_reverse. - - assert (I := H). replace (hd++a++a++a++tl) with ((hd++a)++(a++a++tl)) in I. - assert (count_occ Bool.bool_dec (hd++a) true = count_occ Bool.bool_dec (hd++a) false). - assert (even (length (hd++a)) = true). - rewrite Nat.EvenT_even. reflexivity. apply Nat.Even_EvenT. - rewrite app_length. apply Nat.Odd_Odd_add; assumption. - generalize H2. generalize I. apply tm_step_count_occ. - - assert (J := H). replace (hd++a++a++a++tl) with ((hd++a++a++a)++tl) in J. - assert (count_occ Bool.bool_dec (hd++a++a++a) true = count_occ Bool.bool_dec (hd++a++a++a) false). - assert (even (length (hd++a++a++a)) = true). - rewrite Nat.EvenT_even. reflexivity. apply Nat.Even_EvenT. - rewrite app_length. rewrite app_length. rewrite Nat.add_assoc. rewrite <- app_length. - apply Nat.Even_Even_add. - rewrite app_length. apply Nat.Odd_Odd_add; assumption. - rewrite app_length. apply Nat.Odd_Odd_add; assumption. - generalize H3. generalize J. apply tm_step_count_occ. - - replace (hd++a++a++a) with ((hd++a)++(a++a)) in H3. - rewrite count_occ_app in H3. symmetry in H3. - rewrite count_occ_app in H3. rewrite H2 in H3. - rewrite Nat.add_cancel_l in H3. - - rewrite count_occ_app in H3. rewrite count_occ_app in H3. - replace (count_occ bool_dec a false) with (1*(count_occ bool_dec a false)) in H3. - replace (count_occ bool_dec a true) with (1*(count_occ bool_dec a true)) in H3. - rewrite <- Nat.mul_add_distr_r in H3. rewrite <- Nat.mul_add_distr_r in H3. - rewrite Nat.mul_cancel_l in H3. apply count_occ_bool_list2 in H3. - assumption. easy. apply Nat.mul_1_l. apply Nat.mul_1_l. - apply app_assoc_reverse. - rewrite app_assoc_reverse. rewrite app_inv_head_iff. - rewrite app_assoc_reverse. rewrite app_inv_head_iff. - apply app_assoc_reverse. - apply app_assoc_reverse. -Qed. - - -Lemma tm_step_cube2 : forall (n : nat) (a hd tl: list bool), - tm_step n = hd ++ a ++ a ++ a ++ tl -> 0 < length a -> 0 < n. -Proof. - intros n a hd tl. intros H I. - destruct n. - - assert (3 <= length (a ++ a ++ a)). - rewrite app_length. rewrite app_length. - rewrite <- Nat.le_succ_l in I. - assert (2 <= length a + length a). - generalize I. generalize I. apply Nat.add_le_mono. - generalize H0. generalize I. apply Nat.add_le_mono. - assert (length (tm_step 0) = length (tm_step 0)). reflexivity. - rewrite H in H1 at 2. - assert (0 <= length hd). apply Nat.le_0_l. - assert (0 + 3 <= length hd + length (a ++ a ++ a)). - generalize H0. generalize H2. apply Nat.add_le_mono. - simpl in H3. rewrite <- app_length in H3. - assert (0 <= length tl). apply Nat.le_0_l. - assert (3 + 0 <= length (hd ++ a ++ a ++ a) + length (tl)). - generalize H4. generalize H3. apply Nat.add_le_mono. - rewrite <- app_length in H5. rewrite Nat.add_0_r in H5. - replace ((hd++a++a++a)++tl) with (hd++a++a++a++tl) in H5. - rewrite <- H1 in H5. simpl in H5. apply le_S_n in H5. - apply Nat.nle_succ_0 in H5. contradiction H5. - rewrite app_assoc_reverse. rewrite app_inv_head_iff. - rewrite app_assoc_reverse. rewrite app_inv_head_iff. - rewrite app_assoc_reverse. reflexivity. - - apply Nat.lt_0_succ. -Qed. - - -Lemma tm_step_cube3 : forall (n : nat) (a hd tl: list bool), - tm_step n = hd ++ a ++ a ++ a ++ tl - -> 0 < length a - -> even (length hd) = even (length tl). -Proof. - intros n a hd tl. intros H J. - assert (K : 0 < n). generalize J. generalize H. apply tm_step_cube2. - destruct n. - - apply Nat.lt_irrefl in K. contradiction K. - - assert (Nat.Even (length (tm_step (S n)))). - rewrite tm_size_power2. rewrite Nat.pow_succ_r'. - apply Nat.Even_mul_l. apply Nat.EvenT_Even. - apply Nat.EvenT_2. apply Nat.EvenT_0. - rewrite H in H0. rewrite app_length in H0. rewrite app_length in H0. - rewrite Nat.add_shuffle3 in H0. - assert (I := H). apply tm_step_cube1 in I. - apply Nat.even_EvenT in I. apply Nat.EvenT_Even in I. - assert (Nat.Even (length hd + length (a ++ a ++ tl))). - generalize I. generalize H0. apply Nat.Even_add_Even_inv_r. - rewrite app_length in H1. rewrite Nat.add_shuffle3 in H1. - assert (Nat.Even (length hd + length (a ++ tl))). - generalize I. generalize H1. apply Nat.Even_add_Even_inv_r. - rewrite app_length in H2. rewrite Nat.add_shuffle3 in H2. - assert (Nat.Even (length hd + length tl)). - generalize I. generalize H2. apply Nat.Even_add_Even_inv_r. - - apply Nat.Even_EvenT in H3. apply Nat.EvenT_even in H3. - rewrite Nat.even_add in H3. - destruct (even (length hd)); destruct (even (length tl)). - reflexivity. simpl in H3. inversion H3. - simpl in H3. inversion H3. reflexivity. -Qed. - - -Lemma tm_step_cube4 : forall (n : nat) (a hd tl: list bool), - tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length hd) = false - -> 0 < length a - -> hd_error a = hd_error tl. -Proof. - intros n a hd tl. intros H I J. - assert (even (length hd) = even (length tl)). - generalize J. generalize H. apply tm_step_cube3. - assert (even (length a) = true). generalize H. apply tm_step_cube1. - rewrite I in H0. - destruct a. - - simpl in J. apply Nat.lt_irrefl in J. contradiction J. - - destruct tl. simpl in H0. inversion H0. - simpl. replace (b::a) with ((b::nil) ++ a) in H. - replace (hd ++ ([b] ++ a) ++ ([b] ++ a) ++ ([b] ++ a) ++ (b0::tl)) - with ((hd ++ (b::nil)) ++ (a ++ (b::nil)) ++ (a ++ (b::nil)) ++ (a ++ (b0::nil)) ++ tl) in H. - - assert (even (length (hd ++ (b::nil))) = true). - rewrite last_length. - rewrite Nat.even_succ. rewrite <- Nat.negb_even. rewrite I. reflexivity. - - assert (count_occ Bool.bool_dec (hd ++ (b::nil)) true - = count_occ Bool.bool_dec (hd ++ (b::nil)) false). - generalize H2. generalize H. apply tm_step_count_occ. - - assert (even (length ((hd ++ (b::nil)) ++ (a++ (b::nil)))) = true). - rewrite app_length. rewrite Nat.even_add. rewrite H2. - rewrite last_length. - replace (length (b::a)) with (S (length a)) in H1. rewrite H1. reflexivity. - reflexivity. - - assert (count_occ Bool.bool_dec ((hd ++ [b]) ++ a ++ [b]) true - = count_occ Bool.bool_dec ((hd ++ [b]) ++ a ++ [b]) false). - generalize H4. rewrite app_assoc in H. generalize H. apply tm_step_count_occ. - - assert (K := H5). - rewrite count_occ_app in H5. symmetry in H5. rewrite count_occ_app in H5. - rewrite H3 in H5. rewrite Nat.add_cancel_l in H5. - - assert (even (length ((hd ++ (b::nil)) ++ (a++ (b::nil)) ++ (a++ (b::nil)))) = true). - rewrite app_assoc. rewrite app_length. rewrite Nat.even_add. rewrite H4. - rewrite last_length. - replace (length (b::a)) with (S (length a)) in H1. rewrite H1. reflexivity. - reflexivity. - - assert (count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b])) true - = count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b])) false). - generalize H6. - rewrite app_assoc in H. rewrite app_assoc in H. - replace (((hd ++ [b]) ++ a ++ [b]) ++ a ++ [b]) - with ((hd ++ [b]) ++ (a ++ [b]) ++ a ++ [b]) in H. - generalize H. apply tm_step_count_occ. - - rewrite app_assoc_reverse. rewrite app_assoc_reverse. rewrite app_assoc_reverse. - rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff. - rewrite app_assoc_reverse. reflexivity. - - assert (even (length ((hd ++ (b::nil)) ++ (a++ (b::nil)) ++ (a++ (b::nil)) ++ (a++ (b0::nil)))) = true). - rewrite app_assoc. rewrite app_length. rewrite Nat.even_add. rewrite H4. - rewrite app_length. rewrite last_length. - replace (length (b::a)) with (S (length a)) in H1. rewrite Nat.even_add. rewrite H1. - rewrite last_length. rewrite H1. reflexivity. reflexivity. - - assert (count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b]) ++ (a ++ [b0])) true - = count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b]) ++ (a ++ [b0])) false). - generalize H8. - - rewrite app_assoc in H. rewrite app_assoc in H. rewrite app_assoc in H. - replace ((((hd ++ [b]) ++ a ++ [b]) ++ a ++ [b]) ++ a ++ [b0]) - with ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b]) ++ (a ++ [b0])) in H. - generalize H. apply tm_step_count_occ. - - rewrite app_assoc_reverse. rewrite app_assoc_reverse. rewrite app_assoc_reverse. - rewrite app_assoc_reverse. rewrite app_assoc_reverse. rewrite app_assoc_reverse. - apply app_inv_head_iff. apply app_inv_head_iff. - rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff. - rewrite app_assoc_reverse. reflexivity. - - rewrite count_occ_app in H9. symmetry in H9. rewrite count_occ_app in H9. - rewrite H3 in H9. rewrite Nat.add_cancel_l in H9. - rewrite count_occ_app in H9. symmetry in H9. rewrite count_occ_app in H9. - rewrite H5 in H9. rewrite Nat.add_cancel_l in H9. - rewrite count_occ_app in H9. symmetry in H9. rewrite count_occ_app in H9. - rewrite H5 in H9. rewrite Nat.add_cancel_l in H9. - - destruct b; destruct b0. - + reflexivity. - + rewrite count_occ_app in H9. rewrite count_occ_app in H9. - rewrite count_occ_cons_eq in H9. rewrite count_occ_cons_neq in H9. - rewrite count_occ_nil in H9. rewrite count_occ_nil in H9. - rewrite Nat.add_1_r in H9. rewrite Nat.add_0_r in H9. - rewrite count_occ_app in H5. rewrite count_occ_app in H5. - rewrite count_occ_cons_neq in H5. rewrite count_occ_cons_eq in H5. - rewrite count_occ_nil in H5. rewrite count_occ_nil in H5. - rewrite Nat.add_1_r in H5. rewrite Nat.add_0_r in H5. - rewrite H5 in H9. - rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_1_r in H9. - rewrite <- Nat.add_0_r in H9. rewrite <- Nat.add_assoc in H9. - rewrite Nat.add_cancel_l in H9. inversion H9. - reflexivity. easy. easy. reflexivity. - + rewrite count_occ_app in H9. rewrite count_occ_app in H9. - rewrite count_occ_cons_neq in H9. rewrite count_occ_cons_eq in H9. - rewrite count_occ_nil in H9. rewrite count_occ_nil in H9. - rewrite Nat.add_1_r in H9. rewrite Nat.add_0_r in H9. - rewrite count_occ_app in H5. rewrite count_occ_app in H5. - rewrite count_occ_cons_eq in H5. rewrite count_occ_cons_neq in H5. - rewrite count_occ_nil in H5. rewrite count_occ_nil in H5. - rewrite Nat.add_1_r in H5. rewrite Nat.add_0_r in H5. - rewrite <- H5 in H9. - rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_1_r in H9. - rewrite <- Nat.add_0_r in H9 at 1. rewrite <- Nat.add_assoc in H9. - rewrite Nat.add_cancel_l in H9. inversion H9. - easy. reflexivity. reflexivity. easy. - + reflexivity. - + rewrite app_assoc_reverse. apply app_inv_head_iff. - rewrite app_assoc_reverse. rewrite app_assoc_reverse. - rewrite app_assoc_reverse. rewrite app_assoc_reverse. - apply app_inv_head_iff. apply app_inv_head_iff. - rewrite app_assoc_reverse. - apply app_inv_head_iff. apply app_inv_head_iff. - rewrite app_assoc_reverse. - reflexivity. - + reflexivity. -Qed. - - -Lemma tm_step_cube5 : forall (n : nat) (a hd tl: list bool), - tm_step n = hd ++ a ++ a ++ a ++ tl - -> 0 < length a - -> exists (hd2 b tl2 : list bool), tm_step n = hd2 ++ b ++ b ++ b ++ tl2 - /\ length a = length b - /\ even (length hd2) = true. -Proof. - intros n a hd tl. intros H I. - assert (J: Nat.Even (length hd) \/ Nat.Odd (length hd)). - apply Nat.Even_or_Odd. - destruct J. - - exists hd. exists a. exists tl. - split. assumption. split. reflexivity. - apply Nat.Even_EvenT in H0. - apply Nat.EvenT_even in H0. assumption. - - apply Nat.Odd_OddT in H0. - apply Nat.OddT_odd in H0. - rewrite <- Nat.negb_even in H0. rewrite negb_true_iff in H0. - destruct a. - + simpl in I. apply Nat.lt_irrefl in I. contradiction I. - + assert (Nat.even (length hd) = Nat.even (length tl)). - generalize I. generalize H. apply tm_step_cube3. - rewrite H0 in H1. - destruct tl. - * simpl in H1. inversion H1. - * assert (hd_error (b::a) = hd_error (b0::tl)). - generalize I. generalize H0. generalize H. apply tm_step_cube4. - simpl in H2. inversion H2. rewrite <- H4 in H. - exists (hd ++ (b::nil)). exists (a ++ (b::nil)). exists tl. - split. rewrite H. - rewrite app_assoc_reverse. apply app_inv_head_iff. - replace (b::a) with ([b] ++ a). - rewrite app_assoc_reverse. apply app_inv_head_iff. - rewrite app_assoc_reverse. rewrite app_assoc_reverse. - rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff. - rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff. - rewrite app_assoc_reverse. reflexivity. - reflexivity. - split. rewrite last_length. reflexivity. - rewrite last_length. - rewrite Nat.even_succ. rewrite <- Nat.negb_even. rewrite H0. - reflexivity. -Qed. - - -Lemma tm_step_cube6 : forall (n : nat) (a hd tl: list bool), - tm_step n = hd ++ a ++ a ++ a ++ tl - -> 0 < length a - -> exists (hd2 b tl2 : list bool), - tm_step (Nat.pred n) = hd2 ++ b ++ b ++ b ++ tl2 /\ 0 < length b. -Proof. - intros n a hd tl. intros H I. - assert(J: exists (hd2 b tl2 : list bool), - tm_step n = hd2 ++ b ++ b ++ b ++ tl2 - /\ length a = length b /\ even (length hd2) = true). - generalize I. generalize H. apply tm_step_cube5. - destruct J as [ hd2 J0]. destruct J0 as [ b J1]. destruct J1 as [ tl2 J2]. - destruct J2 as [J3 J4]. destruct J4 as [J5 J6]. - assert (J: even (length b) = true). generalize J3. apply tm_step_cube1. - - assert (K: 0 < n). generalize I. generalize H. apply tm_step_cube2. - destruct n. - - apply Nat.lt_irrefl in K. contradiction K. - - rewrite <- tm_step_lemma in J3. - assert (L: hd2 = tm_morphism (firstn (Nat.div2 (length hd2)) (tm_step n))). - generalize J6. generalize J3. apply tm_morphism_app2. - assert (M: b ++ b ++ b ++ tl2 - = tm_morphism (skipn (Nat.div2 (length hd2)) (tm_step n))). - generalize J6. generalize J3. apply tm_morphism_app3. - assert (N: b = tm_morphism (firstn (Nat.div2 (length b)) - (skipn (Nat.div2 (length hd2)) - (tm_step n)))). - generalize J. symmetry in M. generalize M. apply tm_morphism_app2. - assert (even (length (b++b++b)) = true). - rewrite app_length. rewrite app_length. - rewrite Nat.even_add_even. assumption. - apply Nat.EvenT_Even. apply Nat.even_EvenT. - rewrite Nat.even_add_even. assumption. - apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. - assert (O: tl2 = tm_morphism (skipn (Nat.div2 (length (b++b++b))) - (skipn (Nat.div2 (length hd2)) - (tm_step n)))). - generalize H0. symmetry in M. generalize M. - replace (b++b++b++tl2) with ((b++b++b)++tl2). apply tm_morphism_app3. - rewrite app_assoc_reverse. apply app_inv_head_iff. - apply app_assoc_reverse. - assert (hd2 ++ b ++ b ++ b ++ tl2 - = (tm_morphism (firstn (Nat.div2 (length hd2)) (tm_step n))) - ++ (tm_morphism (firstn (Nat.div2 (length b)) - (skipn (Nat.div2 (length hd2)) (tm_step n)))) - ++ (tm_morphism (firstn (Nat.div2 (length b)) - (skipn (Nat.div2 (length hd2)) (tm_step n)))) - ++ (tm_morphism (firstn (Nat.div2 (length b)) - (skipn (Nat.div2 (length hd2)) (tm_step n)))) - ++ (tm_morphism (skipn (Nat.div2 (length (b ++ b ++ b))) - (skipn (Nat.div2 (length hd2)) (tm_step n))))). - rewrite <- L. rewrite <- N. rewrite <- O. reflexivity. - rewrite <- tm_morphism_app in H1. rewrite <- tm_morphism_app in H1. - rewrite <- tm_morphism_app in H1. rewrite <- tm_morphism_app in H1. - rewrite <- J3 in H1. - - rewrite Nat.pred_succ. rewrite <- tm_morphism_eq in H1. - exists (firstn (Nat.div2 (length hd2)) (tm_step n)). - exists (firstn (Nat.div2 (length b)) - (skipn (Nat.div2 (length hd2)) (tm_step n))). - exists (skipn (Nat.div2 (length (b ++ b ++ b))) - (skipn (Nat.div2 (length hd2)) (tm_step n))). - split. assumption. - - assert (2 <= length b). destruct b. simpl in J5. rewrite J5 in I. - apply Nat.lt_irrefl in I. contradiction I. - destruct b0. simpl in J. inversion J. simpl. rewrite <- Nat.succ_le_mono. - rewrite <- Nat.succ_le_mono. apply Nat.le_0_l. - - assert (length (b++b++b++tl2) - = 2 * length (skipn (Nat.div2 (length hd2)) (tm_step n))). - rewrite M. apply tm_morphism_length. - - assert (2 <= length (b++b++b++tl2)). - rewrite app_length. rewrite <- Nat.add_0_r at 1. - apply Nat.add_le_mono. assumption. apply Nat.le_0_l. - rewrite H3 in H4. rewrite <- Nat.mul_1_r in H4 at 1. - rewrite <- Nat.mul_le_mono_pos_l in H4. - - rewrite firstn_length. rewrite <- Nat.le_succ_l. - assert (1 <= Nat.div2 (length b)). - rewrite Nat.mul_le_mono_pos_l with (p:= 2). rewrite Nat.mul_1_r. - replace (2 * Nat.div2 (length b)) - with (2 * Nat.div2 (length b) + Nat.b2n (Nat.odd (length b))). - rewrite <- Nat.div2_odd. assumption. - rewrite <- Nat.negb_even. rewrite J. simpl. rewrite Nat.add_0_r. reflexivity. - apply Nat.lt_0_2. - generalize H4. generalize H5. apply Nat.min_glb. - apply Nat.lt_0_2. -Qed. - - -Lemma tm_step_cube7 : forall (n : nat), - (exists (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ a ++ tl - /\ 0 < length a) - -> exists (hd2 b tl2 : list bool), tm_step 0 = hd2 ++ b ++ b ++ b ++ tl2 - /\ 0 < length b. -Proof. - intros n. intro H. - induction n; destruct H; destruct H; destruct H; destruct H. - - exists x. exists x0. exists x1. split; assumption. - - assert (J: exists (hd2 b2 tl2 : list bool), - tm_step (Nat.pred (S n)) = hd2 ++ b2 ++ b2 ++ b2 ++ tl2 - /\ 0 < length b2). - generalize H0. generalize H. apply tm_step_cube6. - rewrite Nat.pred_succ in J. apply IHn. apply J. -Qed. - - -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. -Proof. - intros n hd a b tl. intros H I. - - assert (J: {a=b} + {~ a=b}). apply list_eq_dec. apply bool_dec. - destruct J. - - rewrite <- e in H. - assert (J: exists (hd a tl : list bool), - tm_step n = hd ++ a ++ a ++ a ++ tl /\ 0 < length a). - exists hd. exists a. exists tl. split; assumption. - apply tm_step_cube7 in J. destruct J. destruct H0. destruct H0. destruct H0. - assert (0 < 0). generalize H1. generalize H0. apply tm_step_cube2. - apply Nat.lt_irrefl in H2. contradiction H2. - - assumption. -Qed. diff --git a/src/thue_morse2.v b/src/thue_morse2.v index 3e187eb..7f2e76b 100644 --- a/src/thue_morse2.v +++ b/src/thue_morse2.v @@ -1,3 +1,18 @@ +(** * The Thue-Morse sequence (part 2) + + The following lemmas and theorems are all related to + squares of odd length in the Thue-Morse sequence. + + Proofs in this file are long; many parts are repeated + from copy/paste operations. Many ad-hoc lemmas could + probably be written in a better style. + + But some powerful theorems are provided here: + + - tm_step_square_size (all squared factors of odd + length have length 1 or 3). +*) + Require Import thue_morse. Require Import Coq.Lists.List. @@ -9,12 +24,457 @@ Import ListNotations. (** - The following lemmas and theorems are all related to - squares of odd length in the Thue-Morse sequence. - All squared factors of odd length have length 1 or 3. + The following lemmas and theorems are related to the sequence being + cubefree. Only the final theorem is of general interest; all other + lemmas are defined for the very specific purpose of being used in the + final proof. *) -Theorem tm_step_odd_square : forall (n : nat) (hd a tl : list bool), +Lemma tm_step_cube1 : forall (n : nat) (a hd tl: list bool), + tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length a) = true. +Proof. + intros n a hd tl. intro H. + assert (Nat.Even (length hd) \/ Nat.Odd (length hd)). apply Nat.Even_or_Odd. + assert (Nat.Even (length a) \/ Nat.Odd (length a)). apply Nat.Even_or_Odd. + + destruct H1. + - apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption. + - destruct H0. + assert (count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false). + assert (Nat.even (length hd) = true). + apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption. + generalize H2. generalize H. apply tm_step_count_occ. + + assert (I := H). replace (hd++a++a++a++tl) with ((hd++a++a)++(a++tl)) in I. + assert (count_occ Bool.bool_dec (hd++a++a) true = count_occ Bool.bool_dec (hd++a++a) false). + assert (even (length (hd++a++a)) = true). + rewrite app_length. rewrite Nat.even_add_even. + apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption. + + rewrite app_length. replace (length a) with (1*(length a)). + rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_r. + rewrite <- Nat.add_0_l. apply Nat.EvenT_Even. + apply Nat.even_EvenT. + rewrite Nat.even_add_mul_2. reflexivity. + apply Nat.mul_1_l. + generalize H3. generalize I. apply tm_step_count_occ. + + rewrite count_occ_app in H3. symmetry in H3. + rewrite count_occ_app in H3. rewrite H2 in H3. + rewrite Nat.add_cancel_l in H3. + + rewrite count_occ_app in H3. rewrite count_occ_app in H3. + replace (count_occ bool_dec a false) with (1*(count_occ bool_dec a false)) in H3. + replace (count_occ bool_dec a true) with (1*(count_occ bool_dec a true)) in H3. + rewrite <- Nat.mul_add_distr_r in H3. rewrite <- Nat.mul_add_distr_r in H3. + rewrite Nat.mul_cancel_l in H3. apply count_occ_bool_list2 in H3. + assumption. easy. apply Nat.mul_1_l. apply Nat.mul_1_l. + rewrite app_assoc_reverse. rewrite app_inv_head_iff. + apply app_assoc_reverse. + + assert (I := H). replace (hd++a++a++a++tl) with ((hd++a)++(a++a++tl)) in I. + assert (count_occ Bool.bool_dec (hd++a) true = count_occ Bool.bool_dec (hd++a) false). + assert (even (length (hd++a)) = true). + rewrite Nat.EvenT_even. reflexivity. apply Nat.Even_EvenT. + rewrite app_length. apply Nat.Odd_Odd_add; assumption. + generalize H2. generalize I. apply tm_step_count_occ. + + assert (J := H). replace (hd++a++a++a++tl) with ((hd++a++a++a)++tl) in J. + assert (count_occ Bool.bool_dec (hd++a++a++a) true = count_occ Bool.bool_dec (hd++a++a++a) false). + assert (even (length (hd++a++a++a)) = true). + rewrite Nat.EvenT_even. reflexivity. apply Nat.Even_EvenT. + rewrite app_length. rewrite app_length. rewrite Nat.add_assoc. rewrite <- app_length. + apply Nat.Even_Even_add. + rewrite app_length. apply Nat.Odd_Odd_add; assumption. + rewrite app_length. apply Nat.Odd_Odd_add; assumption. + generalize H3. generalize J. apply tm_step_count_occ. + + replace (hd++a++a++a) with ((hd++a)++(a++a)) in H3. + rewrite count_occ_app in H3. symmetry in H3. + rewrite count_occ_app in H3. rewrite H2 in H3. + rewrite Nat.add_cancel_l in H3. + + rewrite count_occ_app in H3. rewrite count_occ_app in H3. + replace (count_occ bool_dec a false) with (1*(count_occ bool_dec a false)) in H3. + replace (count_occ bool_dec a true) with (1*(count_occ bool_dec a true)) in H3. + rewrite <- Nat.mul_add_distr_r in H3. rewrite <- Nat.mul_add_distr_r in H3. + rewrite Nat.mul_cancel_l in H3. apply count_occ_bool_list2 in H3. + assumption. easy. apply Nat.mul_1_l. apply Nat.mul_1_l. + apply app_assoc_reverse. + rewrite app_assoc_reverse. rewrite app_inv_head_iff. + rewrite app_assoc_reverse. rewrite app_inv_head_iff. + apply app_assoc_reverse. + apply app_assoc_reverse. +Qed. + + +Lemma tm_step_cube2 : forall (n : nat) (a hd tl: list bool), + tm_step n = hd ++ a ++ a ++ a ++ tl -> 0 < length a -> 0 < n. +Proof. + intros n a hd tl. intros H I. + destruct n. + - assert (3 <= length (a ++ a ++ a)). + rewrite app_length. rewrite app_length. + rewrite <- Nat.le_succ_l in I. + assert (2 <= length a + length a). + generalize I. generalize I. apply Nat.add_le_mono. + generalize H0. generalize I. apply Nat.add_le_mono. + assert (length (tm_step 0) = length (tm_step 0)). reflexivity. + rewrite H in H1 at 2. + assert (0 <= length hd). apply Nat.le_0_l. + assert (0 + 3 <= length hd + length (a ++ a ++ a)). + generalize H0. generalize H2. apply Nat.add_le_mono. + simpl in H3. rewrite <- app_length in H3. + assert (0 <= length tl). apply Nat.le_0_l. + assert (3 + 0 <= length (hd ++ a ++ a ++ a) + length (tl)). + generalize H4. generalize H3. apply Nat.add_le_mono. + rewrite <- app_length in H5. rewrite Nat.add_0_r in H5. + replace ((hd++a++a++a)++tl) with (hd++a++a++a++tl) in H5. + rewrite <- H1 in H5. simpl in H5. apply le_S_n in H5. + apply Nat.nle_succ_0 in H5. contradiction H5. + rewrite app_assoc_reverse. rewrite app_inv_head_iff. + rewrite app_assoc_reverse. rewrite app_inv_head_iff. + rewrite app_assoc_reverse. reflexivity. + - apply Nat.lt_0_succ. +Qed. + + +Lemma tm_step_cube3 : forall (n : nat) (a hd tl: list bool), + tm_step n = hd ++ a ++ a ++ a ++ tl + -> 0 < length a + -> even (length hd) = even (length tl). +Proof. + intros n a hd tl. intros H J. + assert (K : 0 < n). generalize J. generalize H. apply tm_step_cube2. + destruct n. + - apply Nat.lt_irrefl in K. contradiction K. + - assert (Nat.Even (length (tm_step (S n)))). + rewrite tm_size_power2. rewrite Nat.pow_succ_r'. + apply Nat.Even_mul_l. apply Nat.EvenT_Even. + apply Nat.EvenT_2. apply Nat.EvenT_0. + rewrite H in H0. rewrite app_length in H0. rewrite app_length in H0. + rewrite Nat.add_shuffle3 in H0. + assert (I := H). apply tm_step_cube1 in I. + apply Nat.even_EvenT in I. apply Nat.EvenT_Even in I. + assert (Nat.Even (length hd + length (a ++ a ++ tl))). + generalize I. generalize H0. apply Nat.Even_add_Even_inv_r. + rewrite app_length in H1. rewrite Nat.add_shuffle3 in H1. + assert (Nat.Even (length hd + length (a ++ tl))). + generalize I. generalize H1. apply Nat.Even_add_Even_inv_r. + rewrite app_length in H2. rewrite Nat.add_shuffle3 in H2. + assert (Nat.Even (length hd + length tl)). + generalize I. generalize H2. apply Nat.Even_add_Even_inv_r. + + apply Nat.Even_EvenT in H3. apply Nat.EvenT_even in H3. + rewrite Nat.even_add in H3. + destruct (even (length hd)); destruct (even (length tl)). + reflexivity. simpl in H3. inversion H3. + simpl in H3. inversion H3. reflexivity. +Qed. + + +Lemma tm_step_cube4 : forall (n : nat) (a hd tl: list bool), + tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length hd) = false + -> 0 < length a + -> hd_error a = hd_error tl. +Proof. + intros n a hd tl. intros H I J. + assert (even (length hd) = even (length tl)). + generalize J. generalize H. apply tm_step_cube3. + assert (even (length a) = true). generalize H. apply tm_step_cube1. + rewrite I in H0. + destruct a. + - simpl in J. apply Nat.lt_irrefl in J. contradiction J. + - destruct tl. simpl in H0. inversion H0. + simpl. replace (b::a) with ((b::nil) ++ a) in H. + replace (hd ++ ([b] ++ a) ++ ([b] ++ a) ++ ([b] ++ a) ++ (b0::tl)) + with ((hd ++ (b::nil)) ++ (a ++ (b::nil)) ++ (a ++ (b::nil)) ++ (a ++ (b0::nil)) ++ tl) in H. + + assert (even (length (hd ++ (b::nil))) = true). + rewrite last_length. + rewrite Nat.even_succ. rewrite <- Nat.negb_even. rewrite I. reflexivity. + + assert (count_occ Bool.bool_dec (hd ++ (b::nil)) true + = count_occ Bool.bool_dec (hd ++ (b::nil)) false). + generalize H2. generalize H. apply tm_step_count_occ. + + assert (even (length ((hd ++ (b::nil)) ++ (a++ (b::nil)))) = true). + rewrite app_length. rewrite Nat.even_add. rewrite H2. + rewrite last_length. + replace (length (b::a)) with (S (length a)) in H1. rewrite H1. reflexivity. + reflexivity. + + assert (count_occ Bool.bool_dec ((hd ++ [b]) ++ a ++ [b]) true + = count_occ Bool.bool_dec ((hd ++ [b]) ++ a ++ [b]) false). + generalize H4. rewrite app_assoc in H. generalize H. apply tm_step_count_occ. + + assert (K := H5). + rewrite count_occ_app in H5. symmetry in H5. rewrite count_occ_app in H5. + rewrite H3 in H5. rewrite Nat.add_cancel_l in H5. + + assert (even (length ((hd ++ (b::nil)) ++ (a++ (b::nil)) ++ (a++ (b::nil)))) = true). + rewrite app_assoc. rewrite app_length. rewrite Nat.even_add. rewrite H4. + rewrite last_length. + replace (length (b::a)) with (S (length a)) in H1. rewrite H1. reflexivity. + reflexivity. + + assert (count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b])) true + = count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b])) false). + generalize H6. + rewrite app_assoc in H. rewrite app_assoc in H. + replace (((hd ++ [b]) ++ a ++ [b]) ++ a ++ [b]) + with ((hd ++ [b]) ++ (a ++ [b]) ++ a ++ [b]) in H. + generalize H. apply tm_step_count_occ. + + rewrite app_assoc_reverse. rewrite app_assoc_reverse. rewrite app_assoc_reverse. + rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff. + rewrite app_assoc_reverse. reflexivity. + + assert (even (length ((hd ++ (b::nil)) ++ (a++ (b::nil)) ++ (a++ (b::nil)) ++ (a++ (b0::nil)))) = true). + rewrite app_assoc. rewrite app_length. rewrite Nat.even_add. rewrite H4. + rewrite app_length. rewrite last_length. + replace (length (b::a)) with (S (length a)) in H1. rewrite Nat.even_add. rewrite H1. + rewrite last_length. rewrite H1. reflexivity. reflexivity. + + assert (count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b]) ++ (a ++ [b0])) true + = count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b]) ++ (a ++ [b0])) false). + generalize H8. + + rewrite app_assoc in H. rewrite app_assoc in H. rewrite app_assoc in H. + replace ((((hd ++ [b]) ++ a ++ [b]) ++ a ++ [b]) ++ a ++ [b0]) + with ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b]) ++ (a ++ [b0])) in H. + generalize H. apply tm_step_count_occ. + + rewrite app_assoc_reverse. rewrite app_assoc_reverse. rewrite app_assoc_reverse. + rewrite app_assoc_reverse. rewrite app_assoc_reverse. rewrite app_assoc_reverse. + apply app_inv_head_iff. apply app_inv_head_iff. + rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff. + rewrite app_assoc_reverse. reflexivity. + + rewrite count_occ_app in H9. symmetry in H9. rewrite count_occ_app in H9. + rewrite H3 in H9. rewrite Nat.add_cancel_l in H9. + rewrite count_occ_app in H9. symmetry in H9. rewrite count_occ_app in H9. + rewrite H5 in H9. rewrite Nat.add_cancel_l in H9. + rewrite count_occ_app in H9. symmetry in H9. rewrite count_occ_app in H9. + rewrite H5 in H9. rewrite Nat.add_cancel_l in H9. + + destruct b; destruct b0. + + reflexivity. + + rewrite count_occ_app in H9. rewrite count_occ_app in H9. + rewrite count_occ_cons_eq in H9. rewrite count_occ_cons_neq in H9. + rewrite count_occ_nil in H9. rewrite count_occ_nil in H9. + rewrite Nat.add_1_r in H9. rewrite Nat.add_0_r in H9. + rewrite count_occ_app in H5. rewrite count_occ_app in H5. + rewrite count_occ_cons_neq in H5. rewrite count_occ_cons_eq in H5. + rewrite count_occ_nil in H5. rewrite count_occ_nil in H5. + rewrite Nat.add_1_r in H5. rewrite Nat.add_0_r in H5. + rewrite H5 in H9. + rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_1_r in H9. + rewrite <- Nat.add_0_r in H9. rewrite <- Nat.add_assoc in H9. + rewrite Nat.add_cancel_l in H9. inversion H9. + reflexivity. easy. easy. reflexivity. + + rewrite count_occ_app in H9. rewrite count_occ_app in H9. + rewrite count_occ_cons_neq in H9. rewrite count_occ_cons_eq in H9. + rewrite count_occ_nil in H9. rewrite count_occ_nil in H9. + rewrite Nat.add_1_r in H9. rewrite Nat.add_0_r in H9. + rewrite count_occ_app in H5. rewrite count_occ_app in H5. + rewrite count_occ_cons_eq in H5. rewrite count_occ_cons_neq in H5. + rewrite count_occ_nil in H5. rewrite count_occ_nil in H5. + rewrite Nat.add_1_r in H5. rewrite Nat.add_0_r in H5. + rewrite <- H5 in H9. + rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_1_r in H9. + rewrite <- Nat.add_0_r in H9 at 1. rewrite <- Nat.add_assoc in H9. + rewrite Nat.add_cancel_l in H9. inversion H9. + easy. reflexivity. reflexivity. easy. + + reflexivity. + + rewrite app_assoc_reverse. apply app_inv_head_iff. + rewrite app_assoc_reverse. rewrite app_assoc_reverse. + rewrite app_assoc_reverse. rewrite app_assoc_reverse. + apply app_inv_head_iff. apply app_inv_head_iff. + rewrite app_assoc_reverse. + apply app_inv_head_iff. apply app_inv_head_iff. + rewrite app_assoc_reverse. + reflexivity. + + reflexivity. +Qed. + + +Lemma tm_step_cube5 : forall (n : nat) (a hd tl: list bool), + tm_step n = hd ++ a ++ a ++ a ++ tl + -> 0 < length a + -> exists (hd2 b tl2 : list bool), tm_step n = hd2 ++ b ++ b ++ b ++ tl2 + /\ length a = length b + /\ even (length hd2) = true. +Proof. + intros n a hd tl. intros H I. + assert (J: Nat.Even (length hd) \/ Nat.Odd (length hd)). + apply Nat.Even_or_Odd. + destruct J. + - exists hd. exists a. exists tl. + split. assumption. split. reflexivity. + apply Nat.Even_EvenT in H0. + apply Nat.EvenT_even in H0. assumption. + - apply Nat.Odd_OddT in H0. + apply Nat.OddT_odd in H0. + rewrite <- Nat.negb_even in H0. rewrite negb_true_iff in H0. + destruct a. + + simpl in I. apply Nat.lt_irrefl in I. contradiction I. + + assert (Nat.even (length hd) = Nat.even (length tl)). + generalize I. generalize H. apply tm_step_cube3. + rewrite H0 in H1. + destruct tl. + * simpl in H1. inversion H1. + * assert (hd_error (b::a) = hd_error (b0::tl)). + generalize I. generalize H0. generalize H. apply tm_step_cube4. + simpl in H2. inversion H2. rewrite <- H4 in H. + exists (hd ++ (b::nil)). exists (a ++ (b::nil)). exists tl. + split. rewrite H. + rewrite app_assoc_reverse. apply app_inv_head_iff. + replace (b::a) with ([b] ++ a). + rewrite app_assoc_reverse. apply app_inv_head_iff. + rewrite app_assoc_reverse. rewrite app_assoc_reverse. + rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff. + rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff. + rewrite app_assoc_reverse. reflexivity. + reflexivity. + split. rewrite last_length. reflexivity. + rewrite last_length. + rewrite Nat.even_succ. rewrite <- Nat.negb_even. rewrite H0. + reflexivity. +Qed. + + +Lemma tm_step_cube6 : forall (n : nat) (a hd tl: list bool), + tm_step n = hd ++ a ++ a ++ a ++ tl + -> 0 < length a + -> exists (hd2 b tl2 : list bool), + tm_step (Nat.pred n) = hd2 ++ b ++ b ++ b ++ tl2 /\ 0 < length b. +Proof. + intros n a hd tl. intros H I. + assert(J: exists (hd2 b tl2 : list bool), + tm_step n = hd2 ++ b ++ b ++ b ++ tl2 + /\ length a = length b /\ even (length hd2) = true). + generalize I. generalize H. apply tm_step_cube5. + destruct J as [ hd2 J0]. destruct J0 as [ b J1]. destruct J1 as [ tl2 J2]. + destruct J2 as [J3 J4]. destruct J4 as [J5 J6]. + assert (J: even (length b) = true). generalize J3. apply tm_step_cube1. + + assert (K: 0 < n). generalize I. generalize H. apply tm_step_cube2. + destruct n. + - apply Nat.lt_irrefl in K. contradiction K. + - rewrite <- tm_step_lemma in J3. + assert (L: hd2 = tm_morphism (firstn (Nat.div2 (length hd2)) (tm_step n))). + generalize J6. generalize J3. apply tm_morphism_app2. + assert (M: b ++ b ++ b ++ tl2 + = tm_morphism (skipn (Nat.div2 (length hd2)) (tm_step n))). + generalize J6. generalize J3. apply tm_morphism_app3. + assert (N: b = tm_morphism (firstn (Nat.div2 (length b)) + (skipn (Nat.div2 (length hd2)) + (tm_step n)))). + generalize J. symmetry in M. generalize M. apply tm_morphism_app2. + assert (even (length (b++b++b)) = true). + rewrite app_length. rewrite app_length. + rewrite Nat.even_add_even. assumption. + apply Nat.EvenT_Even. apply Nat.even_EvenT. + rewrite Nat.even_add_even. assumption. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + assert (O: tl2 = tm_morphism (skipn (Nat.div2 (length (b++b++b))) + (skipn (Nat.div2 (length hd2)) + (tm_step n)))). + generalize H0. symmetry in M. generalize M. + replace (b++b++b++tl2) with ((b++b++b)++tl2). apply tm_morphism_app3. + rewrite app_assoc_reverse. apply app_inv_head_iff. + apply app_assoc_reverse. + assert (hd2 ++ b ++ b ++ b ++ tl2 + = (tm_morphism (firstn (Nat.div2 (length hd2)) (tm_step n))) + ++ (tm_morphism (firstn (Nat.div2 (length b)) + (skipn (Nat.div2 (length hd2)) (tm_step n)))) + ++ (tm_morphism (firstn (Nat.div2 (length b)) + (skipn (Nat.div2 (length hd2)) (tm_step n)))) + ++ (tm_morphism (firstn (Nat.div2 (length b)) + (skipn (Nat.div2 (length hd2)) (tm_step n)))) + ++ (tm_morphism (skipn (Nat.div2 (length (b ++ b ++ b))) + (skipn (Nat.div2 (length hd2)) (tm_step n))))). + rewrite <- L. rewrite <- N. rewrite <- O. reflexivity. + rewrite <- tm_morphism_app in H1. rewrite <- tm_morphism_app in H1. + rewrite <- tm_morphism_app in H1. rewrite <- tm_morphism_app in H1. + rewrite <- J3 in H1. + + rewrite Nat.pred_succ. rewrite <- tm_morphism_eq in H1. + exists (firstn (Nat.div2 (length hd2)) (tm_step n)). + exists (firstn (Nat.div2 (length b)) + (skipn (Nat.div2 (length hd2)) (tm_step n))). + exists (skipn (Nat.div2 (length (b ++ b ++ b))) + (skipn (Nat.div2 (length hd2)) (tm_step n))). + split. assumption. + + assert (2 <= length b). destruct b. simpl in J5. rewrite J5 in I. + apply Nat.lt_irrefl in I. contradiction I. + destruct b0. simpl in J. inversion J. simpl. rewrite <- Nat.succ_le_mono. + rewrite <- Nat.succ_le_mono. apply Nat.le_0_l. + + assert (length (b++b++b++tl2) + = 2 * length (skipn (Nat.div2 (length hd2)) (tm_step n))). + rewrite M. apply tm_morphism_length. + + assert (2 <= length (b++b++b++tl2)). + rewrite app_length. rewrite <- Nat.add_0_r at 1. + apply Nat.add_le_mono. assumption. apply Nat.le_0_l. + rewrite H3 in H4. rewrite <- Nat.mul_1_r in H4 at 1. + rewrite <- Nat.mul_le_mono_pos_l in H4. + + rewrite firstn_length. rewrite <- Nat.le_succ_l. + assert (1 <= Nat.div2 (length b)). + rewrite Nat.mul_le_mono_pos_l with (p:= 2). rewrite Nat.mul_1_r. + replace (2 * Nat.div2 (length b)) + with (2 * Nat.div2 (length b) + Nat.b2n (Nat.odd (length b))). + rewrite <- Nat.div2_odd. assumption. + rewrite <- Nat.negb_even. rewrite J. simpl. rewrite Nat.add_0_r. reflexivity. + apply Nat.lt_0_2. + generalize H4. generalize H5. apply Nat.min_glb. + apply Nat.lt_0_2. +Qed. + + +Lemma tm_step_cube7 : forall (n : nat), + (exists (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ a ++ tl + /\ 0 < length a) + -> exists (hd2 b tl2 : list bool), tm_step 0 = hd2 ++ b ++ b ++ b ++ tl2 + /\ 0 < length b. +Proof. + intros n. intro H. + induction n; destruct H; destruct H; destruct H; destruct H. + - exists x. exists x0. exists x1. split; assumption. + - assert (J: exists (hd2 b2 tl2 : list bool), + tm_step (Nat.pred (S n)) = hd2 ++ b2 ++ b2 ++ b2 ++ tl2 + /\ 0 < length b2). + generalize H0. generalize H. apply tm_step_cube6. + rewrite Nat.pred_succ in J. apply IHn. apply J. +Qed. + + +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. +Proof. + intros n hd a b tl. intros H I. + + assert (J: {a=b} + {~ a=b}). apply list_eq_dec. apply bool_dec. + destruct J. + - rewrite <- e in H. + assert (J: exists (hd a tl : list bool), + tm_step n = hd ++ a ++ a ++ a ++ tl /\ 0 < length a). + exists hd. exists a. exists tl. split; assumption. + apply tm_step_cube7 in J. destruct J. destruct H0. destruct H0. destruct H0. + assert (0 < 0). generalize H1. generalize H0. apply tm_step_cube2. + apply Nat.lt_irrefl in H2. contradiction H2. + - assumption. +Qed. + +(** + The following lemma is required for the following parts f the file. +*) + +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. @@ -976,6 +1436,7 @@ Qed. +(* Lemma tm_step_square_pos_even'' : forall (n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> 0 < length a @@ -987,7 +1448,7 @@ Lemma tm_step_square_pos_even'' : forall (n : nat) (hd a tl : list bool), /\ even (length a') = true /\ length a' < length a /\ 0 < length a'. - + *)