Proving facts about the "inner value" of monadic computation

Stream: lean4

[cmlsharp]

Suppose I have a function f [Monad m] : a -> m (List a). Where the list f returns is always non-empty. I'd like to write a theorem that says this is true.

How would I even phrase this in a theorem statement? Something like (. \neq []) <$> f a = pure True type checks, but it is of course wrong. The goal of this helper lemma is to prove that it is always legal to do e.g.

do
    let list <- f a
    let last = list.getLast

I suppose I could modify f to return an m {l : List a // l \neq []} or something, but that would be somewhat unfortunate as it would require cluttering the definition of f with these proofs.

[Aaron Liu]

Well I know of docs#SatisfiesM

[Aaron Liu]

you might find something better in @loogle "Std.Do"

[loogle]

:search: Std.Do.SVal.StateTuple, Std.Do.SVal, and 662 more

[Kim Morrison]

@cmlsharp, please see https://lean-lang.org/doc/reference/latest/The--mvcgen--tactic/Tutorial___-Verifying-Imperative-Programs-Using--mvcgen/#mvcgen-tactic-tutorial

[Eric Wieser]

Kim, does that provide something like docs#satisfying that could be used in the example in this thread?

[Kim Morrison]

Yes, you can write Hoare triples that I think are more expressive than anything SatisfiesM can provide. But I've barely used it myself, and found it quite confusing when I tried!