From 0983513567c02833273c082fecef980c1fd7e77b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 2 May 2021 21:40:13 +0200
Subject: [PATCH] add wp_frame_wand lemma

---
 iris/program_logic/weakestpre.v | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index 3f97d83d4..e5d59481e 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -348,12 +348,18 @@ Proof. iIntros "[H Hwp]". iApply (wp_wand with "Hwp H"). Qed.
 Lemma wp_wand_r s E e Φ Ψ :
   WP e @ s; E {{ Φ }} ∗ (∀ v, Φ v -∗ Ψ v) ⊢ WP e @ s; E {{ Ψ }}.
 Proof. iIntros "[Hwp H]". iApply (wp_wand with "Hwp H"). Qed.
-Lemma wp_frame_wand_l s E e Q Φ :
-  Q ∗ WP e @ s; E {{ v, Q -∗ Φ v }} -∗ WP e @ s; E {{ Φ }}.
+Lemma wp_frame_wand s E e Φ R :
+  R -∗ WP e @ s; E {{ v, R -∗ Φ v }} -∗ WP e @ s; E {{ Φ }}.
 Proof.
-  iIntros "[HQ HWP]". iApply (wp_wand with "HWP").
+  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 *)
-- 
GitLab