From 5d3c508d8c2cdc082d0f08bfdf43430e2d145636 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 26 Oct 2018 11:11:14 +0200
Subject: [PATCH] New lemma `step_fupdN_wand`, and use instead of
 `step_fupdN_mono`.

---
 theories/base_logic/lib/fancy_updates.v |  7 +++----
 theories/bi/updates.v                   | 11 ++++++++++-
 2 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index b04511cec..2277c86d0 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -78,8 +78,8 @@ Proof.
   iPoseProof (Hiter Hinv) as "H". clear Hiter.
   destruct n as [|n].
   - iApply fupd_plainly_mask_empty. iMod "H" as %?; auto.
-  - iPoseProof (step_fupdN_mono _ _ _ _ (|={⊤}=> ⌜φ⌝)%I with "H") as "H'".
-    { iIntros "H". by iApply fupd_plain_mask_empty. }
+  - iDestruct (step_fupdN_wand _ _ _ _ (|={⊤}=> ⌜φ⌝)%I with "H []") as "H'".
+    { by iApply fupd_plain_mask_empty. }
     rewrite -step_fupdN_S_fupd.
     iMod (step_fupdN_plain with "H'") as "Hφ". iModIntro. iNext.
     rewrite -later_laterN laterN_later.
@@ -92,6 +92,5 @@ Lemma step_fupdN_soundness' `{invPreG Σ} φ n :
 Proof.
   iIntros (Hiter). eapply (step_fupdN_soundness _ n).
   iIntros (Hinv). iPoseProof (Hiter Hinv) as "Hiter".
-  iApply (step_fupdN_mono with "Hiter").
-  iIntros (?). iMod (fupd_intro_mask' _ ∅) as "_"; auto.
+  iApply (step_fupdN_wand with "Hiter"). by iApply (fupd_mask_weaken _ _ _).
 Qed.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 775c40330..6dff72c2b 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -359,11 +359,20 @@ Section fupd_derived.
   Qed.
 
   Lemma step_fupdN_mono E1 E2 n P Q :
-    (P ⊢ Q) → (|={E1, E2}▷=>^n P) ⊢ (|={E1, E2}▷=>^n Q).
+    (P ⊢ Q) → (|={E1,E2}▷=>^n P) ⊢ (|={E1,E2}▷=>^n Q).
   Proof.
     intros HPQ. induction n as [|n IH]=> //=. rewrite IH //.
   Qed.
 
+  Lemma step_fupdN_wand E1 E2 n P Q :
+    (|={E1,E2}▷=>^n P) -∗ (P -∗ Q) -∗ (|={E1,E2}▷=>^n Q).
+  Proof.
+    apply wand_intro_l. induction n as [|n IH]=> /=.
+    { by rewrite wand_elim_l. }
+    rewrite -IH -fupd_frame_l later_sep -fupd_frame_l.
+    by apply sep_mono; first apply later_intro.
+  Qed.
+
   Lemma step_fupdN_S_fupd n E P:
     (|={E, ∅}▷=>^(S n) P) ⊣⊢ (|={E, ∅}▷=>^(S n) |={E}=> P).
   Proof.
-- 
GitLab