From 3e1b578728becf13dd4500264ce3cfa8ee2a1c4b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Fri, 23 Feb 2018 18:21:43 +0100
Subject: [PATCH] Show that `plainly` is an internal version of validity.
---
theories/bi/derived_laws.v | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index ae10b0643..f43bf74ed 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1083,6 +1083,13 @@ Qed.
Lemma impl_wand_plainly_2 P Q : (bi_plainly P -∗ Q) ⊢ (bi_plainly P → Q).
Proof. apply impl_intro_l. by rewrite plainly_and_sep_l_1 wand_elim_r. Qed.
+Lemma valid_plainly P : bi_valid (bi_plainly P) ↔ bi_valid P.
+Proof.
+ rewrite /bi_valid. split; intros HP.
+ - by rewrite -(idemp bi_and emp%I) {2}HP plainly_and_emp_elim.
+ - by rewrite (plainly_emp_intro emp%I) HP.
+Qed.
+
Section plainly_affinely_bi.
Context `{BiAffine PROP}.
--
GitLab