From 4811ea4f9483cfa4a0970588aebe026029103283 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 7 May 2016 12:37:02 +0200
Subject: [PATCH] Alternative version of pvs_openI and pvs_closeI.

---
 program_logic/pviewshifts.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index c348df679..96dfa57f5 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -174,6 +174,10 @@ Proof.
   rewrite (pvs_mask_frame _ _ (E1 ∖ E1')); last set_solver.
   by rewrite {2}HEE -!union_difference_L.
 Qed.
+Lemma pvs_openI' E i P : i ∈ E → ownI i P ⊢ (|={E, E ∖ {[i]}}=> ▷ P).
+Proof. intros. etrans. apply pvs_openI. apply pvs_mask_frame'; set_solver. Qed.
+Lemma pvs_closeI' E i P : i ∈ E → (ownI i P ∧ ▷ P) ⊢ (|={E ∖ {[i]}, E}=> True).
+Proof. intros. etrans. apply pvs_closeI. apply pvs_mask_frame'; set_solver. Qed.
 
 Lemma pvs_mask_frame_mono E1 E1' E2 E2' P Q :
   E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' →
-- 
GitLab