From 836b0fb43986a5a429efdcf1f0d564304903f26f Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Thu, 31 Oct 2024 15:47:52 +0100
Subject: [PATCH] state_update_inv_acc

---
 theories/coneris/wp_update.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/theories/coneris/wp_update.v b/theories/coneris/wp_update.v
index 682c4273..b56d9dc8 100644
--- a/theories/coneris/wp_update.v
+++ b/theories/coneris/wp_update.v
@@ -559,6 +559,17 @@ Section state_update.
     by iMod (inv_alloc with "[$]").
   Qed.
 
+  Lemma state_update_inv_acc P E I N:
+    ↑N ⊆ E -> inv N I -∗ (▷I -∗ state_update (E∖↑N) (P∗▷I)) -∗ state_update E P.
+  Proof.
+    iIntros (Hsubset) "#Hinv H".
+    iInv "Hinv" as "?" "Hclose".
+    iMod ("H" with "[$]") as "[??]".
+    iFrame. iMod ("Hclose" with "[$]") as "_".
+    iModIntro.
+    iApply fupd_mask_intro_subseteq; [set_solver|done].
+  Qed.
+  
   Context {A : cmra} `{i : inG Σ A}.
   Lemma state_update_ra_alloc E (a:A):
     ✓ a -> ⊢ state_update E (∃ γ, own γ a).