"Internalizing" external reasoning about monadic actions (SatisfiesM)

[Ericson2314]

I have read the docs on SatisfiesM and appreciate the humility about ergonomics. But my question is not about how annoying something is, but whether it's possible at all.

It's great to be able to reason about Monodic programs externally, so the original program is not given the impossible tax of anticipating all proofs that might be desired in the future and providing them internally. At the same time, if it is only possible to reason externally, then batteries doesn't help us write dependent monadic programs, and just helps us reason post-hoc about "simple" mondic programs. I hope this isn't true.

I was trying to figure out how to "internalize" a SatisfiesM. I was having trouble at first figuring out what exactly that entailed, and in https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/.E2.9C.94.20Proofs.20inside.20monads/near/466762282 I ended up with

def internalizePostCondition
  {m : Type u -> Type u_2}
  [Monad m]
  [LawfulMonad m]
  (action : {action: m t // SatisfiesM p action})
  : m {value: t // p value}
  := sorry

But I am not sure how to prove this; it would seem to require an EvenMoreLawfulMonad. Can anyone point me in the right direction?

[digama0]

#1029 is very relevant to this issue and may close it

[Ericson2314]

Yes I think it closes it!