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 15:20:21 +01:00
parent c8d25340a4
commit 9bbe1abbdb
1 changed files with 24 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
src/thue_morse3.v
View File

@ -1586,6 +1586,18 @@ Proof.
assert (K: even (length (rev a)) = true). rewrite rev_length. assumption.
(*
assert (Q: Nat.div2 (length hd) <= length (tm_step (S n))).
rewrite H. rewrite app_length.
assert (Nat.div2 (length hd) <= length hd).
assert (length hd = 0 \/ 0 < length hd). apply Nat.eq_0_gt_0_cases.
destruct H1. rewrite H1. apply Nat.le_refl.
apply Nat.lt_le_incl. apply Nat.lt_div2. assumption.
assert (length hd <= length hd + length (a ++ rev a ++ tl)).
apply Nat.le_add_r. generalize H2. generalize H1. apply Nat.le_trans.
*)
rewrite app_assoc in H. rewrite <- tm_step_lemma in H.
assert (hd ++ a = tm_morphism (firstn (Nat.div2 (length (hd ++ a)))
@ -1673,6 +1685,17 @@ 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 (H0': even (length (hd' ++ a')) = true).
rewrite app_length. rewrite Nat.even_add.
rewrite I'. rewrite J'. reflexivity.
@ -1770,7 +1793,7 @@ Proof.
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.