@[simp]

theorem monadLift_self {α : Type u} {m : Type u → Type v} (x : m α) : monadLift x = x

class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop

A functor satisfies the functor laws.

The Functor class contains the operations of a functor, but does not require that instances prove they satisfy the laws of a functor. A LawfulFunctor instance includes proofs that the laws are satisfied. Because Functor instances may provide optimized implementations of mapConst, LawfulFunctor instances must also prove that the optimized implementation is equivalent to the standard implementation.

• map_const {α β : Type u} : Functor.mapConst = Functor.map ∘ Function.const β

  The mapConst implementation is equivalent to the default implementation.

• id_map {α : Type u} (x : f α) : id <$> x = x

  The map implementation preserves identity.

• comp_map {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α) : (h ∘ g) <$> x = h <$> g <$> x

  The map implementation preserves function composition.

@[simp]

theorem id_map' {f : Type u_1 → Type u_2} {α : Type u_1} [Functor f] [LawfulFunctor f] (x : f α) : (fun (a : α) => a) <$> x = x

@[simp]

theorem Functor.map_map {f : Type u_1 → Type u_2} {α β γ : Type u_1} [Functor f] [LawfulFunctor f] (m : α → β) (g : β → γ) (x : f α) : g <$> m <$> x = (fun (a : α) => g (m a)) <$> x

theorem Functor.map_unit {f : Type u_1 → Type u_2} [Functor f] [LawfulFunctor f] {a : f PUnit} : (fun (x : PUnit) => PUnit.unit) <$> a = a

class LawfulApplicative (f : Type u → Type v) [Applicative f] extends LawfulFunctor f : Prop

An applicative functor satisfies the laws of an applicative functor.

The Applicative class contains the operations of an applicative functor, but does not require that instances prove they satisfy the laws of an applicative functor. A LawfulApplicative instance includes proofs that the laws are satisfied.

Because Applicative instances may provide optimized implementations of seqLeft and seqRight, LawfulApplicative instances must also prove that the optimized implementation is equivalent to the standard implementation.

• map_const {α β : Type u} : Functor.mapConst = Functor.map ∘ Function.const β
• id_map {α : Type u} (x : f α) : id <$> x = x
• comp_map {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α) : (h ∘ g) <$> x = h <$> g <$> x
• seqLeft_eq {α β : Type u} (x : f α) (y : f β) : x <* y = Function.const β <$> x <*> y

  seqLeft is equivalent to the default implementation.

• seqRight_eq {α β : Type u} (x : f α) (y : f β) : x *> y = Function.const α id <$> x <*> y

  seqRight is equivalent to the default implementation.

• pure_seq {α β : Type u} (g : α → β) (x : f α) : pure g <*> x = g <$> x

  pure before seq is equivalent to Functor.map.

  This means that pure really is pure when occurring immediately prior to seq.

• map_pure {α β : Type u} (g : α → β) (x : α) : g <$> pure x = pure (g x)

  Mapping a function over the result of pure is equivalent to applying the function under pure.

  This means that pure really is pure with respect to Functor.map.

• seq_pure {α β : Type u} (g : f (α → β)) (x : α) : g <*> pure x = (fun (h : α → β) => h x) <$> g

  pure after seq is equivalent to Functor.map.

  This means that pure really is pure when occurring just after seq.

• seq_assoc {α β γ : Type u} (x : f α) (g : f (α → β)) (h : f (β → γ)) : h <*> (g <*> x) = Function.comp <$> h <*> g <*> x

  seq is associative.

  Changing the nesting of seq calls while maintaining the order of computations results in an equivalent computation. This means that seq is not doing any more than sequencing.

@[simp]

theorem pure_id_seq {f : Type u_1 → Type u_2} {α : Type u_1} [Applicative f] [LawfulApplicative f] (x : f α) : pure id <*> x = x

