seq_eq_bind_map
theorem seq_eq_bind_map :
∀ {m : Type u → Type u_1} {α β : Type u} [inst : Monad m] [inst_1 : LawfulMonad m] (f : m (α → β)) (x : m α),
(Seq.seq f fun x_1 => x) = do
let x_1 ← f
x_1 <$> x
The theorem `seq_eq_bind_map` states that, for any types `α` and `β`, any monad `m`, and any two terms (values of the monad), `f : m (α → β)` and `x : m α`, the sequence operation (`Seq.seq`) of `f` and `x` is equivalent to first binding the function `f` to a variable `x_1` and then applying this function `x_1` to `x` using the map operation (`<$>`). This theorem bridges the concepts of sequencing and binding in the context of monads, showing that they are equivalent under these conditions.
More concisely: For any monad `m`, terms `f : m (α → β)` and `x : m α`, `Seq.seq f x` is equal to `do {x_1 ← f; x_2 ← x; return (x_1 x_2)}`.
|
LawfulMonad.mk'
theorem LawfulMonad.mk' :
∀ (m : Type u → Type v) [inst : Monad m],
(∀ {α : Type u} (x : m α), id <$> x = x) →
(∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x) →
(∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g) →
autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <$> y) _auto✝ →
autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝¹ →
autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝² →
autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =
f <$> x)
_auto✝³ →
autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <$> x) =
Seq.seq f fun x_1 => x)
_auto✝⁴ →
LawfulMonad m
The theorem `LawfulMonad.mk'` presents an alternative way to construct a lawful monad `m`. Given a type constructor `m` that forms a monad, it establishes certain laws:
1. The identity law: for any value `x` from the monad `m`, mapping the identity function over `x` should result in `x` itself.
2. The left identity law: for any value `x` and function `f` from `α` to `m β`, the operation `pure x >>= f` should be equivalent to `f x`.
3. The associativity law: for any value `x` from the monad `m`, and functions `f` and `g`, the operation `x >>= f >>= g` should be equivalent to `x >>= fun x => f x >>= g`.
4. The functor law: for any value `x` and `y` from the monad `m`, `Functor.mapConst x y` should be equivalent to `Function.const β x <$> y`.
5. The sequence left law: for any value `x` and `y` from the monad `m`, sequencing `x` and `y` and keeping the value of `x` should be equivalent to the do-notation `do let a ← x; let _ ← y; pure a`.
6. The sequence right law: for any value `x` and `y` from the monad `m`, sequencing `x` and `y` and keeping the value of `y` should be equivalent to the do-notation `do let _ ← x; y`.
7. The function application law: for any function `f` and value `x` from the monad `m`, the do-notation `do let y ← x; pure (f y)` should be equivalent to `f <$> x`.
8. The sequence law: for any function `f` and value `x` from the monad `m`, the do-notation `do let x_1 ← f; x_1 <$> x` should be equivalent to `Seq.seq f fun x_1 => x`.
These laws are expressed with `autoParam`, which allows Lean to fill in some arguments automatically, making it more convenient to use the theorem. If these laws hold, the monad `m` is a lawful monad `LawfulMonad m`.
More concisely: The `LawfulMonad.mk` theorem constructs a lawful monad `m` if and only if the given monad satisfies the identity, left identity, associativity, functor, sequence left and right, function application, and sequence laws.
|
bind_congr
theorem bind_congr :
∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Bind m] {x : m α} {f g : α → m β},
(∀ (a : α), f a = g a) → x >>= f = x >>= g
This theorem, named `bind_congr`, states that for any type constructor `m` with a bind operation, and any types `α` and `β`, if we have two functions `f` and `g` from `α` to `m β` such that `f` and `g` are equal for all inputs `a` of type `α`, then binding `x` (of type `m α`) to `f` is the same as binding `x` to `g`. In simpler terms, if two functions are the same for every input, applying them after a bind operation yields the same result regardless of the function used.
More concisely: For any type constructor `m` with a bind operation, and functions `f` and `g` from type `α` to `m β`, if `f(x) = g(x)` for all `x : α`, then `bind (x : m α) (f x) = bind (x : m α) (g x)`.
|
map_eq_pure_bind
theorem map_eq_pure_bind :
∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [inst_1 : LawfulMonad m] (f : α → β) (x : m α),
f <$> x = do
let a ← x
pure (f a)
This theorem, `map_eq_pure_bind`, states that for any monad `m` and for any two types `α` and `β`, given a function `f` from `α` to `β` and a monadic value `x` of type `m α`, the operation of mapping the function `f` over `x` (denoted as `f <$> x`) is equivalent to binding `x` to `a` and then applying `f` to `a` within the context of the monad (written as `let a ← x, pure (f a)`). This assertion holds under the condition that `m` obeys the laws of a lawful monad.
More concisely: For any lawful monad `m` and functions `f : α → β` and `x : m α`, `f <$> x` is equivalent to `let a ← x in pure (f a)` in the context of `m`.
|
id_map'
theorem id_map' :
∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Functor m] [inst_1 : LawfulFunctor m] (x : m α),
(fun a => a) <$> x = x
This theorem, named 'id_map', states that for any Functor 'm' mapping from 'Type u_1' to 'Type u_2', and any type 'α' of 'Type u_1', given that 'm' is a lawful functor, the application of the identity function (which returns its input unchanged) to any value 'x' of type 'm α' using the fmap operation (denoted as '<$>') results in 'x' itself. In other words, mapping the identity function over any value of a lawful functor leaves the value unchanged.
More concisely: For any lawful functor m and type α, the application of the identity function through fmap (denoted as '<$>') on an element x of type m α results in x itself.
|
bind_pure
theorem bind_pure :
∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [inst_1 : LawfulMonad m] (x : m α), x >>= pure = x := by
sorry
This theorem, `bind_pure`, states that for any monad `m` and any type `α`, if `x` is an instance of `m α`, then binding `x` to the `pure` function (i.e., `x >>= pure`) yields `x` itself. This is essentially asserting a key property of monads in functional programming, where the `pure` function acts as an identity with respect to the monadic bind operation `>>=`. This property is required for `m` to obey the monadic laws and thus be a lawful monad (`LawfulMonad m`).
More concisely: For any monad `m` and type `α`, the application of `pure` after `bind` (`>>=`) on an instance `x` of `m α` results in the identity `x`. That is, `x >>= pure = x`.
|