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 ofwp_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 triple, 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. -
What about some support for introducing the postcondition into the context (avoiding a manual iIntros
all the time)?
Blocked by #130