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 18:54:32 +01:00
parent 7e3d1d5746
commit a21f147de0
1 changed files with 51 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

51
src/thue_morse3.v
View File

@ -486,6 +486,57 @@ Proof.
(* un sous-cas :
(T F) | F T T F || F T T F | (T F) impossible à droite
*)
destruct M. left. assumption. (* ici on postule le modulo = 2 *)
rewrite e in H1.
assert (length (((b3 :: hd) ++ [b; b1; b1; b2]) ++ [b2]) mod 4 = 3).
rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite H1.
reflexivity. easy.
replace(
removelast (b3 :: hd) ++ [last (b3 :: hd) false] ++
b :: b1 :: b1 :: b2 :: b2 :: b1 :: b1 :: b :: b1 :: tl )
with (
(((b3 :: hd) ++ [b; b1; b1; b2]) ++ [b2]) ++ [b1; b1;b;b1] ++ tl) in H.
assert (exists x, skipn 2 [b1;b1;b;b1] = [x;x]). generalize H2.
assert (length [b1;b1;b;b1] = 4). reflexivity. generalize H3.
generalize H. apply tm_step_factor4_3mod4.
destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
contradiction n1. reflexivity.
symmetry. rewrite app_assoc. rewrite <- app_removelast_last.
rewrite <- app_assoc. rewrite <- app_assoc. reflexivity. easy.
(* un sous-cas
(T F) | F T T F || F T T F | (F T) cube
*)
assert (b4 = b). destruct b4; destruct b1; destruct b.
reflexivity. contradiction n3. reflexivity. reflexivity.
contradiction n1. reflexivity. contradiction n1. reflexivity.
reflexivity. contradiction n3. reflexivity. reflexivity. rewrite H1 in H.
assert (b2 = b). destruct b2; destruct b1; destruct b.
reflexivity. contradiction n0. reflexivity. reflexivity.
contradiction n1. reflexivity. contradiction n1. reflexivity.
reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H2 in H.
assert (last (b3::hd) false = b).
destruct (last (b3::hd) false); destruct b1; destruct b.
reflexivity. contradiction n2. reflexivity. reflexivity.
contradiction n1. reflexivity. contradiction n1. reflexivity.
reflexivity. contradiction n2. reflexivity. reflexivity. rewrite H3 in H.
Lemma tm_step_factor4_3mod4 : forall (n' : nat) (w z y : list bool),
tm_step n' = w ++ z ++ y
-> length z = 4 -> length w mod 4 = 3
-> exists (x : bool), skipn 2 z = [x;x].
rewrite app_length in H1. rewrite app_length in H1.
rewrite <- Nat.add_assoc in H1. rewrite <- Nat.add_mod_idemp_l in H1.
rewrite H2 in H1. inversion H1. easy. easy. easy.