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-22 15:38:57 +01:00
parent 4d0d28abae
commit 775f08c49c
1 changed files with 22 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
src/thue_morse3.v
View File

@ -779,7 +779,28 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
with (l := removelast (removelast (b3::b5::b7::hd))) (d := false) in H.
pose (b8 := last (removelast (removelast (b3 :: b5 :: b7 :: hd))) false).
fold b8 in H. rewrite <- app_assoc in H. rewrite <- app_assoc in H.
pose (hd' := removelast (removelast (removelast (b3 :: b5 :: b7 :: hd)))).
fold hd' in H.
(* on étend tl *)
destruct tl.
assert (tm_step n = rev (tm_step n)
\/ tm_step n = map negb (rev (tm_step n))).
apply tm_step_rev. destruct H7; rewrite H in H7 at 2;
rewrite rev_app_distr in H7; simpl in H5.
assert (odd 3 = true). reflexivity.
rewrite <- tm_step_pred with (n := n) (k := 0) in H8.
rewrite H7 in H8. simpl in H8. inversion H8. rewrite H10 in n1.
contradiction n1. reflexivity. simpl.
replace 8 with (2^3). rewrite <- Nat.pow_lt_mono_r_iff.
assumption. apply Nat.lt_1_2. reflexivity.
assert (odd 3 = true). reflexivity.
rewrite <- tm_step_pred with (n := n) (k := 0) in H8.
rewrite H7 in H8. simpl in H8. inversion H8.
destruct b0; destruct b1. contradiction n1. reflexivity.
inversion H10. inversion H10. contradiction n1. reflexivity. simpl.
replace 8 with (2^3). rewrite <- Nat.pow_lt_mono_r_iff.
assumption. apply Nat.lt_1_2. reflexivity.