From fd2acffe5793be48d4260bb35a883ac57ce01e1e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 15 Nov 2017 17:49:44 +0100
Subject: [PATCH] show an alternative characterization of plainly

---
 theories/base_logic/derived.v   | 11 +++++++++++
 theories/base_logic/primitive.v |  2 +-
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index c8c289e43..f8b24ad03 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -978,6 +978,17 @@ Lemma plainly_plainly P `{!Plain P} : ■ P ⊣⊢ P.
 Proof. apply (anti_symm (⊢)); eauto. Qed.
 Lemma plainly_intro P Q `{!Plain P} : (P ⊢ Q) → P ⊢ ■ Q.
 Proof. rewrite -(plainly_plainly P); apply plainly_intro'. Qed.
+Lemma plainly_alt P : ■ P ⊣⊢ P ≡ True.
+Proof.
+  apply (anti_symm (⊢)).
+  - rewrite -prop_ext. apply plainly_intro'. rewrite plainly_elim.
+    apply and_intro; apply impl_intro_r.
+    + apply True_intro.
+    + apply and_elim_l.
+  - rewrite internal_eq_sym (internal_eq_rewrite _ _ (λ P, ■ P)%I).
+    eapply impl_elim; first reflexivity.
+    rewrite plainly_pure. apply True_intro.
+Qed.
 
 Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P.
 Proof. by rewrite -{1}(plainly_plainly P) bupd_plainly. Qed.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 46768bd2e..1e123fa4b 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -650,7 +650,7 @@ Proof.
   - intros i a b; eapply Hf, ucmra_unit_validN.
 Qed.
 
-(* Functions *)
+(* Function extensionality *)
 Lemma ofe_funC_equivI {A B} (f g : A -c> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof. by unseal. Qed.
 Lemma ofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
-- 
GitLab