Skip to content
Snippets Groups Projects
  1. Oct 27, 2016
    • Ralf Jung's avatar
      fix README links · 6b9eb87e
      Ralf Jung authored
      6b9eb87e
    • Ralf Jung's avatar
      tactics: rename auto_proper => auto_equiv · b863b045
      Ralf Jung authored
      b863b045
    • Ralf Jung's avatar
      improve f_equiv doc · 4653cb6d
      Ralf Jung authored
      4653cb6d
    • Ralf Jung's avatar
      Merge branch 'janno/hoare-notation' into 'master' · 39b9a3c5
      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
      39b9a3c5
    • Ralf Jung's avatar
      add texan triples in uPred_scope · 90ba4346
      Ralf Jung authored
      90ba4346
    • Ralf Jung's avatar
    • Robbert Krebbers's avatar
      Simplify Texan triple notations. · 679d06d1
      Robbert Krebbers authored
      679d06d1
    • Ralf Jung's avatar
      add a later in texan triples · c1120a90
      Ralf Jung authored
      c1120a90
    • Ralf Jung's avatar
      port a lot of our specs to texan triples · 24b6bc9c
      Ralf Jung authored
      24b6bc9c
    • Janno's avatar
      3e2fda9e
  2. Oct 26, 2016
  3. Oct 25, 2016
  4. Oct 22, 2016
  5. Oct 21, 2016
  6. Oct 18, 2016
Loading