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-21 20:41:23 +01:00
parent b95fe2fb75
commit 6507761b38
1 changed files with 39 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
src/thue_morse3.v
View File

@ -595,14 +595,52 @@ Proof.
(T F) | T F T F || F T F T | (T F) diff + impossible à gauche (T F) | T F T F || F T F T | (T F) diff + impossible à gauche
*) *)
assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1. rewrite e in H. assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1. rewrite e in H.
(*
assert (b2 = b0). destruct (b2); destruct b1; destruct b0. assert (b2 = b0). destruct (b2); destruct b1; destruct b0.
reflexivity. contradiction n0. reflexivity. reflexivity. reflexivity. contradiction n0. reflexivity. reflexivity.
contradiction n1. reflexivity. contradiction n1. reflexivity. contradiction n1. reflexivity. contradiction n1. reflexivity.
reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H. reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H.
*)
(* cas b = b1 T F T F || F T F T *) rewrite app_removelast_last with (l := b3::hd) (d := false) in H.
rewrite <- app_assoc in H.
assert ({last (b3::hd) false=b0} + {~ last (b3::hd) false=b0}).
apply bool_dec. destruct H1. rewrite e0 in H.
(* problème à gauche *)
destruct M. left. assumption. (* ici on postule le modulo = 2 *)
rewrite app_removelast_last with (l := b3::hd) (d := false) in Q.
rewrite last_length in Q. rewrite Nat.even_succ in Q. apply odd_mod4 in Q.
destruct Q.
assert (exists x, firstn 2 [b0;b1;b0;b1] = [x;x]). generalize H2.
assert (length [b0;b1;b0;b1] = 4). reflexivity. generalize H3.
replace (
removelast (b3 :: hd) ++
[b0] ++ b1 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl )
with (
removelast (b3 :: hd) ++ [b0;b1;b0;b1]
++ (b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl )) in H.
generalize H. apply tm_step_factor4_1mod4. reflexivity.
destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
contradiction n1. reflexivity.
assert (exists x, skipn 2 [b0;b1;b0;b1] = [x;x]). generalize H2.
assert (length [b0;b1;b0;b1] = 4). reflexivity. generalize H3.
replace (
removelast (b3 :: hd) ++
[b0] ++ b1 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl )
with (
removelast (b3 :: hd) ++ [b0;b1;b0;b1]
++ (b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl )) in H.
generalize H. apply tm_step_factor4_3mod4. reflexivity.
destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
contradiction n1. reflexivity. easy.
(* nouveau cas : last (b3 :: hd) false <> b0
(F T) | T F T F || F T F T | (F T) diff + impossible à droite
(F T) | T F T F || F T F T | (T F) 4n+2 a/rev a/a possible ?
*)