From 101c4e5da0c82222d0f0d07bcf99501d7c8c4ee2 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 9 May 2018 11:11:05 +0200 Subject: [PATCH] =?UTF-8?q?lemmas=20about=20=E2=96=A1=3Fp=20P=20and=20<aff?= =?UTF-8?q?ine>=3Fp=20P?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- theories/bi/derived_laws_bi.v | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v index f3e5d9502..954707291 100644 --- a/theories/bi/derived_laws_bi.v +++ b/theories/bi/derived_laws_bi.v @@ -1181,6 +1181,9 @@ Proof. destruct p; simpl; auto using intuitionistically_sep. Qed. Lemma intuitionistically_if_idemp p P : □?p □?p P ⊣⊢ □?p P. Proof. destruct p; simpl; auto using intuitionistically_idemp. Qed. +Lemma intuitionistically_if_unfold p P : □?p P ⊣⊢ <affine>?p <pers>?p P. +Proof. by destruct p. Qed. + (* Properties of persistent propositions *) Global Instance Persistent_proper : Proper ((≡) ==> iff) (@Persistent PROP). Proof. solve_proper. Qed. @@ -1288,6 +1291,8 @@ Global Instance sep_affine P Q : Affine P → Affine Q → Affine (P ∗ Q). Proof. rewrite /Affine=>-> ->. by rewrite left_id. Qed. Global Instance affinely_affine P : Affine (<affine> P). Proof. rewrite /bi_affinely. apply _. Qed. +Global Instance affinely_if_affine p P : Affine P → Affine (<affine>?p P). +Proof. destruct p; simpl; apply _. Qed. Global Instance intuitionistically_affine P : Affine (□ P). Proof. rewrite /bi_intuitionistically. apply _. Qed. -- GitLab