This commit is contained in:
Thomas Baruchel 2023-01-26 15:28:49 +01:00
parent b8b836fb53
commit 5b0894346a
2 changed files with 268 additions and 170 deletions

View File

@ -1237,3 +1237,169 @@ Proof.
apply app_inv_head_iff. apply app_inv_head_iff.
rewrite app_assoc. rewrite firstn_skipn. reflexivity. rewrite app_assoc. rewrite firstn_skipn. reflexivity.
Qed. Qed.
(**
Some more lemmas are added there as convenient tools for further
investigations; they have been added quite late, after many
following results were proved, but they are inserted here in
case some proofs are re-written later.
*)
Lemma tm_step_morphism2 :
forall (n : nat) (hd tl : list bool),
tm_step (S n) = hd ++ tl
-> even (length hd) = true
-> tm_step (S n) = tm_morphism
(firstn (Nat.div2 (length hd)) (tm_step n) ++
skipn (Nat.div2 (length hd)) (tm_step n)).
Proof.
intros n hd tl. intros H I.
assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
generalize I. generalize H. apply tm_morphism_app2.
assert (tl = tm_morphism (skipn (Nat.div2 (length hd)) (tm_step n))).
generalize I. generalize H. apply tm_morphism_app3.
rewrite H0 in H. rewrite H1 in H. rewrite <- tm_morphism_app in H.
assumption.
Qed.
Lemma tm_step_morphism3 :
forall (n : nat) (hd a tl : list bool),
tm_step (S n) = hd ++ a ++ tl
-> even (length hd) = true
-> even (length a) = true
-> tm_morphism (tm_step n) = tm_morphism
(firstn (Nat.div2 (length hd)) (tm_step n) ++
firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length hd)) (tm_step n)) ++
skipn (Nat.div2 (length hd + length a)) (tm_step n)).
Proof.
intros n hd a tl. intros H I J. rewrite <- tm_step_lemma in H.
assert (even (length (hd ++ a)) = true). rewrite app_length.
rewrite Nat.even_add. rewrite I. rewrite J. reflexivity.
rewrite app_assoc in H.
assert (hd ++ a = tm_morphism (firstn (Nat.div2 (length (hd ++ a)))
(tm_step n))).
generalize H0. generalize H. apply tm_morphism_app2.
assert (tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a)))
(tm_step n))).
generalize H0. generalize H. apply tm_morphism_app3.
rewrite <- app_assoc in H.
assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
generalize I. generalize H. apply tm_morphism_app2.
assert (a = tm_morphism (skipn (Nat.div2 (length hd))
(firstn (Nat.div2 (length (hd ++ a))) (tm_step n)))).
generalize I. symmetry in H1. generalize H1. apply tm_morphism_app3.
rewrite skipn_firstn_comm in H4.
rewrite H3 in H. rewrite H4 in H. rewrite H2 in H.
rewrite app_length in H.
rewrite <- tm_morphism_app in H.
rewrite <- tm_morphism_app in H.
replace (Nat.div2 (length hd + length a))
with ((length hd) / 2 + Nat.div2 (length a)) in H.
rewrite <- Nat.div2_div in H. rewrite Nat.add_sub_swap in H.
rewrite Nat.sub_diag in H. rewrite Nat.add_0_l in H.
rewrite Nat.div2_div in H at 3. rewrite <- Nat.div_add in H.
rewrite Nat.mul_comm in H.
replace (2 * Nat.div2 (length a))
with (2 * Nat.div2 (length a) + Nat.b2n (Nat.odd (length a))) in H.
rewrite <- Nat.div2_odd in H. rewrite <- Nat.div2_div in H.
assumption.
rewrite <- Nat.negb_even. rewrite J.
rewrite <- Nat.add_0_r. reflexivity. easy.
apply Nat.le_refl.
replace (length a) with (Nat.div2 (length a) * 2) at 2.
rewrite <- Nat.div_add. rewrite <- Nat.div2_div. reflexivity.
easy. 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. reflexivity.
rewrite <- Nat.negb_even. rewrite J.
rewrite <- Nat.add_0_r. reflexivity.
Qed.
Lemma tm_step_morphism4 :
forall (n : nat) (hd a b tl : list bool),
tm_step (S n) = hd ++ a ++ b ++ tl
-> even (length hd) = true
-> even (length a) = true
-> even (length b) = true
-> tm_step (S n) = tm_morphism
(firstn (Nat.div2 (length hd)) (tm_step n) ++
firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length hd)) (tm_step n)) ++
firstn (Nat.div2 (length b))
(skipn (Nat.div2 (length (hd ++ a))) (tm_step n)) ++
skipn (Nat.div2 (length (hd ++ a ++ b))) (tm_step n)).
Proof.
intros n hd a b tl. intros H I J K.
assert (even (length (hd ++ a)) = true).
rewrite app_length. rewrite Nat.even_add.
rewrite I. rewrite J. reflexivity.
rewrite app_assoc in H. rewrite <- tm_step_lemma in H.
assert (hd ++ a = tm_morphism (firstn (Nat.div2 (length (hd ++ a)))
(tm_step n))).
generalize H0. generalize H. apply tm_morphism_app2.
assert (b ++ tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a)))
(tm_step n))).
generalize H0. generalize H. apply tm_morphism_app3.
rewrite <- app_assoc in H. symmetry in H1. symmetry in H2.
assert (even (length (hd ++ a ++ b)) = true).
rewrite app_length. rewrite Nat.even_add. rewrite I.
rewrite app_length. rewrite Nat.even_add. rewrite J. rewrite K.
reflexivity.
assert (tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a ++ b)))
(tm_step n))).
replace (hd ++ a ++ b ++ tl) with ((hd ++ a ++ b) ++ tl) in H.
generalize H3. generalize H. apply tm_morphism_app3.
rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
generalize I. generalize H. apply tm_morphism_app2.
assert (a = tm_morphism (skipn (Nat.div2 (length hd))
(firstn (Nat.div2 (length (hd ++ a))) (tm_step n)))).
generalize I. generalize H1. apply tm_morphism_app3.
assert (b = tm_morphism (firstn (Nat.div2 (length b))
(skipn (Nat.div2 (length (hd ++ a))) (tm_step n)))).
generalize K. generalize H2. apply tm_morphism_app2.
rewrite skipn_firstn_comm in H6. rewrite app_length in H6.
replace (Nat.div2 (length hd + length a))
with ((length hd) / 2 + Nat.div2 (length a)) in H6.
rewrite <- Nat.div2_div in H6. rewrite Nat.add_sub_swap in H6.
rewrite Nat.sub_diag in H6. rewrite Nat.add_0_l in H6.
rewrite H5 in H. rewrite H6 in H. rewrite H7 in H. rewrite H4 in H.
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
rewrite <- tm_morphism_app in H. rewrite tm_step_lemma in H.
assumption.
apply Nat.le_refl.
rewrite <- Nat.div_add. rewrite <- Nat.div2_div.
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. reflexivity.
rewrite <- Nat.negb_even. rewrite J.
rewrite <- Nat.add_0_r. reflexivity.
easy.
Qed.

