From 5b43a080c04c4a6d23b2bd1d37c052c39692dc42 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 11 May 2021 09:39:01 +0200
Subject: [PATCH] use wp_frame_wand in awp_apply; get rid of _l/_r variants

---
 iris/program_logic/weakestpre.v | 6 ------
 iris_heap_lang/proofmode.v      | 8 ++++++--
 2 files changed, 6 insertions(+), 8 deletions(-)

diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index e5d59481e..883d401af 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -354,12 +354,6 @@ Proof.
   iIntros "HR HWP". iApply (wp_wand with "HWP").
   iIntros (v) "HΦ". by iApply "HΦ".
 Qed.
-Lemma wp_frame_wand_l s E e Q Φ :
-  Q ∗ WP e @ s; E {{ v, Q -∗ Φ v }} -∗ WP e @ s; E {{ Φ }}.
-Proof. iIntros "[HQ HWP]". by iApply (wp_frame_wand with "HQ"). Qed.
-Lemma wp_frame_wand_r s E e Q Φ :
-  WP e @ s; E {{ v, Q -∗ Φ v }} ∗ Q -∗ WP e @ s; E {{ Φ }}.
-Proof. iIntros "[HWP HQ]". by iApply (wp_frame_wand with "HQ"). Qed.
 End wp.
 
 (** Proofmode class instances *)
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index ab4d71704..55314fede 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import coq_tactics reduction.
+From iris.proofmode Require Import coq_tactics reduction spec_patterns.
 From iris.proofmode Require Export tactics.
 From iris.program_logic Require Import atomic.
 From iris.heap_lang Require Export tactics derived_laws.
@@ -556,9 +556,13 @@ Tactic Notation "awp_apply" open_constr(lem) :=
   wp_apply_core lem ltac:(fun H => iApplyHyp H) ltac:(fun cont => fail);
   last iAuIntro.
 Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
+  (* Convert "list of hypothesis" into specialization pattern. *)
+  let Hs := words Hs in
+  let Hs := eval vm_compute in (INamed <$> Hs) in
   wp_apply_core lem
     ltac:(fun H =>
-      iApply wp_frame_wand_l; iSplitL Hs; [iAccu|iApplyHyp H]) 
+      iApply (wp_frame_wand with
+        [SGoal $ SpecGoal GSpatial false [] Hs false]); [iAccu|iApplyHyp H])
     ltac:(fun cont => fail);
   last iAuIntro.
 
-- 
GitLab