-
Notifications
You must be signed in to change notification settings - Fork 106
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
Enlarge the prefix_refinement rule set #738
Conversation
3efa780
to
ff96052
Compare
ff96052
to
ebaa0c2
Compare
(*FIXME: the following lemmas were originally solved by monad_eq, which doesn't yet exist for the | ||
trace monad due to traces making equality more complicated.*) |
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.
I think that's perfectly acceptable for the trace monad (not using monad_eq
). Did you gain an impression on whether it would be feasible to update monad_eq
in a way that would make sense for the trace monad? It's not used that much in the main refinement proofs, so it wouldn't be big loss, but if the work sparked an insight, it'd be good to know.
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.
I think it might be doable but it would be complicated.
The main issue is that for the nondet monad, equality can be nicely separated into in_monad
style set membership and equality of the failure flag, both of which are resolved by rules we want anyway.
However, the trace monad version of in_monad
only handles completed monad results, it doesn't say anything about the trace that leads to the result or about Failed
or Incomplete
results. My guess is that with lemmas about those as well then we could update monad_eq
to work for the trace monad, but there's a good chance that that would end up being more effort than it saves.
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.
Ok, we should definitely defer until we know we want this then, esp since monad_eq
is not used that often.
"triv_refinement aprog cprog = (\<forall>s. cprog s \<subseteq> aprog s)" | ||
|
||
lemmas triv_refinement_elemD = triv_refinement_def[THEN iffD1, rule_format, THEN subsetD] | ||
|
||
lemma triv_refinement_trans: |
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.
Not sure if we did this before, but it'd be nice to have that triv_refinement
is a partial order, i.e. reflexive, transitive, and and antisymmetric. We could even instantiate it into the order class which would make a bunch of consequences of that available. Not that we are likely to need it much, but it'd be a nice setup.
Edit: let me retract the bit about the order class -- if we made it a class instance (if that even works for the type), we would be declaring <
globally for programs. We don't really want that. What would make sense though, is interpreting the order locale for it. That should only make theorems available.
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.
I'm also almost tempted to rename this into trace_refinement
if that name is still available. Because it's not trivial at all, it is actually the classical version of refinement on traces (it's just not data refinement).
\<comment> \<open>FIXME: it would be good to show this but the last assumption needs to be a lot more complicated | ||
and the nondet equivalent isn't used anywhere. | ||
lemma prefix_refinement_propagate_no_fail: | ||
"\<lbrakk>prefix_refinement sr isr osr rvr AR R P Q f f'; | ||
no_fail P' f; \<forall>t0 t. Q t0 t \<longrightarrow> (\<exists>s0 s. P s0 s \<and> sr s0 t0 \<and> isr s t)\<rbrakk> | ||
\<Longrightarrow> no_fail Q' f'" |
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.
It's interesting that this doesn't fall out easily. It's one of the fundamental properties of refinement. We don't make explicit use of it, but it's a good sanity check and it could be a sign that our definition of data refinement is still a bit too complex. No need to resolve this in the short term, but maybe there is a tweak or two yet to be discovered that might make things easier in the future. (It's not unexpected that there would be side conditions since the type for programs is a lot tighter in the nondet monad, whereas for the trace monad there are many traces that don't really make sense as programs. So maybe it's just a reflection of that).
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.
This was one of the things I tried to prove pretty early on in the process of working on all this, so it might be easier now that I have a better understanding of the prefix_refinement
definition. I was sort of thinking to leave it though, until we have a chance to put more thought into how we want to handle failure. Currently it is very different to how corres
handles it.
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.
Having played around with this a bit more, it's actually a bit more complicated than I was previously thinking. The current definition allows us to show refinement between a non-failing abstract function and a failing concrete function, as long as all of the failing traces in the concrete function do not satisfy the rely.
It is almost definitely possible to resolve this, it will just require a bit of thought and possible some worked examples to find the nicest way off expressing things.
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.
No need to do this now. As long as it's flagged we can do this at any time later.
\<comment> \<open>FIXME: is it more usable to have this lemma combined like this or to split it up like Corres_UL's version\<close> | ||
lemma prefix_refinement_gen_asm: | ||
"\<lbrakk>P \<Longrightarrow> prefix_refinement sr isr osr rvr AR R P' Q' f g\<rbrakk> | ||
\<Longrightarrow> prefix_refinement sr isr osr rvr AR R (P' and (\<lambda>_ _. P)) Q' f g" | ||
"\<lbrakk>P \<Longrightarrow> prefix_refinement sr isr osr rvr AR R P' Q' f g\<rbrakk> | ||
\<Longrightarrow> prefix_refinement sr isr osr rvr AR R P' (Q' and (\<lambda>_ _. P)) f g" |
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.
Depends on how this is used. If it is used with instantiation, then having them separate is better. If it is used by matching against a current goal to extract P
, then a single name is better. We could get both but providing two separate names and a lemmas
statement for the collection.
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.
It looks like the corres
version is used both ways, so I've split this up and added lemmas prefix_refinement_gen_asms = ...
like you suggested.
\<comment> \<open>FIXME: an equivalent doesn't seem to exist for corres, do we want it to or does it mean we | ||
shouldn't bother with this?\<close> | ||
lemma prefix_refinement_unless: | ||
"\<lbrakk>G = G'; prefix_refinement sr isr isr rvr AR R P Q a c; rvr () ()\<rbrakk> |
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 would be really good to add to corres. We always unfold unless_def
for no good reason.
\<comment> \<open>FIXME: an equivalent doesn't seem to exist for corres, do we want it to or does it mean we | ||
shouldn't bother with this?\<close> | ||
lemma prefix_refinement_unlessE: |
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.
same as above: good to add to corres
\<comment> \<open>FIXME: Put more thought into whether we want this section, and if not what alternative rules | ||
would we want. The comment copied from Corres_UL suggests we might not want them. | ||
They would be a fair bit more complicated to prove for prefix_refinement.\<close> | ||
section \<open>Some equivalences about liftM and other useful simps\<close> |
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.
Good to remove this section -- even if they were easy to prove, it'd be better not to introduce this temptation for prefix refinement.
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 we want non-simp rules for use when the return relation is already instantiated?
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.
It'd be better to provide the intro
version of those. If those exist, then it doesn't harm to have the equality as well, but if we have only the equality, people will just use it with simp
anyway.
\<comment> \<open>FIXME: not sure why this isn't using \<top>\<top> (or dc)\<close> | ||
abbreviation (input) | ||
"dc2 \<equiv> (\<lambda>_ _. True)" |
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.
It really should be using \<top>\<top>
. Would it be hard to remove?
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.
Very easy to remove, the only concern is that I'm not sure why it was added in the first place.
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.
Esp as an input abbreviation, there is really no point introducing it -- maybe to make it look more familiar. I'd actually rather get rid of dc
as well, it has been the source of much annoyance.
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.
Excellent. This is what I had in mind when we started this.
9ff81c8
to
407d224
Compare
b37e88d
to
ab6b1b9
Compare
These rules are based on equivalent versions from Nondet_Monad_Equations. They were previously left out due to their proofs using the monad_eq tactic, which does not yet exist for the trace monad. Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
This describes an implicit condition that programs need to satisfy to be sensibly combined by parallel. Signed-off-by: Corey Lewis <[email protected]>
The preconditions are generally more interesting and complicated than the relies, so they now come afterwards. Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
ab6b1b9
to
086f0ca
Compare
Signed-off-by: Corey Lewis <[email protected]>
086f0ca
to
dfef55f
Compare
This roughly follows the structure and naming conventions of the
corres_underlying
rule set, as inCorres.thy
andExtraCorres.thy
.