1. 14 Dec, 2017 1 commit
  2. 11 Dec, 2017 1 commit
  3. 04 Dec, 2017 2 commits
  4. 14 Nov, 2017 1 commit
  5. 01 Nov, 2017 1 commit
    • Jacques-Henri Jourdan's avatar
      Remove notations for bi_bare and bi_persistently. · a38db108
      Jacques-Henri Jourdan authored
      (□ P) now means (bi_bare (bi_persistently P)).
      This is motivated by the fact that these two modalities are rarely
      used separately.
      In the case of an affine BI, we keep the □ notation. This means that a
      bi_bare is inserted each time we use □. Hence, a few adaptations need
      to be done in the proof mode class instances.
  6. 31 Oct, 2017 1 commit
  7. 30 Oct, 2017 4 commits
    • 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.
    • Robbert Krebbers's avatar
      Remove axiom that emp is timeless. · 4e82b191
      Robbert Krebbers authored
      As Aleš observed, in the ordered RA model it is not, unless the order on the
      unit is timeless.
    • Robbert Krebbers's avatar
      Simplify box axioms. · d18747b6
      Robbert Krebbers authored
      Thanks to discussions with Ales and Amin.
    • Robbert Krebbers's avatar
      Generalize proofmode. · 52c3006d
      Robbert Krebbers authored