View File

@ -1377,173 +1377,6 @@ Qed.
Lemma tm_step_morphism2 :
forall (n : nat) (hd tl : list bool),
tm_step (S n) = hd ++ tl
-> even (length hd) = true
-> tm_step (S n) = tm_morphism
(firstn (Nat.div2 (length hd)) (tm_step n) ++
skipn (Nat.div2 (length hd)) (tm_step n)).
Proof.
intros n hd tl. intros H I.
assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
generalize I. generalize H. apply tm_morphism_app2.
assert (tl = tm_morphism (skipn (Nat.div2 (length hd)) (tm_step n))).
generalize I. generalize H. apply tm_morphism_app3.
rewrite H0 in H. rewrite H1 in H. rewrite <- tm_morphism_app in H.
assumption.
Qed.
Lemma tm_step_morphism3 :
forall (n : nat) (hd a tl : list bool),
tm_step (S n) = hd ++ a ++ tl
-> even (length hd) = true
-> even (length a) = true
-> tm_morphism (tm_step n) = tm_morphism
(firstn (Nat.div2 (length hd)) (tm_step n) ++
firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length hd)) (tm_step n)) ++
skipn (Nat.div2 (length hd + length a)) (tm_step n)).
Proof.
intros n hd a tl. intros H I J. rewrite <- tm_step_lemma in H.
assert (even (length (hd ++ a)) = true). rewrite app_length.
rewrite Nat.even_add. rewrite I. rewrite J. reflexivity.
rewrite app_assoc in H.
assert (hd ++ a = tm_morphism (firstn (Nat.div2 (length (hd ++ a)))
(tm_step n))).
generalize H0. generalize H. apply tm_morphism_app2.
assert (tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a)))
(tm_step n))).
generalize H0. generalize H. apply tm_morphism_app3.
rewrite <- app_assoc in H.
assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
generalize I. generalize H. apply tm_morphism_app2.
assert (a = tm_morphism (skipn (Nat.div2 (length hd))
(firstn (Nat.div2 (length (hd ++ a))) (tm_step n)))).
generalize I. symmetry in H1. generalize H1. apply tm_morphism_app3.
rewrite skipn_firstn_comm in H4.
rewrite H3 in H. rewrite H4 in H. rewrite H2 in H.
rewrite app_length in H.
rewrite <- tm_morphism_app in H.
rewrite <- tm_morphism_app in H.
replace (Nat.div2 (length hd + length a))
with ((length hd) / 2 + Nat.div2 (length a)) in H.
rewrite <- Nat.div2_div in H. rewrite Nat.add_sub_swap in H.
rewrite Nat.sub_diag in H. rewrite Nat.add_0_l in H.
rewrite Nat.div2_div in H at 3. rewrite <- Nat.div_add in H.
rewrite Nat.mul_comm in H.
replace (2 * Nat.div2 (length a))
with (2 * Nat.div2 (length a) + Nat.b2n (Nat.odd (length a))) in H.
rewrite <- Nat.div2_odd in H. rewrite <- Nat.div2_div in H.
assumption.
rewrite <- Nat.negb_even. rewrite J.
rewrite <- Nat.add_0_r. reflexivity. easy.
apply Nat.le_refl.
replace (length a) with (Nat.div2 (length a) * 2) at 2.
rewrite <- Nat.div_add. rewrite <- Nat.div2_div. reflexivity.
easy. 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. reflexivity.
rewrite <- Nat.negb_even. rewrite J.
rewrite <- Nat.add_0_r. reflexivity.
Qed.
Lemma tm_step_morphism4 :
forall (n : nat) (hd a b tl : list bool),
tm_step (S n) = hd ++ a ++ b ++ tl
-> even (length hd) = true
-> even (length a) = true
-> even (length b) = true
-> tm_step (S n) = tm_morphism
(firstn (Nat.div2 (length hd)) (tm_step n) ++
firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length hd)) (tm_step n)) ++
firstn (Nat.div2 (length b))
(skipn (Nat.div2 (length (hd ++ a))) (tm_step n)) ++
skipn (Nat.div2 (length (hd ++ a ++ b))) (tm_step n)).
Proof.
intros n hd a b tl. intros H I J K.
assert (even (length (hd ++ a)) = true).
rewrite app_length. rewrite Nat.even_add.
rewrite I. rewrite J. reflexivity.
rewrite app_assoc in H. rewrite <- tm_step_lemma in H.
assert (hd ++ a = tm_morphism (firstn (Nat.div2 (length (hd ++ a)))
(tm_step n))).
generalize H0. generalize H. apply tm_morphism_app2.
assert (b ++ tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a)))
(tm_step n))).
generalize H0. generalize H. apply tm_morphism_app3.
rewrite <- app_assoc in H. symmetry in H1. symmetry in H2.
assert (even (length (hd ++ a ++ b)) = true).
rewrite app_length. rewrite Nat.even_add. rewrite I.
rewrite app_length. rewrite Nat.even_add. rewrite J. rewrite K.
reflexivity.
assert (tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a ++ b)))
(tm_step n))).
replace (hd ++ a ++ b ++ tl) with ((hd ++ a ++ b) ++ tl) in H.
generalize H3. generalize H. apply tm_morphism_app3.
rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
generalize I. generalize H. apply tm_morphism_app2.
assert (a = tm_morphism (skipn (Nat.div2 (length hd))
(firstn (Nat.div2 (length (hd ++ a))) (tm_step n)))).
generalize I. generalize H1. apply tm_morphism_app3.
assert (b = tm_morphism (firstn (Nat.div2 (length b))
(skipn (Nat.div2 (length (hd ++ a))) (tm_step n)))).
generalize K. generalize H2. apply tm_morphism_app2.
rewrite skipn_firstn_comm in H6. rewrite app_length in H6.
replace (Nat.div2 (length hd + length a))
with ((length hd) / 2 + Nat.div2 (length a)) in H6.
rewrite <- Nat.div2_div in H6. rewrite Nat.add_sub_swap in H6.
rewrite Nat.sub_diag in H6. rewrite Nat.add_0_l in H6.
rewrite H5 in H. rewrite H6 in H. rewrite H7 in H. rewrite H4 in H.
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
rewrite <- tm_morphism_app in H. rewrite tm_step_lemma in H.
assumption.
apply Nat.le_refl.
rewrite <- Nat.div_add. rewrite <- Nat.div2_div.
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. reflexivity.
rewrite <- Nat.negb_even. rewrite J.
rewrite <- Nat.add_0_r. reflexivity.
easy.
Qed.
Lemma tm_step_palindromic_even_morphism1 : Lemma tm_step_palindromic_even_morphism1 :
forall (n : nat) (hd a tl : list bool), forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ (rev a) ++ tl tm_step n = hd ++ a ++ (rev a) ++ tl
@ -1558,9 +1391,11 @@ Lemma tm_step_palindromic_even_morphism1 :
(rev (rev
(firstn (Nat.div2 (length a)) (firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length hd)) (tm_step (pred n))))) ++ (skipn (Nat.div2 (length hd)) (tm_step (pred n))))) ++
skipn (length a + Nat.div2 (length hd)) (tm_step (pred n))). skipn (Nat.div2 (length hd) + length a) (tm_step (pred n))).
Proof. Proof.
intros n hd a tl. intros H I J. intros n hd a tl. intros H Z J.
(* proof that n <> 0 *)
destruct n. assert (length (tm_step 0) <= length (tm_step 0)). destruct n. assert (length (tm_step 0) <= length (tm_step 0)).
apply Nat.le_refl. apply Nat.le_refl.
rewrite H in H0 at 1. rewrite app_length in H0. rewrite app_length in H0. rewrite H in H0 at 1. rewrite app_length in H0. rewrite app_length in H0.
@ -1570,7 +1405,104 @@ Proof.
assert (K: 1 <= length a + (length tl + length hd)). assert (K: 1 <= length a + (length tl + length hd)).
rewrite Nat.le_succ_l. apply Nat.lt_lt_add_r. assumption. rewrite Nat.le_succ_l. apply Nat.lt_lt_add_r. assumption.
rewrite <- Nat.sub_0_le in K. rewrite K in H0. apply Nat.le_0_r in H0. rewrite <- Nat.sub_0_le in K. rewrite K in H0. apply Nat.le_0_r in H0.
rewrite H0 in I. inversion I. rewrite H0 in Z. inversion Z.
assert (even (length (hd ++ a)) = true). generalize Z. generalize H.
apply tm_step_palindromic_even_center.
assert (I: even (length hd) = true). rewrite app_length in H0.
rewrite Nat.even_add in H0. rewrite J in H0.
destruct (even (length hd)). reflexivity. inversion H0.
assert (K: even (length (rev a)) = true). rewrite rev_length. assumption.
rewrite app_assoc in H. rewrite <- tm_step_lemma in H.
assert (hd ++ a = tm_morphism (firstn (Nat.div2 (length (hd ++ a)))
(tm_step n))).
generalize H0. generalize H. apply tm_morphism_app2.
rewrite <- app_assoc in H. symmetry in H1.
assert (even (length (hd ++ a ++ (rev a))) = true).
rewrite app_length. rewrite Nat.even_add. rewrite I.
rewrite app_length. rewrite Nat.even_add. rewrite J. rewrite K.
reflexivity.
assert (tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a ++ (rev a))))
(tm_step n))).
replace (hd ++ a ++ (rev a) ++ tl) with ((hd ++ a ++ (rev a)) ++ tl) in H.
generalize H2. generalize H. apply tm_morphism_app3.
rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
generalize I. generalize H. apply tm_morphism_app2.
assert (a = tm_morphism (skipn (Nat.div2 (length hd))
(firstn (Nat.div2 (length (hd ++ a))) (tm_step n)))).
generalize I. generalize H1. apply tm_morphism_app3.
rewrite skipn_firstn_comm in H5. rewrite app_length in H5.
replace (Nat.div2 (length hd + length a))
with ((length hd) / 2 + Nat.div2 (length a)) in H5.
rewrite <- Nat.div2_div in H5. rewrite Nat.add_sub_swap in H5.
rewrite Nat.sub_diag in H5. rewrite Nat.add_0_l in H5.
rewrite H4 in H. rewrite H5 in H. rewrite H3 in H.
rewrite tm_morphism_rev in H.
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
rewrite <- tm_morphism_app in H. rewrite tm_step_lemma in H.
rewrite app_length in H. rewrite app_length in H. rewrite rev_length in H.
replace (length a + length a) with ((length a)*2) in H.
replace (Nat.div2 (length hd + length a * 2))
with ((length hd + length a * 2) / 2) in H.
rewrite Nat.div_add in H. rewrite <- Nat.div2_div in H.
assumption. easy.
rewrite Nat.div2_div. reflexivity. rewrite Nat.mul_comm. simpl.
rewrite Nat.add_0_r. reflexivity.
apply Nat.le_refl.
rewrite <- Nat.div_add. rewrite <- Nat.div2_div.
rewrite Nat.mul_comm.
rewrite Nat.div2_odd with (a := length a) at 2.
rewrite <- Nat.negb_even. rewrite J. simpl.
rewrite Nat.add_0_r. rewrite Nat.add_0_r. reflexivity. easy.
Qed.
assert (tm_step (S n) = tm_morphism
(firstn (Nat.div2 (length hd)) (tm_step n) ++
firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length hd)) (tm_step n)) ++
firstn (Nat.div2 (length (rev a)))
(skipn (Nat.div2 (length (hd ++ a))) (tm_step n)) ++
skipn (Nat.div2 (length (hd ++ a ++ (rev a)))) (tm_step n))).
assert (K : even (length (rev a)) = true).
rewrite rev_length. assumption.
generalize K. generalize J. generalize H1. generalize H.
apply tm_step_morphism4. rewrite rev_length in H2.
rewrite <- pred_Sn.
assert (even (length (hd ++ a)) = true). generalize I. generalize H. assert (even (length (hd ++ a)) = true). generalize I. generalize H.
apply tm_step_palindromic_even_center. apply tm_step_palindromic_even_center.