From e2639ac15b9cdd60cfe26d644601a781e6c60511 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 4 Jul 2020 15:28:43 +0200
Subject: [PATCH] prove the view shift invariant accessor

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

diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index baff426f0..7401005bd 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -77,6 +77,17 @@ Proof.
   by iApply "Hclose".
 Qed.
 
+Lemma vs_inv_acc N E P :
+  ↑N ⊆ E →
+  ⊢ inv N P ={E,E∖↑N}=> ▷ P ∗ ∃ R, R ∗ (R ∗ ▷ P ={E∖↑N,E}=> True).
+Proof.
+  (* FIXME: scope printing is weird, there are [%stdpp]. *)
+  iIntros (?) "!# #Hinv".
+  iMod (inv_acc with "Hinv") as "[$ Hclose]"; first done.
+  iModIntro. iExists (▷ P ={E ∖ ↑N,E}=∗ True)%I. iFrame.
+  iIntros "!# [Hclose HP]". iMod ("Hclose" with "HP"). done.
+Qed.
+
 Lemma vs_alloc N P : ⊢ ▷ P ={↑N}=> inv N P.
 Proof. iIntros "!> HP". by iApply inv_alloc. Qed.
 
-- 
GitLab