1. 28 Feb, 2018 1 commit
  2. 27 Feb, 2018 2 commits
  3. 25 Feb, 2018 1 commit
  4. 23 Feb, 2018 7 commits
  5. 22 Feb, 2018 1 commit
  6. 20 Feb, 2018 1 commit
  7. 13 Feb, 2018 3 commits
  8. 12 Feb, 2018 5 commits
  9. 07 Feb, 2018 3 commits
    • Robbert Krebbers's avatar
      Better framing support for disjunctions. · 2fb90ca6
      Robbert Krebbers authored
      For example, framing `P` in `(P ∨ Q) ∗ R` now succeeds and turns the goal into `R`.
      2fb90ca6
    • Robbert Krebbers's avatar
    • Robbert Krebbers's avatar
      Generic `iAlways` tactic. · 6dc83bcb
      Robbert Krebbers authored
      This commit implements a generic `iAlways` tactic that is not tied to
      `persistently`, `affinely` and `plainly` but can be instantiated with a
      variety of always-style modalities.
      
      In order to plug in an always-style modality, one has to decide for both
      the persistent and spatial what action should be performed upon introducing
      the modality:
      
      - Introduction is only allowed when the context is empty.
      - Introduction is only allowed when all hypotheses satisfy some predicate
        `C : PROP → Prop` (where `C` should be a type class).
      - Introduction will only keep the hypotheses that satisfy some predicate
        `C : PROP → Prop` (where `C` should be a type class).
      - Introduction will clear the context.
      - Introduction will keep the context as-if.
      
      Formally, these actions correspond to the following inductive type:
      
      ```coq
      Inductive always_intro_spec (PROP : bi) :=
        | AIEnvIsEmpty
        | AIEnvForall (C : PROP → Prop)
        | AIEnvFilter (C : PROP → Prop)
        | AIEnvClear
        | AIEnvId.
      ```
      
      An always-style modality is then a record `always_modality` packing together the
      modality with the laws it should satisfy to justify the given actions for both
      contexts.
      6dc83bcb
  10. 02 Feb, 2018 1 commit
  11. 25 Jan, 2018 1 commit
  12. 24 Jan, 2018 1 commit
  13. 20 Jan, 2018 1 commit
  14. 16 Jan, 2018 1 commit
    • Robbert Krebbers's avatar
      Special proof mode class for adding a modality to a goal. · a63f256e
      Robbert Krebbers authored
      This used to be done by using `ElimModal` in backwards direction. Having
      a separate type class for this gets rid of some hacks:
      
      - Both `Hint Mode`s in forward and backwards direction for `ElimModal`.
      - Weird type class precedence hacks to make sure the right instance is picked.
        These were needed because using `ElimModal` in backwards direction caused
        ambiguity.
      a63f256e
  15. 20 Dec, 2017 1 commit
  16. 03 Dec, 2017 1 commit
  17. 01 Nov, 2017 2 commits
  18. 30 Oct, 2017 5 commits
    • Robbert Krebbers's avatar
      Use the sink modality in the proof mode. · f0e57c42
      Robbert Krebbers authored
      Whenever we iSpecialize something whose conclusion is persistent, we now have
      to prove all the premises under the sink modality. This is strictly more powerful,
      as we now have to use just some of the hypotheses to prove the premises, instead of
      all.
      f0e57c42
    • Robbert Krebbers's avatar
    • Robbert Krebbers's avatar
      Generalize iAlways to also introduce ■ modalities. · 386f169a
      Robbert Krebbers authored
      This also applies to the introduction pattern `!#`. Both will now
      introduce as many ■ or □ as possible. This behavior is consistent
      with the dual, `#`, which also gets rid of as many ■ and □ modalities
      as possible.
      386f169a
    • 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
      Generalize proofmode. · 52c3006d
      Robbert Krebbers authored
      52c3006d
  19. 28 Oct, 2017 1 commit
  20. 26 Oct, 2017 1 commit