baruchel
/
coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

This commit is contained in:
Thomas Baruchel 2023-01-21 21:11:47 +01:00
parent dd3eaf8497
commit 080c8e5291
1 changed files with 24 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
src/thue_morse3.v
View File

@ -644,17 +644,34 @@ reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H.
(* régler d'abord la question du modulo au centre *)
destruct M. left. assumption. (* ici on postule le modulo = 2 *)
assert ({b4=b0} + {~ b4=b0}). apply bool_dec. destruct H2. rewrite e0 in H.
assert (last (b3::hd) false = b1).
destruct (last (b3::hd) false); destruct b1; destruct b0.
reflexivity. reflexivity. contradiction n2. reflexivity.
contradiction n1. reflexivity. contradiction n1. reflexivity.
contradiction n2. reflexivity. reflexivity. reflexivity.
assert ({b4=b0} + {~ b4=b0}). apply bool_dec. destruct H3. rewrite e0 in H.
assert (exists x, skipn 2 [b1;b0;b1;b0] = [x;x]).
replace (removelast (b3 :: hd) ++ [last (b3 :: hd) false] ++
b1 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b1 :: b0 :: tl)
with ((removelast (b3 :: hd) ++
[last (b3 :: hd) false] ++ [b1;b0;b1;b2;b2])
with (((b3 :: hd) ++ [b1;b0;b1;b2;b2])
++ [b1;b0;b1;b0] ++ tl) in H.
assert (length (removelast (b3 :: hd) ++ [last (b3 :: hd) false]
++ [b1; b0; b1; b2; b2]) mod 4 = 3).
assert (length ((b3::hd) ++ [b1; b0; b1; b2; b2]) mod 4 = 3). rewrite e in H1.
replace ([b1;b0;b1;b2;b2]) with ([b1;b0;b1;b2] ++ [b2]).
rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_mod_idemp_l.
rewrite H1. reflexivity. easy. reflexivity.
assert (length [b1;b0;b1;b0] = 4). reflexivity.
generalize H3. generalize H4. generalize H. apply tm_step_factor4_3mod4.
symmetry. rewrite app_assoc. rewrite <- app_removelast_last.
rewrite <- app_assoc. reflexivity. easy.
destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
contradiction n1. reflexivity.
assert (b4 = b1). destruct b4; destruct b1; destruct b0.
reflexivity. reflexivity. contradiction n3. reflexivity.
contradiction n1. reflexivity. contradiction n1. reflexivity.
contradiction n3. reflexivity. reflexivity. reflexivity.
rewrite H3 in H. rewrite H2 in H.