Documentation

Init.Control.Lawful.Basic

@[simp]
theorem monadLift_self {m : Type u_1 → Type u_2} {α : Type u_1} [] (x : m α) :
= x
class LawfulFunctor (f : Type u → Type v) [] :

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
• id_map : ∀ {α : Type u} (x : f α), id <$> x = x • comp_map : ∀ {α β γ : Type u} (g : αβ) (h : βγ) (x : f α), (h g) <$> x = h <$> g <$> x
Instances
theorem LawfulFunctor.map_const {f : Type u → Type v} [] [self : ] {α : Type u} {β : Type u} :
Functor.mapConst = Functor.map
@[simp]
theorem LawfulFunctor.id_map {f : Type u → Type v} [] [self : ] {α : Type u} (x : f α) :
id <$> x = x theorem LawfulFunctor.comp_map {f : Type u → Type v} [] [self : ] {α : Type u} {β : Type u} {γ : 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} [] [] (x : m α) :
(fun (a : α) => a) <$> x = x class LawfulApplicative (f : Type u → Type v) [] extends : 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  Instances theorem LawfulApplicative.seqLeft_eq {f : Type u → Type v} [] [self : ] {α : Type u} {β : Type u} (x : f α) (y : f β) : (SeqLeft.seqLeft x fun (x : Unit) => y) = Seq.seq () fun (x : Unit) => y theorem LawfulApplicative.seqRight_eq {f : Type u → Type v} [] [self : ] {α : Type u} {β : Type u} (x : f α) (y : f β) : (SeqRight.seqRight x fun (x : Unit) => y) = Seq.seq ( <$> x) fun (x : Unit) => y
theorem LawfulApplicative.pure_seq {f : Type u → Type v} [] [self : ] {α : Type u} {β : 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} [] [self : ] {α : Type u} {β : Type u} (g : αβ) (x : α) : g <$> pure x = pure (g x)
@[simp]
theorem LawfulApplicative.seq_pure {f : Type u → Type v} [] [self : ] {α : Type u} {β : 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} [] [self : ] {α : Type u} {β : Type u} {γ : 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} [] (x : f α) :
(Seq.seq (pure id) fun (x_1 : Unit) => x) = x
class LawfulMonad (m : Type u → Type v) [] extends :

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
• 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 () fun (x : Unit) => y
• seqRight_eq : ∀ {α β : Type u} (x : m α) (y : m β), (SeqRight.seqRight x fun (x : Unit) => y) = Seq.seq ( <$> 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 ax pure (f a)) = f <$> x
• bind_map : ∀ {α β : Type u} (f : m (αβ)) (x : m α), (do let x_1f 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 Instances theorem LawfulMonad.bind_pure_comp {m : Type u → Type v} [] [self : ] {α : Type u} {β : Type u} (f : αβ) (x : m α) : (do let ax pure (f a)) = f <$> x
theorem LawfulMonad.bind_map {m : Type u → Type v} [] [self : ] {α : Type u} {β : Type u} (f : m (αβ)) (x : m α) :
(do let x_1f x_1 <$> x) = Seq.seq f fun (x_1 : Unit) => x @[simp] theorem LawfulMonad.pure_bind {m : Type u → Type v} [] [self : ] {α : Type u} {β : Type u} (x : α) (f : αm β) : pure x >>= f = f x @[simp] theorem LawfulMonad.bind_assoc {m : Type u → Type v} [] [self : ] {α : Type u} {β : Type u} {γ : 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} [] [] (x : m α) : x >>= pure = x theorem map_eq_pure_bind {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [] [] (f : αβ) (x : m α) : f <$> x = do let ax pure (f a)
theorem seq_eq_bind_map {m : Type u → Type u_1} {α : Type u} {β : Type u} [] [] (f : m (αβ)) (x : m α) :
(Seq.seq f fun (x_1 : Unit) => x) = do let x_1f 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} [] [] {x : } : (do x ) = x theorem map_congr {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [] {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} [] [] (mf : m (αβ)) (x : m α) : (Seq.seq mf fun (x_1 : Unit) => x) = do let fmf f <$> x
theorem seqRight_eq_bind {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [] [] (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} [] [] (x : m α) (y : m β) :
(SeqLeft.seqLeft x fun (x : Unit) => y) = do let ax let _ ← y pure a
theorem LawfulMonad.mk' (m : Type u → Type v) [] (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 β), = <$> y) _auto✝) (seqLeft_eq : autoParam (∀ {α β : Type u} (x : m α) (y : m β), (SeqLeft.seqLeft x fun (x : Unit) => y) = do let ax 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 yx pure (f y)) = f <$> x) _auto✝) (bind_map : autoParam (∀ {α β : Type u} (f : m (αβ)) (x : m α), (do let x_1f x_1 <$> x) = Seq.seq f fun (x_1 : Unit) => x) _auto✝) :

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
Equations

Option #

Equations
Equations
Equations