1. 11 Dec, 2017 2 commits
  2. 04 Dec, 2017 4 commits
  3. 14 Nov, 2017 2 commits
  4. 11 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.
      a38db108
  6. 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.
      f2eaf912
    • 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.
      4e82b191
    • Robbert Krebbers's avatar
      Simplify box axioms. · d18747b6
      Robbert Krebbers authored
      Thanks to discussions with Ales and Amin.
      d18747b6
    • Robbert Krebbers's avatar
      Generalize proofmode. · 52c3006d
      Robbert Krebbers authored
      52c3006d
  7. 25 Oct, 2017 1 commit
    • Robbert Krebbers's avatar
      Consistently de-capitalize acronyms. · a3028b92
      Robbert Krebbers authored
      Rename `UCMRA` → `Ucmra`
      Rename `CMRA` → `Cmra`
      Rename `OFE` → `Ofe` (`Ofe` was already used partially, but many occurences were missing)
      Rename `STS` → `Sts`
      Rename `DRA` → `Dra`
      a3028b92
  8. 07 Apr, 2017 1 commit
  9. 05 Apr, 2017 1 commit
  10. 04 Apr, 2017 1 commit
  11. 09 Mar, 2017 1 commit
  12. 01 Mar, 2017 1 commit
  13. 05 Jan, 2017 2 commits
  14. 03 Jan, 2017 1 commit
  15. 21 Dec, 2016 1 commit
  16. 13 Dec, 2016 1 commit
    • Robbert Krebbers's avatar
      Use different module structuring of uPred. · 766dbcd2
      Robbert Krebbers authored
      This fixes the following issue by JH Jourdan:
      
        The fact of including uPred_[...] in the module uPred (in base_logic.v),
        implies that typeclasses instances are declared twice. Once in module
        uPred and once in module uPred_[...]. This has the unfortunate
        consequence that it has to backtrack to both instances each time the
        first one fails, making failure of type class search for e.g.
        PersistentP potentially exponential.
      
        Goal ((□ ∀ (x1 x2 x3 x4 x5: nat), True -∗ True) -∗ True : iProp Σ).
          Time iIntros "#H".
          Undo.
          Remove Hints uPred_derived.forall_persistent : typeclass_instances.
          Time iIntros "#H".
      
      Thanks to Jason Gross @ Coq club for suggesting this fix.
      766dbcd2
  17. 09 Dec, 2016 1 commit
  18. 05 Dec, 2016 1 commit
    • Robbert Krebbers's avatar
      New definition of contractive. · 176a588c
      Robbert Krebbers authored
      Using this new definition we can express being contractive using a
      Proper. This has the following advantages:
      
      - It makes it easier to state that a function with multiple arguments
        is contractive (in all or some arguments).
      - A solve_contractive tactic can be implemented by extending the
        solve_proper tactic.
      176a588c
  19. 22 Nov, 2016 1 commit
  20. 25 Oct, 2016 1 commit