From ba841bb086d5a392cbaf2bda64875f4fd1f40296 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 7 Jul 2021 11:57:35 +0200
Subject: [PATCH] prove 'weird' monotonicity rule for logatom triple masks

---
 iris/program_logic/atomic.v | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

diff --git a/iris/program_logic/atomic.v b/iris/program_logic/atomic.v
index 97ea858a7..02a1b3fe2 100644
--- a/iris/program_logic/atomic.v
+++ b/iris/program_logic/atomic.v
@@ -143,7 +143,7 @@ Section lemmas.
     rewrite ->!tele_app_bind. iApply "HΦ".
   Qed.
 
-  (* Sequential triples with a persistent precondition and no initial quantifier
+  (** Sequential triples with a persistent precondition and no initial quantifier
   are atomic. *)
   Lemma persistent_seq_wp_atomic e Eo (α : [tele] → iProp) (β : [tele] → TB → iProp)
         (f : [tele] → TB → val Λ) {HP : Persistent (α [tele_arg])} :
@@ -158,8 +158,19 @@ Section lemmas.
     rewrite ->!tele_app_bind. done.
   Qed.
 
-  (* We can open invariants around atomic triples.
-     (Just for demonstration purposes; we always use [iInv] in proofs.) *)
+  (** The polarity of [Eo] is the opposite of what one might expect: if you have
+      an atomic triple with some mask, you can always *shrink* that mask. *)
+  Lemma wp_atomic_mask e Eo1 Eo2 α β f :
+    Eo2 ⊆ Eo1 →
+    atomic_wp e Eo1 α β f -∗
+    atomic_wp e Eo2 α β f.
+  Proof.
+    intros ?. iIntros "Hwp" (Φ) "AU". iApply "Hwp".
+    iApply atomic_update_mask_weaken; done.
+  Qed.
+
+  (** We can open invariants around atomic triples.
+      (Just for demonstration purposes; we always use [iInv] in proofs.) *)
   Lemma wp_atomic_inv e Eo α β f N I :
     ↑N ⊆ Eo →
     atomic_wp e Eo (λ.. x, ▷ I ∗ α x) (λ.. x y, ▷ I ∗ β x y) f -∗
-- 
GitLab