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

Update

This commit is contained in:
Thomas Baruchel 2023-02-11 11:14:49 +01:00
parent 8c7bd4940a
commit 6a9c177d2f
1 changed files with 16 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
src/thue_morse3.v
View File

@ -507,19 +507,16 @@ Proof.
(* un sous-cas (* un sous-cas
(T F) | F T T F || F T T F | (F T) cube (T F) | F T T F || F T T F | (F T) cube
*) *)
assert (b4 = b). destruct b4; destruct b1; destruct b. assert (b4 = b). destruct b4; destruct b1; destruct b;
reflexivity. contradiction n3. reflexivity. reflexivity. reflexivity || contradiction n3 || contradiction n1; reflexivity.
contradiction n1. reflexivity. contradiction n1. reflexivity. rewrite H1 in H.
reflexivity. contradiction n3. reflexivity. reflexivity. rewrite H1 in H.
assert (b2 = b). destruct b2; destruct b1; destruct b. assert (b2 = b). destruct b2; destruct b1; destruct b.
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 H2 in H. reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H2 in H.
assert (last (b3::hd) false = b). assert (last (b3::hd) false = b).
destruct (last (b3::hd) false); destruct b1; destruct b. destruct (last (b3::hd) false); destruct b1; destruct b;
reflexivity. contradiction n2. reflexivity. reflexivity. reflexivity || contradiction n2 || contradiction n1; reflexivity.
contradiction n1. reflexivity. contradiction n1. reflexivity.
reflexivity. contradiction n2. reflexivity. reflexivity.
(* élargir hd et tl à l'aide des booléens b5 (gauche) et b6 (droite) *) (* élargir hd et tl à l'aide des booléens b5 (gauche) et b6 (droite) *)
destruct hd. inversion Q. destruct tl. destruct hd. inversion Q. destruct tl.
@ -562,10 +559,9 @@ Proof.
++ [b] ++ [b] ++ [b] ++ tl) in H. ++ [b] ++ [b] ++ [b] ++ tl) in H.
apply tm_step_cubefree in H. contradiction H. reflexivity. apply tm_step_cubefree in H. contradiction H. reflexivity.
apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity. apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.
assert (b6 = b1). destruct (b6); destruct b1; destruct b. assert (b6 = b1). destruct (b6); destruct b1; destruct b;
reflexivity. reflexivity. contradiction n5. reflexivity. reflexivity || contradiction n5 || contradiction n1; reflexivity.
contradiction n1. reflexivity. contradiction n1. reflexivity. rewrite H5 in H.
contradiction n5. reflexivity. reflexivity. reflexivity. rewrite H5 in H.
(* contradiction *) (* contradiction *)
replace ( replace (
@ -642,10 +638,8 @@ reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H.
destruct M. left. assumption. (* ici on postule le modulo = 2 *) destruct M. left. assumption. (* ici on postule le modulo = 2 *)
assert (last (b3::hd) false = b1). assert (last (b3::hd) false = b1).
destruct (last (b3::hd) false); destruct b1; destruct b0. destruct (last (b3::hd) false); destruct b1; destruct b0;
reflexivity. reflexivity. contradiction n2. reflexivity. reflexivity || contradiction n2 || contradiction n1; 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 ({b4=b0} + {~ b4=b0}). apply bool_dec. destruct H3. rewrite e0 in H.
assert (exists x, skipn 2 [b1;b0;b1;b0] = [x;x]). assert (exists x, skipn 2 [b1;b0;b1;b0] = [x;x]).
@ -664,10 +658,8 @@ reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H.
destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1. destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
contradiction n1. reflexivity. contradiction n1. reflexivity.
assert (b4 = b1). destruct b4; destruct b1; destruct b0. assert (b4 = b1). destruct b4; destruct b1; destruct b0;
reflexivity. reflexivity. contradiction n3. reflexivity. reflexivity || contradiction n3 || contradiction n1; reflexivity.
contradiction n1. reflexivity. contradiction n1. reflexivity.
contradiction n3. reflexivity. reflexivity. reflexivity.
rewrite H3 in H. rewrite H2 in H. rewrite H3 in H. rewrite H2 in H.
assert (b2 = b0). destruct b2; destruct b1; destruct b0. assert (b2 = b0). destruct b2; destruct b1; destruct b0.
@ -751,17 +743,13 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
rewrite <- app_assoc. reflexivity. rewrite <- app_assoc. reflexivity.
(* on assigne les valeurs correctes aux deux extrémités *) (* on assigne les valeurs correctes aux deux extrémités *)
assert (b6 = b0). destruct b6; destruct b1; destruct b0. assert (b6 = b0). destruct b6; destruct b1; destruct b0;
reflexivity. contradiction n5. reflexivity. reflexivity. reflexivity || contradiction n5 || contradiction n1; reflexivity.
contradiction n1. reflexivity. contradiction n1. reflexivity.
reflexivity. contradiction n5. reflexivity. reflexivity.
rewrite H5 in H. rewrite H5 in H.
assert (last (removelast (b3 :: b5 :: hd)) false = b0). assert (last (removelast (b3 :: b5 :: hd)) false = b0).
destruct (last (removelast (b3 :: b5 :: hd)) false); destruct (last (removelast (b3 :: b5 :: hd)) false);
destruct b1; destruct b0. destruct b1; destruct b0;
reflexivity. contradiction n4. reflexivity. reflexivity. reflexivity || contradiction n4 || contradiction n1; reflexivity.
contradiction n1. reflexivity. contradiction n1. reflexivity.
reflexivity. contradiction n4. reflexivity. reflexivity.
rewrite H6 in H. rewrite H6 in H.
(* on étend hd *) (* on étend hd *)