From 18221e5f531c3c933a6aeac6b4d4b3d2d57f26cd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 17 Feb 2016 15:23:49 +0100
Subject: [PATCH] wp tactical to apply lemmas under contexts.

---
 barrier/barrier.v      |  2 +-
 heap_lang/tests.v      | 25 +++++++------------------
 heap_lang/wp_tactics.v | 10 ++++++++++
 3 files changed, 18 insertions(+), 19 deletions(-)

diff --git a/barrier/barrier.v b/barrier/barrier.v
index 7a0a9bb2d..88f0f1e5e 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -129,7 +129,7 @@ Section proof.
     ⊑ wp ⊤ (newchan '()) Q.
   Proof.
     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.
     rewrite !assoc. apply pvs_wand_r.
     (* The core of this proof: Allocating the STS and the saved prop. *)
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 150917f08..0d5da4916 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -31,19 +31,10 @@ Section LiftingTests.
   Goal ∀ N, heap_ctx N ⊑ wp N e (λ v, v = '2).
   Proof.
     move=> N. rewrite /e.
-    wp_focus (ref '1)%L. eapply wp_alloc; eauto; [].
-    rewrite -later_intro; apply forall_intro=>l; apply wand_intro_l.
-    wp_rec.
-    wp_focus (! LocV l)%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.
+    wp> eapply wp_alloc; eauto. 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_bin_op. wp> eapply wp_store; eauto with I. apply sep_mono_r, wand_intro_l.
+    wp_rec. wp> eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
     by apply const_intro.
   Qed.
 
@@ -74,17 +65,15 @@ Section LiftingTests.
   Proof.
     wp_rec>; apply later_mono; wp_bin_op=> ?; wp_if.
     - wp_un_op. wp_bin_op.
-      wp_focus (FindPred _ _); rewrite -FindPred_spec.
+      ewp apply FindPred_spec.
       apply and_intro; first auto with I 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.
 
   Goal ∀ E,
     True ⊑ wp (Σ:=globalF Σ) E (let: "x" := Pred '42 in Pred "x") (λ v, v = '40).
   Proof.
-    intros E.
-    wp_focus (Pred _); rewrite -Pred_spec -later_intro.
-    wp_rec. rewrite -Pred_spec -later_intro; auto with I.
+    intros. ewp> apply Pred_spec. wp_rec. ewp> apply Pred_spec. auto with I.
   Qed.
 End LiftingTests.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 1b461ddd2..2f3722446 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -81,3 +81,13 @@ Tactic Notation "wp_focus" open_constr(efoc) :=
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match e' with efoc => unify e' efoc; wp_bind K 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]).
-- 
GitLab