From 135f1298d6bfab88896342e7545599d80bd4b9d6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 23 Feb 2018 20:22:08 +0100
Subject: [PATCH] Describe `plainly` in terms of equality.

---
 theories/bi/derived_laws.v | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index f43bf74ed..9229c6a02 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1916,7 +1916,17 @@ Proof.
   rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
 Qed.
 
-Lemma plainly_alt P `{!Absorbing P} : bi_plainly P ⊣⊢ P ≡ True.
+Lemma plainly_alt P : bi_plainly P ⊣⊢ bi_affinely P ≡ emp.
+Proof.
+  rewrite -plainly_affinely. apply (anti_symm (⊢)).
+  - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l.
+    + by rewrite affinely_elim_emp left_id.
+    + by rewrite left_id.
+  - rewrite internal_eq_sym (internal_eq_rewrite _ _ bi_plainly).
+    by rewrite -plainly_True_emp plainly_pure True_impl.
+Qed.
+
+Lemma plainly_alt_absorbing P `{!Absorbing P} : bi_plainly P ⊣⊢ P ≡ True.
 Proof.
   apply (anti_symm (⊢)).
   - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
-- 
GitLab