class LawfulMonad (m : Type u → Type v) [Monad m] extends LawfulApplicative m : Prop

Lawful monads are those that satisfy a certain behavioral specification. While all instances of Monad should satisfy these laws, not all implementations are required to prove this.

LawfulMonad.mk' is an alternative constructor that contains useful defaults for many fields.

• map_const {α β : Type u} : Functor.mapConst = Functor.map ∘ Function.const β
• id_map {α : Type u} (x : m α) : id <$> x = x
• comp_map {α β γ : Type u} (g : α → β) (h : β → γ) (x : m α) : (h ∘ g) <$> x = h <$> g <$> x
• seqLeft_eq {α β : Type u} (x : m α) (y : m β) : x <* y = Function.const β <$> x <*> y
• seqRight_eq {α β : Type u} (x : m α) (y : m β) : x *> y = Function.const α id <$> x <*> y
• pure_seq {α β : Type u} (g : α → β) (x : m α) : pure g <*> x = g <$> x
• map_pure {α β : Type u} (g : α → β) (x : α) : g <$> pure x = pure (g x)
• seq_pure {α β : Type u} (g : m (α → β)) (x : α) : g <*> pure x = (fun (h : α → β) => h x) <$> g
• seq_assoc {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)) : h <*> (g <*> x) = Function.comp <$> h <*> g <*> x
• bind_pure_comp {α β : Type u} (f : α → β) (x : m α) : (do let a ← x pure (f a)) = f <$> x

  A bind followed by pure composed with a function is equivalent to a functorial map.

  This means that pure really is pure after a bind and has no effects.

• bind_map {α β : Type u} (f : m (α → β)) (x : m α) : (do let x_1 ← f x_1 <$> x) = f <*> x

  A bind followed by a functorial map is equivalent to Applicative sequencing.

  This means that the effect sequencing from Monad and Applicative are the same.

• pure_bind {α β : Type u} (x : α) (f : α → m β) : pure x >>= f = f x

  pure followed by bind is equivalent to function application.

  This means that pure really is pure before a bind and has no effects.

• bind_assoc {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ) : x >>= f >>= g = x >>= fun (x : α) => f x >>= g

  bind is associative.

  Changing the nesting of bind calls while maintaining the order of computations results in an equivalent computation. This means that bind is not doing more than data-dependent sequencing.

@[simp]

theorem bind_pure {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] (x : m α) : x >>= pure = x

theorem map_eq_pure_bind {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] (f : α → β) (x : m α) : f <$> x = do let a ← x pure (f a)

Use simp [← bind_pure_comp] rather than simp [map_eq_pure_bind], as bind_pure_comp is in the default simp set, so also using map_eq_pure_bind would cause a loop.

theorem seq_eq_bind_map {m : Type u → Type u_1} {α β : Type u} [Monad m] [LawfulMonad m] (f : m (α → β)) (x : m α) : f <*> x = do let x_1 ← f x_1 <$> x

theorem bind_congr {m : Type u_1 → Type u_2} {α β : Type u_1} [Bind m] {x : m α} {f g : α → m β} (h : ∀ (a : α), f a = g a) : x >>= f = x >>= g

theorem bind_pure_unit {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] {x : m PUnit} : (do x pure PUnit.unit) = x

theorem map_congr {m : Type u_1 → Type u_2} {α β : Type u_1} [Functor m] {x : m α} {f g : α → β} (h : ∀ (a : α), f a = g a) : f <$> x = g <$> x

theorem seq_eq_bind {m : Type u → Type u_1} {α β : Type u} [Monad m] [LawfulMonad m] (mf : m (α → β)) (x : m α) : mf <*> x = do let f ← mf f <$> x

