From 7575aa52f5e030c280d78077ed8d9015d871f48f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 15 Feb 2021 12:10:39 +0100
Subject: [PATCH] another naming scheme

---
 iris/base_logic/lib/fancy_updates.v   |  6 +++---
 iris/bi/lib/atomic.v                  |  2 +-
 iris/bi/monpred.v                     |  2 +-
 iris/bi/updates.v                     | 29 +++++++++++++++++++--------
 iris/program_logic/adequacy.v         |  3 +--
 iris/program_logic/total_weakestpre.v |  2 +-
 iris/program_logic/weakestpre.v       |  2 +-
 tests/proofmode_monpred.v             |  4 ++--
 8 files changed, 31 insertions(+), 19 deletions(-)

diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index 44ddb2875..5471682db 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -19,9 +19,9 @@ Lemma uPred_fupd_mixin `{!invG Σ} : BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd
 Proof.
   split.
   - rewrite uPred_fupd_eq. solve_proper.
-  - intros E1 E2 P (E1''&->&?)%subseteq_disjoint_union_L.
+  - intros E1 E2 (E1''&->&?)%subseteq_disjoint_union_L.
     rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
-    by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" .
+    by iIntros "($ & $ & HE) !> !> [$ $] !> !>" .
   - rewrite uPred_fupd_eq. iIntros (E1 E2 P) ">H [Hw HE]". iApply "H"; by iFrame.
   - rewrite uPred_fupd_eq. iIntros (E1 E2 P Q HPQ) "HP HwE". rewrite -HPQ. by iApply "HP".
   - rewrite uPred_fupd_eq. iIntros (E1 E2 E3 P) "HP HwE".
@@ -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".
-  { iApply (fupd_mask_weaken E1); first done. iIntros "_". iApply Hfupd. }
+  { iMod (fupd_mask_subseteq E1) as "_"; first done. iApply Hfupd. }
   rewrite uPred_fupd_eq /uPred_fupd_def.
   iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
 Qed.
diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index 266e3ec89..c75b517ac 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -56,7 +56,7 @@ Section definition.
     atomic_acc Eo1 Ei α P β Φ -∗ atomic_acc Eo2 Ei α P β Φ.
   Proof.
     iIntros (HE) "Hstep".
-    iApply (fupd_mask_weaken Eo1); first done. iIntros "Hclose1".
+    iMod (fupd_mask_subseteq Eo1) as "Hclose1"; first done.
     iMod "Hstep" as (x) "[Hα Hclose2]". iIntros "!>". iExists x.
     iFrame. iSplitWith "Hclose2".
     - iIntros "Hα". iMod ("Hclose2" with "Hα") as "$". done.
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index 74b2e3fb7..48bd047d8 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -894,7 +894,7 @@ Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredI monPred_fupd.
 Proof.
   split; rewrite monPred_fupd_eq.
   - split=>/= i. solve_proper.
-  - intros E1 E2 P HE12. split=>/= i. by apply fupd_mask_intro_subseteq.
+  - intros E1 E2 HE12. split=>/= i. by apply fupd_mask_intro_subseteq.
   - intros E1 E2 P. split=>/= i. by rewrite monPred_at_except_0 except_0_fupd.
   - intros E1 E2 P Q HPQ. split=>/= i. by rewrite HPQ.
   - intros E1 E2 E3 P. split=>/= i. apply fupd_trans.
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 5a1c70516..60c88f31c 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -70,8 +70,8 @@ Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := {
 Record BiFUpdMixin (PROP : bi) `(FUpd PROP) := {
   bi_fupd_mixin_fupd_ne E1 E2 :
     NonExpansive (fupd (PROP:=PROP) E1 E2);
-  bi_fupd_mixin_fupd_mask_intro_subseteq E1 E2 (P : PROP) :
-    E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P;
+  bi_fupd_mixin_fupd_mask_subseteq E1 E2 :
+    E2 ⊆ E1 → ⊢@{PROP} |={E1,E2}=> |={E2,E1}=> emp;
   bi_fupd_mixin_except_0_fupd E1 E2 (P : PROP) :
     ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P;
   bi_fupd_mixin_fupd_mono E1 E2 (P Q : PROP) :
@@ -153,8 +153,12 @@ Section fupd_laws.
 
   Global Instance fupd_ne E1 E2 : NonExpansive (@fupd PROP _ E1 E2).
   Proof. eapply bi_fupd_mixin_fupd_ne, bi_fupd_mixin. Qed.
-  Lemma fupd_mask_intro_subseteq E1 E2 (P : PROP) : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
-  Proof. eapply bi_fupd_mixin_fupd_mask_intro_subseteq, bi_fupd_mixin. Qed.
+  (** [iMod] with this lemma is useful to change the current mask to a subset,
+  and obtain a fupd for changing it back. For the case where you want to get rid
+  of a mask-changing fupd in the goal, [iApply fupd_mask_intro] avoids having to
+  specify the mask. *)
+  Lemma fupd_mask_subseteq {E1} E2 : E2 ⊆ E1 → ⊢@{PROP} |={E1,E2}=> |={E2,E1}=> emp.
+  Proof. eapply bi_fupd_mixin_fupd_mask_subseteq, bi_fupd_mixin. Qed.
   Lemma except_0_fupd E1 E2 (P : PROP) : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P.
   Proof. eapply bi_fupd_mixin_except_0_fupd, bi_fupd_mixin. Qed.
   Lemma fupd_mono E1 E2 (P Q : PROP) : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
@@ -251,10 +255,17 @@ Section fupd_derived.
     Proper (flip (⊢) ==> flip (⊢)) (fupd (PROP:=PROP) E1 E2).
   Proof. intros P Q; apply fupd_mono. Qed.
 
+  Lemma fupd_mask_intro_subseteq E1 E2 P :
+    E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
+  Proof.
+    intros HE.
+    (* Get an [emp] so we can apply [fupd_mask_subseteq]. *)
+    rewrite -{1}[P](left_id emp%I bi_sep).
+    rewrite fupd_mask_subseteq; last exact: HE.
+    rewrite !fupd_frame_r. rewrite left_id. done.
+  Qed.
   Lemma fupd_intro E P : P ={E}=∗ P.
   Proof. by rewrite {1}(fupd_mask_intro_subseteq E E P) // fupd_trans. Qed.
-  Lemma fupd_mask_intro_subseteq_emp E1 E2 : E2 ⊆ E1 → ⊢@{PROP} |={E1,E2}=> |={E2,E1}=> emp.
-  Proof. exact: fupd_mask_intro_subseteq. Qed.
   Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=∗ P.
   Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.
   Lemma fupd_idemp E P : (|={E}=> |={E}=> P) ⊣⊢ |={E}=> P.
@@ -265,7 +276,9 @@ Section fupd_derived.
   Qed.
 
   (** Weaken the first mask of the goal from [E1] to [E2].
-      This lemma is intended to be [iApply]ed. *)
+      This lemma is intended to be [iApply]ed.
+      However, usually you can [iMod (fupd_mask_subseteq E2)] instead and that
+      will be slightly more convenient. *)
   Lemma fupd_mask_weaken {E1} E2 {E3 P} :
     E2 ⊆ E1 →
     ((|={E2,E1}=> emp) ={E2,E3}=∗ P) -∗ |={E1,E3}=> P.
