From e7b3486a2c54cebb3cf3b835a39b08f088898f1d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 21 Feb 2018 10:57:59 +0100
Subject: [PATCH] BI interface: more comments; also simplify a proof

---
 theories/bi/derived_laws.v | 2 +-
 theories/bi/interface.v    | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 4f2c323cf..9064ea39c 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1124,7 +1124,7 @@ Qed.
 
 Lemma affinely_persistently_sep_dup P : □ P ⊣⊢ □ P ∗ □ P.
 Proof.
-  by rewrite -persistently_and_affinely_sep_l affinely_and_r affinely_and idemp.
+  by rewrite -persistently_and_affinely_sep_l affinely_and_r idemp.
 Qed.
 
 Lemma impl_wand_affinely_persistently P Q : (bi_persistently P → Q) ⊣⊢ (□ P -∗ Q).
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index cf3780875..89d31c8c1 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -48,9 +48,9 @@ Section bi_mixin.
   that combine both kinds of resources. In particular, we have an "ordered RA"
   model satisfying all these axioms. For this model, we extend RAs with an
   arbitrary partial order, and up-close resources wrt. that order (instead of
-  extension order).  We demand composition to be monotone wrt. the order.  We
-  define [emp := λ r, ε ≼ r]; persisently is still defined with the core: [□ P
-  := λ r, P (core r)].  *)
+  extension order).  We demand composition to be monotone wrt. the order: [x1 ≼
+  x2 → x1 ⋅ y ≼ x2 ⋅ y].  We define [emp := λ r, ε ≼ r]; persisently is still
+  defined with the core: [□ P := λ r, P (core r)].  *)
 
   Record BiMixin := {
     bi_mixin_entails_po : PreOrder bi_entails;
@@ -142,7 +142,7 @@ Section bi_mixin.
     (* In the ordered RA model: [x ≼ₑₓₜ y → core x ≼ core y] *)
     bi_mixin_persistently_absorbing P Q :
       bi_persistently P ∗ Q ⊢ bi_persistently P;
-    (* In the ordered RA model: [ε ≼ core x] *)
+    (* In the ordered RA model: [x ⋅ core x = core x], AND [ε ≼ core x]. *)
     bi_mixin_persistently_and_sep_elim P Q :
       bi_persistently P ∧ Q ⊢ (emp ∧ P) ∗ Q;
   }.
-- 
GitLab