From 7041c0433a8b185ab674228daa1a73f17af5f531 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 13 Oct 2018 17:37:47 +0200
Subject: [PATCH] =?UTF-8?q?`(P=20=E2=86=92=20Q)=20=E2=8A=A3=E2=8A=A2=20?=
=?UTF-8?q?=E2=88=83=20R,=20R=20=E2=88=A7=20<pers>=20(P=20=E2=88=A7=20R=20?=
=?UTF-8?q?-=E2=88=97=20Q)`=20holds=20for=20general=20BIs.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
theories/bi/derived_laws_bi.v | 20 ++++++++++----------
1 file changed, 10 insertions(+), 10 deletions(-)
diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index f924a6f9b..8b7b27536 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -962,16 +962,6 @@ Section persistently_affine_bi.
rewrite assoc -persistently_and_sep_r.
by rewrite persistently_elim impl_elim_r.
Qed.
- Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ <pers> (P ∧ R -∗ Q).
- Proof.
- apply (anti_symm (⊢)).
- - rewrite -(right_id True%I bi_and (P → Q)%I) -(exist_intro (P → Q)%I).
- apply and_mono_r. rewrite -persistently_pure.
- apply persistently_intro', wand_intro_l.
- by rewrite impl_elim_r persistently_pure right_id.
- - apply exist_elim=> R. apply impl_intro_l.
- by rewrite assoc persistently_and_sep_r persistently_elim wand_elim_r.
- Qed.
End persistently_affine_bi.
(* The intuitionistic modality *)
@@ -1082,6 +1072,16 @@ Proof.
apply sep_mono; first done. apply and_elim_r.
Qed.
+Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ <pers> (P ∧ R -∗ Q).
+Proof.
+ apply (anti_symm (⊢)).
+ - rewrite -(right_id True%I bi_and (P → Q)%I) -(exist_intro (P → Q)%I).
+ apply and_mono_r. rewrite impl_elim_r -entails_wand //.
+ apply persistently_emp_intro.
+ - apply exist_elim=> R. apply impl_intro_l.
+ rewrite assoc persistently_and_intuitionistically_sep_r.
+ by rewrite intuitionistically_elim wand_elim_r.
+Qed.
Section bi_affine_intuitionistically.
Context `{BiAffine PROP}.
--
GitLab