-
Notifications
You must be signed in to change notification settings - Fork 105
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Make hoare_seq_ext and hoare_vcg_seqE wp rules #748
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Cool, thank you for doing that. This should make the setup more consistent overall.
Surprising that it still did need a bunch of changes, but it looks like most of them actually made the proofs shorter, which is good.
A couple of the changes were because of |
apply (wp whenE_throwError_wp hoare_vcg_imp_lift hoare_drop_imps | ||
| strengthen aag_Control_owns_strg | ||
| simp add: o_def del: hoare_True_E_R)+ | ||
apply (wpsimp wp: weak_if_wp) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
could you say something about what weak_if_wp
is or when to use it? (not in the commits, but I've either not heard of it or completely forgot)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
⟦ ⦃P⦄ f ⦃Q⦄; ⦃P'⦄ f ⦃Q'⦄ ⟧ ⟹ ⦃P and P'⦄ f ⦃λr. if C r then Q r else Q' r⦄
In my mind it's for when there's an if
in the postcondition where you don't need to know the if
condition and don't want to lift it across the function for whatever reason.
From memory, my cases in this PR were generally if
conditions on the return value that would have been painful to lift, and where the two branches were either roughly the same or one was a form of True
. As an alternative I probably could have used the simplifier to handle the if
, but this approach with weak_if_wp
was the one I found first.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That's awesome, I hope I won't forget it. It feels better than exciting combination of if_apply_def2
and hoare_drop_imps
, and should work in more cases. It's interesting that this isn't achieved with a wp <some_rule>
, but I guess it does need to shuffle the order.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks like bomb disarming footage. Thank you for digging into this.
We want them as wp rules instead of wp_split rules so that they are used with the correct priority and in combination with wp_comb rules when necessary. This also adds new validE_R and validE_E variants, along with rules for when bind appears inside a validE term. Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
This is no longer necessary now that the nondet monad setup already makes it a wp rule. Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
034bf83
to
bf45b3d
Compare
hoare_seq_ext
was previously made awp
rule in the middle ofainvs
, which was surprising and could lead to different behaviour depending on which session a proof was inside of. This change makes it awp
rule in the baseMonads
setup, along with improving consistency by adding similar rules forvalidE
and its variants.