Simplify box axioms.

Thanks to discussions with Ales and Amin.

theories/base_logic/upred.v

@@ -451,21 +451,13 @@ Proof.
     by unseal.
   - (* P ⊢ □ emp (ADMISSIBLE) *)
     intros P. unfold uPred_emp; unseal; by split=> n x ? _.
-  - (* emp ∧ □ P ⊢ P *)
-    intros P. unseal; split=> n x ? [_ ?]; simpl in *.
-    eauto using uPred_mono, @cmra_included_core, cmra_included_includedN.
   - (* □ P ∗ Q ⊢ □ P (ADMISSIBLE) *)
     intros P Q. move: (uPred_persistently P)=> P'.
     unseal; split; intros n x ? (x1&x2&?&?&_); ofe_subst;
       eauto using uPred_mono, cmra_includedN_l.
-  - (* □ P ∧ (Q ∗ R) ⊢ (□ P ∧ Q) ∗ R (ADMISSIBLE) *)
-    intros P Q R. unseal; split; intros n x ? [? (x1&x2&Hx&?&?)]; simpl in *.
-    exists (core (x1 ⋅ x2) ⋅ x1), x2. split_and!.
-    + by rewrite -assoc cmra_core_l.
-    + eapply uPred_mono; first done. rewrite -{1}cmra_core_idemp Hx.
-      eapply cmra_core_monoN, cmra_includedN_l.
-    + eauto using uPred_mono, cmra_includedN_r.
-    + done.
+  - (* □ P ∧ Q ⊢ (emp ∧ P) ∗ Q *)
+    intros P Q. unseal; split=> n x ? [??]; simpl in *.
+    exists (core x), x; rewrite ?cmra_core_l; auto.
 Qed.
 
 Lemma uPred_sbi_mixin (M : ucmraT) : SBIMixin

theories/bi/derived.v

@@ -872,6 +872,15 @@ Proof. intros P Q; apply persistently_mono. Qed.
 Global Instance persistently_absorbing P : Absorbing (□ P).
 Proof. rewrite /Absorbing=> R. apply persistently_absorbing. Qed.
 
+Lemma persistently_and_sep_assoc_1 P Q R : □ P ∧ (Q ∗ R) ⊢ (□ P ∧ Q) ∗ R.
+Proof.
+  rewrite {1}persistently_idemp_2 persistently_and_sep_elim assoc.
+  apply sep_mono_l, and_intro.
+  - by rewrite and_elim_r absorbing.
+  - by rewrite and_elim_l left_id.
+Qed.
+Lemma persistently_and_emp_elim P : emp ∧ □ P ⊢ P.
+Proof. by rewrite comm persistently_and_sep_elim right_id and_elim_r. Qed.
 Lemma persistently_elim P : □ P ⊢ P ∗ True.
 Proof.
   rewrite -(right_id True%I _ (□ _)%I) -{1}(left_id emp%I _ True%I).

theories/bi/interface.v

@@ -111,10 +111,8 @@ Section bi_mixin.
       □ (∃ a, Ψ a) ⊢ ∃ a, □ Ψ a;
 
     bi_mixin_persistently_emp_intro P : P ⊢ □ emp;
-    bi_mixin_persistently_and_emp_elim P : emp ∧ □ P ⊢ P;
-
     bi_mixin_persistently_absorbing P Q : □ P ∗ Q ⊢ □ P;
-    bi_mixin_persistently_and_sep_assoc_1 P Q R : □ P ∧ (Q ∗ R) ⊢ (□ P ∧ Q) ∗ R;
+    bi_mixin_persistently_and_sep_elim P Q : □ P ∧ Q ⊢ (emp ∧ P) ∗ Q;
   }.
 
   Record SBIMixin := {
@@ -420,12 +418,10 @@ Proof. eapply bi_mixin_persistently_exist_1, bi_bi_mixin. Qed.
 
 Lemma persistently_emp_intro P : P ⊢ □ emp.
 Proof. eapply bi_mixin_persistently_emp_intro, bi_bi_mixin. Qed.
-Lemma persistently_and_emp_elim P : emp ∧ □ P ⊢ P.
-Proof. eapply bi_mixin_persistently_and_emp_elim, bi_bi_mixin. Qed.
 Lemma persistently_absorbing P Q : □ P ∗ Q ⊢ □ P.
 Proof. eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_mixin. Qed.
-Lemma persistently_and_sep_assoc_1 P Q R : □ P ∧ (Q ∗ R) ⊢ (□ P ∧ Q) ∗ R.
-Proof. eapply bi_mixin_persistently_and_sep_assoc_1, bi_bi_mixin. Qed.
+Lemma persistently_and_sep_elim P Q : □ P ∧ Q ⊢ (emp ∧ P) ∗ Q.
+Proof. eapply bi_mixin_persistently_and_sep_elim, bi_bi_mixin. Qed.
 End bi_laws.
 
 Section sbi_laws.