 28 Oct, 2016 8 commits


Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored
Move global functor to base_logic Sorry to bring this up again, I just think it's important to get this as right as we can, right now. ;) This moves the global functor and dynamic composeable ownership to `base_logic`. The reasoning behind this is that if someone builds another program logic in our base logic, they will likely want to reuse this, so it makes more sense to have it in base_logic than in program_logic. The rule for stuff to be in program_logic is: It depends on the Iris' notion of a language, or on world satisfaction (i.e., on our specific way to do invariants). Thus, `saved_prop` also moves to `base_logic` and becomes reusable by other program logics. (If we want, we can talk about changing this to just "anything that depends on our notion of a language". Is it conceivable that our world satisfaction is reusable?) When we talked about this previously, Robbert raised concerns about the name `iProp`. However, considering that we also have `iTactics` and use `I` for the `uPred_scope`, I feel like the letter "i" has already leaked way beyond `program_logic`, so this PR doesn't actually change anything. If you want, interpret `iProp` as "internal propositions", that even makes sense. ;) Cc @robbertkrebbers @jjourdan See merge request !18

Robbert Krebbers authored
This commit fixes #41.

Robbert Krebbers authored
Otherwise, some ifs are being pretty printed as  or &&.

Robbert Krebbers authored
This is more consistent with our current consensus of not using implication. Also, it allows one to reintroduce the persistent hypothesis into the spatial context.

Robbert Krebbers authored

Ralf Jung authored

 27 Oct, 2016 17 commits


Robbert Krebbers authored

Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored

Robbert Krebbers authored
Since env_cbv does not unfold these apps, we should do it ourselves, to avoid ending up with partially evaluated terms.

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored
Add triple notation for generalized postcondition This changeset defines notation for the Iris style of writing Hoare triples: `{{{ P }}} e {{{ v1 .. vn; T, Q }}} := P ★ (∀ v1 .. vn, Q → Φ T) ⊢ WP e {{ Φ }}` For no good reason the notation is parsing only, although I do not declare it as such. We might want to do that though, since it might be too hard to understand a Hoare triple goal without unfolding it. I have changed the barrier specifications to use the new notation in an attempt to demonstrate their usefulness (or, at a minimum, their applicability). The changes are rather minimal, as you can see. ## Changes First and foremost, the specifications change. (Duh!) Then, there are three kinds of changes to the proofs: 1. The first `iIntros` needs to take care of introducing `Φ`. No big deal, in my opinion. 2. Introducing the spatial assumptions needs one additional level of structure since we go from ```P1 ★ P2 ★ (∀ v, Q v ★ Φ v)``` to ```(P1 ★ P2) ★ (∀ v, Q v ★ Φ v)``` 3. A postcondition of `True` leads to the rather annoying hypothesis `True ★ Φ v`, which (as far as I can tell) cannot be made to behave the same as just (Φ v) in the context of `iFrame`. ## Applicability I have also looked at most other examples of specifications in heap_lang/lib. The notation seems to be applicable to almost all of them. The only place where I spotted an obvious mismatch is par.v, where the current lemmas have a later before the generalized postcondition, as in `... ★ (∀ .., ... ★ ▷ Φ ..) ⊢ WP ..`. We could always add another pair of notations for this special case, I suppose. ## Nomenclature I think "Texan triple" would be a good name, seeing how everything is bigger in Texas, including the number of curly braces. See merge request !9

Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored

Ralf Jung authored

Ralf Jung authored

Janno authored

 26 Oct, 2016 6 commits


Robbert Krebbers authored
This fixes issue 39.

Ralf Jung authored

Ralf Jung authored

JacquesHenri Jourdan authored

JacquesHenri Jourdan authored

Ralf Jung authored

 25 Oct, 2016 9 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
There are now two proof mode tactics for dealing with modalities:  `iModIntro` : introduction of a modality  `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality The behavior of these tactics can be controlled by instances of the `IntroModal` and `ElimModal` type class. We have declared instances for later, except 0, basic updates and fancy updates. The tactic `iMod` is flexible enough that it can also eliminate an updates around a weakest pre, and so forth. The corresponding introduction patterns of these tactics are `!>` and `>`. These tactics replace the tactics `iUpdIntro`, `iUpd` and `iTimeless`. Source of backwards incompatability: the introduction pattern `!>` is used for introduction of arbitrary modalities. It used to introduce laters by stripping of a later of each hypotheses.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
And also rename the corresponding proof mode tactics.
