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 17:41:51 +01:00
parent 1aeaa1050f
commit 64537d4f50
1 changed files with 47 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

60
src/thue_morse3.v
View File

@ -803,11 +803,34 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
assumption. apply Nat.lt_1_2. reflexivity.
(* termes à prouver *)
assert (Y: forall (k: bool) (x : list bool),
(* lemmes initiaux *)
assert (Y: forall (k : bool) (x : list bool),
length (removelast (k::x)) = length x).
intros k x. rewrite removelast_firstn_len. simpl.
rewrite firstn_length_le. reflexivity. simpl.
apply Nat.le_succ_diag_r.
intros k x. rewrite removelast_firstn_len.
replace (length (k::x)) with (S (length x)). rewrite Nat.pred_succ.
rewrite firstn_length. simpl. apply Nat.min_l. apply Nat.le_succ_diag_r.
reflexivity.
assert (Y': forall (k1 k2 : bool) (x : list bool),
length (removelast (removelast (k1::k2::x))) = length x).
intros k1 k2 x.
rewrite removelast_firstn_len. rewrite Y.
replace (length (k2::x)) with (S (length x)).
rewrite Nat.pred_succ. rewrite firstn_length. rewrite Y.
apply Nat.min_l. apply Nat.le_succ_diag_r. reflexivity.
assert (Y'': forall (k1 k2 k3 : bool) (x : list bool),
length (removelast (removelast (removelast (k1::k2::k3::x)))) = length x).
intros k1 k2 k3 x.
rewrite removelast_firstn_len. rewrite removelast_firstn_len.
rewrite Y. replace (length (k2::k3::x)) with (S (length (k3::x))).
rewrite Nat.pred_succ. rewrite firstn_length.
rewrite firstn_length. rewrite Y. rewrite Nat.min_l. rewrite Nat.min_l.
reflexivity. apply Nat.le_succ_diag_r. rewrite Nat.min_l.
replace (length (k3 :: x)) with (S (length x)). rewrite Nat.pred_succ.
apply Nat.le_succ_diag_r. reflexivity.
replace (length (k2 :: k3::x)) with (S (length (k3::x))).
apply Nat.le_succ_diag_r. reflexivity. reflexivity.
(* preuves *)
assert (U:
nth_error (b3 :: b5 :: b7 :: hd) (length (b3 :: b5 :: b7 :: hd) - 3)
= Some b8). unfold b8.
@ -817,16 +840,27 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
rewrite app_removelast_last
with (l := (removelast (removelast (b3::b5::b7::hd)))) (d := false) at 1.
rewrite <- app_assoc. rewrite <- app_assoc. rewrite nth_error_app2.
rewrite removelast_firstn_len at 2. rewrite Y.
replace (length (b5::b7::hd)) with (S (S (length hd))).
rewrite <- pred_Sn. rewrite removelast_firstn. rewrite firstn_length_le.
replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))).
rewrite <- Nat.sub_add_distr. rewrite Nat.sub_diag.
reflexivity. reflexivity.
rewrite Y. simpl.
rewrite Y''. rewrite <- Nat.sub_add_distr.
replace (length (b3::b5::b7::hd)) with (3 + length hd).
rewrite Nat.sub_diag. reflexivity. reflexivity. rewrite Y''.
replace (length (b3::b5::b7::hd)) with (length hd + 3).
rewrite Nat.add_sub. apply Nat.le_refl. rewrite Nat.add_comm.
reflexivity.
assert (0 < length (removelast (removelast (b3 :: b5 :: b7 :: hd)))).
rewrite Y'. simpl. apply Nat.lt_0_succ.
assert ({removelast (removelast (b3 :: b5 :: b7 :: hd))=nil}
+ {~ removelast (removelast (b3 :: b5 :: b7 :: hd))=nil}).
apply list_eq_dec. apply bool_dec. destruct H8.
rewrite e0 in H7. inversion H7. assumption.
assert (0 < length (removelast (b3 :: b5 :: b7 :: hd))).
rewrite Y. simpl. apply Nat.lt_0_succ.
assert ({removelast (b3 :: b5 :: b7 :: hd)=nil}
+ {~ removelast (b3 :: b5 :: b7 :: hd)=nil}).
apply list_eq_dec. apply bool_dec. destruct H8.
rewrite e0 in H7. inversion H7. assumption.
easy.
False, True, True, False, True, False, False, True, True, False, False