Commit 18221e5f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

wp tactical to apply lemmas under contexts.

parent d80e20a8
...@@ -129,7 +129,7 @@ Section proof. ...@@ -129,7 +129,7 @@ Section proof.
wp (newchan '()) Q. wp (newchan '()) Q.
Proof. Proof.
rewrite /newchan. wp_rec. (* TODO: wp_seq. *) rewrite /newchan. wp_rec. (* TODO: wp_seq. *)
rewrite -wp_pvs. eapply wp_alloc; eauto with I ndisj. rewrite -later_intro. rewrite -wp_pvs. wp> eapply wp_alloc; eauto with I ndisj.
apply forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l. apply forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l.
rewrite !assoc. apply pvs_wand_r. rewrite !assoc. apply pvs_wand_r.
(* The core of this proof: Allocating the STS and the saved prop. *) (* The core of this proof: Allocating the STS and the saved prop. *)
......
...@@ -31,19 +31,10 @@ Section LiftingTests. ...@@ -31,19 +31,10 @@ Section LiftingTests.
Goal N, heap_ctx N wp N e (λ v, v = '2). Goal N, heap_ctx N wp N e (λ v, v = '2).
Proof. Proof.
move=> N. rewrite /e. move=> N. rewrite /e.
wp_focus (ref '1)%L. eapply wp_alloc; eauto; []. wp> eapply wp_alloc; eauto. apply forall_intro=>l; apply wand_intro_l.
rewrite -later_intro; apply forall_intro=>l; apply wand_intro_l. wp_rec. wp> eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
wp_rec. wp_bin_op. wp> eapply wp_store; eauto with I. apply sep_mono_r, wand_intro_l.
wp_focus (! LocV l)%L. wp_rec. wp> eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
eapply wp_load; eauto with I; []. rewrite -later_intro. apply sep_mono_r.
rewrite -later_intro; apply wand_intro_l.
wp_bin_op.
wp_focus (_ <- _)%L.
eapply wp_store; eauto with I; []. rewrite -later_intro. apply sep_mono_r.
rewrite -later_intro. apply wand_intro_l.
wp_rec.
eapply wp_load; eauto with I; []. rewrite -later_intro. apply sep_mono_r.
rewrite -later_intro. apply wand_intro_l.
by apply const_intro. by apply const_intro.
Qed. Qed.
...@@ -74,17 +65,15 @@ Section LiftingTests. ...@@ -74,17 +65,15 @@ Section LiftingTests.
Proof. Proof.
wp_rec>; apply later_mono; wp_bin_op=> ?; wp_if. wp_rec>; apply later_mono; wp_bin_op=> ?; wp_if.
- wp_un_op. wp_bin_op. - wp_un_op. wp_bin_op.
wp_focus (FindPred _ _); rewrite -FindPred_spec. ewp apply FindPred_spec.
apply and_intro; first auto with I omega. apply and_intro; first auto with I omega.
wp_un_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega. wp_un_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
- rewrite -FindPred_spec. auto with I omega. - ewp apply FindPred_spec. auto with I omega.
Qed. Qed.
Goal E, Goal E,
True wp (Σ:=globalF Σ) E (let: "x" := Pred '42 in Pred "x") (λ v, v = '40). True wp (Σ:=globalF Σ) E (let: "x" := Pred '42 in Pred "x") (λ v, v = '40).
Proof. Proof.
intros E. intros. ewp> apply Pred_spec. wp_rec. ewp> apply Pred_spec. auto with I.
wp_focus (Pred _); rewrite -Pred_spec -later_intro.
wp_rec. rewrite -Pred_spec -later_intro; auto with I.
Qed. Qed.
End LiftingTests. End LiftingTests.
...@@ -81,3 +81,13 @@ Tactic Notation "wp_focus" open_constr(efoc) := ...@@ -81,3 +81,13 @@ Tactic Notation "wp_focus" open_constr(efoc) :=
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => | |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match e' with efoc => unify e' efoc; wp_bind K end) match e' with efoc => unify e' efoc; wp_bind K end)
end. end.
Tactic Notation "wp" tactic(tac) :=
match goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => wp_bind K; tac)
end.
Tactic Notation "wp" ">" tactic(tac) := (wp tac); wp_strip_later.
(* In case the precondition does not match *)
Tactic Notation "ewp" tactic(tac) := wp (etransitivity; [|tac]).
Tactic Notation "ewp" ">" tactic(tac) := wp> (etransitivity; [|tac]).
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment