 31 Oct, 2017 1 commit


Robbert Krebbers authored

 30 Oct, 2017 3 commits


Robbert Krebbers authored
The absence of this axiom has two consequences:  We no longer have `■ (P ∗ Q) ⊢ ■ P ∗ ■ Q` and `□ (P ∗ Q) ⊢ □ P ∗ □ Q`, and as a result, separating conjunctions in the unrestricted/persistent context cannot be eliminated.  When having `(P ∗ ⬕ Q) ∗ P`, we do not get `⬕ Q ∗ P`. In the proof mode this means when having: H1 : P ∗ ⬕ Q H2 : P We cannot say `iDestruct ("H1" with "H2") as "#H1"` and keep `H2`. However, there is now a type class `PositiveBI PROP`, and when there is an instance of this type class, one gets the above reasoning principle back. TODO: Can we describe positivity of individual propositions instead of the whole BI? That way, we would get the above reasoning principles even when the BI is not positive, but the propositions involved are.

Robbert Krebbers authored
Otherwise, ownership of cores in our ordered RA model will not be persistent.

Robbert Krebbers authored
