Lemmas about OptionT

theorem OptionT.monad_pure_eq_pure {m : Type u → Type v} {α : Type u} [Monad m] (x : α) : pure x = OptionT.pure x

theorem OptionT.monad_bind_eq_bind {m : Type u → Type v} {α β : Type u} [Monad m] (x : OptionT m α) (y : α → OptionT m β) : x >>= y = x.bind y

theorem OptionT.liftM_def {m : Type u → Type v} [Monad m] {α : Type u} (x : m α) : liftM x = OptionT.lift x

def OptionT.mapM {m : Type u → Type v} {n : Type u → Type w} [AlternativeMonad n] (f : {α : Type u} → m α → n α) {α : Type u} (x : OptionT m α) : n α

Canonical lifting of a map from m α → n α to one from OptionT m α → n α given an Alternative n instance to handle failure.

def OptionT.mapM' {m : Type u → Type v} {n : Type u → Type w} [Monad m] [AlternativeMonad n] [LawfulMonad n] [LawfulAlternative n] (f : m →ᵐ n) : OptionT m →ᵐ n

Bundled version of mapM. dtumad: we should probably just pick one of these (probably the hom class non-bundled approach).

@[simp]

theorem OptionT.mapM'_lift {α : Type u} {m : Type u → Type v} {n : Type u → Type w} [Monad m] [AlternativeMonad n] [LawfulMonad n] [LawfulAlternative n] (f : m →ᵐ n) (x : m α) : (fun {α : Type u} (x : OptionT m α) => (OptionT.mapM' f).toFun α x) (OptionT.lift x) = (fun {α : Type u} (x : m α) => f.toFun α x) x

@[simp]

theorem OptionT.mapM'_failure {α : Type u} {m : Type u → Type v} {n : Type u → Type w} [Monad m] [AlternativeMonad n] [LawfulMonad n] [LawfulAlternative n] (f : m →ᵐ n) : (fun {α : Type u} (x : OptionT m α) => (OptionT.mapM' f).toFun α x) failure = failure

@[simp]

theorem OptionT.mk_bind {α β : Type u} (m : Type u → Type v) [Monad m] [LawfulMonad m] (mx : m α) (my : α → m (Option β)) : OptionT.mk (mx >>= my) = do let x ← liftM mx OptionT.mk (my x)

@[simp]

theorem OptionT.liftM_elimM {m : Type u_1 → Type u_2} [Monad m] {α β : Type u_1} (x : m (Option α)) (y : m β) (z : α → m β) {n : Type u_1 → Type u_3} [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] : liftM (Option.elimM x y z) = Option.elimM (liftM x) (liftM y) fun (x : α) => liftM (z x)

theorem OptionT.map_mk_bind_eq_of_body {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β γ δ : Type u} (sample : m α) (body₁ : α → m (Option β)) (body₂ : α → m (Option γ)) (f : β → δ) (post : α → γ → δ) (hBody : ∀ (a : α), Option.map f <$> body₁ a = Option.map (post a) <$> body₂ a) : (f <$> OptionT.mk do let a ← sample body₁ a) = OptionT.mk do let a ← sample let r ← body₂ a pure (Option.map (post a) r)

Rewrite a mapped OptionT.mk'd bind through a pointwise Option.map relation between two bodies: if Option.map f <$> body₁ a agrees with Option.map (post a) <$> body₂ a for every sample a, then mapping f over OptionT.mk (sample >>= body₁) equals OptionT.mk of binding body₂ and post-processing with post. Useful for re-expressing a mapped OptionT computation through an alternative body with sample-dependent post-processing.