1. 18 Jul, 2021 1 commit
  2. 07 Jan, 2021 2 commits
  3. 03 Dec, 2020 1 commit
  4. 11 Nov, 2020 1 commit
  5. 05 Nov, 2020 1 commit
  6. 04 Nov, 2020 1 commit
  7. 03 Nov, 2020 3 commits
  8. 30 Oct, 2020 1 commit
  9. 27 Oct, 2020 1 commit
  10. 28 Sep, 2020 1 commit
  11. 10 Sep, 2020 1 commit
  12. 24 May, 2020 1 commit
  13. 13 May, 2019 1 commit
  14. 01 May, 2019 1 commit
  15. 25 Apr, 2019 1 commit
  16. 21 Mar, 2018 1 commit
  17. 19 Mar, 2018 1 commit
  18. 15 Feb, 2018 1 commit
  19. 01 Nov, 2017 1 commit
  20. 30 Oct, 2017 3 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
      Define `Persistent P` as `P ⊢ □ P` instead of `□ P ⊣⊢ P`. · 96501a4f
      Robbert Krebbers authored
      Otherwise, ownership of cores in our ordered RA model will not be persistent.
      96501a4f
    • Robbert Krebbers's avatar
      Generalize proofmode. · 52c3006d
      Robbert Krebbers authored
      52c3006d
  21. 25 Oct, 2017 3 commits
  22. 24 Mar, 2017 1 commit
  23. 21 Mar, 2017 2 commits
  24. 20 Mar, 2017 1 commit
  25. 15 Mar, 2017 4 commits
  26. 06 Feb, 2017 1 commit
  27. 05 Jan, 2017 1 commit
  28. 03 Jan, 2017 1 commit
  29. 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