baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2023-01-26 14:48:30 +01:00
parent a59cfa8944
commit b8b836fb53
1 changed files with 204 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

205
src/thue_morse3.v
View File

@ -1374,12 +1374,191 @@ Proof.
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 :
forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ (rev a) ++ tl
-> 0 < length a
-> even (length a) = true
-> 11= 42.
-> tm_morphism (tm_step (pred n)) =
tm_morphism
(firstn (Nat.div2 (length hd)) (tm_step (pred n)) ++
firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length hd)) (tm_step (pred n))) ++
map negb
(rev
(firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length hd)) (tm_step (pred n))))) ++
skipn (length a + Nat.div2 (length hd)) (tm_step (pred n))).
Proof.
intros n hd a tl. intros H I J.
destruct n. assert (length (tm_step 0) <= length (tm_step 0)).
@ -1401,9 +1580,33 @@ Proof.
destruct (even (length hd)). reflexivity. inversion H0.
rewrite <- tm_step_lemma in H.
assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
generalize H1. generalize H. apply tm_morphism_app2.
assert (a ++ (rev a) ++ tl
= tm_morphism (skipn (Nat.div2 (length hd)) (tm_step n))).
generalize H1. generalize H. apply tm_morphism_app3. symmetry in H3.
assert (a = tm_morphism (firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length hd)) (tm_step n)))).
generalize J. generalize H3. apply tm_morphism_app2.
assert (tl = tm_morphism (skipn (Nat.div2 (length (a ++ (rev a))))
(skipn (Nat.div2 (length hd)) (tm_step n)))).
assert (even (length (a ++ (rev a))) = true). rewrite app_length.
rewrite rev_length. rewrite Nat.even_add. rewrite J. reflexivity.
generalize H5. rewrite app_assoc in H3. generalize H3.
apply tm_morphism_app3.
rewrite H2 in H. rewrite H4 in H. rewrite tm_morphism_rev in H.
rewrite H5 in H. rewrite <- tm_morphism_app in H.
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
rewrite app_length in H. rewrite rev_length in H.
replace (Nat.div2 (length a + length a)) with (length a) in H.
rewrite <- pred_Sn.