Improve WP_README's description of rule ordering

[corlewis]

This tries to remove ambiguity around the order in which wp, wp_comb and wp_split rules are applied.

[lsf37]

👍 This works for me, but I will defer to others who haven't spent the last few days thinking about the problem :-)

[Xaphiosis]

I had some difficulty understanding this (Department of Redundancy Department might also want to have a word), and so tried to distil it into a less brain-intensive form. Can you check that my understanding is correct, and if so maybe make use of it to tune/update the original?

The 'wp' tool's semantics are defined entirely by these sets of rules.
Selection from a set of rules ('wp' and 'wp_split') or combinators ('wp_comb')
occurs in last-to-first order, i.e. always preferring to apply the theorem most
recently added to a set.
First, each 'wp' rule is attempted in the following order:
- on its own, as an introduction rule
- prefixed by a 'wp_comb' rule (i.e. 'rule wp_comb_rule, rule wp_rule')
If no 'wp' rule can be applied, rules from the 'wp_split' set are attempted
(on their own, without 'wp_comb' prefixes).

[corlewis]

Thank you, that's exactly the sort of feedback that I was hoping for.

The original misunderstanding that I was trying to avoid was the idea that the order of rule application is first all of the wp rules on their own before any attempts prefixed by wp_comb rules, i.e. that no wp_comb rules will be used if any wp rule applies as an introduction rule. The implementation instead iterates through all wp rules, trying each one on it's own and then with the wp_comb rules.

Your phrasing keeps this distinction unambiguous and also improves the overall readability, so I've included it.

[Xaphiosis]

@lsf37 can arm cabin doors and cross-check, otherwise all good from my side

[corlewis]

The original misunderstanding that I was trying to avoid was the idea that the order of rule application is first all of the wp rules on their own before any attempts prefixed by wp_comb rules, i.e. that no wp_comb rules will be used if any wp rule applies as an introduction rule.

As an aside, I sort of think that this alternative order would actually be more intuitive and allow for better control of rule application, but the potential improvements from changing the wp tool like this probably aren't worth the time it would take to update all of the proofs that would break.

[Xaphiosis]

As an aside, I sort of think that this alternative order would actually be more intuitive and allow for better control of rule application, but the potential improvements from changing the wp tool like this probably aren't worth the time it would take to update all of the proofs that would break.

Could you elaborate on why you think that's the case? (that it would be more intuitive etc)

[Xaphiosis]

Yeah, in that case it probably will only lead to confusion. Your argument has merit though. The way we did such a changeover in the past relatively quickly was to update the mechanism, keep the old one as _deprecated, and rip through the proofs (most of which won't care about the change), using _deprecated where thought is needed, and then cleaning up the _deprecated later (which I think you did once).
@lsf37 what do you think?

[lsf37]

I think wp is so fundamental that having both variants around is going to be problematic. If we want to change it, we should put in the effort to change over and then we have clean state again.

In addition to the Corey's ordering idea, I was also thinking last night if it would make sense to have a user-declared distinction between safe and unsafe wp rules, e.g. wp! and wp. The safe rules would get high priority, the unsafe ones low priority. That way, things like hoare_vcg_prop and other convenient, but not quite safe rules could be handled in a more principled way. Another way to think about it would be to distinguish real weakest precondition rules from only somewhat-weak precondition rules, where the actually weakest preconditions rules should be always safe to apply and should not need comb rules.

All of that needs a bit more thinking and experimentation, though.

[lsf37]

@lsf37 can arm cabin doors and cross-check, otherwise all good from my side

👍 good from my side as well.

[corlewis]

Hmm, is there a good way to extract this conversation about wp into its own issue? My feeling is that it's unlikely that we'll explore this idea in detail any time soon but if we do it would be nice to be able to find this discussion again.

[lsf37]

Main options are to copy/paste the important bits or to put a link to the comments into the issue.