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-22 14:17:44 +01:00
parent e94afc71e1
commit c10a003026
1 changed files with 46 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
src/thue_morse3.v
View File

@ -698,6 +698,17 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
(* on étend hd *)
destruct hd. inversion Q.
(* TODO : sortir les trucs de removelast *)
rewrite app_removelast_last
with (l := removelast (b3::b5::hd)) (d := false) in H.
assert ({last (removelast (b3 :: b5 :: hd)) false = b1}
+ {~ last (removelast (b3 :: b5 :: hd)) false = b1}).
apply bool_dec. destruct H5. rewrite e0 in H.
rewrite <- app_assoc in H.
replace (b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: tl)
with ([b1] ++ b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: tl) in H.
apply tm_step_cubefree in H. contradiction H. reflexivity.
apply Nat.lt_0_1. reflexivity.
(* on étend tl*)
destruct tl.
@ -718,12 +729,47 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
apply tm_step_pred. simpl. rewrite <- Nat.pow_0_r with (a := 2) at 1.
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption. inversion H6.
assert ({b6=b1} + {~ b6=b1}). apply bool_dec. destruct H5. rewrite e0 in H.
replace (
(removelast (removelast (b3 :: b5 :: hd)) ++
[last (removelast (b3 :: b5 :: hd)) false]) ++
[b1] ++ b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: b1 :: tl)
with (
(removelast (removelast (b3 :: b5 :: hd)) ++
[last (removelast (b3 :: b5 :: hd)) false] ++
[b1] ++ b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: nil)
++ [b1] ++ [b1] ++ [b1] ++ tl) in H.
apply tm_step_cubefree in H. contradiction H. reflexivity.
apply Nat.lt_0_1.
rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
rewrite <- app_assoc. reflexivity.
assert (b6 = b0). destruct b6; destruct b1; destruct b0.
reflexivity. contradiction n5. reflexivity. reflexivity.
contradiction n1. reflexivity. contradiction n1. reflexivity.
reflexivity. contradiction n5. reflexivity. reflexivity.
rewrite H5 in H.
assert (last (removelast (b3 :: b5 :: hd)) false = b0).
destruct (last (removelast (b3 :: b5 :: hd)) false);
destruct b1; destruct b0.
reflexivity. contradiction n4. reflexivity. reflexivity.
contradiction n1. reflexivity. contradiction n1. reflexivity.
reflexivity. contradiction n4. reflexivity. reflexivity.
rewrite H6 in H.
(* TODO : étendre encolre hd ??? *)
Admitted.
TFFT TFTF FTFT TFFT (µ de TF TT FF TF) pourquoi impossible ?
FTFT TFTF FTFT TFTF (µ de FF TT FF TT) pourquoi impossible ?
FTTFTFFT FTTFTF (pb avec le repeating_pattern de 8 ???)
TFT TFT FF TFT TFT (si on part sur 2 mod 8)
(idem en partant de la droite pour 6 mod 8)
Le lemme repeating_patterns se base sur les huit premiers termes de TM :