Recovering information about monadic bind

Stream: general

[Mai]

How can I recover the necessary information to prove this?

structure PosVar where
  n : Nat
  level : Nat

def freshPos (level : Nat) : StateM Nat PosVar :=
  modifyGet fun n => (⟨n, level⟩, n + 1)

example (a : Nat) : StateM Nat Unit := do
  let x <- freshPos a
  have : x.level = a := by
    sorry

[Henrik Böving]

For reasoning about monadic code we would generally recommend using https://lean-lang.org/doc/tutorials/4.28.0-rc1/mvcgen/#mvcgen-tactic-tutorial

[Mai]

I am not sure this helps me here. I would like to have the information about the monad in the computation that is chained to it

[Mai]

Judging by the InfoView, I think using <- loses all information about the source of the value?

[Eric Wieser]

This works but isn't very useful:

import Batteries

structure PosVar where
  n : Nat
  level : Nat

def freshPos (level : Nat) : StateM Nat PosVar :=
  modifyGet fun n => (⟨n, level⟩, n + 1)

theorem freshPosSat (level) : SatisfiesM (fun x => x.level = level) (freshPos level) := by
  refine ⟨modifyGet fun n => (⟨⟨n, level⟩, rfl⟩, n + 1), ?_⟩
  ext <;> simp [freshPos]

example (a : Nat) : StateM Nat Unit := do
  let x <- satisfying (x := freshPos a) (by exact?)
  have : x.1.level = a := by
    exact x.2