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-23 22:22:56 +01:00
parent acdc1a613c
commit 6ccbfa81a4
1 changed files with 29 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
src/thue_morse3.v
View File

@ -1176,7 +1176,36 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
rewrite <- tm_morphism_eq in H.
pose (h0 := firstn (Nat.div2 (length hd'')) (tm_step n)).
pose (s0 := firstn (Nat.div2 (length s))
(skipn (Nat.div2 (length hd'')) (tm_step n))).
pose (t0 := skipn (Nat.div2 (length s))
(skipn (Nat.div2 (length hd'')) (tm_step n))).
fold h0 in H. fold s0 in H. fold t0 in H.
(* fin de la preuve pour cette partie : morphisme impossible *)
assert (s0 = [b0;b0;b1;b1;b0;b0;b1;b1]). fold s0 in H15.
unfold s in H15. destruct s0. inversion H15.
destruct s0. inversion H15. destruct s0. inversion H15.
destruct s0. inversion H15. destruct s0; inversion H15.
destruct s0. inversion H15. destruct s0. inversion H15.
destruct s0. inversion H15. destruct s0; inversion H15.
inversion H15. reflexivity.
(*
assert (b13 = b0). destruct b13; destruct b1; destruct b0.
reflexivity. inversion H46. reflexivity. inversion H45.
inversion H45. reflexivity. inversion H45. reflexivity.
rewrite H17 in H15. rewrite H17 in H47. rewrite <- H47 in H15.
rewrite <- H47 in H33. rewrite <- H33 in H15.
rewrite <- H47 in H24. rewrite <- H24 in H15.
rewrite <- H47 in H26. rewrite <- H26 in H15.
rewrite <- H47 in H39. rewrite <- H39 in H15.
rewrite <- H47 in H41. rewrite <- H41 in H15.
rewrite <- H47 in H43. rewrite <- H43 in H15.
rewrite negb_involutive in H15. rewrite negb_involutive in H15.
fold s in H15.
*)
rewrite H17 in H.
Lemma tm_morphism_app : forall (l1 l2 : list bool),