wp_apply/Texan triple improvements (#138) · Issues · Iris / Iris

wp_apply/Texan triple improvements

wp_apply could be able to apply a total WP when the goal is a partial WP, removing some duplication in heap_lang/lib.
wp_apply could automatically try to prove that the expression is not a value, and then apply some variant of wp_step. This would remove the need to have a \later in the definition of Texan triples, making them equivalent to a WP in all cases (as opposed to just the non-value case). I think right now I regret that we decided for Texan triples to contain the \later, this makes them slightly harder to teach and destroys their equivalence with WP/"normal" triples.
[More far-fetched?] Make the precondition of Texan triples a list of assertions, so that we can (a) desugar them to something curried, and (b) not have silly True preconditions when the list is empty.
When proving a tirple, the postcondition could be wrapped in a fancy update, removing the need to rewrite -wp_fupd in some of our proofs. Of course, when applying a triple, that update must not be in the way.

Blocked by #130

* `wp_apply` could be able to apply a total WP when the goal is a partial WP, removing some duplication in heap_lang/lib.
* `wp_apply` could automatically try to prove that the expression is not a value, and then apply some variant of `wp_step`.  This would remove the need to have a `\later` in the definition of Texan triples, making them equivalent to a WP in all cases (as opposed to just the non-value case).  I think right now I regret that we decided for Texan triples to contain the `\later`, this makes them slightly harder to teach and destroys their equivalence with WP/"normal" triples.
* [More far-fetched?] Make the precondition of Texan triples a list of assertions, so that we can (a) desugar them to something curried, and (b) not have silly `True` preconditions when the list is empty.
* When proving a tirple, the postcondition could be wrapped in a fancy update, removing the need to `rewrite -wp_fupd` in some of our proofs. Of course, when applying a triple, that update must not be in the way.

Blocked by #130

Edited Feb 20, 2019 by Ralf Jung