From 249edc6c19f37c0dfaf8ac783eae790d51d3c558 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Sun, 3 Dec 2017 21:29:35 +0100 Subject: [PATCH] More properties about the relation between wand and impl. --- theories/bi/derived.v | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/theories/bi/derived.v b/theories/bi/derived.v index 29a897439..e19e4d577 100644 --- a/theories/bi/derived.v +++ b/theories/bi/derived.v @@ -1339,6 +1339,13 @@ Proof. by rewrite -persistently_and_affinely_sep_l affinely_and_r affinely_and idemp. Qed. +Lemma wand_impl_affinely_persistently P Q : (□ P -∗ Q) ⊣⊢ (bi_persistently P → Q). +Proof. + apply (anti_symm (⊢)). + - apply impl_intro_l. by rewrite persistently_and_affinely_sep_l wand_elim_r. + - apply wand_intro_l. by rewrite -persistently_and_affinely_sep_l impl_elim_r. +Qed. + (* The combined affinely plainly modality *) Lemma affinely_plainly_elim P : ■P ⊢ P. Proof. apply plainly_and_emp_elim. Qed. @@ -1377,6 +1384,9 @@ Proof. by rewrite -plainly_and_affinely_sep_l affinely_and_r affinely_and idemp. Qed. +Lemma wand_impl_affinely_plainly P Q : (■P -∗ Q) ⊣⊢ (bi_plainly P → Q). +Proof. by rewrite -(persistently_plainly P) wand_impl_affinely_persistently. Qed. + (* Conditional affinely modality *) Global Instance affinely_if_ne p : NonExpansive (@bi_affinely_if PROP p). Proof. solve_proper. Qed. -- GitLab