baruchel
/
coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
coqbooks/src/thue_morse2.v

1465 lines
63 KiB
Coq
Raw Blame History

(** * The Thue-Morse sequence (part 2)
The following lemmas and theorems are all related to
squares and cubes 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_cubefree (there is no cube in the sequence)
- tm_step_square_size (about length of squared factrs)
- tm_step_square_pos (length of the prefix has the same
parity than the length of the factor being squared)
*)
Require Import thue_morse.
Require Import Coq.Lists.List.
Require Import PeanoNat.
Require Import Nat.
Require Import Bool.
Import ListNotations.
(**
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.
(**
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.
assert (J: 4 < length a \/ length a <= 4).
apply Nat.lt_ge_cases. destruct J.
assert (exists b c d, a = b ++ [d;d] ++ c).
generalize H0. generalize H. apply tm_step_consecutive_identical_length.
destruct H1. destruct H1. destruct H1. rewrite H1 in H.
replace (hd ++ (x ++ [x1; x1] ++ x0) ++ (x ++ [x1; x1] ++ x0) ++ tl)
with ((hd ++ x) ++ [x1;x1] ++ (x0++x) ++ [x1;x1] ++ (x0 ++ tl)) in H.
apply tm_step_consecutive_identical' in H.
assert (J: even (length (x0 ++ x)) = false).
rewrite H1 in I. rewrite app_length in I. rewrite app_length in I.
rewrite Nat.add_shuffle3 in I. rewrite Nat.add_comm in I.
rewrite Nat.odd_add_even in I.
rewrite app_length. rewrite Nat.add_comm. rewrite <- Nat.negb_odd.
rewrite I. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT.
reflexivity. rewrite H in J. inversion J.
rewrite <- app_assoc. apply app_inv_head_iff.
rewrite <- app_assoc. rewrite <- app_assoc. apply app_inv_head_iff.
rewrite <- app_assoc. apply app_inv_head_iff. apply app_inv_head_iff.
rewrite <- app_assoc. apply app_inv_head_iff.
reflexivity.
apply Nat.le_lteq in H0. destruct H0. assumption.
rewrite H0 in I. inversion I.
Qed.
(**
New following lemmas and theorems are related to the size
of squares in the Thue-Morse sequence, namely lengths of
2^n or 3 * 2^n only.
*)
Lemma tm_step_shift_odd_prefix_even_squares :
forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> even (length a) = true
-> odd (length hd) = true
-> exists (hd' b tl': list bool), tm_step n = hd' ++ b ++ b ++ tl'
/\ even (length hd') = true /\ length a = length b.
Proof.
intros n hd a tl. intros H I J.
assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
destruct W. rewrite e in J. simpl in J. rewrite Nat.odd_0 in J.
inversion J.
assert (Z: {a=nil} + {~ a=nil}). apply list_eq_dec. apply bool_dec.
destruct Z.
exists (removelast hd). exists nil. exists ((last hd true)::nil++tl).
split. rewrite app_nil_l. rewrite app_nil_l. rewrite app_nil_l.
replace ((last hd true)::tl) with ([last hd true] ++ tl).
rewrite app_assoc. rewrite <- app_removelast_last.
rewrite H. rewrite e. rewrite app_nil_l. rewrite app_nil_l. reflexivity.
assumption.
split. rewrite app_removelast_last with (l := hd) (d := last hd true) in J.
rewrite app_length in J. rewrite Nat.add_1_r in J. rewrite Nat.odd_succ in J.
rewrite J. split. reflexivity. rewrite e. reflexivity. assumption.
rewrite app_removelast_last with (l := hd) (d := true) in H.
rewrite app_removelast_last with (l := a) (d := true) in H.
rewrite app_assoc_reverse in H.
rewrite app_removelast_last with (l := hd) (d := true) in J.
rewrite app_length in J. rewrite Nat.add_1_r in J. rewrite Nat.odd_succ in J.
rewrite app_removelast_last with (l := a) (d := true) in I.
rewrite app_length in I. rewrite Nat.add_1_r in I.
exists (removelast hd).
rewrite app_assoc_reverse in H. rewrite app_assoc_reverse in H.
replace (
removelast hd ++ [last hd true] ++
removelast a ++ [last a true] ++ removelast a ++ [last a true] ++ tl)
with (
removelast hd ++
([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a) ++
([last a true] ++ tl)) in H.
assert (K: count_occ Bool.bool_dec (removelast hd) true
= count_occ Bool.bool_dec (removelast hd) false).
generalize J. generalize H. apply tm_step_count_occ.
assert (L: count_occ Bool.bool_dec (
removelast hd ++
([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a)) true
= count_occ Bool.bool_dec (
removelast hd ++
([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a)) false).
assert (M: even (length (
removelast hd ++
([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a))) = true).
rewrite app_length. rewrite Nat.even_add_even. apply J.
rewrite app_length. apply Nat.EvenT_Even. apply Nat.even_EvenT.
rewrite Nat.even_add_even. rewrite app_length.
rewrite Nat.add_1_l. assumption.
rewrite app_length. apply Nat.EvenT_Even. apply Nat.even_EvenT.
rewrite Nat.add_1_l. assumption.
generalize M.
replace (
removelast hd ++
([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a) ++
([last a true] ++ tl))
with ((
removelast hd ++
([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a)) ++
([last a true] ++ tl)) in H.
generalize H. apply tm_step_count_occ.
rewrite <- app_assoc. apply app_inv_head_iff.
rewrite <- app_assoc. reflexivity.
assert (M: count_occ Bool.bool_dec (
removelast hd ++
([last hd true] ++ removelast a)) true
= count_occ Bool.bool_dec (
removelast hd ++
([last hd true] ++ removelast a)) false).
assert (N: even (length (
removelast hd ++
([last hd true] ++ removelast a))) = true).
rewrite app_length. rewrite Nat.even_add_even. assumption.
rewrite app_length. apply Nat.EvenT_Even. apply Nat.even_EvenT.
rewrite Nat.add_1_l. assumption.
generalize N.
rewrite app_assoc in H. generalize H. apply tm_step_count_occ.
rewrite count_occ_app in M. symmetry in M. rewrite count_occ_app in M.
rewrite K in M. rewrite Nat.add_cancel_l in M.
rewrite count_occ_app in L. symmetry in L. rewrite count_occ_app in L.
rewrite K in L. rewrite Nat.add_cancel_l in L.
rewrite count_occ_app in L. symmetry in L. rewrite count_occ_app in L.
rewrite M in L. rewrite Nat.add_cancel_l in L.
assert (O: forall (m: nat), m <> S (S m)).
induction m. easy. apply not_eq_S. assumption.
assert (N: last hd true = last a true).
destruct (last hd true); destruct (last a true).
reflexivity.
rewrite count_occ_app in L. rewrite count_occ_app in L. simpl in L.
rewrite count_occ_app in M. rewrite count_occ_app in M. simpl in M.
rewrite L in M. apply O in M. contradiction M.
rewrite count_occ_app in L. rewrite count_occ_app in L. simpl in L.
rewrite count_occ_app in M. rewrite count_occ_app in M. simpl in M.
rewrite <- L in M. symmetry in M. apply O in M. contradiction M.
reflexivity.
rewrite N in H. exists ([last a true] ++ removelast a).
exists ([last a true] ++ tl). rewrite H.
split. reflexivity.
split. assumption.
rewrite app_length. rewrite app_removelast_last with (l := a) (d := true).
rewrite app_length. rewrite last_last. rewrite removelast_app.
rewrite Nat.add_1_r. rewrite app_nil_r. reflexivity. easy.
assumption.
rewrite <- app_assoc. apply app_inv_head_iff. reflexivity.
assumption. assumption. assumption. assumption.
Qed.
Lemma tm_step_normalize_prefix_even_squares :
forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> even (length a) = true
-> exists (hd' b tl': list bool), tm_step n = hd' ++ b ++ b ++ tl'
/\ even (length hd') = true /\ length a = length b.
Proof.
intros n hd a tl. intros H I.
assert (odd (length hd) = true \/ odd (length hd) = false).
destruct (odd (length hd)). left. reflexivity. right. reflexivity.
destruct H0.
generalize H0. generalize I. generalize H.
apply tm_step_shift_odd_prefix_even_squares.
exists hd. exists a. exists tl.
split. assumption. split. rewrite <- Nat.negb_odd. rewrite H0.
reflexivity. reflexivity.
Qed.
Lemma tm_step_square_half : forall (n : nat) (hd a tl : list bool),
tm_step (S n) = hd ++ a ++ a ++ tl
-> even (length a) = true
-> exists (hd' a' tl' : list bool), tm_step n = hd' ++ a' ++ a' ++ tl'
/\ length a = Nat.double (length a').
Proof.
intros n hd a tl. intros H I.
assert (
exists (hd' b tl': list bool), tm_step (S n) = hd' ++ b ++ b ++ tl'
/\ even (length hd') = true /\ length a = length b).
generalize I. generalize H. apply tm_step_normalize_prefix_even_squares.
destruct H0. destruct H0. destruct H0.
destruct H0. destruct H1. rewrite H2 in I.
rewrite <- tm_step_lemma in H0.
assert (x = tm_morphism (firstn (Nat.div2 (length x)) (tm_step n))).
apply tm_morphism_app2 with (tl := x0 ++ x0 ++ x1). apply H0.
assumption.
assert (x0 ++ x0 ++ x1 = tm_morphism (skipn (Nat.div2 (length x)) (tm_step n))).
apply tm_morphism_app3. apply H0. assumption.
assert (Z := H0).
assert (H7: length (tm_morphism (tm_step n)) = length (tm_morphism (tm_step n))).
reflexivity. rewrite Z in H7 at 2. rewrite tm_morphism_length in H7.
rewrite app_length in H7.
rewrite app_length in H7.
rewrite Nat.Even_double with (n := length x) in H7.
rewrite Nat.Even_double with (n := length x0) in H7.
rewrite Nat.Even_double with (n := length (x0 ++ x1)) in H7.
rewrite Nat.double_twice in H7.
rewrite Nat.double_twice in H7.
rewrite Nat.double_twice in H7.
rewrite <- Nat.mul_add_distr_l in H7.
rewrite <- Nat.mul_add_distr_l in H7.
rewrite Nat.mul_cancel_l in H7.
assert (x0 = tm_morphism (firstn (Nat.div2 (length x0)) (skipn (Nat.div2 (length x)) (tm_step n)))).
apply tm_morphism_app2 with (tl := x0 ++ x1). symmetry. assumption.
assumption.
assert (x1 = tm_morphism (skipn (Nat.div2 (length (x0++x0)))
(skipn (Nat.div2 (length x)) (tm_step n)))).
apply tm_morphism_app3. symmetry. rewrite app_assoc_reverse. apply H4.
rewrite app_length. rewrite Nat.even_add_even. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
rewrite H3 in H0. rewrite H5 in H0. rewrite H6 in H0.
rewrite <- tm_morphism_app in H0.
rewrite <- tm_morphism_app in H0.
rewrite <- tm_morphism_app in H0.
rewrite <- tm_morphism_eq in H0.
rewrite H0.
exists (firstn (Nat.div2 (length x)) (tm_step n)).
exists (firstn (Nat.div2 (length x0)) (skipn (Nat.div2 (length x)) (tm_step n))).
exists (skipn (Nat.div2 (length (x0 ++ x0))) (skipn (Nat.div2 (length x)) (tm_step n))).
split. reflexivity.
rewrite firstn_length_le. rewrite <- Nat.Even_double. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
rewrite skipn_length.
rewrite H7. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
rewrite Nat.add_0_l. rewrite <- Nat.add_0_r at 1.
rewrite <- Nat.add_le_mono_l.
apply le_0_n. apply le_n. easy.
rewrite <- Nat.Even_double in H7. rewrite <- Nat.Even_double in H7.
rewrite Nat.add_assoc in H7.
assert (Nat.even (2 * (length (tm_step n))) = true).
apply Nat.even_mul. rewrite H7 in H5.
rewrite Nat.even_add in H5.
rewrite Nat.even_add in H5.
rewrite I in H5. rewrite H1 in H5.
apply Nat.EvenT_Even. apply Nat.even_EvenT.
destruct (Nat.even (length (x0 ++ x1))). reflexivity.
inversion H5.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
Qed.
Theorem tm_step_square_size : forall (n k j : nat) (hd a tl : list bool),
tm_step (S n) = hd ++ a ++ a ++ tl
-> length a = (S (Nat.double k)) * 2^j
-> (k = 0 \/ k = 1).
Proof.
intros n k j hd a tl.
generalize hd. generalize a. generalize tl. induction j.
- intros tl0 a0 hd0. intros H I. simpl in I. rewrite Nat.mul_1_r in I.
assert (odd (length a0) = true). rewrite I.
rewrite Nat.odd_succ. rewrite Nat.double_twice.
apply Nat.even_mul.
assert (J: length a0 < 4). generalize H0. generalize H.
apply tm_step_odd_square.
rewrite I in J.
destruct k. left. reflexivity.
destruct k. right. reflexivity.
apply Nat.succ_lt_mono in J.
apply Nat.lt_lt_succ_r in J.
rewrite Nat.double_twice in J. replace (4) with (2*2) in J.
rewrite <- Nat.mul_lt_mono_pos_l in J.
apply Nat.succ_lt_mono in J.
apply Nat.succ_lt_mono in J.
apply Nat.nlt_0_r in J. contradiction J.
apply Nat.lt_0_2. reflexivity.
- intros tl0 a0 hd0. intros H I.
assert (exists (hd' a' tl' : list bool), tm_step n = hd' ++ a' ++ a' ++ tl'
/\ length a0 = Nat.double (length a')).
assert (even (length a0) = true).
rewrite I. rewrite Nat.pow_succ_r'. rewrite Nat.mul_comm.
rewrite <- Nat.mul_assoc. apply Nat.even_mul.
generalize H0. generalize H. apply tm_step_square_half.
destruct H0. destruct H0. destruct H0. destruct H0.
rewrite H1 in I. rewrite Nat.pow_succ_r' in I. rewrite Nat.mul_comm in I.
rewrite <- Nat.mul_assoc in I. rewrite Nat.double_twice in I.
rewrite Nat.mul_cancel_l in I. rewrite Nat.mul_comm in I.
generalize I.
assert (tm_step (S n) = x ++ x0 ++ x0 ++ x1 ++ (map negb (tm_step n))).
rewrite tm_build. rewrite H0.
rewrite <- app_assoc. apply app_inv_head_iff.
rewrite <- app_assoc. apply app_inv_head_iff.
rewrite <- app_assoc. reflexivity.
generalize H2. apply IHj. easy.
Qed.
(**
This section contains lemmas and theorems related to the length of the
prefix being odd or even in front of a squared pattern.
*)
Lemma tm_step_odd_prefix_square : forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> odd (length a) = true -> even (length hd) = false.
Proof.
intros n hd a tl. intros H I.
assert (length a < 4). generalize I. generalize H. apply tm_step_odd_square.
destruct a. inversion I. destruct a.
- rewrite <- negb_true_iff. rewrite Nat.negb_even.
generalize H. apply tm_step_consecutive_identical.
- destruct a. inversion I. destruct a.
assert (J: {b0 = b1} + {b0 <> b1}). apply bool_dec. destruct J.
rewrite e in H.
replace (hd ++ [b;b1;b1] ++ [b;b1;b1] ++ tl)
with ((hd ++ [b]) ++ [b1;b1] ++ [b] ++ [b1;b1] ++ tl) in H.
assert (K: even (length [b]) = true). generalize H.
apply tm_step_consecutive_identical'. inversion K.
rewrite <- app_assoc. reflexivity.
assert (J: {b = b0} + {b <> b0}). apply bool_dec. destruct J.
rewrite e in H.
replace (hd ++ [b0;b0;b1] ++ [b0;b0;b1] ++ tl)
with (hd ++ [b0;b0] ++ [b1] ++ [b0;b0] ++ [b1] ++ tl) in H.
assert (K: even (length [b1]) = true). generalize H.
apply tm_step_consecutive_identical'. inversion K.
reflexivity.
assert (J: {b = b1} + {b <> b1}). apply bool_dec. destruct J.
rewrite e in H.
assert (J: Nat.even (length hd) || Nat.odd (length hd) = true).
apply Nat.orb_even_odd. apply orb_prop in J. destruct J.
assert (K: count_occ Bool.bool_dec hd true
= count_occ Bool.bool_dec hd false).
generalize H1. generalize H. apply tm_step_count_occ.
assert (L: count_occ Bool.bool_dec (hd ++ [b1;b0;b1;b1]) true
= count_occ Bool.bool_dec (hd ++ [b1;b0;b1;b1]) false).
assert (M: even (length (hd ++ [b1;b0;b1;b1])) = true).
rewrite app_length. rewrite Nat.even_add. rewrite H1. reflexivity.
replace (hd ++ [b1;b0;b1] ++ [b1;b0;b1] ++ tl)
with ((hd ++ [b1;b0;b1;b1]) ++ [b0;b1] ++ tl) in H.
generalize M. generalize H. apply tm_step_count_occ.
rewrite <- app_assoc. reflexivity.
rewrite count_occ_app in L. symmetry in L. rewrite count_occ_app in L.
rewrite K in L. rewrite Nat.add_cancel_l in L.
destruct b0; destruct b1; inversion L.
rewrite <- Nat.negb_odd. rewrite H1. reflexivity.
destruct b; destruct b0; destruct b1.
contradiction n0. contradiction n2. contradiction n1. contradiction n2.
contradiction n0. reflexivity.
contradiction n0. contradiction n2. reflexivity.
contradiction n1. reflexivity. contradiction n0. reflexivity.
simpl in H0.
rewrite <- Nat.succ_lt_mono in H0.
rewrite <- Nat.succ_lt_mono in H0.
rewrite <- Nat.succ_lt_mono in H0.
rewrite <- Nat.succ_lt_mono in H0.
apply Nat.nlt_0_r in H0. contradiction H0.
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
-> odd (length hd) = true
-> even (length a) = true
-> exists (hd' a' tl' : list bool),
tm_step n = hd' ++ a' ++ a' ++ tl'
/\ length hd' = S (length hd)
/\ length a' = length a.
Proof.
intros n hd a tl. intros H I J K.
(* proof that tl is not nil *)
assert (W: nil <> tl).
assert (even (length (a++a)) = true). rewrite app_length.
rewrite Nat.even_add. rewrite K. reflexivity.
assert (0 < length (a ++ a)). rewrite <- Nat.add_0_r at 1.
rewrite app_length. apply Nat.add_lt_mono; assumption.
generalize H0. generalize J. generalize H1.
replace (hd++a++a++tl) with (hd++(a++a)++tl) in H. generalize H.
apply tm_step_tail_not_nil_prefix_odd. rewrite <- app_assoc. reflexivity.
destruct tl. contradiction W. reflexivity.
(* proof that a is not nil *)
destruct a. inversion I.
replace (hd ++ (b0 :: a) ++ (b0 :: a) ++ b :: tl)
with ((hd ++ [b0]) ++ a ++ (b0::a) ++ b::tl) in H.
assert (even (length (hd ++ [b0])) = true).
rewrite app_length. rewrite Nat.add_1_r. rewrite Nat.even_succ.
assumption.
assert (L: count_occ Bool.bool_dec (hd ++ [b0]) true
= count_occ Bool.bool_dec (hd ++ [b0]) false).
generalize H0. generalize H. apply tm_step_count_occ.
replace ((hd ++ [b0]) ++ a ++ (b0::a) ++ b::tl)
with ((hd ++ [b0] ++ a ++ [b0] ++ a ++ [b]) ++ tl) in H.
assert (even (length (hd ++ [b0] ++ a ++ [b0] ++ a ++ [b])) = true).
rewrite <- app_assoc_reverse. rewrite app_length.
rewrite Nat.even_add. rewrite H0.
rewrite app_length. rewrite app_length. rewrite app_length.
rewrite Nat.add_1_r. rewrite <- Nat.add_succ_comm.
rewrite Nat.even_add.
destruct (even (S (length a))); reflexivity.
assert (M: count_occ Bool.bool_dec (hd ++ [b0]++a++[b0]++a++[b]) true
= count_occ Bool.bool_dec (hd ++ [b0]++a++[b0]++a++[b]) false).
generalize H1. generalize H. apply tm_step_count_occ.
rewrite app_assoc in M. rewrite count_occ_app in M.
symmetry in M. rewrite count_occ_app in M. rewrite L in M.
rewrite Nat.add_cancel_l in M.
assert (forall x , x + x = 2*x).
intro x. rewrite <- Nat.mul_1_l with (n := x).
rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_r.
rewrite Nat.mul_1_l. reflexivity.
Opaque even. simpl in K. Transparent even.
assert (b = b0). destruct b0; destruct b.
- reflexivity.
- rewrite count_occ_app in M. rewrite count_occ_app in M.
rewrite count_occ_app in M. rewrite count_occ_app in M.
rewrite count_occ_app in M. rewrite count_occ_app in M.
simpl in M. rewrite Nat.add_1_r in M. rewrite Nat.add_0_r in M.
rewrite Nat.add_succ_r in M. rewrite Nat.add_succ_r in M.
inversion M.
rewrite H2 in H4. rewrite H2 in H4.
rewrite Nat.mul_cancel_l in H4.
apply count_occ_bool_list2 in H4.
rewrite <- K in H4. rewrite Nat.even_succ in H4.
rewrite <- Nat.negb_even in H4.
destruct (even (length a)); inversion H4. easy.
- rewrite count_occ_app in M. rewrite count_occ_app in M.
rewrite count_occ_app in M. rewrite count_occ_app in M.
rewrite count_occ_app in M. rewrite count_occ_app in M.
simpl in M. rewrite Nat.add_1_r in M. rewrite Nat.add_0_r in M.
rewrite Nat.add_succ_r in M. rewrite Nat.add_succ_r in M.
inversion M.
rewrite H2 in H4. rewrite H2 in H4.
rewrite Nat.mul_cancel_l in H4.
apply count_occ_bool_list2 in H4.
rewrite <- K in H4. rewrite Nat.even_succ in H4.
rewrite <- Nat.negb_even in H4.
destruct (even (length a)); inversion H4. easy.
- reflexivity.
- rewrite H3 in H.
exists (hd ++ [b0]). exists (a ++ [b0]). exists tl.
split. rewrite H. rewrite <- app_assoc. rewrite <- app_assoc.
rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
split. apply last_length. apply last_length.
- rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
reflexivity.
- rewrite <- app_assoc. reflexivity.
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
-> odd (length hd) = true
-> even (length a) = true
-> exists (hd' a' tl' : list bool),
tm_step n = hd' ++ a' ++ a' ++ tl'
/\ length hd' = Nat.pred (length hd)
/\ length a' = length a.
Proof.
intros n hd a tl. intros H I J K.
assert (L: hd = removelast hd ++ last hd false :: nil).
apply app_removelast_last. destruct hd. inversion J. easy.
rewrite L in H.
assert (M: a = removelast a ++ last a false :: nil).
apply app_removelast_last. destruct a. inversion I. easy.
rewrite M in H.
rewrite <- app_assoc in H. rewrite <- app_assoc in H.
rewrite <- app_assoc in H.
assert (U: even (length (removelast hd)) = true).
rewrite L in J. rewrite app_length in J.
rewrite Nat.add_1_r in J. rewrite Nat.odd_succ in J.
assumption.
assert (N: count_occ Bool.bool_dec (removelast hd) true
= count_occ Bool.bool_dec (removelast hd) false).
generalize U. generalize H. apply tm_step_count_occ.
rewrite app_assoc in H. rewrite app_assoc in H.
assert (V: even (length ((removelast hd ++ [last hd false])
++ removelast a)) = true).
rewrite app_length. rewrite <- L. rewrite Nat.even_add.
rewrite <- Nat.negb_odd. rewrite J. rewrite M in K.
rewrite app_length in K. rewrite Nat.add_1_r in K.
rewrite Nat.even_succ in K. rewrite <- Nat.negb_odd.
rewrite K. reflexivity.
assert (O: count_occ Bool.bool_dec
((removelast hd ++ [last hd false]) ++ removelast a) true
= count_occ Bool.bool_dec
((removelast hd ++ [last hd false]) ++ removelast a) false).
generalize V. generalize H. apply tm_step_count_occ.
replace ((removelast hd ++ [last hd false]) ++ removelast a)
with (removelast hd ++ ([last hd false] ++ removelast a)) in O.
rewrite count_occ_app in O. symmetry in O. rewrite count_occ_app in O.
rewrite N in O. rewrite Nat.add_cancel_l in O.
rewrite app_assoc in H. rewrite app_assoc in H.
assert (W: even (length ((((removelast hd ++ [last hd false])
++ removelast a) ++ [last a false])
++ removelast a)) = true).
rewrite app_length. rewrite app_length. rewrite Nat.even_add.
rewrite Nat.even_add. rewrite V.
assert (even (length (removelast a)) = false).
rewrite M in K. rewrite app_length in K. rewrite Nat.add_1_r in K.
rewrite Nat.even_succ in K. rewrite <- Nat.negb_odd. rewrite K.
reflexivity. rewrite H0. reflexivity.
assert (P: count_occ Bool.bool_dec
((((removelast hd ++ [last hd false]) ++ removelast a) ++ [last a false]) ++ removelast a) true
= count_occ Bool.bool_dec
((((removelast hd ++ [last hd false]) ++ removelast a) ++ [last a false]) ++ removelast a) false).
generalize W. generalize H. apply tm_step_count_occ.
rewrite <- app_assoc in P. rewrite <- app_assoc in P.
rewrite <- app_assoc in P.
rewrite count_occ_app in P. symmetry in P. rewrite count_occ_app in P.
rewrite N in P. rewrite Nat.add_cancel_l in P.
rewrite app_assoc in P. rewrite count_occ_app in P. symmetry in P.
rewrite count_occ_app in P. rewrite O in P. rewrite Nat.add_cancel_l in P.
assert (last hd false = last a false).
destruct (last hd false); destruct (last a false).
reflexivity.
simpl in O. simpl in P. rewrite O in P.
rewrite <- Nat.add_1_l in P. rewrite <- Nat.add_succ_comm in P.
rewrite <- Nat.add_0_l in P at 1. rewrite Nat.add_cancel_r in P.
inversion P.
simpl in O. simpl in P. rewrite <- O in P. symmetry in P.
rewrite <- Nat.add_1_l in P. rewrite <- Nat.add_succ_comm in P.
rewrite <- Nat.add_0_l in P at 1. rewrite Nat.add_cancel_r in P.
inversion P.
reflexivity.
rewrite H0 in H.
exists (removelast hd). exists ([last a false] ++ removelast a).
exists ([last a false] ++ tl).
split. rewrite H.
rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
reflexivity.
split.
assert (X: length hd = length hd). reflexivity.
rewrite app_removelast_last with (l := hd) (d := false) in X at 2.
rewrite app_length in X. rewrite Nat.add_1_r in X.
rewrite <- Nat.succ_pred_pos with (n := length hd) in X.
apply Nat.succ_inj. rewrite X. reflexivity.
destruct (length hd). inversion J. apply Nat.lt_0_succ.
destruct hd. inversion J. easy.
rewrite app_length. rewrite Nat.add_comm. rewrite <- app_length.
rewrite <- M. reflexivity.
rewrite <- app_assoc. reflexivity.
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
-> odd (length hd) = true
-> even (length a) = true
-> exists (hd' a' tl' : list bool),
tm_step (Nat.pred n) = hd' ++ a' ++ a' ++ tl'
/\ 0 < length a'
/\ odd (length hd') = true
/\ even (length a') = true.
Proof.
intros n hd a tl. intros H I J K.
assert (L: exists (hd' a' tl' : list bool),
tm_step n = hd' ++ a' ++ a' ++ tl'
/\ length hd' = S (length hd) /\ length a' = length a).
generalize K. generalize J. generalize I. generalize H.
apply tm_step_square_pos_even.
assert (M: exists (hd' a' tl' : list bool),
tm_step n = hd' ++ a' ++ a' ++ tl'
/\ length hd' = Nat.pred (length hd) /\ length a' = length a).
generalize K. generalize J. generalize I. generalize H.
apply tm_step_square_pos_even'.
destruct L as [hd' L2]. destruct L2 as [a' L3]. destruct L3 as [tl' L].
destruct M as [hd'' M2]. destruct M2 as [a'' M3]. destruct M3 as [tl'' M].
destruct L as [L1 L2]. destruct L2 as [L2 L3].
destruct M as [M1 M2]. destruct M2 as [M2 M3].
assert (L0 := L1). assert (M0 := M1).
assert (N: 0 < n).
generalize K. generalize I. generalize H. apply tm_step_not_nil_factor_even.
destruct n. inversion N.
assert (L4: even (length hd') = true). rewrite L2. rewrite Nat.even_succ.
assumption.
assert (M4: even (length hd'') = true). rewrite M2. rewrite Nat.even_pred.
assumption. destruct hd. inversion J. easy.
rewrite <- tm_step_lemma in L1.
assert (L5: hd' = tm_morphism (firstn (Nat.div2 (length hd')) (tm_step n))).
generalize L4. generalize L1. apply tm_morphism_app2.
rewrite <- tm_step_lemma in M1.
assert (M5: hd'' = tm_morphism (firstn (Nat.div2 (length hd'')) (tm_step n))).
generalize M4. generalize M1. apply tm_morphism_app2.
assert (L6: a' ++ a' ++ tl'
= tm_morphism (skipn (Nat.div2 (length hd')) (tm_step n))).
generalize L4. generalize L1. apply tm_morphism_app3.
assert (M6: a'' ++ a'' ++ tl''
= tm_morphism (skipn (Nat.div2 (length hd'')) (tm_step n))).
generalize M4. generalize M1. apply tm_morphism_app3.
assert (L7: even (length a') = true). rewrite L3. assumption.
assert (L8: a' = tm_morphism (firstn (Nat.div2 (length a'))
(skipn (Nat.div2 (length hd')) (tm_step n)))).
generalize L7. symmetry in L6. generalize L6. apply tm_morphism_app2.
assert (M7: even (length a'') = true). rewrite M3. assumption.
assert (M8: a'' = tm_morphism (firstn (Nat.div2 (length a''))
(skipn (Nat.div2 (length hd'')) (tm_step n)))).
generalize M7. symmetry in M6. generalize M6. apply tm_morphism_app2.
rewrite app_assoc in L6. symmetry in L6.
rewrite app_assoc in M6. symmetry in M6.
assert (L9: even (length (a' ++ a')) = true). rewrite app_length.
rewrite Nat.even_add. rewrite L7. reflexivity.
assert (M9: even (length (a'' ++ a'')) = true). rewrite app_length.
rewrite Nat.even_add. rewrite M7. reflexivity.
assert (L10: tl' = tm_morphism (skipn (Nat.div2 (length (a' ++ a')))
(skipn (Nat.div2 (length hd')) (tm_step n)))).
generalize L9. generalize L6. apply tm_morphism_app3.
assert (M10: tl'' = tm_morphism (skipn (Nat.div2 (length (a'' ++ a'')))
(skipn (Nat.div2 (length hd'')) (tm_step n)))).
generalize M9. generalize M6. apply tm_morphism_app3.
rewrite L5 in L1. rewrite L8 in L1. rewrite L10 in L1.
rewrite <- tm_morphism_app in L1. rewrite <- tm_morphism_app in L1.
rewrite <- tm_morphism_app in L1. rewrite <- tm_morphism_eq in L1.
rewrite M5 in M1. rewrite M8 in M1. rewrite M10 in M1.
rewrite <- tm_morphism_app in M1. rewrite <- tm_morphism_app in M1.
rewrite <- tm_morphism_app in M1. rewrite <- tm_morphism_eq in M1.
(* now we easily discard the case where a'0 would be odd since we
can freely choose either L1 or M1 to find an even prefix *)
assert (Nat.Even (Nat.div2 (length a)) \/ Nat.Odd (Nat.div2 (length a))).
apply Nat.Even_or_Odd. destruct H0 as [Z | Z].
- (* first case, a'0 is even and we are looking for an odd prefix *)
assert (Nat.Even (Nat.div2 (length hd')) \/ Nat.Odd (Nat.div2 (length hd'))).
apply Nat.Even_or_Odd. destruct H0.
+ (* case Nat.div2 (length hd'') has an odd length *)
exists (firstn (Nat.div2 (length hd'')) (tm_step n)).
exists (firstn (Nat.div2 (length a''))
(skipn (Nat.div2 (length hd'')) (tm_step n))).
exists (skipn (Nat.div2 (length (a'' ++ a'')))
(skipn (Nat.div2 (length hd'')) (tm_step n))).
split. rewrite <- pred_Sn. rewrite M1 at 1. reflexivity.
assert (Nat.div2 (length hd'') <= length (tm_step n)).
rewrite Nat.mul_le_mono_pos_l with (p := 2).
rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
rewrite tm_size_power2. rewrite <- Nat.pow_succ_r'.
rewrite <- tm_size_power2. rewrite M0.
rewrite app_length. rewrite <- Nat.add_0_r at 1.
apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity.
apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT.
assumption. apply Nat.lt_0_2.
split.
rewrite firstn_length_le.
rewrite Nat.mul_lt_mono_pos_l with (p := 2).
rewrite Nat.mul_0_r. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double. rewrite M3. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.lt_0_2.
rewrite skipn_length.
rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd'')).
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
rewrite Nat.sub_diag. rewrite Nat.add_0_l.
rewrite Nat.mul_le_mono_pos_l with (p := 2).
rewrite tm_size_power2. rewrite Nat.mul_add_distr_l.
rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double. rewrite <- Nat.Even_double.
rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite M0.
rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1.
apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl.
reflexivity.
apply le_0_n.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
assumption.
split.
rewrite firstn_length_le.
apply eq_S in M2. rewrite Nat.succ_pred_pos in M2.
apply eq_S in M2. rewrite <- L2 in M2. rewrite <- M2 in H0.
rewrite <- Nat.Odd_div2 in H0. rewrite <- Nat.Even_div2 in H0.
apply Nat.Even_succ in H0. apply Nat.Odd_OddT in H0.
apply Nat.OddT_odd in H0. apply H0.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.OddT_Odd. apply Nat.odd_OddT. rewrite Nat.odd_succ.
assumption.
destruct (length hd). inversion J. apply Nat.lt_0_succ.
assumption.
rewrite firstn_length_le.
rewrite M3. apply Nat.EvenT_even. apply Nat.Even_EvenT.
assumption. rewrite skipn_length.
rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd'')).
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
rewrite Nat.sub_diag. rewrite Nat.add_0_l.
rewrite Nat.mul_le_mono_pos_l with (p := 2).
rewrite tm_size_power2. rewrite Nat.mul_add_distr_l.
rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double. rewrite <- Nat.Even_double.
rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite M0.
rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1.
apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl.
reflexivity.
apply le_0_n.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
assumption.
+ (* case Nat.div2 (length hd') has an odd length *)
exists (firstn (Nat.div2 (length hd')) (tm_step n)).
exists (firstn (Nat.div2 (length a'))
(skipn (Nat.div2 (length hd')) (tm_step n))).
exists (skipn (Nat.div2 (length (a' ++ a')))
(skipn (Nat.div2 (length hd')) (tm_step n))).
split. rewrite <- pred_Sn. rewrite L1 at 1. reflexivity.
assert (Nat.div2 (length hd') <= length (tm_step n)).
rewrite Nat.mul_le_mono_pos_l with (p := 2).
rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
rewrite tm_size_power2. rewrite <- Nat.pow_succ_r'.
rewrite <- tm_size_power2. rewrite L0.
rewrite app_length. rewrite <- Nat.add_0_r at 1.
apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity.
apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT.
assumption. apply Nat.lt_0_2.
split.
rewrite firstn_length_le.
rewrite Nat.mul_lt_mono_pos_l with (p := 2).
rewrite Nat.mul_0_r. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double. rewrite L3. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.lt_0_2.
rewrite skipn_length.
rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd')).
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
rewrite Nat.sub_diag. rewrite Nat.add_0_l.
rewrite Nat.mul_le_mono_pos_l with (p := 2).
rewrite tm_size_power2. rewrite Nat.mul_add_distr_l.
rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double. rewrite <- Nat.Even_double.
rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite L0.
rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1.
apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl.
reflexivity.
apply le_0_n.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
assumption.
split.
rewrite firstn_length_le.
apply Nat.OddT_odd. apply Nat.Odd_OddT. assumption.
assumption.
rewrite firstn_length_le.
rewrite L3. apply Nat.EvenT_even. apply Nat.Even_EvenT.
assumption. rewrite skipn_length.
rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd')).
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
rewrite Nat.sub_diag. rewrite Nat.add_0_l.
rewrite Nat.mul_le_mono_pos_l with (p := 2).
rewrite tm_size_power2. rewrite Nat.mul_add_distr_l.
rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double. rewrite <- Nat.Even_double.
rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite L0.
rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1.
apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl.
reflexivity.
apply le_0_n.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
assumption.
- (* second case, a'0 is odd and we are looking for an even prefix *)
assert (Nat.Even (Nat.div2 (length hd')) \/ Nat.Odd (Nat.div2 (length hd'))).
apply Nat.Even_or_Odd. destruct H0.
+ assert (Nat.div2 (length hd') <= length (tm_step n)).
rewrite Nat.mul_le_mono_pos_l with (p := 2).
rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
rewrite tm_size_power2. rewrite <- Nat.pow_succ_r'.
rewrite <- tm_size_power2. rewrite L0.
rewrite app_length. rewrite <- Nat.add_0_r at 1.
apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity.
apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT.
assumption. apply Nat.lt_0_2.
assert (even (length (firstn (Nat.div2 (length hd')) (tm_step n))) = false).
assert (odd (length (firstn (Nat.div2 (length a'))
(skipn (Nat.div2 (length hd')) (tm_step n)))) = true).
rewrite firstn_length_le. rewrite L3.
apply Nat.OddT_odd. apply Nat.Odd_OddT. assumption.
rewrite skipn_length.
rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd')).
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
rewrite Nat.sub_diag. rewrite Nat.add_0_l.
rewrite Nat.mul_le_mono_pos_l with (p := 2).
rewrite tm_size_power2. rewrite Nat.mul_add_distr_l.
rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double. rewrite <- Nat.Even_double.
rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite L0.
rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1.
apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl.
reflexivity.
apply le_0_n.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
assumption.
generalize H2. generalize L1. apply tm_step_odd_prefix_square.
rewrite firstn_length_le in H2.
apply Nat.Even_EvenT in H0. apply Nat.EvenT_even in H0.
rewrite H0 in H2. inversion H2. assumption.
+ assert (Nat.div2 (length hd'') <= length (tm_step n)).
rewrite Nat.mul_le_mono_pos_l with (p := 2).
rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
rewrite tm_size_power2. rewrite <- Nat.pow_succ_r'.
rewrite <- tm_size_power2. rewrite M0.
rewrite app_length. rewrite <- Nat.add_0_r at 1.
apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity.
apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT.
assumption. apply Nat.lt_0_2.
assert (even (length (firstn (Nat.div2 (length hd'')) (tm_step n))) = false).
assert (odd (length (firstn (Nat.div2 (length a''))
(skipn (Nat.div2 (length hd'')) (tm_step n)))) = true).
rewrite firstn_length_le. rewrite M3.
apply Nat.OddT_odd. apply Nat.Odd_OddT. assumption.
rewrite skipn_length.
rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd'')).
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
rewrite Nat.sub_diag. rewrite Nat.add_0_l.
rewrite Nat.mul_le_mono_pos_l with (p := 2).
rewrite tm_size_power2. rewrite Nat.mul_add_distr_l.
rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double. rewrite <- Nat.Even_double.
rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite M0.
rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1.
apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl.
reflexivity.
apply le_0_n.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
assumption.
generalize H2. generalize M1. apply tm_step_odd_prefix_square.
rewrite firstn_length_le in H2.
apply eq_S in M2. rewrite Nat.succ_pred_pos in M2.
apply eq_S in M2. rewrite <- L2 in M2. rewrite <- M2 in H0.
rewrite <- Nat.Odd_div2 in H0. rewrite <- Nat.Even_div2 in H0.
apply Nat.Even_succ in H0. rewrite Nat.Even_succ_succ in H0.
apply Nat.Even_EvenT in H0. apply Nat.EvenT_even in H0.
rewrite H0 in H2. inversion H2.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.OddT_Odd. apply Nat.odd_OddT. rewrite Nat.odd_succ.
assumption.
destruct (length hd). inversion J. apply Nat.lt_0_succ.
assumption.
Qed.
Lemma tm_step_square_pos_even''' : forall (n : nat),
(exists (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl /\ 0 < length a
/\ odd (length hd) = true /\ even (length a) = true)
-> (exists (hd' a' tl' : list bool),
tm_step 0 = hd' ++ a' ++ a' ++ tl' /\ 0 < length a'
/\ odd (length hd') = true /\ even (length a') = true).
Proof.
intro n. intro.
induction n.
- destruct H. destruct H. destruct H.
exists x. exists x0. exists x1. assumption.
- assert (exists hd' a' tl' : list bool,
tm_step (Nat.pred (S n)) = hd' ++ a' ++ a' ++ tl' /\
0 < length a' /\
odd (length hd') = true /\ even (length a') = true).
destruct H. destruct H. destruct H.
destruct H. destruct H0. destruct H1.
generalize H2. generalize H1. generalize H0. generalize H.
apply tm_step_square_pos_even''. rewrite <- pred_Sn in H0.
apply IHn in H0. assumption.
Qed.
Theorem tm_step_square_pos : forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> 0 < length a -> even (length (hd ++ a)) = true.
Proof.
intros n hd a tl. intros H I.
assert (J: Nat.even (length a) || Nat.odd (length a) = true).
apply Nat.orb_even_odd. apply orb_prop in J.
assert (K: Nat.even (length hd) || Nat.odd (length hd) = true).
apply Nat.orb_even_odd. apply orb_prop in K.
destruct J; destruct K.
- rewrite app_length. rewrite Nat.even_add. rewrite H0. rewrite H1.
reflexivity.
- assert (exists (hd' a' tl' : list bool),
tm_step 0 = hd' ++ a' ++ a' ++ tl' /\ 0 < length a'
/\ odd (length hd') = true /\ even (length a') = true).
assert (exists (hd' a' tl' : list bool),
tm_step n = hd' ++ a' ++ a' ++ tl' /\ 0 < length a'
/\ odd (length hd') = true /\ even (length a') = true).
exists hd. exists a. exists tl. split. assumption.
split. assumption. split. assumption. assumption.
generalize H2. apply tm_step_square_pos_even'''.
destruct H2. destruct H2. destruct H2.
destruct H2. destruct H3. destruct H4.
assert (0 < 0). generalize H5. generalize H3. generalize H2.
apply tm_step_not_nil_factor_even. inversion H6.
- assert (even (length hd) = false).
generalize H0. generalize H. apply tm_step_odd_prefix_square.
rewrite H1 in H2. inversion H2.
- rewrite app_length. rewrite Nat.even_add.
rewrite <- Nat.negb_odd. rewrite <- Nat.negb_odd.
rewrite H0. rewrite H1. reflexivity.
Qed.
Reference in New Issue View Git Blame Copy Permalink