Weaken BI axiom `P ⊢ <pers> emp` into `emp ⊢ <pers> emp`.

The old one is admissable.

Thanks to @jtassaro and @jung.

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.
 

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).

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, _.