Rules for Lib, February '25 edition

[michaelmcinerney]

No description provided.

[michaelmcinerney]

Should I give this one the attributes [simp, corres_no_simp], like corres_gets above?

[lsf37]

Better not to make it simp. I would in fact want to remove the simp from corres_gets if that wouldn't break so many proofs.

[lsf37]

This rule doesn't really fit the calculus, because it needs P to unify to something in the first subgoal that then happens to work for discharging the second subgoal. You can only really use this rule when P is already concrete and not schematic (or when you are lucky :-))

Of course, we occasionally do have a concrete P, so it's still useful, but it would be better to have a safe rule instead. Or at least mark this one as unsafe for the weary traveler.

A safer option would be to put it into the assumption, i.e.

lemma corres_assert_opt_assume_lhs:
  assumes "⋀x. P' = Some x ⟹ corres_underlying sr nf nf' r P Q (f x) g"
  shows "corres_underlying sr nf nf' r (P and K (P' != None)) Q (assert_opt P' >>= f) g"

Although this is safe, it might be not as nice to use, so maybe we should have both options.

[lsf37]

Come to think of it, we probably shouldn't call it P'. It's an option value, not a predicate, so it should be x or something like that.

[michaelmcinerney]

I was using this rule in some work in progress, and it was with a concrete guard. But I'm happy to rename the P' and also give your version of the rule. As with a lot of these things, I was just being a good sociopath and following almost exactly what was done in the previous rule, corres_assert_opt_assume

[lsf37]

Yup, that one has exactly the same problems :-). I'm happy with keeping the rule for the concrete guard occasions, but adding the safe version would be nice.

To be fair, our collection of corres rules is a bit of a mess with no clear structure on which rules are good for which situations. It's a bit like forward/backward reasoning in wp -- what parts you want concrete and what parts you want schematic changes with the direction.

[michaelmcinerney]

To save the poor testing in case this needs to be revised again, how about

lemma corres_assert_opt_assume:
  assumes "⋀x. opt = Some x ⟹ corres_underlying sr nf nf' r P Q f (g x)"
  assumes "⋀s. Q s ⟹ opt ≠ None"
  shows "corres_underlying sr nf nf' r P Q f (assert_opt opt >>= g)" using assms
  by (auto simp: bind_def assert_opt_def assert_def fail_def return_def
                 corres_underlying_def split: option.splits)

lemma corres_assert_opt_assume':
  "(⋀x. opt = Some x ⟹ corres_underlying sr nf nf' r P Q f (g x))
   ⟹ corres_underlying sr nf nf' r P (Q and K (opt ≠ None)) f (assert_opt opt >>= g)"
  by (fastforce intro: corres_gen_asm2 stronger_corres_guard_imp corres_assert_opt_assume)

lemma corres_assert_opt_assume_lhs:
  assumes "⋀x. opt = Some x ⟹ corres_underlying sr nf nf' r P Q (f x) g"
  assumes "⋀s. P s ⟹ opt ≠ None"
  shows "corres_underlying sr nf nf' r P Q (assert_opt opt >>= f) g" using assms
  by (auto simp: bind_def assert_opt_def assert_def fail_def return_def
                 corres_underlying_def split: option.splits)

lemma corres_assert_opt_assume_lhs':
  "(⋀x. opt = Some x ⟹ corres_underlying sr nf nf' r P Q (f x) g)
   ⟹ corres_underlying sr nf nf' r (P and K (opt ≠ None)) Q (assert_opt opt >>= f) g"
  by (fastforce intro: corres_gen_asm stronger_corres_guard_imp corres_assert_opt_assume_lhs)

The rule corres_assert_opt_assume is not being used with instantiated schematics anywhere, so I'm pretty sure the blue variables can be renamed without thinks breaking. And I thought that since the argument to assert_opt is a value of some option type, then maybe opt was a reasonable and informative name. I also didn't know what sort of naming we'd like for these, so I've gone with the good ol' apostrophe.

[lsf37]

👍 Those look good!

[michaelmcinerney]

I've forced pushed this to update the commit message of the last commit, now that we're modifying things that were there previously and adding other rules. I thought this PR was small enough that this wouldn't create a problem with reviewing. I hope it's alright.