From 5e7d9ca72c2b7bc413e3c887b928fc44cdd436f9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 3 Apr 2018 20:35:23 +0200
Subject: [PATCH] Stronger version of `inv_open` that allows to close
 invariants in a different order.

---
 theories/base_logic/lib/invariants.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 4b73a4465..92c01ed09 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -94,6 +94,20 @@ Proof.
   iApply "HP'". iFrame.
 Qed.
 
+Lemma inv_open_strong E N P :
+  ↑N ⊆ E →
+  inv N P ={E,E∖↑N}=∗ ▷ P ∗ ∀ E', ⌜ ↑N ⊆ E' ⌝ → ▷ P ={E'∖↑N,E'}=∗ True.
+Proof.
+  iIntros (?) "Hinv".
+  iPoseProof (inv_open (↑ N) N P 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". iSpecialize ("H" with "HP").
+  iPoseProof (fupd_mask_frame_r _ _ (E' ∖ ↑ N) with "H") as "H"; first set_solver.
+  by rewrite left_id_L -union_difference_L.
+Qed.
+
 Lemma inv_open_timeless E N P `{!Timeless P} :
   ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ P ∗ (P ={E∖↑N,E}=∗ True).
 Proof.
-- 
GitLab