@[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

The Functor typeclass only contains the operations of a functor. LawfulFunctor further asserts that these operations satisfy the laws of a functor, including the preservation of the identity and composition laws:

id <$> x = x
(h ∘ g) <$> x = h <$> g <$> x

• 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

theorem LawfulFunctor.map_const {f : Type u → Type v} : ∀ {inst : Functor f} [self : LawfulFunctor f] {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β

@[simp]

theorem LawfulFunctor.id_map {f : Type u → Type v} : ∀ {inst : Functor f} [self : LawfulFunctor f] {α : Type u} (x : f α), id <$> x = x

theorem LawfulFunctor.comp_map {f : Type u → Type v} : ∀ {inst : Functor f} [self : LawfulFunctor f] {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x

@[simp]

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

@[simp]

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

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

The Applicative typeclass only contains the operations of an applicative functor. LawfulApplicative further asserts that these operations satisfy the laws of an applicative functor:

pure id <*> v = v
pure (·∘·) <*> u <*> v <*> w = u <*> (v <*> w)
pure f <*> pure x = pure (f x)
u <*> pure y = pure (· y) <*> u

• 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 β), (SeqLeft.seqLeft x fun (x : Unit) => y) = Seq.seq (Function.const β <$> x) fun (x : Unit) => y
• seqRight_eq : ∀ {α β : Type u} (x : f α) (y : f β), (SeqRight.seqRight x fun (x : Unit) => y) = Seq.seq (Function.const α id <$> x) fun (x : Unit) => y
• pure_seq : ∀ {α β : Type u} (g : α → β) (x : f α), (Seq.seq (pure g) fun (x_1 : Unit) => x) = g <$> x
• map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)
• seq_pure : ∀ {α β : Type u} (g : f (α → β)) (x : α), (Seq.seq g fun (x_1 : Unit) => pure x) = (fun (h : α → β) => h x) <$> g
• seq_assoc : ∀ {α β γ : Type u} (x : f α) (g : f (α → β)) (h : f (β → γ)), (Seq.seq h fun (x_1 : Unit) => Seq.seq g fun (x_2 : Unit) => x) = Seq.seq (Seq.seq (Function.comp <$> h) fun (x : Unit) => g) fun (x_1 : Unit) => x

theorem LawfulApplicative.seqLeft_eq {f : Type u → Type v} : ∀ {inst : Applicative f} [self : LawfulApplicative f] {α β : Type u} (x : f α) (y : f β), (SeqLeft.seqLeft x fun (x : Unit) => y) = Seq.seq (Function.const β <$> x) fun (x : Unit) => y

theorem LawfulApplicative.seqRight_eq {f : Type u → Type v} : ∀ {inst : Applicative f} [self : LawfulApplicative f] {α β : Type u} (x : f α) (y : f β), (SeqRight.seqRight x fun (x : Unit) => y) = Seq.seq (Function.const α id <$> x) fun (x : Unit) => y

theorem LawfulApplicative.pure_seq {f : Type u → Type v} : ∀ {inst : Applicative f} [self : LawfulApplicative f] {α β : Type u} (g : α → β) (x : f α), (Seq.seq (pure g) fun (x_1 : Unit) => x) = g <$> x

@[simp]

theorem LawfulApplicative.map_pure {f : Type u → Type v} : ∀ {inst : Applicative f} [self : LawfulApplicative f] {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)

@[simp]

theorem LawfulApplicative.seq_pure {f : Type u → Type v} : ∀ {inst : Applicative f} [self : LawfulApplicative f] {α β : Type u} (g : f (α → β)) (x : α), (Seq.seq g fun (x_1 : Unit) => pure x) = (fun (h : α → β) => h x) <$> g

theorem LawfulApplicative.seq_assoc {f : Type u → Type v} : ∀ {inst : Applicative f} [self : LawfulApplicative f] {α β γ : Type u} (x : f α) (g : f (α → β)) (h : f (β → γ)), (Seq.seq h fun (x_1 : Unit) => Seq.seq g fun (x_2 : Unit) => x) = Seq.seq (Seq.seq (Function.comp <$> h) fun (x : Unit) => g) fun (x_1 : Unit) => x

@[simp]

theorem pure_id_seq {f : Type u_1 → Type u_2} {α : Type u_1} [Applicative f] [LawfulApplicative f] (x : f α) : (Seq.seq (pure id) fun (x_1 : Unit) => x) = x

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

The Monad typeclass only contains the operations of a monad. LawfulMonad further asserts that these operations satisfy the laws of a monad, including associativity and identity laws for bind:

pure x >>= f = f x
x >>= pure = x
x >>= f >>= g = x >>= (fun x => f x >>= g)

LawfulMonad.mk' is an alternative constructor containing 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 β), (SeqLeft.seqLeft x fun (x : Unit) => y) = Seq.seq (Function.const β <$> x) fun (x : Unit) => y
• seqRight_eq : ∀ {α β : Type u} (x : m α) (y : m β), (SeqRight.seqRight x fun (x : Unit) => y) = Seq.seq (Function.const α id <$> x) fun (x : Unit) => y
• pure_seq : ∀ {α β : Type u} (g : α → β) (x : m α), (Seq.seq (pure g) fun (x_1 : Unit) => x) = g <$> x
• map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)
• seq_pure : ∀ {α β : Type u} (g : m (α → β)) (x : α), (Seq.seq g fun (x_1 : Unit) => pure x) = (fun (h : α → β) => h x) <$> g
• seq_assoc : ∀ {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)), (Seq.seq h fun (x_1 : Unit) => Seq.seq g fun (x_2 : Unit) => x) = Seq.seq (Seq.seq (Function.comp <$> h) fun (x : Unit) => g) fun (x_1 : Unit) => x
• bind_pure_comp : ∀ {α β : Type u} (f : α → β) (x : m α), (do let a ← x pure (f a)) = f <$> x
• bind_map : ∀ {α β : Type u} (f : m (α → β)) (x : m α), (do let x_1 ← f x_1 <$> x) = Seq.seq f fun (x_1 : Unit) => 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

