Module docstring
{"# Id ","# Option "}
monadLift_self
theorem
{m : Type u → Type v} (x : m α) : monadLift x = x
Full source
@[simp] theorem monadLift_self {m : Type u → Type v} (x : m α) : monadLift x = x :=
rflInformal description
For any monad `m` and any element `x : m α`, the monad lifting of `x` to itself is equal to `x`, i.e., $\text{monadLift}(x) = x$.
LawfulFunctor
structure
(f : Type u → Type v) [Functor f]
Full source
/--
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.
-/
class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop where
/--
The `mapConst` implementation is equivalent to the default implementation.
-/
map_const : (Functor.mapConst : α → f β → f α) = Functor.mapFunctor.map ∘ const β
/--
The `map` implementation preserves identity.
-/
id_map (x : f α) : idid <$> x = x
/--
The `map` implementation preserves function composition.
-/
comp_map (g : α → β) (h : β → γ) (x : f α) : (h ∘ g) <$> x = h <$> g <$> xInformal description
A `LawfulFunctor` is a functor in functional programming that satisfies the functor laws. Specifically, for a type constructor `f : Type → Type` equipped with a mapping operation, the following properties must hold for all terms `v : f α`:
1. **Identity**: `id <$> v = v`
2. **Composition**: For any functions `h : β → γ` and `g : α → β`, `(h ∘ g) <$> v = h <$> (g <$> v)`
This structure ensures that the functor adheres to the category-theoretic notion of a functor in the category of types and functions between them.
id_map'
theorem
[Functor m] [LawfulFunctor m] (x : m α) : (fun a => a) <$> x = x
Full source
@[simp] theorem id_map' [Functor m] [LawfulFunctor m] (x : m α) : (fun a => a) <$> x = x :=
id_map xInformal description
For any functor `m` that satisfies the functor laws (`LawfulFunctor m`) and any element `x : m α`, mapping the identity function over `x` leaves `x` unchanged, i.e., `id <$> x = x`.
Functor.map_map
theorem
[Functor f] [LawfulFunctor f] (m : α → β) (g : β → γ) (x : f α) : g <$> m <$> x = (fun a => g (m a)) <$> x
Full source
@[simp] theorem Functor.map_map [Functor f] [LawfulFunctor f] (m : α → β) (g : β → γ) (x : f α) :
g <$> m <$> x = (fun a => g (m a)) <$> x :=
(comp_map _ _ _).symmInformal description
For any lawful functor $f$ and functions $m : \alpha \to \beta$, $g : \beta \to \gamma$, and element $x : f \alpha$, the composition of mapping $m$ followed by $g$ over $x$ is equal to mapping the composition $g \circ m$ over $x$, i.e.,
$$ g <$> (m <$> x) = (g \circ m) <$> x. $$
LawfulApplicative
structure
(f : Type u → Type v) [Applicative f] : Prop extends LawfulFunctor f
Full source
/--
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.
-/
class LawfulApplicative (f : Type u → Type v) [Applicative f] : Prop extends LawfulFunctor f where
/-- `seqLeft` is equivalent to the default implementation. -/
seqLeft_eq (x : f α) (y : f β) : x <* y = constconst β <$> xconst β <$> x <*> y
/-- `seqRight` is equivalent to the default implementation. -/
seqRight_eq (x : f α) (y : f β) : x *> y = constconst α id <$> xconst α id <$> x <*> y
/--
`pure` before `seq` is equivalent to `Functor.map`.
This means that `pure` really is pure when occurring immediately prior to `seq`.
-/
pure_seq (g : α → β) (x : f α) : purepure g <*> x = 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`.
-/
map_pure (g : α → β) (x : α) : g <$> (pure x : f α) = pure (g x)
/--
`pure` after `seq` is equivalent to `Functor.map`.
This means that `pure` really is pure when occurring just after `seq`.
-/
seq_pure {α β : Type u} (g : f (α → β)) (x : α) : g <*> pure x = (fun h => h x) <$> g
/--
`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.
-/
seq_assoc {α β γ : Type u} (x : f α) (g : f (α → β)) (h : f (β → γ)) : h <*> (g <*> x) = ((@comp α β γ) <$> h) <*> g((@comp α β γ) <$> h) <*> g <*> x
comp_map g h x := (by
repeat rw [← pure_seq]
simp [seq_assoc, map_pure, seq_pure])Informal description
A structure that extends an applicative functor `f` with proofs that it satisfies the laws of an applicative functor, including the preservation of identity and composition laws for sequencing computations.
pure_id_seq
theorem
[Applicative f] [LawfulApplicative f] (x : f α) : pure id <*> x = x
Full source
@[simp] theorem pure_id_seq [Applicative f] [LawfulApplicative f] (x : f α) : purepure id <*> x = x := by
simp [pure_seq]Informal description
For any lawful applicative functor $f$ and any element $x$ of type $f \alpha$, applying the pure identity function to $x$ via the applicative sequencing operation `<*>` yields $x$ itself, i.e.,
$$ \text{pure } \text{id} \ <*> \ x = x. $$
LawfulMonad
structure
(m : Type u → Type v) [Monad m] : Prop extends LawfulApplicative m
Full source
/--
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.
-/
class LawfulMonad (m : Type u → Type v) [Monad m] : Prop extends LawfulApplicative m where
/--
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_pure_comp (f : α → β) (x : m α) : x >>= (fun a => pure (f a)) = 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.
-/
bind_map {α β : Type u} (f : m (α → β)) (x : m α) : f >>= (. <$> x) = 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.
-/
pure_bind (x : α) (f : α → m β) : purepure x >>= f = f x
/--
`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.
-/
bind_assoc (x : m α) (f : α → m β) (g : β → m γ) : x >>= fx >>= f >>= g = x >>= fun x => f x >>= g
map_pure g x := (by rw [← bind_pure_comp, pure_bind])
seq_pure g x := (by rw [← bind_map]; simp [map_pure, bind_pure_comp])
seq_assoc x g h := (by simp [← bind_pure_comp, ← bind_map, bind_assoc, pure_bind])Informal description
A `LawfulMonad` is a monad that satisfies certain behavioral laws, ensuring that its operations behave as expected. Specifically, it extends `LawfulApplicative` and includes laws such as `bind_pure` (binding with `pure` is the identity) and `map_eq_pure_bind` (mapping is equivalent to binding with a pure function). While all monads should satisfy these laws, not all implementations are required to prove them.
bind_pure
theorem
[Monad m] [LawfulMonad m] (x : m α) : x >>= pure = x
Full source
@[simp] theorem bind_pure [Monad m] [LawfulMonad m] (x : m α) : x >>= pure = x := by
show x >>= (fun a => pure (id a)) = x
rw [bind_pure_comp, id_map]Informal description
For any monad $m$ that satisfies the monad laws, and for any element $x$ of type $m \alpha$, the monadic bind operation of $x$ with the pure function is equal to $x$ itself, i.e.,
$$ x \mathbin{>>=} \text{pure} = x. $$
map_eq_pure_bind
theorem
[Monad m] [LawfulMonad m] (f : α → β) (x : m α) : f <$> x = x >>= fun a => pure (f a)
Full source
/--
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 map_eq_pure_bind [Monad m] [LawfulMonad m] (f : α → β) (x : m α) : f <$> x = x >>= fun a => pure (f a) := by
rw [← bind_pure_comp]Informal description
For any monad `m` that satisfies the monad laws, and for any function `f : α → β` and monadic value `x : m α`, the map operation `f <$> x` is equal to binding `x` with the composition of `pure` and `f`, i.e., `x >>= (pure ∘ f)`.
seq_eq_bind_map
theorem
{α β : Type u} [Monad m] [LawfulMonad m] (f : m (α → β)) (x : m α) : f <*> x = f >>= (. <$> x)
Full source
theorem seq_eq_bind_map {α β : Type u} [Monad m] [LawfulMonad m] (f : m (α → β)) (x : m α) : f <*> x = f >>= (. <$> x) := by
rw [← bind_map]Informal description
For any monad `m` that satisfies the monad laws (`LawfulMonad m`), and for any types `α` and `β`, given a monadic function `f : m (α → β)` and a monadic value `x : m α`, the sequential application `f <*> x` is equal to binding `f` with the function that maps `x` over the contained function, i.e., `f >>= (λ g, g <$> x)`.
bind_congr
theorem
[Bind m] {x : m α} {f g : α → m β} (h : ∀ a, f a = g a) : x >>= f = x >>= g
Full source
theorem bind_congr [Bind m] {x : m α} {f g : α → m β} (h : ∀ a, f a = g a) : x >>= f = x >>= g := by
simp [funext h]Informal description
For any monadic type constructor `m` with a `Bind` instance, and for any monadic value `x : m α` and functions `f, g : α → m β`, if `f(a) = g(a)` for all `a : α`, then the monadic bind operations `x >>= f` and `x >>= g` are equal.
bind_pure_unit
theorem
[Monad m] [LawfulMonad m] {x : m PUnit} : (x >>= fun _ => pure ⟨⟩) = x
Full source
theorem bind_pure_unit [Monad m] [LawfulMonad m] {x : m PUnit} : (x >>= fun _ => pure ⟨⟩) = x := by
rw [bind_pure]Informal description
For any monad $m$ that satisfies the monad laws, and for any monadic value $x : m \text{PUnit}$ (where $\text{PUnit}$ is the unit type), the monadic bind operation of $x$ with the constant pure unit function is equal to $x$ itself, i.e.,
$$ x \mathbin{>>=} (\lambda \_, \text{pure} \, ()) = x. $$
map_congr
theorem
[Functor m] {x : m α} {f g : α → β} (h : ∀ a, f a = g a) : (f <$> x : m β) = g <$> x
Informal description
For any functor `m` and any element `x : m α`, if two functions `f, g : α → β` satisfy `f a = g a` for all `a : α`, then applying these functions to `x` via the functor's map operation yields equal results, i.e., `f <$> x = g <$> x`.
seq_eq_bind
theorem
{α β : Type u} [Monad m] [LawfulMonad m] (mf : m (α → β)) (x : m α) : mf <*> x = mf >>= fun f => f <$> x
Full source
theorem seq_eq_bind {α β : Type u} [Monad m] [LawfulMonad m] (mf : m (α → β)) (x : m α) : mf <*> x = mf >>= fun f => f <$> x := by
rw [bind_map]Informal description
For any monad `m` that is lawful (i.e., satisfies the monad laws), and for any types $\alpha$ and $\beta$, given a monadic value `mf : m (α → β)` and `x : m α`, the sequential application `mf <*> x` is equal to binding `mf` to a function `f` and then mapping `f` over `x`, i.e., `mf >>= fun f => f <$> x`.
In mathematical notation:
$$ \text{mf} \mathbin{<*>} \text{x} = \text{mf} \mathbin{>>=} \lambda f, f \mathbin{<\$>} \text{x} $$
seqRight_eq_bind
theorem
[Monad m] [LawfulMonad m] (x : m α) (y : m β) : x *> y = x >>= fun _ => y
Full source
theorem seqRight_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x *> y = x >>= fun _ => y := by
rw [seqRight_eq]
simp only [map_eq_pure_bind, const, seq_eq_bind_map, bind_assoc, pure_bind, id_eq, bind_pure]Informal description
For any monad $m$ that satisfies the monad laws, and for any monadic values $x : m \alpha$ and $y : m \beta$, the right-sequence operation $x \mathbin{*>} y$ is equal to binding $x$ with a function that discards its argument and returns $y$, i.e.,
$$ x \mathbin{*>} y = x \mathbin{>>=} \lambda \_, y. $$
seqLeft_eq_bind
theorem
[Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y = x >>= fun a => y >>= fun _ => pure a
Full source
theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y = x >>= fun a => y >>= fun _ => pure a := by
rw [seqLeft_eq]
simp only [map_eq_pure_bind, seq_eq_bind_map, bind_assoc, pure_bind, const_apply]Informal description
For any lawful monad `m` and monadic values `x : m α` and `y : m β`, the left sequence operation `x <* y` is equal to binding `x` to a value `a` and then binding `y` to discard its result, returning `pure a`.
In mathematical notation:
$$ x \mathbin{<*} y = x \mathbin{>>=} \lambda a, y \mathbin{>>=} \lambda \_, \text{pure}\ a $$
map_bind
theorem
[Monad m] [LawfulMonad m] (f : β → γ) (x : m α) (g : α → m β) : f <$> (x >>= g) = x >>= fun a => f <$> g a
Full source
@[simp] theorem map_bind [Monad m] [LawfulMonad m] (f : β → γ) (x : m α) (g : α → m β) :
f <$> (x >>= g) = x >>= fun a => f <$> g a := by
rw [← bind_pure_comp, LawfulMonad.bind_assoc]
simp [bind_pure_comp]Informal description
For any lawful monad `m`, any function `f : β → γ`, any monadic value `x : m α`, and any function `g : α → m β`, the following equality holds:
\[ f <\$> (x \gg= g) = x \gg= \lambda a, f <\$> g(a). \]
Here, `<\$>` denotes the `map` operation and `\gg=` denotes the `bind` operation of the monad.
bind_map_left
theorem
[Monad m] [LawfulMonad m] (f : α → β) (x : m α) (g : β → m γ) : ((f <$> x) >>= fun b => g b) = (x >>= fun a => g (f a))
Full source
@[simp] theorem bind_map_left [Monad m] [LawfulMonad m] (f : α → β) (x : m α) (g : β → m γ) :
((f <$> x) >>= fun b => g b) = (x >>= fun a => g (f a)) := by
rw [← bind_pure_comp]
simp only [bind_assoc, pure_bind]Informal description
For any lawful monad `m`, any function `f : α → β`, any monadic value `x : m α`, and any function `g : β → m γ`, the following equality holds:
$$(f <$> x) \gg= g = x \gg= (g \circ f)$$
where `<$>` denotes the `map` operation and `>>=` denotes the `bind` operation.
Functor.map_unit
theorem
[Monad m] [LawfulMonad m] {a : m PUnit} : (fun _ => PUnit.unit) <$> a = a
Full source
theorem Functor.map_unit [Monad m] [LawfulMonad m] {a : m PUnit} : (fun _ => PUnit.unit) <$> a = a := by
simp [map]Informal description
For any lawful monad `m` and any monadic value `a : m PUnit`, mapping the constant function `fun _ => PUnit.unit` over `a` yields `a` itself, i.e., `(fun _ => PUnit.unit) <$> a = a`.
LawfulMonad.map_pure'
theorem
[Monad m] [LawfulMonad m] {a : α} : (f <$> pure a : m β) = pure (f a)
Full source
/--
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_pure' [Monad m] [LawfulMonad m] {a : α} :
(f <$> pure a : m β) = pure (f a) := by
simp only [map_pure]Informal description
For any monad `m` that is lawful (i.e., satisfies the monad laws), and for any element `a` of type `α`, the mapping of a function `f` over the pure value `pure a` is equal to the pure value of `f a`, i.e., $f <$> \text{pure } a = \text{pure } (f a)$.
LawfulMonad.map_map
theorem
{m} [Monad m] [LawfulMonad m] {x : m α} : g <$> f <$> x = (fun a => g (f a)) <$> x
Full source
/--
This is just a duplicate of `Functor.map_map`, but sometimes applies when that doesn't.
-/
@[simp] theorem LawfulMonad.map_map {m} [Monad m] [LawfulMonad m] {x : m α} :
g <$> f <$> x = (fun a => g (f a)) <$> x := by
simp only [Functor.map_map]Informal description
For any lawful monad $m$ and any monadic value $x : m \alpha$, the composition of mapping $f$ followed by $g$ over $x$ is equal to mapping the composition $g \circ f$ over $x$, i.e.,
$$ g <$> (f <$> x) = (g \circ f) <$> x. $$
Id.map_eq
theorem
(x : Id α) (f : α → β) : f <$> x = f x
Informal description
For any element $x$ of type `Id α` and any function $f : α → β$, the mapping operation satisfies $f <$> $x = f x$.
Id.bind_eq
theorem
(x : Id α) (f : α → id β) : x >>= f = f x
Informal description
For any element $x$ of type `Id α` and any function $f : α → \text{Id} β$, the monadic bind operation satisfies $x \gg= f = f x$.
Id.pure_eq
theorem
(a : α) : (pure a : Id α) = a
Informal description
For any element $a$ of type $\alpha$, the monadic `pure` operation in the identity monad `Id` satisfies $\text{pure}(a) = a$.
Id.instLawfulMonad
instance
: LawfulMonad Id
Full source
instance : LawfulMonad Id := by
refine LawfulMonad.mk' _ ?_ ?_ ?_ <;> intros <;> rflInformal description
The identity monad `Id` satisfies the laws of a lawful monad, meaning its operations (such as `pure` and `bind`) behave as expected according to monadic laws.
instLawfulMonadOption
instance
: LawfulMonad Option
Full source
instance : LawfulMonad Option := LawfulMonad.mk'
(id_map := fun x => by cases x <;> rfl)
(pure_bind := fun _ _ => rfl)
(bind_assoc := fun x _ _ => by cases x <;> rfl)
(bind_pure_comp := fun _ x => by cases x <;> rfl)Informal description
The `Option` type constructor forms a lawful monad, satisfying all the monad laws (such as associativity of bind and identity laws) in addition to the applicative and functor laws.
instLawfulApplicativeOption
instance
: LawfulApplicative Option
Full source
instance : LawfulApplicative Option := inferInstanceInformal description
The `Option` type constructor forms a lawful applicative functor, satisfying all the applicative functor laws in addition to the functor laws.
instLawfulFunctorOption
instance
: LawfulFunctor Option
Full source
instance : LawfulFunctor Option := inferInstanceInformal description
The `Option` type constructor is a lawful functor, meaning it satisfies the functor laws:
1. **Identity**: Mapping the identity function over an optional value preserves the value.
2. **Composition**: Mapping the composition of two functions over an optional value is the same as sequentially mapping each function.