From 9f605f77dfb069b7d43e080bb1b8c50b55bd04ef Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 7 Mar 2017 16:40:50 +0100
Subject: [PATCH] later-P and static-borrow-of-P are view-shift equivalent

---
 theories/lifetime/lifetime.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index a2439938..ad2291ec 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -63,6 +63,20 @@ Proof.
   - iIntros "!> !>". iMod "Hclose" as "_". by iApply (bor_fake with "LFT").
 Qed.
 
+Lemma later_bor_static E P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ ▷ P ={E}=∗ &{static} P.
+Proof.
+  iIntros (?) "#LFT HP". iMod (bor_create with "LFT HP") as "[$ _]"; done.
+Qed.
+Lemma bor_static_later E P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{static} P ={E}=∗ ▷ P.
+Proof.
+  iIntros (?) "LFT HP". iMod (bor_acc _ 1%Qp with "LFT HP []") as "[$ _]"; try done.
+  iApply lft_tok_static.
+Qed.
+
 Lemma bor_later_tok E q κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}(▷ P) -∗ q.[κ] ={E}▷=∗ &{κ}P ∗ q.[κ].
-- 
GitLab