From d18747b6d8f56cd126d83db371db31eb1b986fe7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 21 Aug 2017 20:58:16 +0200
Subject: [PATCH] Simplify box axioms.

Thanks to discussions with Ales and Amin.
---
 theories/base_logic/upred.v | 14 +++-----------
 theories/bi/derived.v       |  9 +++++++++
 theories/bi/interface.v     | 10 +++-------
 3 files changed, 15 insertions(+), 18 deletions(-)

diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index b1ade65d7..01f98884d 100644
--- a/theories/base_logic/upred.v
+++ b/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
diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index 75359fd75..7e2b43b7c 100644
--- a/theories/bi/derived.v
+++ b/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).
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 17ebac6b6..524aaf831 100644
--- a/theories/bi/interface.v
+++ b/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.
-- 
GitLab