Document BI axioms in terms of the axioms in the ordered RA model.

theories/bi/interface.v

@@ -112,20 +112,27 @@ Section bi_mixin.
     bi_mixin_plainly_absorbing P Q : bi_plainly P ∗ Q ⊢ bi_plainly P;
 
     (* Persistently *)
+    (* In the ordered RA model: `core` is monotone *)
     bi_mixin_persistently_mono P Q :
       (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q;
+    (* In the ordered RA model: `core` is idempotent *)
     bi_mixin_persistently_idemp_2 P :
       bi_persistently P ⊢ bi_persistently (bi_persistently P);
     bi_mixin_plainly_persistently_1 P :
       bi_plainly (bi_persistently P) ⊢ bi_plainly P;
 
+    (* In the ordered RA model [P ⊢ □ emp] (which can currently still be derived
+    from the plainly axioms, which will be removed): `ε ≼ core x` *)
+
     bi_mixin_persistently_forall_2 {A} (Ψ : A → PROP) :
       (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a);
     bi_mixin_persistently_exist_1 {A} (Ψ : A → PROP) :
       bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a);
 
+    (* 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] *)
     bi_mixin_persistently_and_sep_elim P Q :
       bi_persistently P ∧ Q ⊢ (emp ∧ P) ∗ Q;
   }.

[Ralf Jung]

You're assuming here that persistently is defined as "holds for the core"; that should be mentioned somewhere.

[Robbert Krebbers]

This documentation is clearly insider only at the moment. It requires some more text, namely what's the ordered RA model, and how do we interpret the main connectives.

[Robbert Krebbers]

Would you like to write a couple of paragraphs documentation in this file about that?

[Ralf Jung]

I can try, but I think you know more about that model than I do. You have seen it's Coq version. ^ ^

[Ralf Jung]

Done: https://gitlab.mpi-sws.org/FP/iris-coq/commit/f30188af9d3846512c2d89260f9474358a333be0

[Ralf Jung]

Wait, really? Shouldn't this follow from [P ⊢ □ emp] then, or exhibit some other connection to that axiom?

[Robbert Krebbers]

If you could prove it follows from that, (or P ⊢ □ emp follows from this property) that would be great. I tried & failed.