1. 05 Nov, 2016 1 commit
  2. 04 Nov, 2016 1 commit
  3. 03 Nov, 2016 4 commits
    • Robbert Krebbers's avatar
      Rename "inc" of counter into "incr". · 7527bd61
      Robbert Krebbers authored
      7527bd61
    • Robbert Krebbers's avatar
      Forgot something as part of 7d74f654. · 3f678b90
      Robbert Krebbers authored
      3f678b90
    • Robbert Krebbers's avatar
      Merge branch 'new_star' into 'master' · 7d74f654
      Robbert Krebbers authored
      Use symbol ∗ for separating conjunction.
      
      The old choice for ★ was a arbitrary: the precedence of the ASCII asterisk * was fixed at a wrong level in Coq, so we had to pick another symbol. The ★ was a random choice from a unicode chart.
      
      The new symbol ∗ (as proposed by David Swasey) corresponds better to conventional practise and matches the symbol we use on paper.
      
      See merge request !21
      7d74f654
    • Robbert Krebbers's avatar
      Use symbol ∗ for separating conjunction. · cc31476d
      Robbert Krebbers authored
      The old choice for ★ was a arbitrary: the precedence of the ASCII asterisk *
      was fixed at a wrong level in Coq, so we had to pick another symbol. The ★ was
      a random choice from a unicode chart.
      
      The new symbol ∗ (as proposed by David Swasey) corresponds better to
      conventional practise and matches the symbol we use on paper.
      cc31476d
  4. 02 Nov, 2016 1 commit
    • Ralf Jung's avatar
      Merge branch 'ralf/texan' into 'master' · 6cb76aaa
      Ralf Jung authored
      Change the way we handle view shifts in post-conditions
      
      Now we try to avoid adding them unnecessarily, so we don't have to remove them automatically any more.
      
      The overall tally in the proofs (i.e., excluding changes in proof mode and lifting lemmas) is: 14 removed `iModIntro` (and equivalent tactics), 7 insertions of `wp_fupd`. So it seems we actually more often do not need that final update than we do need it. Not to mention this also simplifies the lifting lemmas and the proof mode, doing less unnecessary work (adding updates and then removing them again).
      
      On the minus side, *if* the update is missing, unexperienced users will have a hard time figuring out what to do. The change typically needs to be made at the beginning of the proof, the problem only surfaces at the end. This could be mitigated by providing a tactic for proving texan triples that does the `wp_fupd` (and the introducing the `\Phi`). While this would re-add most of the 14 removed `iModIntro`, we could still keep the simplified lifting lemmas and proof mode.
      
      Cc @robbertkrebbers @jjourdan what do you think?
      
      See merge request !20
      6cb76aaa
  5. 01 Nov, 2016 6 commits
  6. 31 Oct, 2016 4 commits
  7. 30 Oct, 2016 1 commit
  8. 28 Oct, 2016 10 commits
  9. 27 Oct, 2016 12 commits
    • Robbert Krebbers's avatar
      Fix typo. · 634fdbb6
      Robbert Krebbers authored
      634fdbb6
    • Ralf Jung's avatar
      97c4d39f
    • Ralf Jung's avatar
      Makefile: hide recursive make calls · 8559d95c
      Ralf Jung authored
      8559d95c
    • Robbert Krebbers's avatar
      02001691
    • Robbert Krebbers's avatar
      Fix inefficiency in proof mode. · a1be30d3
      Robbert Krebbers authored
      Since env_cbv does not unfold these apps, we should do it ourselves,
      to avoid ending up with partially evaluated terms.
      a1be30d3
    • Ralf Jung's avatar
      be019f76
    • Ralf Jung's avatar
    • 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