Update
This commit is contained in:
parent
7cc18437c9
commit
1aeaa1050f
@ -803,6 +803,11 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
|
|||||||
assumption. apply Nat.lt_1_2. reflexivity.
|
assumption. apply Nat.lt_1_2. reflexivity.
|
||||||
|
|
||||||
(* termes à prouver *)
|
(* termes à prouver *)
|
||||||
|
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.
|
||||||
assert (U:
|
assert (U:
|
||||||
nth_error (b3 :: b5 :: b7 :: hd) (length (b3 :: b5 :: b7 :: hd) - 3)
|
nth_error (b3 :: b5 :: b7 :: hd) (length (b3 :: b5 :: b7 :: hd) - 3)
|
||||||
= Some b8). unfold b8.
|
= Some b8). unfold b8.
|
||||||
@ -812,6 +817,14 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
|
|||||||
rewrite app_removelast_last
|
rewrite app_removelast_last
|
||||||
with (l := (removelast (removelast (b3::b5::b7::hd)))) (d := false) at 1.
|
with (l := (removelast (removelast (b3::b5::b7::hd)))) (d := false) at 1.
|
||||||
rewrite <- app_assoc. rewrite <- app_assoc. rewrite nth_error_app2.
|
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.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user