From 65e4effad8eaf78332d7b29fff666a17db2e447b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 21 Feb 2016 20:20:57 +0100
Subject: [PATCH] prove pvs_sep

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

diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 189e50eb8..5ccf36ab2 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -159,6 +159,9 @@ Proof. intros ->. rewrite pvs_frame_l. apply pvs_mono, wand_elim_l. Qed.
 Lemma pvs_wand_r E1 E2 P Q R :
   P ⊑ (|={E1,E2}=> Q) → (P ★ (Q -★ R)) ⊑ (|={E1,E2}=> R).
 Proof. rewrite comm. apply pvs_wand_l. Qed.
+Lemma pvs_sep E P Q:
+  ((|={E}=> P) ★ (|={E}=> Q)) ⊑ (|={E}=> P ★ Q).
+Proof. rewrite pvs_frame_r pvs_frame_l pvs_trans //. set_solver. Qed.
 
 Lemma pvs_mask_frame' E1 E1' E2 E2' P :
   E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' →
-- 
GitLab