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:48:33 +01:00
parent 6507761b38
commit dd3eaf8497
1 changed files with 11 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/thue_morse3.v
View File

@ -641,6 +641,17 @@ reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H.
(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 ?
*)
(* 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.
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])
++ [b1;b0;b1;b0] ++ tl) in H.
assert (length (removelast (b3 :: hd) ++ [last (b3 :: hd) false]
++ [b1; b0; b1; b2; b2]) mod 4 = 3).