From 6c6d0d65b32d0d9c943031e9fa709c6c833d7ed1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 16 Mar 2018 13:40:09 +0100
Subject: [PATCH] =?UTF-8?q?Weaken=20BI=20axiom=20`P=20=E2=8A=A2=20<pers>?=
 =?UTF-8?q?=20emp`=20into=20`emp=20=E2=8A=A2=20<pers>=20emp`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The old one is admissable.

Thanks to @jtassaro and @jung.
---
 theories/bi/derived_laws.v | 5 +++++
 theories/bi/interface.v    | 6 +++---
 theories/bi/monpred.v      | 2 +-
 3 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index d60d9a75e..a00d21347 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -742,6 +742,11 @@ Proof.
   apply persistently_mono, impl_elim with P; auto.
 Qed.
 
+Lemma persistently_emp_intro P : P ⊢ <pers> emp.
+Proof.
+  by rewrite -(left_id emp%I bi_sep P) {1}persistently_emp_2 persistently_absorbing.
+Qed.
+
 Lemma persistently_True_emp : <pers> True ⊣⊢ <pers> emp.
 Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.
 
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 33061f942..21a05c617 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -111,7 +111,7 @@ Section bi_mixin.
     bi_mixin_persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P;
 
     (* In the ordered RA model: [ε ≼ core x]. *)
-    bi_mixin_persistently_emp_intro P : P ⊢ <pers> emp;
+    bi_mixin_persistently_emp_2 : emp ⊢ <pers> emp;
 
     bi_mixin_persistently_forall_2 {A} (Ψ : A → PROP) :
       (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a);
@@ -394,8 +394,8 @@ Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
 Lemma persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P.
 Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
 
-Lemma persistently_emp_intro P : P ⊢ <pers> emp.
-Proof. eapply bi_mixin_persistently_emp_intro, bi_bi_mixin. Qed.
+Lemma persistently_emp_2 : (emp : PROP) ⊢ <pers> emp.
+Proof. eapply bi_mixin_persistently_emp_2, bi_bi_mixin. Qed.
 
 Lemma persistently_forall_2 {A} (Ψ : A → PROP) :
   (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a).
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index c7fb6c752..d6ea57fc1 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -303,7 +303,7 @@ Proof.
     rewrite HP /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
   - intros P Q [?]. split=> i /=. by f_equiv.
   - intros P. split=> i. by apply bi.persistently_idemp_2.
-  - intros P. split=> i. by apply bi.persistently_emp_intro.
+  - split=> i. by apply bi.persistently_emp_intro.
   - 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