RFC: Option.get API

When experimenting with partial_fixpoint functions, I noticed that we did not have all the theorems about Option.get (and Option.isSome) that we could have. I was hoping for something like

theorem Option.of_isSome_bind_left {o : Option α} {f : α → Option β} (h : (o >>= f).isSome) :
    o.isSome := by
  cases o <;> simp_all

theorem Option.of_isSome_bind_right {o : Option α} {f : α → Option β} (h : (o >>= f).isSome) :
    (f (o.get (Option.of_isSome_bind_left h))).isSome := by
  cases o <;> simp [h] at h |-

@[simp] theorem Option.get_bind (o : Option α) (f : α → Option β) (h : (o >>= f).isSome) :
    (o >>= f).get h = (f (o.get (Option.of_isSome_bind_left h))).get (Option.of_isSome_bind_right h) := by
  cases o <;> simp at h |-

The use-case is to automate the conversion of a possibly partial function returning Option to a pure one, once one has proved it to be total.

I could envision that a set of such lemmas could exist for every higher-order monadic function, including things like List.mapM, turning them into their non-monadic counterparts:

theorem Option.of_isSome_mapM {xs : List α} {f : α → Option β} (h : (xs.mapM f).isSome) {x : α} (hx : x ∈ xs) :
  (f x).isSome := by
  rw [← List.mapM'_eq_mapM] at h
  induction hx with 
  | head xs =>
    apply Option.of_isSome_bind_left h
  | tail x xs ih =>
    apply ih
    apply Option.of_isSome_bind_left
    apply Option.of_isSome_bind_right h

theorem Option.of_isSome_mapM_cons {x : α} {xs : List α} {f : α → Option β} (h : ((x::xs).mapM f).isSome) :
  (xs.mapM f).isSome := by
  simp only [List.mapM_cons, pure_def, bind_eq_bind] at *
  apply Option.of_isSome_bind_left
  apply Option.of_isSome_bind_right h


theorem Option.get_mapM {xs : List α} {f : α → Option β} (h : (xs.mapM f).isSome) :
  (xs.mapM f).get h = xs.attach.map (fun ⟨x, hx⟩ => (f x).get (Option.of_isSome_mapM h hx)) := by
  induction xs with
  | nil =>
    simp
  | cons x xs ih =>
    simp -- Why does simp not apply Option.get_bind?
    apply (Option.get_bind _ _ _).trans
    apply (Option.get_bind _ _ _).trans
    simp [ih (Option.of_isSome_mapM_cons ‹_›)]

(With the hope that the attach can eventually also be simplified.)

Not a high priority now, but I thought it’s worth noting this down.

For reasons I don’t fully understand theorem Option.get_bind is not a good simp lemma, so there maybe more work needed to make this API as smooth as it could be.

Community Feedback

This came up while discussing the McCarthy 91 function on zulip:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/McCarthy.2091.20function.20using.20partial_fixpoint

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reviewing the existing Option.get and Option.isSome API, then compare it with the proposed bind and List.mapM lemmas in the issue. Investigate why Option.get_bind is not a suitable simp lemma and determine the intended scope of the higher-order monadic API. Done means an agreed, tested API that supports converting proven-total Option computations to pure ones.