This is a bit terse, which is the Isabelle tradition, but we're trying not to do that :-)

As a heading (eg. section) it is fine, but it should be followed by a bit more text that describes what it does and what it is intended for (can be a forward reference to examples after the defs/lemmas are there).

If you're doing using assms you don't need to name them:

For consideration:

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.

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.

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 :-)

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

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.

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.

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?

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

I would suggest adding the following rule for when you don't want to spell out F:

lemma rcorres_assume_pre:
  "⟦⋀s s'. R s s' ⟹ rcorres R f f' R'⟧ ⟹ rcorres R f f' R'"
  by (rule rcorres_req)

Did you mean to put an and (%_ _. F) or something in there?

no F at all in this rule (this is not a replacement of the _req rule, but an additional rule)

Oh OK. I think I have seen rules like this before, but they're not something I've used. I'll add this one in, thanks.

I don't think this behaves nicely in backward reasoning -- requiring R s s' ==> P means that you already need to have a fully instantiated R that is also strong enough for P.

I'd have expected something like

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

Maybe we do want both, though. Your formulation is nice at the beginning for sp-style reasoning when you have a bunch of asserts at the beginning of a function that you want to remove.

I would be using this one for forwards reasoning. I could definitely look to add backwards versions of many of the rules I have here.

Early on when we were discussing rcorres, you said that I shouldn't try to write a complete rule set for it, so the rules I have here are all actually used. But I can look to flesh things out some more.

If you have a backwards rule, you can immediately use it after corres_pre even if you are going forward, so I would usually write the more general rule.

(same as for assert_l)

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.

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.

I would also add rcorres_del here as a parameter and pass it through to rcorres_step, since rcorres will be the main method.

Oh yep, that was a bad oversight. Thanks.

The methods look good, we should add a few examples in an experiment sections for showing intended use. You can also add an RCorres_Test file instead if you don't want to clutter up the theory here, but I think it's probably small enough.

This is also an sp-style rule. Again, I would keep it, because it is useful at the beginning of functions, but I'd also provide a wp rule where the post condition is just Q and the precondition is some transformation of Q. (Probably just Q rv rv' s s' with some conjunction about rrel rv rv', but I haven't investigated further).

We should almost always write implications as nested implications, not as conjunctions. The difference is that nested implications can be solved step-wise, whereas if it is a conjunction, you have to do all in one go. Automation deals better with the first kind.

I would in this case probably make them all meta implications anyway, i.e.

[| !!rv rv' s s'. [| P s s'; f s = Some rv; f' s' = Some rv' |] ==> rrel rv rv'; ...

Interesting rule. I have the feeling there is something more general lurking here, some equivalent of use_valid for normal wp. Probably something like:

  "⟦rcorres P f g Q; P s s'; (rv, t) : f s; (rv', t') : g s'⟧ ⟹ Q rv rv' s s'"

You could then use that to prove the gets_the variant.

I think this would require determinacy for the function f. This will still give us the gets_the variant, so I guess it's OK. Shall I go with that?

Stating det_wp in the assumptions for f is not quite what we want, instead it should be fst (f s) = { (rv, t) }, so that's what I'd put, if we wanted this.

The shared R between the conclusion and the rcorres and no_ofail assumption means you can only use this in forward reasoning at the beginning. If you write it as

you can also use it in the middle of a proof (might be slightly messed up, GitHub is not the best place to type formulas).

We might also a variant of this, where the gets_the rule is already applied to the first assumption, not sure.

These also only work for instantiated preconditions. You'd generally want the preconditions of the two branches to be independent and the precondition of the entire if the conjunction of the two.

(We should also add an _l rule)

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)

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.

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.

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.

This one should move down to where the bind rule is (unless it's needed before)