theorem seqRight_eq_bind {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x *> y = do let _ ← x y

theorem seqLeft_eq_bind {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y = do let a ← x let _ ← y pure a

@[simp]

theorem map_bind {m : Type u_1 → Type u_2} {β γ α : Type u_1} [Monad m] [LawfulMonad m] (f : β → γ) (x : m α) (g : α → m β) : f <$> (x >>= g) = do let a ← x f <$> g a

@[simp]

theorem bind_map_left {m : Type u_1 → Type u_2} {α β γ : Type u_1} [Monad m] [LawfulMonad m] (f : α → β) (x : m α) (g : β → m γ) : (do let b ← f <$> x g b) = do let a ← x g (f a)

@[simp]

theorem LawfulMonad.map_pure' {m : Type u_1 → Type u_2} {α β : Type u_1} {f : α → β} [Monad m] [LawfulMonad m] {a : α} : f <$> pure a = pure (f a)

This is just a duplicate of LawfulApplicative.map_pure, but sometimes applies when that doesn't.

It is named with a prime to avoid conflict with the inherited field LawfulMonad.map_pure.

@[simp]

theorem LawfulMonad.map_map {α α✝ a✝ : Type u_1} {g : α✝ → a✝} {f : α → α✝} {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] {x : m α} : g <$> f <$> x = (fun (a : α) => g (f a)) <$> x

This is just a duplicate of Functor.map_map, but sometimes applies when that doesn't.

theorem LawfulMonad.mk' (m : Type u → Type v) [Monad m] (id_map : ∀ {α : Type u} (x : m α), id <$> x = x) (pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x) (bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun (x : α) => f x >>= g) (map_const : ∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <$> y := by intros; rfl) (seqLeft_eq : ∀ {α β : Type u} (x : m α) (y : m β), x <* y = do let a ← x let _ ← y pure a := by intros; rfl) (seqRight_eq : ∀ {α β : Type u} (x : m α) (y : m β), x *> y = do let _ ← x y := by intros; rfl) (bind_pure_comp : ∀ {α β : Type u} (f : α → β) (x : m α), (do let y ← x pure (f y)) = f <$> x := by intros; rfl) (bind_map : ∀ {α β : Type u} (f : m (α → β)) (x : m α), (do let x_1 ← f x_1 <$> x) = f <*> x := by intros; rfl) : LawfulMonad m

An alternative constructor for LawfulMonad which has more defaultable fields in the common case.

Id

theorem Id.ext {α : Type u_1} {x y : Id α} (h : x.run = y.run) : x = y

theorem Id.ext_iff {α : Type u_1} {x y : Id α} : x = y ↔ x.run = y.run

instance Id.instLawfulMonad : LawfulMonad Id

@[simp]

theorem Id.run_map {α β : Type u_1} (x : Id α) (f : α → β) : (f <$> x).run = f x.run

@[simp]

theorem Id.run_bind {α β : Type u_1} (x : Id α) (f : α → Id β) : (x >>= f).run = (f x.run).run

@[simp]

theorem Id.run_pure {α : Type u_1} (a : α) : (pure a).run = a

@[simp]

theorem Id.run_seqRight {α : Type u_1} (x y : Id α) : (x *> y).run = y.run

@[simp]

theorem Id.run_seqLeft {α : Type u_1} (x y : Id α) : (x <* y).run = x.run

@[simp]

theorem Id.run_seq {α β : Type u_1} (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run

@[deprecated Id.run_map (since := "2025-03-05")]

theorem Id.map_eq {α β : Type u_1} (x : Id α) (f : α → β) : f <$> x = f x

@[deprecated Id.run_bind (since := "2025-03-05")]

theorem Id.bind_eq {α β : Type u_1} (x : Id α) (f : α → id β) : x >>= f = f x

@[deprecated Id.run_pure (since := "2025-03-05")]

theorem Id.pure_eq {α : Type u_1} (a : α) : pure a = a

Option

instance instLawfulMonadOption : LawfulMonad Option

instance instLawfulApplicativeOption : LawfulApplicative Option

instance instLawfulFunctorOption : LawfulFunctor Option