Show that `plainly` is an internal version of validity.

3e1b5787 · Robbert Krebbers · 2c2f36f5 · 3e1b5787
Commit 3e1b5787 authored Feb 23, 2018 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 7 additions and 0 deletions

theories/bi/derived_laws.v theories/bi/derived_laws.v +7 -0

No files found.
--- 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}.