- Oct 27, 2016
-
-
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 post-condition 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 post-condition 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 post-condition, 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
-
- Oct 26, 2016
-
-
Robbert Krebbers authored
This fixes issue 39.
-
Ralf Jung authored
-
Ralf Jung authored
-
Jacques-Henri Jourdan authored
-
Jacques-Henri Jourdan authored
-
Ralf Jung authored
-
- Oct 25, 2016
-
-
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.
-
Robbert Krebbers authored
-
- Oct 22, 2016
-
-
Ralf Jung authored
-
Ralf Jung authored
docs: make the borders slightly larger This makes it so that lines of text don't become so ridiculously long and are easier to read. What do you think @robbertkrebbers @jjourdan ? See merge request !17
-
Ralf Jung authored
-
Ralf Jung authored
docs: make the borders slightly larger, so that lines of text dont become so ridicolously long and are easier to read
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
- Oct 21, 2016
- Oct 18, 2016
-
-
Robbert Krebbers authored
-