From 23178b78f6c4ffa5717c5c474867459e1027cf3e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 3 Apr 2018 20:45:48 +0200
Subject: [PATCH] Slightly more easy to use version of strong `inv_open`.

The closing view shift's LHS mask is now universally quantified, which
makes it easier to execute the closing view shift.
---
 theories/base_logic/lib/invariants.v | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 92c01ed09..bff17b568 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -95,17 +95,16 @@ Proof.
 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.
+  ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ ∀ 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.
+  iIntros (E') "HP". iSpecialize ("H" with "HP").
+  iPoseProof (fupd_mask_frame_r _ _ E' with "H") as "H"; first set_solver.
+  by rewrite left_id_L.
 Qed.
 
 Lemma inv_open_timeless E N P `{!Timeless P} :
-- 
GitLab