2023-01-15 10:12:10 -05:00
|
|
|
(** * The Thue-Morse sequence (part 2)
|
|
|
|
|
|
|
|
The following lemmas and theorems are all related to
|
2023-01-15 10:14:48 -05:00
|
|
|
squares and cubes in the Thue-Morse sequence.
|
2023-01-15 10:12:10 -05:00
|
|
|
|
|
|
|
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:
|
|
|
|
|
2023-01-15 10:14:48 -05:00
|
|
|
- tm_step_cubefree (there is no cube in the sequence)
|
2023-01-31 16:03:20 -05:00
|
|
|
- tm_step_square_size (about length of squared factors)
|
2023-01-15 11:55:37 -05:00
|
|
|
- tm_step_square_pos (length of the prefix has the same
|
|
|
|
parity than the length of the factor being squared)
|
2023-01-31 16:03:20 -05:00
|
|
|
- tm_step_square_prefix_not_nil (no square at the beginning
|
|
|
|
of the sequence)
|
2023-02-02 04:22:38 -05:00
|
|
|
- tm_step_square_tail_not_nil (no square at the end
|
|
|
|
of the partial sequence)
|
2023-01-15 10:12:10 -05:00
|
|
|
*)
|
|
|
|
|
2023-01-07 05:27:20 -05:00
|
|
|
Require Import thue_morse.
|
|
|
|
|
|
|
|
Require Import Coq.Lists.List.
|
|
|
|
Require Import PeanoNat.
|
|
|
|
Require Import Nat.
|
|
|
|
Require Import Bool.
|
|
|
|
|
|
|
|
Import ListNotations.
|
|
|
|
|
|
|
|
|
2023-01-11 03:19:23 -05:00
|
|
|
(**
|
2023-01-15 10:12:10 -05:00
|
|
|
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.
|
2023-01-11 03:19:23 -05:00
|
|
|
*)
|
|
|
|
|
2023-01-15 10:12:10 -05:00
|
|
|
Lemma tm_step_odd_square : forall (n : nat) (hd a tl : list bool),
|
2023-01-11 03:03:32 -05:00
|
|
|
tm_step n = hd ++ a ++ a ++ tl -> odd (length a) = true -> length a < 4.
|
2023-01-10 12:04:42 -05:00
|
|
|
Proof.
|
|
|
|
intros n hd a tl. intros H I.
|
2023-01-11 03:03:32 -05:00
|
|
|
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).
|
2023-01-13 16:36:11 -05:00
|
|
|
generalize H0. generalize H. apply tm_step_consecutive_identical_length.
|
2023-01-11 03:03:32 -05:00
|
|
|
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.
|
2023-01-13 17:24:40 -05:00
|
|
|
apply tm_step_consecutive_identical' in H.
|
2023-01-11 03:03:32 -05:00
|
|
|
|
|
|
|
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.
|
2023-01-10 12:04:42 -05:00
|
|
|
|
2023-01-11 03:03:32 -05:00
|
|
|
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.
|
2023-01-07 05:27:20 -05:00
|
|
|
|
2023-01-11 03:03:32 -05:00
|
|
|
apply Nat.le_lteq in H0. destruct H0. assumption.
|
|
|
|
rewrite H0 in I. inversion I.
|
|
|
|
Qed.
|
2023-01-07 05:27:20 -05:00
|
|
|
|
|
|
|
|
2023-01-11 03:19:23 -05:00
|
|
|
(**
|
2023-01-11 08:50:03 -05:00
|
|
|
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.
|
2023-01-11 03:19:23 -05:00
|
|
|
*)
|
2023-01-07 05:27:20 -05:00
|
|
|
|
2023-01-11 05:34:08 -05:00
|
|
|
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.
|
|
|
|
|
2023-01-11 07:54:07 -05:00
|
|
|
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.
|
2023-01-07 05:27:20 -05:00
|
|
|
|
|
|
|
|
2023-01-11 07:54:07 -05:00
|
|
|
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.
|
2023-01-10 12:04:42 -05:00
|
|
|
|
2023-01-11 07:54:07 -05:00
|
|
|
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.
|
2023-02-08 11:32:34 -05:00
|
|
|
apply Nat.le_0_l. apply le_n. easy.
|
2023-01-11 07:54:07 -05:00
|
|
|
|
|
|
|
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.
|
2023-01-10 12:04:42 -05:00
|
|
|
|
|
|
|
|
2023-01-11 08:50:03 -05:00
|
|
|
Theorem tm_step_square_size : forall (n k j : nat) (hd a tl : list bool),
|
2023-01-11 08:43:04 -05:00
|
|
|
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.
|
2023-01-11 10:55:50 -05:00
|
|
|
|
2023-01-12 12:18:17 -05:00
|
|
|
(**
|
|
|
|
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.
|
2023-01-14 14:04:32 -05:00
|
|
|
assert (length a < 4). generalize I. generalize H. apply tm_step_odd_square.
|
|
|
|
destruct a. inversion I. destruct a.
|
2023-01-14 15:37:37 -05:00
|
|
|
- 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.
|
2023-01-12 12:18:17 -05:00
|
|
|
Qed.
|
2023-01-15 01:05:26 -05:00
|
|
|
|
|
|
|
|
2023-01-15 05:39:53 -05:00
|
|
|
Lemma tm_step_square_pos_even : forall (n : nat) (hd a tl : list bool),
|
2023-01-15 02:29:10 -05:00
|
|
|
tm_step n = hd ++ a ++ a ++ tl
|
2023-01-15 01:05:26 -05:00
|
|
|
-> 0 < length a
|
|
|
|
-> odd (length hd) = true
|
|
|
|
-> even (length a) = true
|
2023-01-15 02:29:10 -05:00
|
|
|
-> exists (hd' a' tl' : list bool),
|
|
|
|
tm_step n = hd' ++ a' ++ a' ++ tl'
|
|
|
|
/\ length hd' = S (length hd)
|
|
|
|
/\ length a' = length a.
|
2023-01-15 01:05:26 -05:00
|
|
|
Proof.
|
|
|
|
intros n hd a tl. intros H I J K.
|
|
|
|
|
2023-01-15 02:29:10 -05:00
|
|
|
(* 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.
|
2023-01-15 01:05:26 -05:00
|
|
|
|
|
|
|
|
2023-01-15 05:39:53 -05:00
|
|
|
Lemma tm_step_square_pos_even' : forall (n : nat) (hd a tl : list bool),
|
2023-01-15 02:29:10 -05:00
|
|
|
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.
|
2023-01-15 01:05:26 -05:00
|
|
|
|
2023-01-15 02:29:10 -05:00
|
|
|
assert (L: hd = removelast hd ++ last hd false :: nil).
|
|
|
|
apply app_removelast_last. destruct hd. inversion J. easy.
|
|
|
|
rewrite L in H.
|
2023-01-15 01:05:26 -05:00
|
|
|
|
2023-01-15 02:29:10 -05:00
|
|
|
assert (M: a = removelast a ++ last a false :: nil).
|
|
|
|
apply app_removelast_last. destruct a. inversion I. easy.
|
|
|
|
rewrite M in H.
|
2023-01-15 01:05:26 -05:00
|
|
|
|
2023-01-15 02:29:10 -05:00
|
|
|
rewrite <- app_assoc in H. rewrite <- app_assoc in H.
|
|
|
|
rewrite <- app_assoc in H.
|
2023-01-12 12:18:17 -05:00
|
|
|
|
2023-01-15 02:29:10 -05:00
|
|
|
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.
|
2023-01-12 12:18:17 -05:00
|
|
|
|
2023-01-15 02:29:10 -05:00
|
|
|
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.
|
2023-01-11 10:55:50 -05:00
|
|
|
|
2023-01-15 02:29:10 -05:00
|
|
|
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.
|
2023-01-11 10:55:50 -05:00
|
|
|
|
|
|
|
|
2023-01-15 05:39:53 -05:00
|
|
|
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),
|
2023-01-15 10:24:02 -05:00
|
|
|
tm_step (Nat.pred n) = hd' ++ a' ++ a' ++ tl'
|
2023-01-15 11:40:57 -05:00
|
|
|
/\ 0 < length a'
|
2023-01-15 05:39:53 -05:00
|
|
|
/\ odd (length hd') = true
|
2023-01-15 11:40:57 -05:00
|
|
|
/\ even (length a') = true.
|
2023-01-15 05:39:53 -05:00
|
|
|
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].
|
2023-01-15 09:23:55 -05:00
|
|
|
assert (L0 := L1). assert (M0 := M1).
|
2023-01-15 05:39:53 -05:00
|
|
|
|
|
|
|
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.
|
|
|
|
|
2023-01-15 09:23:55 -05:00
|
|
|
(* 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'')))
|
2023-01-15 10:24:02 -05:00
|
|
|
(skipn (Nat.div2 (length hd'')) (tm_step n))).
|
|
|
|
split. rewrite <- pred_Sn. rewrite M1 at 1. reflexivity.
|
2023-01-15 09:23:55 -05:00
|
|
|
|
|
|
|
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.
|
2023-02-08 11:32:34 -05:00
|
|
|
apply Nat.le_0_l. apply Nat.EvenT_Even. apply Nat.even_EvenT.
|
2023-01-15 09:23:55 -05:00
|
|
|
assumption. apply Nat.lt_0_2.
|
|
|
|
|
|
|
|
split.
|
|
|
|
|
2023-01-15 11:40:57 -05:00
|
|
|
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.
|
2023-02-08 11:32:34 -05:00
|
|
|
apply Nat.le_0_l.
|
2023-01-15 11:40:57 -05:00
|
|
|
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.
|
2023-01-15 09:23:55 -05:00
|
|
|
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.
|
|
|
|
|
2023-01-15 11:40:57 -05:00
|
|
|
rewrite firstn_length_le.
|
2023-01-15 09:23:55 -05:00
|
|
|
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.
|
2023-02-08 11:32:34 -05:00
|
|
|
apply Nat.le_0_l.
|
2023-01-15 09:23:55 -05:00
|
|
|
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')))
|
2023-01-15 10:24:02 -05:00
|
|
|
(skipn (Nat.div2 (length hd')) (tm_step n))).
|
|
|
|
split. rewrite <- pred_Sn. rewrite L1 at 1. reflexivity.
|
2023-01-15 09:23:55 -05:00
|
|
|
|
|
|
|
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.
|
2023-02-08 11:32:34 -05:00
|
|
|
apply Nat.le_0_l. apply Nat.EvenT_Even. apply Nat.even_EvenT.
|
2023-01-15 09:23:55 -05:00
|
|
|
assumption. apply Nat.lt_0_2.
|
|
|
|
|
|
|
|
split.
|
|
|
|
|
2023-01-15 11:40:57 -05:00
|
|
|
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.
|
2023-02-08 11:32:34 -05:00
|
|
|
apply Nat.le_0_l.
|
2023-01-15 11:40:57 -05:00
|
|
|
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.
|
|
|
|
|
2023-01-15 09:23:55 -05:00
|
|
|
rewrite firstn_length_le.
|
|
|
|
apply Nat.OddT_odd. apply Nat.Odd_OddT. assumption.
|
|
|
|
assumption.
|
|
|
|
|
2023-01-15 11:40:57 -05:00
|
|
|
rewrite firstn_length_le.
|
2023-01-15 09:23:55 -05:00
|
|
|
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.
|
2023-02-08 11:32:34 -05:00
|
|
|
apply Nat.le_0_l.
|
2023-01-15 09:23:55 -05:00
|
|
|
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.
|
2023-02-08 11:32:34 -05:00
|
|
|
apply Nat.le_0_l. apply Nat.EvenT_Even. apply Nat.even_EvenT.
|
2023-01-15 09:23:55 -05:00
|
|
|
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.
|
2023-02-08 11:32:34 -05:00
|
|
|
apply Nat.le_0_l.
|
2023-01-15 09:23:55 -05:00
|
|
|
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.
|
2023-02-08 11:32:34 -05:00
|
|
|
apply Nat.le_0_l. apply Nat.EvenT_Even. apply Nat.even_EvenT.
|
2023-01-15 09:23:55 -05:00
|
|
|
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.
|
2023-02-08 11:32:34 -05:00
|
|
|
apply Nat.le_0_l.
|
2023-01-15 09:23:55 -05:00
|
|
|
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.
|
2023-01-15 05:39:53 -05:00
|
|
|
|
2023-01-15 11:40:57 -05:00
|
|
|
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.
|
2023-01-15 09:42:12 -05:00
|
|
|
|
2023-01-15 11:54:43 -05:00
|
|
|
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.
|
2023-01-29 15:16:56 -05:00
|
|
|
|
|
|
|
|
|
|
|
Lemma tm_step_square_prefix_not_nil0 :
|
|
|
|
forall (n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ a ++ tl -> 0 < length a
|
|
|
|
-> hd <> nil
|
|
|
|
\/ exists a' tl', tm_step (pred n) = a' ++ a' ++ tl'
|
|
|
|
/\ 0 < length a'.
|
|
|
|
Proof.
|
|
|
|
intros n hd a tl. intros H I.
|
|
|
|
destruct a. inversion I.
|
|
|
|
|
|
|
|
destruct a.
|
|
|
|
assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
|
|
|
|
destruct W. rewrite e in H.
|
|
|
|
assert (1 < 2^n). rewrite <- tm_size_power2. rewrite H. simpl.
|
|
|
|
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
|
|
|
assert (Z : 0 < 2^n). apply Nat.lt_succ_l. assumption.
|
|
|
|
assert (nth_error (tm_step n) 0 <> nth_error (tm_step (S n)) (S (2*0))).
|
|
|
|
generalize Z. apply tm_step_succ_double_index.
|
|
|
|
rewrite tm_step_stable with (k := S (2*0)) (m := n) in H1. rewrite H in H1.
|
|
|
|
simpl in H1. contradiction H1. reflexivity. rewrite Nat.pow_succ_r.
|
|
|
|
replace (S (2*0)) with (1*1). apply Nat.mul_lt_mono. apply Nat.lt_1_2.
|
2023-02-08 11:32:34 -05:00
|
|
|
assumption. reflexivity. apply Nat.le_0_l. assumption. left. assumption.
|
2023-01-29 15:16:56 -05:00
|
|
|
|
|
|
|
destruct a.
|
|
|
|
assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
|
|
|
|
destruct W. rewrite e in H.
|
|
|
|
assert (2 < 2^n). rewrite <- tm_size_power2. rewrite H. simpl.
|
|
|
|
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
|
|
|
assert (nth_error (tm_step n) 1 = nth_error (tm_step (S n)) (2*1)).
|
|
|
|
apply tm_step_double_index.
|
|
|
|
rewrite tm_step_stable with (k := (2*1)) (m := n) in H1. rewrite H in H1.
|
|
|
|
simpl in H1. inversion H1. rewrite H3 in H.
|
|
|
|
replace ([] ++ [b;b] ++ [b;b] ++ tl)
|
|
|
|
with ([b] ++ [b] ++ [b] ++ [b] ++ tl) in H.
|
|
|
|
apply tm_step_cubefree in H. contradiction H. reflexivity.
|
|
|
|
apply Nat.lt_0_1. reflexivity. rewrite Nat.pow_succ_r.
|
|
|
|
apply Nat.mul_lt_mono_pos_l. apply Nat.lt_0_succ.
|
2023-02-08 11:32:34 -05:00
|
|
|
apply Nat.lt_succ_l. assumption. apply Nat.le_0_l. assumption.
|
2023-01-29 15:16:56 -05:00
|
|
|
left. assumption.
|
|
|
|
|
|
|
|
destruct a.
|
|
|
|
assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
|
|
|
|
destruct W. rewrite e in H.
|
|
|
|
assert (5 < 2^n). rewrite <- tm_size_power2. rewrite H. simpl.
|
|
|
|
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
|
|
|
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
|
|
|
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
|
|
|
assert (nth_error (tm_step n) 2 <> nth_error (tm_step (S n)) (S (2*2))).
|
|
|
|
apply tm_step_succ_double_index.
|
|
|
|
apply Nat.lt_succ_l. apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption.
|
|
|
|
rewrite tm_step_stable with (k := S (2*2)) (m := n) in H1. rewrite H in H1.
|
|
|
|
simpl in H1. contradiction H1. reflexivity. rewrite Nat.pow_succ_r.
|
|
|
|
apply Nat.lt_succ_l. replace (S (S (2*2))) with (2*3).
|
|
|
|
apply Nat.mul_lt_mono_pos_l. apply Nat.lt_0_2.
|
|
|
|
apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption. reflexivity.
|
2023-02-08 11:32:34 -05:00
|
|
|
apply Nat.le_0_l. assumption. left. assumption.
|
2023-01-29 15:16:56 -05:00
|
|
|
|
|
|
|
pose (a' := b::b0::b1::b2::a). fold a' in H.
|
|
|
|
assert (J : 4 <= length a'). unfold a'. simpl.
|
|
|
|
rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono.
|
2023-02-08 11:32:34 -05:00
|
|
|
rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. apply Nat.le_0_l.
|
2023-01-29 15:16:56 -05:00
|
|
|
|
|
|
|
assert (K: {odd (length a') = true} + {~ odd (length a') = true}).
|
|
|
|
apply bool_dec. destruct K.
|
|
|
|
assert (length a' < 4). generalize e. generalize H.
|
|
|
|
apply tm_step_odd_square.
|
|
|
|
apply Nat.le_ngt in J. apply J in H0. contradiction H0.
|
|
|
|
apply not_true_iff_false in n0.
|
|
|
|
assert (K: even (length a') = true).
|
|
|
|
rewrite <- Nat.negb_odd. rewrite n0. reflexivity.
|
|
|
|
|
|
|
|
assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
|
|
|
|
destruct W. rewrite e in H. right.
|
|
|
|
destruct n. inversion H. rewrite app_nil_l in H.
|
|
|
|
|
|
|
|
assert (N: tm_morphism (tm_step n) = tm_morphism
|
|
|
|
(firstn (Nat.div2 (length a')) (tm_step n) ++
|
|
|
|
firstn (Nat.div2 (length a'))
|
|
|
|
(skipn (Nat.div2 (length a')) (tm_step n)) ++
|
|
|
|
skipn (Nat.div2 (length a' + length a')) (tm_step n))).
|
|
|
|
generalize K. generalize K. generalize H. apply tm_step_morphism3.
|
|
|
|
assert (O := N). rewrite tm_step_lemma in N.
|
|
|
|
rewrite tm_morphism_app in N. rewrite tm_morphism_app in N.
|
|
|
|
|
|
|
|
assert (length a' + length a' <= 2 * length (tm_step n)).
|
|
|
|
rewrite tm_size_power2. rewrite <- Nat.pow_succ_r.
|
|
|
|
rewrite <- tm_size_power2. rewrite H. rewrite app_assoc.
|
|
|
|
rewrite app_length. rewrite <- app_length. apply Nat.le_add_r.
|
2023-02-08 11:32:34 -05:00
|
|
|
apply Nat.le_0_l. replace (length a' + length a') with (2 * length a') in H0.
|
2023-01-29 15:16:56 -05:00
|
|
|
rewrite <- Nat.mul_le_mono_pos_l in H0.
|
|
|
|
|
|
|
|
assert (length a' = length
|
|
|
|
(tm_morphism (firstn (Nat.div2 (length a')) (tm_step n)))).
|
|
|
|
rewrite tm_morphism_length. rewrite firstn_length_le.
|
|
|
|
rewrite <- Nat.add_0_r. replace 0 with (Nat.b2n (Nat.odd (length a'))) at 2.
|
|
|
|
rewrite <- Nat.div2_odd. reflexivity. rewrite n0. reflexivity.
|
|
|
|
assert (Nat.div2 (length a') < length a').
|
|
|
|
apply Nat.lt_div2. apply Nat.lt_succ_l in J.
|
|
|
|
apply Nat.lt_succ_l in J. apply Nat.lt_succ_l in J. assumption.
|
|
|
|
|
|
|
|
apply Nat.lt_le_incl. generalize H0. generalize H1.
|
|
|
|
apply Nat.lt_le_trans.
|
|
|
|
|
|
|
|
assert (Nat.div2 (length a') < length a'). apply Nat.lt_div2.
|
|
|
|
apply Nat.lt_succ_l in J. apply Nat.lt_succ_l in J.
|
|
|
|
apply Nat.lt_succ_l in J. assumption.
|
|
|
|
|
|
|
|
assert (length a' = length
|
|
|
|
(tm_morphism (firstn (Nat.div2 (length a'))
|
|
|
|
(skipn (Nat.div2 (length a')) (tm_step n))))).
|
|
|
|
rewrite tm_morphism_length. rewrite firstn_length_le.
|
|
|
|
rewrite <- Nat.add_0_r. replace 0 with (Nat.b2n (Nat.odd (length a'))) at 2.
|
|
|
|
rewrite <- Nat.div2_odd. reflexivity. rewrite n0. reflexivity.
|
|
|
|
rewrite skipn_length.
|
|
|
|
|
|
|
|
rewrite Nat.add_le_mono_r with (p := Nat.div2 (length a')).
|
|
|
|
rewrite Nat.sub_add. rewrite Nat.div2_div at 2. rewrite <- Nat.div_add_l.
|
|
|
|
rewrite Nat.mul_comm.
|
|
|
|
replace (2 * Nat.div2 (length a'))
|
|
|
|
with (2 * Nat.div2 (length a') + Nat.b2n (Nat.odd (length a'))).
|
|
|
|
rewrite <- Nat.div2_odd. replace (length a' + length a') with (2 * length a').
|
|
|
|
replace 2 with (2*1) at 2. rewrite Nat.div_mul_cancel_l.
|
|
|
|
rewrite Nat.div_1_r. assumption. easy. easy. reflexivity.
|
|
|
|
simpl. rewrite Nat.add_0_r. reflexivity. rewrite n0.
|
|
|
|
simpl. rewrite Nat.add_0_r. reflexivity. easy.
|
|
|
|
|
|
|
|
apply Nat.lt_le_incl. generalize H0. generalize H2.
|
|
|
|
apply Nat.lt_le_trans.
|
|
|
|
|
|
|
|
assert (a' = tm_morphism (firstn (Nat.div2 (length a')) (tm_step n))).
|
|
|
|
generalize H1. rewrite H in N. generalize N. apply app_eq_length_head.
|
|
|
|
rewrite <- H4 in N. rewrite H in N. rewrite app_inv_head_iff in N.
|
|
|
|
|
|
|
|
assert (a' =
|
|
|
|
tm_morphism
|
|
|
|
(firstn (Nat.div2 (length a'))
|
|
|
|
(skipn (Nat.div2 (length a')) (tm_step n)))).
|
|
|
|
generalize H3. generalize N. apply app_eq_length_head.
|
|
|
|
|
|
|
|
exists (firstn (Nat.div2 (length a')) (tm_step n)).
|
|
|
|
exists (skipn (Nat.div2 (length a' + length a')) (tm_step n)).
|
|
|
|
split.
|
|
|
|
rewrite tm_morphism_app in O.
|
|
|
|
rewrite tm_morphism_app in O.
|
|
|
|
rewrite <- H5 in O. rewrite H4 in O at 2.
|
|
|
|
rewrite <- tm_morphism_app in O.
|
|
|
|
rewrite <- tm_morphism_app in O.
|
|
|
|
rewrite <- tm_morphism_eq in O. rewrite <- pred_Sn.
|
|
|
|
rewrite O at 1. reflexivity.
|
|
|
|
rewrite firstn_length_le.
|
|
|
|
apply Nat.div_le_mono with (c := 2) in J.
|
|
|
|
rewrite Nat.div2_div. replace (4/2) with 2 in J.
|
|
|
|
apply Nat.lt_succ_l in J. assumption. reflexivity. easy.
|
|
|
|
apply Nat.lt_le_incl. generalize H0. generalize H2.
|
|
|
|
apply Nat.lt_le_trans. apply Nat.lt_0_2.
|
|
|
|
simpl. rewrite Nat.add_0_r. reflexivity.
|
|
|
|
left. assumption.
|
|
|
|
Qed.
|
2023-02-02 02:44:03 -05:00
|
|
|
|
|
|
|
Theorem tm_step_square_prefix_not_nil :
|
|
|
|
forall (n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ a ++ tl -> 0 < length a -> hd <> nil.
|
|
|
|
Proof.
|
|
|
|
intros n hd a tl. intros H I.
|
|
|
|
|
|
|
|
assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
|
|
|
|
destruct W. rewrite e in H. rewrite app_nil_l in H.
|
|
|
|
generalize dependent a.
|
|
|
|
generalize dependent tl.
|
|
|
|
induction n.
|
|
|
|
- intros tl a. intros H I.
|
|
|
|
destruct a. inversion I. inversion H.
|
|
|
|
assert (length (nil : list bool) = length (nil : list bool)).
|
|
|
|
reflexivity. rewrite H2 in H0 at 2. rewrite app_length in H0.
|
|
|
|
rewrite Nat.add_comm in H0. inversion H0.
|
|
|
|
- intros tl a. intros H I.
|
|
|
|
assert (hd <> nil
|
|
|
|
\/ exists a' tl', tm_step (pred (S n)) = a' ++ a' ++ tl' /\ 0 < length a').
|
|
|
|
generalize I. generalize H. replace (a++a++tl) with (hd ++ a ++ a ++ tl).
|
|
|
|
apply tm_step_square_prefix_not_nil0. rewrite e. reflexivity.
|
|
|
|
destruct H0. assumption. destruct H0. destruct H0.
|
|
|
|
rewrite <- pred_Sn in H0.
|
|
|
|
destruct H0.
|
|
|
|
generalize H1. generalize H0. apply IHn.
|
|
|
|
- assumption.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
Theorem tm_step_square_tail_not_nil :
|
|
|
|
forall (n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ a ++ tl -> 0 < length a -> tl <> nil.
|
|
|
|
Proof.
|
|
|
|
intros n hd a tl. intros H I.
|
|
|
|
assert (W: {tl=nil} + {~ tl=nil}). apply list_eq_dec. apply bool_dec.
|
|
|
|
destruct W. rewrite e in H. rewrite app_nil_r in H.
|
|
|
|
|
|
|
|
assert (X: n = 2 * Nat.div2 n + Nat.b2n (Nat.odd n)). apply Nat.div2_odd.
|
|
|
|
rewrite <- Nat.double_twice in X.
|
|
|
|
|
|
|
|
assert (Y: rev (hd ++ a ++ a) = rev (hd ++ a ++ a)). reflexivity.
|
|
|
|
rewrite <- H in Y at 1.
|
|
|
|
rewrite rev_app_distr in Y. rewrite rev_app_distr in Y.
|
|
|
|
rewrite <- app_assoc in Y. rewrite X in Y.
|
|
|
|
|
|
|
|
assert (Z : { odd n = true } + {~ odd n = true}). apply bool_dec.
|
|
|
|
destruct Z. rewrite e0 in Y. rewrite Nat.add_1_r in Y.
|
|
|
|
rewrite tm_step_odd_step in Y.
|
|
|
|
|
|
|
|
assert (map negb (rev a ++ rev a ++ rev hd)
|
|
|
|
= map negb (rev a ++ rev a ++ rev hd)). reflexivity.
|
|
|
|
rewrite <- Y in H0 at 1.
|
|
|
|
|
|
|
|
assert (forall l, map negb (map negb l) = l).
|
|
|
|
intro l. induction l. reflexivity. simpl. rewrite negb_involutive.
|
|
|
|
rewrite IHl. reflexivity. rewrite H1 in H0.
|
|
|
|
|
|
|
|
rewrite map_app in H0. rewrite map_app in H0.
|
|
|
|
rewrite <- app_nil_l in H0.
|
|
|
|
assert ((nil : list bool) <> nil).
|
|
|
|
assert (0 < length (map negb (rev a))). rewrite map_length.
|
|
|
|
rewrite rev_length. assumption. generalize H2. generalize H0.
|
|
|
|
apply tm_step_square_prefix_not_nil. contradiction H2.
|
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
apply not_true_is_false in n0. rewrite n0 in Y.
|
|
|
|
rewrite Nat.add_0_r in Y. rewrite tm_step_even_step in Y.
|
|
|
|
rewrite <- app_nil_l in Y.
|
|
|
|
assert ((nil : list bool) <> nil).
|
|
|
|
assert (0 < length (rev a)). rewrite rev_length. assumption.
|
|
|
|
generalize H0. generalize Y.
|
|
|
|
apply tm_step_square_prefix_not_nil. contradiction H0.
|
|
|
|
reflexivity. assumption.
|
|
|
|
Qed.
|