pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-12-01 00:26:18 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

SepCancel: be more cautious in a few ways

Browse source
This commit is contained in:
Adam Chlipala 2016-04-19 18:36:25 -04:00
parent 68b01b1047
commit 60c21c07ec
1 changed files with 26 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
SepCancel.v
View file

@ -211,13 +211,15 @@ Module Make(Import S : SEP).
Qed. Qed.
Ltac normalize0 := Ltac normalize0 :=
setoid_rewrite exis_gulp match goal with
|| setoid_rewrite lift_combine | [ |- context[star ?p (exis ?q)] ] => rewrite (exis_gulp p q)
|| setoid_rewrite star_assoc | [ |- context[star (star ?p (lift ?q)) (lift ?r)] ] => rewrite (lift_combine p q r)
|| setoid_rewrite star_combine_lift | [ |- context[star ?p (star ?q ?r)] ] => rewrite (star_assoc p q r)
|| setoid_rewrite star_comm_lift | [ |- context[star (lift ?p) (lift ?q)] ] => rewrite (star_combine_lift p q)
|| setoid_rewrite star_assoc_lift | [ |- context[star (lift ?p) ?q ] ] => rewrite (star_comm_lift p q)
|| setoid_rewrite star_comm_exis. | [ |- context[star (star ?p (lift ?q)) ?r] ] => rewrite (star_assoc_lift p q r)
| [ |- context[star (exis ?p) ?q] ] => rewrite (star_comm_exis p q)
end.
Ltac normalizeL := Ltac normalizeL :=
(apply exis_left || apply lift_left; intro; try congruence) (apply exis_left || apply lift_left; intro; try congruence)
@ -248,8 +250,11 @@ Module Make(Import S : SEP).
lift. lift.
Qed. Qed.
Ltac normalize2 := setoid_rewrite lift_uncombine Ltac normalize2 :=
|| setoid_rewrite star_assoc. match goal with
| [ |- context[star ?p lift (?P /\ ?Q)] ] => rewrite (lift_uncombine p P Q)
| [ |- context[star ?p (star ?q ?r)] ] => rewrite (star_assoc p q r)
end.
Ltac normalizeLeft := Ltac normalizeLeft :=
let s := fresh "s" in intro s; let s := fresh "s" in intro s;
@ -307,7 +312,19 @@ Module Make(Import S : SEP).
reflexivity. reflexivity.
Qed. Qed.
Definition try_me_first (_ : hprop) := True.
Ltac cancel1 := Ltac cancel1 :=
match goal with
| [ |- ?p ===> ?q ] =>
forAllAtoms p ltac:(fun p0 =>
(let H := fresh in assert (H : try_me_first p0) by eauto; clear H);
sendToBack p0;
forAllAtoms q ltac:(fun q0 =>
(let H := fresh in assert (H : try_me_first q0) by eauto; clear H);
sendToBack q0;
apply star_cancel'))
end ||
match goal with match goal with
| [ |- _ ===> ?Q ] => | [ |- _ ===> ?Q ] =>
match Q with match Q with