From 1f24d0204fd59e731b5723316431be48d6382ef9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 23 Feb 2018 17:34:19 +0100
Subject: [PATCH] Remove admissable rule for `plainly`.

---
 theories/base_logic/upred.v | 2 --
 theories/bi/derived_laws.v  | 7 +++++--
 theories/bi/interface.v     | 5 -----
 theories/bi/monpred.v       | 1 -
 4 files changed, 5 insertions(+), 10 deletions(-)

diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index e9fa2cacb..3afa3312d 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -486,8 +486,6 @@ Proof.
     intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN.
   - (* bi_persistently P ⊢ bi_persistently (bi_persistently P) *)
     intros P. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp.
-  - (* bi_plainly (bi_persistently P) ⊢ bi_plainly P (ADMISSIBLE) *)
-    intros P. unseal; split=> n  x ?? /=. by rewrite -(core_id_core ε).
   - (* (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a) *)
     by unseal.
   - (* bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a) *)
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 0c7b86bd9..4e8803833 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -957,8 +957,11 @@ Proof.
 Qed.
 Lemma plainly_persistently P : bi_plainly (bi_persistently P) ⊣⊢ bi_plainly P.
 Proof.
-  apply (anti_symm _); first apply plainly_persistently_1.
-  by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P).
+  apply (anti_symm _).
+  - rewrite -{1}(left_id True%I bi_and (bi_plainly _)) (plainly_emp_intro True%I).
+    rewrite -{2}(persistently_and_emp_elim P).
+    rewrite !and_alt -plainly_forall_2. by apply forall_mono=> -[].
+  - by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P).
 Qed.
 
 Lemma absorbingly_plainly P : bi_absorbingly (bi_plainly P) ⊣⊢ bi_plainly P.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 227fc6c29..72e484cd7 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -129,8 +129,6 @@ Section bi_mixin.
     (* In the ordered RA model: `core` is idempotent *)
     bi_mixin_persistently_idemp_2 P :
       bi_persistently P ⊢ bi_persistently (bi_persistently P);
-    bi_mixin_plainly_persistently_1 P :
-      bi_plainly (bi_persistently P) ⊢ bi_plainly P;
 
     (* In the ordered RA model [P ⊢ persisently emp] (which can currently still
     be derived from the plainly axioms, which will be removed): `ε ≼ core x` *)
@@ -453,9 +451,6 @@ Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
 Lemma persistently_idemp_2 P :
   bi_persistently P ⊢ bi_persistently (bi_persistently P).
 Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
-Lemma plainly_persistently_1 P :
-  bi_plainly (bi_persistently P) ⊢ bi_plainly P.
-Proof. eapply (bi_mixin_plainly_persistently_1 bi_entails), bi_bi_mixin. Qed.
 
 Lemma persistently_forall_2 {A} (Ψ : A → PROP) :
   (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a).
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 1c216f2bc..c7bedbc19 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -326,7 +326,6 @@ Proof.
   - intros P Q. split=> i. apply bi.sep_elim_l, _.
   - intros P Q [?]. split=> i /=. by f_equiv.
   - intros P. split=> i. by apply bi.persistently_idemp_2.
-  - intros P. split=> i /=. by setoid_rewrite bi.plainly_persistently_1.
   - intros A Ψ. split=> i. by apply bi.persistently_forall_2.
   - intros A Ψ. split=> i. by apply bi.persistently_exist_1.
   - intros P Q. split=> i. apply bi.sep_elim_l, _.
-- 
GitLab