Add rcorres definition, lemmas, and automation

[michaelmcinerney]

This work should be rebased over the work Gerwin has adding the declaring method, and then the automation should be updated to support the del: feature. I will do that once that work is merged. But I thought I would make this PR now so that people could comment on it, just in case it generated a lot of thoughts/comments.

[lsf37]

The declaring method from #950 is now merged.

[michaelmcinerney]

Now including the rcorres_del feature, as well as a method I have used to solve or make progress on rcorres goals via lifting.

Instead of targeting the other PR with Lib rules, this now targets master, and I have included from that PR only one commit that was necessary.

[lsf37]

For consideration:

Suggested change

	using assms
	apply (clarsimp simp: rcorres_def det_wp_def)
	apply (rename_tac s s' rv' t')
	apply (drule_tac x=s' in meta_spec)
	apply (drule_tac x=s in spec)
	apply (force simp: det_wp_def rcorres_def valid_def)
	done
	using assms
	by (force simp: rcorres_def det_wp_def valid_def)

works, but is slow. The by means it doesn't matter much that it is slow, but it's still a trade-off. Personally I like to avoid instantiations when I can, but it is mostly a matter of preference, I guess.

[michaelmcinerney]

I like avoiding instantiations, too, and if you're happy with slow proofs in Lib, I'll go with your suggestion. I sometimes try to imagine how much an extra 2 seconds in Lib that's run all the time will affect the overall time these proofs will run in the future. But I guess that's already a lost cause.

[lsf37]

It won't affect the wall time of a run of Lib -- because of the by the force will run in parallel with the rest and we rarely actually use all cores. This one only affects CPU time and potential impatience :-)

[michaelmcinerney]

Good point. I’ll go with the by, thanks

[lsf37]

What does req stand for? Not that I have a better name. The normal corres rules have something similar with corres_gen_asm. Not quite the same, though.

[michaelmcinerney]

I'm actually not sure what req stands for. I'm just copying the format of corres_req, which also has just a plain schematic in the guard and then produces a new assumption. I would only use this rule when the precondition is schematic and I'm doing a bit of forwards reasoning, and it works nicely for that.

[lsf37]

Ah, that's where it comes from. I don't think I have used that rule yet. The req is a bit obscure, I'm not sure we should proliferate it, but I also don't have a good suggestion. @Xaphiosis or @corlewis do you have any ideas on this one?

[michaelmcinerney]

I do also have monadic_rewrite_req in the other PR, so yeah we should definitely decide on that before we go futher.

[lsf37]

@Xaphiosis, @corlewis do you have any naming input on _req?

[corlewis]

Ah, I've seen corres_req before but also never had an idea of what the req stood for.

For an alternative name, I think the equivalent valid lemma is hoare_gen_asm_spec, so maybe this one could be rcorres_gen_asm_spec?

[lsf37]

I've just ran a grep, and apparently we've been using ccorres_req and ccorres_req quite a bit (>270 occurrences). Maybe we should just leave it as _req after all even though nobody knows what it was supposed to mean. It's probably more confusing if we use the valid convention here than the corres one.

[lsf37]

This works (and I would keep it), but do we also want an assert_l/assert_r style rule for stateAssert? It's a bit more awkward in backwards style, because of the state dependency, so you might only do something like:

lemma rcorres_stateAssert_l:
  "⟦P ⟹ rcorres R (b ()) c R'⟧ ⟹ rcorres (λs s'. R s s' ∧ P s) (stateAssert P xs >>= b) c R'"
  by (fastforce intro: rcorres_assume_pre)

That seems roughly equivalent to what we get in the return_stateAssert rule.

[michaelmcinerney]

Because the P depends on the abstract state, the P in the assumptions for this rule doesn't type check. If you just remove the P, it works, it would then be exactly like corres_stateAssert_r, so I guess that's nice and maybe what we'd like. I think that if we want to add the asserted property to the guard, then we'd need to use the forwards style rule, which has the analogue in corres world of corres_stateAssert_add_assertion. Or maybe my brain isn't sufficiently backwards(-style) and I'm wrong.

[lsf37]

Because the P depends on the abstract state, the P in the assumptions for this rule doesn't type check.

You are right, of course. We could do !!s. P s ==> .., but that is generally not so nice (it's sound but will usually just pollute the goal, because the s is not related to anything, and making it related to the precondition will make the precondition not schematic). So just leaving it out gives us the backwards rule, yes.

[lsf37]

The det_wp in this one is surprising, I'd have thought it would work without. Is there a similar rule that would work without it? Not saying we should get rid of this one, just trying to get an intuition. (I see it's a theme in the other rules as well)

[michaelmcinerney]

This was the argument about not having a conj lift rule for exs_valid, or not being able to go from (Ex x. P x) /\ (Ex x. Q x) to Ex x. P x /\ Q x. We may be able to have one state that satisfies R' and then perhaps another state that satisfies Q', but not one state that satisfies both. Forcing the function to be deterministic means that the unique state satisfies both.

[lsf37]

Oh, of course, that's what it is and that is also why it doesn't behave like any of the other forms of Hoare triples -- the post condition is existential in one and universal in the other state parameter, so you get effects of both. I think that would be worth a comment somewhere, either at this rule or at the definition of rcorres. Because it's really something slightly new.

[michaelmcinerney]

Sure thing. I could even explain there why we might not want to introduce anything about failure into rcorres itself. It might be a bit of an essay, but I could try if you'd like.

[lsf37]

Thanks for adding the explanation, I think that is good. I would add a summary side sentence on the universal/existential duality, will comment above.

[lsf37]

Some suggestions for tweaks and a request for more documentation (mostly examples). But I think this is looking pretty nice!

It's interesting to see where it behaves exactly like Hoare triples and where it deviates -- mostly around failure. Maybe it would correspond more closely to total correctness, but I don't think it quite does that either.

[michaelmcinerney]

I've updated this, addressing all the comments so far, except the experiment section for the lifting method. I'll do that early next week.

I'm expecting that we will want to still tweak things quite a lot, so please let me know if there are any further changes I should make to these changes.

[michaelmcinerney]

Actually, I'm not sure if chapter is the right keyword, or if it's section or subsection that we want. I guess it's chapter to begin with, and then section. But I can change this later.

[michaelmcinerney]

Now with the experiment section, using section instead of chapter, and some adjustments to the comments.

[lsf37]

We should change all of these to:

Suggested change

	apply rcorres
	by simp
	apply rcorres
	apply simp
	done

apply scripts should generally end with done. We use by when it's a one-liner or when there is a good other reason like the last step taking long and therefore benefitting from concurrency.

There are a few in the original PR that I didn't comment on because they looked like they are slow steps (e.g. by force or by (fastforce ..)), but if they are not slow we should also change them to apply/done for consistency.

[lsf37]

Suggested change

	It does not seem possible for us to state an adequate lifting rule for conjunction for
	Overall, because the precondition is universal, but the postcondition is existential,
	it does not seem possible for us to state an adequate lifting rule for conjunction for

[michaelmcinerney]

Do you mean the precondition and the postcondition, or do you mean the concrete state is universal and the abstract state is existential?

[lsf37]

I mean the conditions. The definition is forall s s' in P, there exists t t' in execution such that Q t t', so the P behaves universally and the Q existentially.

Thinking more about it, I wonder if we should change it so that that Q is also universal, but that doesn't make sense if we view Q as a state relation instead of a kind of validity. So probably not.

[michaelmcinerney]

It doesn't make sense to me, but I can add this.

[lsf37]

Which bit doesn't make sense? That a condition behaves universally/existentially? I admit that's not exactly a defined expression, but I thought it carries some intuition at least. If it just confuses people we should not add it.

[michaelmcinerney]

I think that if we were to say the precondition is universal, but the postcondition is existential, then someone would think we're doing something along the lines of "for all preconditions P, there is a postcondition Q, such that...", which is not what we're doing, so might be more confusing than helpful. I think the comment I have there now is way too long, but I can't think of a way to make it both precise and short. I think some will be happy to just go along with the det_wp assumption being there, and for those who are sceptical or interested, the explanation is easy enough to follow.

[lsf37]

I had not thought of that reading. Ok, let's not add anything, your explanation is clear enough.

[lsf37]

The Isabelle convention is without the underscore (unlike LaTeX) -- mostly because the underscore is not rendered as subscript. We could use actual Isabelle subscript notation (that is fine), but it's awkward to type, so we usually don't.

I.e. I would propose just

Suggested change

	From our assumptions, we know that there is there is some pair @{term "(rv_1, t_1)"} in the result
	of @{term f} such that @{term "R' rv_1 rv' t_1 t'"} holds, and that there is some pair
	@{term "(rv_2, t_2)"} in the result of @{term f} such that @{term "Q' rv_2 rv' t_2 t' holds"}.
	From our assumptions, we know that there is there is some pair @{term "(rv1, t1)"} in the result
	of @{term f} such that @{term "R' rv1 rv' t1 t'"} holds, and that there is some pair
	@{term "(rv2, t2)"} in the result of @{term f} such that @{term "Q' rv2 rv' t2 t' holds"}.

[lsf37]

Suggested change

	@{term "(rv_1, t_1) = (rv_2, t_2)"} and therefore that there is a pair @{term "(rv, t)"} in the
	@{term "(rv1, t1) = (rv2, t2)"} and therefore that there is a pair @{term "(rv, t)"} in the

[lsf37]

Nitpick: @{term } is a good default, but if we're referring to a single constant, we should use @{const } because Isabelle will then check that the constant exists, which means you get an error if someone changes the constant and you can update the documentation.

Suggested change

	generalisation of our usual @{term corres_underlying} framework, which allows for us to state a
	generalisation of our usual @{const corres_underlying} framework, which allows for us to state a

(For that to work, the constant has to be declared already, so it often can't be used in the explanation of the constant at the definition place, but it is available everywhere after).

[lsf37]

Suggested change

	@{term Nondet_Monad.bind}, as well as the lifting rules, though there are some important
	@{const Nondet_Monad.bind}, as well as the lifting rules, though there are some important

[lsf37]

Suggested change

	Note that rcorres is not a full generalisation of @{term corres_underlying}, in that it does not
	Note that rcorres is not a full generalisation of @{const corres_underlying}, in that it does not

[lsf37]

Suggested change

	one of the two monads. These lifting rules often require @{term no_fail} assumptions, and so when
	one of the two monads. These lifting rules often require @{const no_fail} assumptions, and so when

[lsf37]

Suggested change

	functions, we will immediately be required to show @{term no_fail} for the composite function
	functions, we will immediately be required to show @{const no_fail} for the composite function

[lsf37]

Suggested change

	interactions with @{term no_fail} includes a rule that allows us to show @{term no_fail} for
	interactions with @{const no_fail} includes a rule that allows us to show @{const no_fail} for

[lsf37]

Suggested change

	@{term corres_underlying} shows the relation between rcorres and @{term corres_underlying}.\<close>
	@{const corres_underlying} shows the relation between rcorres and @{const corres_underlying}.\<close>

[lsf37]

(I've only done this paragraph, because I've just re-read it -- please have a look if there are more instances below. We might as well make it nice while we're here.)

[lsf37]

Now that I've understood the need for the det_wp -- do we really want it to be !!s'?

I think the following would be equivalent

Suggested change

	"\<lbrakk>\<And>s'. det_wp (\<lambda>s. P s s') f; rcorres Q f f' R'; rcorres R f f' Q'\<rbrakk>
	\<Longrightarrow> rcorres
	(\<lambda>s s'. P s s' \<and> Q s s' \<and> R s s')
	"\<lbrakk>det_wp P f; rcorres Q f f' R'; rcorres R f f' Q'\<rbrakk>
	\<Longrightarrow> rcorres
	(\<lambda>s s'. P s \<and> Q s s' \<and> R s s')

because P can always be instantiated as %s. Ex s'. P s s' if we want it to. The only time we'd want the forall form is if we want to use this rule as a forward rule where the P already exists in the rcorres goal and instantiates the one for det_wp.

[michaelmcinerney]

I can make this change, but then I'm not sure how I would use a lemmas statement to get the forwards version. So I think I'd have to write the forwards version out in full. If that's alright, I'll go with that.

[lsf37]

if we decide to change the forall for det_wp above, we should also change it here and below

[lsf37]

Thanks for adding the experiments section, I think that works fine. The new explanations prompted me to go back through some of the details -- have a look what you think.