From 4f9deccf62eafc564079449bc98c38cc6d867db3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 May 2017 11:33:03 +0200
Subject: [PATCH] =?UTF-8?q?Prove=20(P=20-=E2=88=97=20Q)=20=E2=8A=A3?=
 =?UTF-8?q?=E2=8A=A2=20=E2=88=83=20R,=20R=20=E2=88=97=20=E2=96=A1=20(P=20?=
 =?UTF-8?q?=E2=88=97=20R=20=E2=86=92=20Q)=20and=20dually=20for=20=E2=86=92?=
 =?UTF-8?q?.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/base_logic/derived.v        | 18 ++++++++++++++++++
 theories/base_logic/lib/viewshifts.v |  3 +++
 2 files changed, 21 insertions(+)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index a7e08c030..904a1eef2 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -536,6 +536,24 @@ Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
 Lemma always_laterN n P : □ ▷^n P ⊣⊢ ▷^n □ P.
 Proof. induction n as [|n IH]; simpl; auto. by rewrite always_later IH. Qed.
 
+Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ □ (P ∗ R → Q).
+Proof.
+  apply (anti_symm (⊢)).
+  - rewrite -(right_id True%I uPred_sep (P -∗ Q)%I) -(exist_intro (P -∗ Q)%I).
+    apply sep_mono_r. rewrite -always_pure. apply always_mono, impl_intro_l.
+    by rewrite wand_elim_r right_id.
+  - apply exist_elim=> R. apply wand_intro_l. rewrite assoc -always_and_sep_r'.
+    by rewrite always_elim impl_elim_r.
+Qed.
+Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ □ (P ∧ R -∗ Q).
+Proof.
+  apply (anti_symm (⊢)).
+  - rewrite -(right_id True%I uPred_and (P → Q)%I) -(exist_intro (P → Q)%I).
+    apply and_mono_r. rewrite -always_pure. apply always_mono, wand_intro_l.
+    by rewrite impl_elim_r right_id.
+  - apply exist_elim=> R. apply impl_intro_l. rewrite assoc always_and_sep_r'.
+    by rewrite always_elim wand_elim_r.
+Qed.
 
 (* Later derived *)
 Lemma later_proper P Q : (P ⊣⊢ Q) → ▷ P ⊣⊢ ▷ Q.
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index b786ec65a..a4dd55485 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -79,4 +79,7 @@ Qed.
 
 Lemma vs_alloc N P : ▷ P ={↑N}=> inv N P.
 Proof. iIntros "!# HP". by iApply inv_alloc. Qed.
+
+Lemma wand_fupd_alt E1 E2 P Q : (P ={E1,E2}=∗ Q) ⊣⊢ ∃ R, R ∗ (P ∗ R ={E1,E2}=> Q).
+Proof. rewrite uPred.wand_alt. by setoid_rewrite <-uPred.always_wand_impl. Qed.
 End vs.
-- 
GitLab