@@ -273,7 +286,7 @@ Section fupd_derived.
     intros HE.
     (* Get an [emp] so we can apply [fupd_intro_mask']. *)
     rewrite -[X in (X -∗ _)](left_id emp%I bi_sep).
-    rewrite {1}(fupd_mask_intro_subseteq_emp E1 E2) //.
+    rewrite {1}(fupd_mask_subseteq E2) //.
     rewrite fupd_frame_r. by rewrite wand_elim_r fupd_trans.
   Qed.
 
diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index 274987333..356b7ff75 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -131,8 +131,7 @@ Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ :
          ([∗ list] v ∈ omap to_val t2', fork_post v) -∗
          (* Under all these assumptions, and while opening all invariants, we
          can conclude [φ] in the logic. After opening all required invariants,
-         one can use [fupd_intro_mask'] or [fupd_mask_weaken] to introduce the
-         fancy update. *)
+         one can use [fupd_mask_subseteq] to introduce the fancy update. *)
          |={⊤,∅}=> ⌜ φ ⌝)) →
   nsteps n (es, σ1) κs (t2, σ2) →
   (* Then we can conclude [φ] at the meta-level. *)
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index e7e7f9bc3..f3458227f 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -116,7 +116,7 @@ Proof.
   rewrite !twp_unfold /twp_pre. destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
   iIntros (σ1 κs n) "Hσ".
-  iApply (fupd_mask_weaken E1); first done. iIntros "Hclose".
+  iMod (fupd_mask_subseteq E1) as "Hclose"; first done.
   iMod ("IH" with "[$]") as "[% IH]".
   iModIntro; iSplit; [by destruct s1, s2|]. iIntros (κ e2 σ2 efs Hstep).
   iMod ("IH" with "[//]") as (?) "(Hσ & IH & IHefs)"; auto.
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index 63e77fdf1..b0880ff8f 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -102,7 +102,7 @@ Proof.
   destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
   iIntros (σ1 κ κs n) "Hσ".
-  iApply (fupd_mask_weaken E1); first done. iIntros "Hclose".
+  iMod (fupd_mask_subseteq E1) as "Hclose"; first done.
   iMod ("H" with "[$]") as "[% H]".
   iModIntro. iSplit; [by destruct s1, s2|]. iIntros (e2 σ2 efs Hstep).
   iMod ("H" with "[//]") as "H". iIntros "!> !>".
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 1e12166da..5b0cc65a3 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -106,9 +106,9 @@ Section tests.
   Lemma test_apply_fupd_intro_mask_subseteq E1 E2 P :
     E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.
   Proof. iIntros. by iApply @fupd_mask_intro_subseteq. Qed.
-  Lemma test_apply_fupd_intro_mask_subseteq_emp E1 E2 P :
+  Lemma test_apply_fupd_mask_subseteq E1 E2 P :
     E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.
-  Proof. iIntros. iFrame. by iApply @fupd_mask_intro_subseteq_emp. Qed.
+  Proof. iIntros. iFrame. by iApply @fupd_mask_subseteq. Qed.
 
   Lemma test_iFrame_embed_persistent (P : PROP) (Q: monPred) :
     Q ∗ □ ⎡P⎤ ⊢ Q ∗ ⎡P ∗ P⎤.
-- 
GitLab