• Robbert Krebbers's avatar
    Drop positivity axiom of the BI canonical structure. · f2eaf912
    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.
    f2eaf912
own.v 8.61 KB