Lemmas for StateM Monad manipulation

Stream: Is there code for X?

[Bolton Bailey]

I recently wrote this lemma

@[simp]
def StateM.set_set_then (s : σ) (q : StateM σ β) :
    (do
      set s
      set s'
      q)
    =
    (do
      set (σ := σ) s'
      q) := by
  ext s
  simp only [StateT.run_bind, StateT.run_set, Id.pure_eq, Id.bind_eq]

And several others like it to manipulate State monadic programs. @Mario Carneiro is this the sort of thing that counts as "monadic verification support" on the Std4 roadmap? Should I think about cleaning these lemmas up and PRing them there/does there already exist something like this in Lean/Std/Mathlib?

[Eric Rodriguez]

this should probably be done in the generality of StateT when possible

[Mario Carneiro]

I'm a bit dubious that this actually scales up to a full verification rewrite system

[Mario Carneiro]

my impression playing with similar projects is that you end up just unfolding the do notation into lambdas and state properties about the result of StateT.run ...

[Mario Carneiro]

I mean, it seems fine enough as a rewrite rule, it just doesn't look like enough in general

[Kim Morrison]

I think some combination of @Joe Hendrix and Leo will say more about this in the near future, but "monadic verification support" is a big undertaking, and we very much want a good solution, but are not excited about having partial solutions in Std.

[Bolton Bailey]

Ok then, I won't PR it. Mario, I am indeed trying to unfold properties about the result of StateT.run, but simp kept timing out, so I wrote these lemmas hoping I could do some intermediate simplification to speed things up.

[Mario Carneiro]

That sounds worth investigation, do you have a MWE?

[Bolton Bailey]

Well, I think the issue is that if I minimized it, it probably wouldn't time out any more.

[Bolton Bailey]

Let me try and rework it.

[Bolton Bailey]

Incredible, after months of trying to prove this lemma I have miraculously found the right combination of maxHeartbeats maxRecDepth and order of simp lemma applications to prove it. I have no idea why it didn't work before, I could have sworn I had tried all of these tricks in almost every conceivable permutation.