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-27 17:06:04 +01:00
parent 9bbe1abbdb
commit 10abcb7965
1 changed files with 19 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
src/thue_morse3.v
View File

@ -1553,6 +1553,9 @@ Lemma tm_step_palindromic_even_morphism2 :
-> (length a) mod 4 = 0
-> hd = tm_morphism (tm_morphism (firstn (length hd / 4)
(tm_step (pred (pred n)))))
/\ a = tm_morphism (tm_morphism
(firstn (length a / 4) (skipn (length hd / 4)
(tm_step (pred (pred n))))))
/\ 11 = 42.
Proof.
intros n hd a tl. intros H W J0.
@ -1685,13 +1688,12 @@ Proof.
assert (K': even (length (map negb (rev a'))) = true).
rewrite map_length. rewrite rev_length. assumption.
assert (Q: length hd' <= length (tm_step n)).
rewrite H. rewrite app_length. apply Nat.le_add_r.
assert (Q': length hd' + length a' <= length (tm_step n)).
rewrite H. rewrite app_assoc. rewrite app_length.
rewrite <- app_length. apply Nat.le_add_r.
@ -1788,29 +1790,31 @@ Proof.
split.
rewrite <- pred_Sn. rewrite <- pred_Sn.
rewrite H4 at 1. fold hd'. rewrite H4'. unfold hd'.
rewrite firstn_length_le. rewrite Nat.div2_div. rewrite Nat.div2_div.
rewrite Nat.div_div. reflexivity. easy. easy.
rewrite <- H6. assumption.
split.
rewrite <- pred_Sn. rewrite <- pred_Sn. rewrite H5 at 1. fold a'.
rewrite H5'. unfold a'.
rewrite firstn_length_le. rewrite Nat.div2_div. rewrite Nat.div2_div.
rewrite Nat.div_div.
replace (length hd / 4) with (Nat.div2 (length hd')). reflexivity.
replace 4 with (2*2). rewrite <- Nat.div_div.
rewrite <- Nat.div2_div. rewrite <- Nat.div2_div. rewrite <- H6. reflexivity.
easy. easy. reflexivity. easy. easy.
rewrite skipn_length.
apply Nat.le_add_le_sub_l.
rewrite <- H6. rewrite <- H7. assumption.
Nat.div2 (length hd) + Nat.div2 (length a) <= length (tm_step (S n))
assert (hd = hd). reflexivity. rewrite H4 in H12 at 2. fold hd' in H12.
rewrite H4' in H12. unfold hd' in H12.
rewrite firstn_length_le in H12.
rewrite Nat.div2_div in H12.
rewrite Nat.div2_div in H12. rewrite Nat.div_div in H12.
replace (2*2) with 4 in H12.
Admitted.