Stating properties of the results of monads

Stream: general

[Eric Wieser]

Is there a nicer way to state "the value returned by a monad satisfies this property"? My attempt was

import control.random

universes u
variables {α : Type u} {g : Type}

/-- Chooses a random element from a list. -/
def list.random [random_gen g] : list α → rand_g g (option α)
| [] := pure none
| l@(h :: t) := do
  ulift.up i ← uliftable.up $ (rand.random (fin t.length.succ) : rand_g g _),
  pure (l.nth_le i i.prop)

/-- When choosing a random element, the result is in the list. -/
lemma list.run_random_mem [random_gen g] (l : list α) (gen : g) :
  ((l.random : rand_g g (option α)).run ⟨gen⟩).fst.elim true (∈ l) :=
begin
  cases l,
  { trivial },
  { exact list.nth_le_mem _ _ _ }
end

but this lemma feels impossible to actually use in any meaninful way

[Reid Barton]

In this case, returning a subtype in the first place seems like the obvious approach

[Eric Wieser]

That only works if you put every property you could possibly care about in the subtype though, right?

[Reid Barton]

Yes but in this case, there is only one such possible property.

[Eric Wieser]

Indeed; but presumably there are cases where this is not so

[Reid Barton]

It could also work more generally; try to write a refined version of the action that returns whatever subtype you're interested in at the moment

[Reid Barton]

I think this is effectively what you have to do in any case, since your goal is that you have some code like m >>= fun a => f a and you want, in the context of f, to also have some h : p a

[Reid Barton]

so you could try to rewrite this to m' >>= fun a => f a.val