@[simp]

theorem LawfulMonad.bind_pure_comp {m : Type u → Type v} : ∀ {inst : Monad m} [self : LawfulMonad m] {α β : Type u} (f : α → β) (x : m α), (do let a ← x pure (f a)) = f <$> x

theorem LawfulMonad.bind_map {m : Type u → Type v} : ∀ {inst : Monad m} [self : LawfulMonad m] {α β : Type u} (f : m (α → β)) (x : m α), (do let x_1 ← f x_1 <$> x) = Seq.seq f fun (x_1 : Unit) => x

@[simp]

theorem LawfulMonad.pure_bind {m : Type u → Type v} : ∀ {inst : Monad m} [self : LawfulMonad m] {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

@[simp]

theorem LawfulMonad.bind_assoc {m : Type u → Type v} : ∀ {inst : Monad m} [self : LawfulMonad m] {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun (x : α) => f x >>= g

@[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} {β : 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} {β : Type u} [Monad m] [LawfulMonad m] (f : m (α → β)) (x : m α) : (Seq.seq f fun (x_1 : Unit) => x) = do let x_1 ← f x_1 <$> x

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

@[simp]

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} {β : 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} {β : Type u} [Monad m] [LawfulMonad m] (mf : m (α → β)) (x : m α) : (Seq.seq mf fun (x_1 : Unit) => x) = do let f ← mf f <$> x

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

theorem seqLeft_eq_bind {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [Monad m] [LawfulMonad m] (x : m α) (y : m β) : (SeqLeft.seqLeft x fun (x : Unit) => y) = do let a ← x let _ ← y pure a

@[simp]

theorem map_bind {m : Type u_1 → Type u_2} {β : Type u_1} {γ : Type u_1} {α : 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} {β : Type u_1} {γ : 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 Functor.map_unit {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] {a : m PUnit} : (fun (x : PUnit) => PUnit.unit) <$> a = a

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 : autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <$> y) _auto✝) (seqLeft_eq : autoParam (∀ {α β : Type u} (x : m α) (y : m β), (SeqLeft.seqLeft x fun (x : Unit) => y) = do let a ← x let _ ← y pure a) _auto✝) (seqRight_eq : autoParam (∀ {α β : Type u} (x : m α) (y : m β), (SeqRight.seqRight x fun (x : Unit) => y) = do let _ ← x y) _auto✝) (bind_pure_comp : autoParam (∀ {α β : Type u} (f : α → β) (x : m α), (do let y ← x pure (f y)) = f <$> x) _auto✝) (bind_map : autoParam (∀ {α β : Type u} (f : m (α → β)) (x : m α), (do let x_1 ← f x_1 <$> x) = Seq.seq f fun (x_1 : Unit) => x) _auto✝) : LawfulMonad m

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

Id

@[simp]

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

@[simp]

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

@[simp]

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

instance Id.instLawfulMonad : LawfulMonad Id

Equations

• Id.instLawfulMonad = ⋯

Option

instance instLawfulMonadOption : LawfulMonad Option

Equations

• instLawfulMonadOption = ⋯

instance instLawfulApplicativeOption : LawfulApplicative Option

Equations

• instLawfulApplicativeOption = ⋯

instance instLawfulFunctorOption : LawfulFunctor Option

Equations

• instLawfulFunctorOption = ⋯