From 97f90263be1b6b54c43fbecb2f7b079b1a4ff161 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 5 Jan 2021 11:07:59 +0100
Subject: [PATCH] Make use of better `iMod` for updates.

---
 iris/base_logic/lib/cancelable_invariants.v | 22 +++++++++------------
 iris/base_logic/lib/fancy_updates.v         |  2 +-
 iris/base_logic/lib/invariants.v            | 15 ++++++--------
 iris/bi/lib/atomic.v                        |  4 ++--
 4 files changed, 18 insertions(+), 25 deletions(-)

diff --git a/iris/base_logic/lib/cancelable_invariants.v b/iris/base_logic/lib/cancelable_invariants.v
index 5ad576c95..06ff79fb4 100644
--- a/iris/base_logic/lib/cancelable_invariants.v
+++ b/iris/base_logic/lib/cancelable_invariants.v
@@ -114,14 +114,11 @@ Section proofs.
     ▷ P ∗ cinv_own γ p ∗ (∀ E' : coPset, ▷ P ∨ cinv_own γ 1 ={E',↑N ∪ E'}=∗ True)).
   Proof.
     iIntros (?) "Hinv Hown".
-    iPoseProof (inv_acc (↑ N) N with "Hinv") as "H"; first done.
-    rewrite difference_diag_L.
-    iPoseProof (fupd_mask_frame_r _ _ (E ∖ ↑ N) with "H") as "H"; first set_solver.
-    rewrite left_id_L -union_difference_L //. iMod "H" as "[[$ | >Hown'] H]".
-    - iIntros "{$Hown} !>" (E') "HP".
-      iPoseProof (fupd_mask_frame_r _ _ E' with "(H [HP])") as "H"; first set_solver.
-      { iDestruct "HP" as "[?|?]"; eauto. }
-      by rewrite left_id_L.
+    iMod (inv_acc (↑ N) N with "Hinv") as "[[$ | >Hown'] H]"; first done.
+    - iApply fupd_intro_mask_eq; [set_solver|].
+      iIntros "{$Hown}" (E') "HP".
+      iMod ("H" with "[HP]") as "_"; [by iModIntro|set_solver|..].
+      by iApply fupd_intro_mask_eq; [set_solver|].
     - iDestruct (cinv_own_1_l with "Hown' Hown") as %[].
   Qed.
 
@@ -131,9 +128,8 @@ Section proofs.
   Proof.
     iIntros (?) "#Hinv Hγ".
     iMod (cinv_acc_strong with "Hinv Hγ") as "($ & $ & H)"; first done.
-    iIntros "!> HP".
-    rewrite {2}(union_difference_L (↑N) E)=> //.
-    iApply "H". by iLeft.
+    iIntros "!> HP". iMod ("H" with "[$HP]") as "_".
+    by rewrite -union_difference_L.
   Qed.
 
   (*** Other *)
@@ -141,8 +137,8 @@ Section proofs.
   Proof.
     iIntros (?) "#Hinv Hγ".
     iMod (cinv_acc_strong with "Hinv Hγ") as "($ & Hγ & H)"; first done.
-    rewrite {2}(union_difference_L (↑N) E)=> //.
-    iApply "H". by iRight.
+    iMod ("H" with "[$Hγ]") as "_".
+    by rewrite -union_difference_L.
   Qed.
 
   Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N := {}.
diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index 7bdce06e5..bce9c942b 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -65,7 +65,7 @@ Lemma fupd_plain_soundness `{!invPreG Σ} E1 E2 (P: iProp Σ) `{!Plain P} :
 Proof.
   iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hinv) "[Hw HE]".
   iAssert (|={⊤,E2}=> P)%I as "H".
-  { iMod fupd_intro_mask'; last iApply Hfupd. done. }
+  { iMod Hfupd as "$". iApply fupd_intro_mask_subseteq; [set_solver|]; auto. }
   rewrite uPred_fupd_eq /uPred_fupd_def.
   iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
 Qed.
diff --git a/iris/base_logic/lib/invariants.v b/iris/base_logic/lib/invariants.v
index e7cc9b638..5f0c74fcc 100644
--- a/iris/base_logic/lib/invariants.v
+++ b/iris/base_logic/lib/invariants.v
@@ -140,8 +140,8 @@ Section inv.
     rewrite inv_eq. iIntros (??) "#HinvP #HinvQ !>"; iIntros (E ?).
     iMod ("HinvP" with "[%]") as "[$ HcloseP]"; first set_solver.
     iMod ("HinvQ" with "[%]") as "[$ HcloseQ]"; first set_solver.
-    iMod (fupd_intro_mask' _ (E ∖ ↑N)) as "Hclose"; first set_solver.
-    iIntros "!> [HP HQ]".
+    iApply fupd_mask_subseteq; first set_solver.
+    iIntros "Hclose !> [HP HQ]".
     iMod "Hclose" as %_. iMod ("HcloseQ" with "HQ") as %_. by iApply "HcloseP".
   Qed.
 
@@ -174,13 +174,10 @@ Section inv.
     ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ ∀ E', ▷ P ={E',↑N ∪ E'}=∗ True.
   Proof.
     iIntros (?) "Hinv".
-    iPoseProof (inv_acc (↑ N) N with "Hinv") as "H"; first done.
-    rewrite difference_diag_L.
-    iPoseProof (fupd_mask_frame_r _ _ (E ∖ ↑ N) with "H") as "H"; first set_solver.
-    rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro.
-    iIntros (E') "HP".
-    iPoseProof (fupd_mask_frame_r _ _ E' with "(H HP)") as "H"; first set_solver.
-    by rewrite left_id_L.
+    iMod (inv_acc (↑ N) N with "Hinv") as "[$ H]"; first done.
+    iApply fupd_intro_mask_eq; [set_solver|].
+    iIntros (E') "HP". iMod ("H" with "HP") as "_"; [set_solver|].
+    by iApply fupd_intro_mask_eq; first set_solver.
   Qed.
 
   Lemma inv_acc_timeless E N P `{!Timeless P} :
diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index 2658652ec..98907c921 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -311,7 +311,7 @@ Section lemmas.
     atomic_acc Eo Ei α P β Φ).
   Proof.
     iIntros (? x) "Hα Hclose".
-    iMod fupd_intro_mask' as "Hclose'"; last iModIntro; first set_solver.
+    iApply fupd_intro_mask_subseteq; [done|]; iIntros "Hclose'".
     iExists x. iFrame. iSplitWith "Hclose".
     - iIntros "Hα". iMod "Hclose'" as "_". iApply "Hclose". done.
     - iIntros (y) "Hβ". iMod "Hclose'" as "_". iApply "Hclose". done.
@@ -331,7 +331,7 @@ Section lemmas.
        to happen only if one argument is a constructor. *)
     iIntros "Hinner >Hacc". iDestruct "Hacc" as (x') "[Hα' Hclose]".
     iMod ("Hinner" with "Hα'") as (x) "[Hα Hclose']".
-    iMod (fupd_intro_mask') as "Hclose''"; last iModIntro; first done.
+    iApply fupd_intro_mask_subseteq; [done|]; iIntros "Hclose''".
     iExists x. iFrame. iSplitWith "Hclose'".
     - iIntros "Hα". iMod "Hclose''" as "_".
       iMod ("Hclose'" with "Hα") as "[Hβ' HPas]".
-- 
GitLab