Update
This commit is contained in:
Thomas Baruchel
parent
71831f8b89
commit
94e65475a3
448
src/thue_morse.v
448
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.
|
||||
|
|
|
|||
|
|
@ -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'.
|
||||
|
||||
*)
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user