From fb1de8a829222a772de741f9eb9a9a9eb15d966d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 6 Dec 2016 13:32:41 +0100
Subject: [PATCH] na_inv: avoid tying the masks together, that makes it
 hard(er) to apply the lemma

---
 base_logic/lib/na_invariants.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/base_logic/lib/na_invariants.v b/base_logic/lib/na_invariants.v
index 2a4fe8013..508b88300 100644
--- a/base_logic/lib/na_invariants.v
+++ b/base_logic/lib/na_invariants.v
@@ -71,14 +71,14 @@ Section proofs.
     iNext. iLeft. by iFrame.
   Qed.
 
-  Lemma na_inv_open tid E N P :
-    ↑N ⊆ E →
-    na_inv tid N P -∗ na_own tid E ={E}=∗ ▷ P ∗ na_own tid (E∖↑N) ∗
-                       (▷ P ∗ na_own tid (E∖↑N) ={E}=∗ na_own tid E).
+  Lemma na_inv_open tid E F N P :
+    ↑N ⊆ E → ↑N ⊆ F →
+    na_inv tid N P -∗ na_own tid F ={E}=∗ ▷ P ∗ na_own tid (F∖↑N) ∗
+                       (▷ P ∗ na_own tid (F∖↑N) ={E}=∗ na_own tid F).
   Proof.
-    rewrite /na_inv. iIntros (?) "#Htlinv Htoks".
+    rewrite /na_inv. iIntros (??) "#Htlinv Htoks".
     iDestruct "Htlinv" as (i) "[% Hinv]".
-    rewrite [E as X in na_own tid X](union_difference_L (↑N) E) //.
+    rewrite [F as X in na_own tid X](union_difference_L (↑N) F) //.
     rewrite [X in (X ∪ _)](union_difference_L {[i]} (↑N)) ?na_own_union; [|set_solver..].
     iDestruct "Htoks" as "[[Htoki $] $]".
     iInv N as "[[$ >Hdis]|>Htoki2]" "Hclose".
-- 
GitLab