map_seq
theorem map_seq :
∀ {α β γ : Type u} {F : Type u → Type v} [inst : Applicative F] [inst_1 : LawfulApplicative F] (f : β → γ)
(x : F (α → β)) (y : F α), (f <$> Seq.seq x fun x => y) = Seq.seq ((fun x => f ∘ x) <$> x) fun x => y
The theorem `map_seq` is a statement about the interaction of function composition with sequential application in the context of an applicative functor. Specifically, for any types `α`, `β`, and `γ`, any applicative functor `F`, any lawful applicative `F`, any function `f` from `β` to `γ`, any value `x` of type `F (α → β)`, and any value `y` of type `F α`, the theorem states that mapping `f` over the result of applying `x` to `y` sequentially (using `Seq.seq`) is the same as sequentially applying the result of mapping the function `(fun x => f ∘ x)` over `x` to `y`. In other words, function composition can be "pulled out" of a sequential application, a fundamental property in functional programming and category theory.
More concisely: For any applicative functor `F`, any lawful applicative `F`, any function `f` from `β` to `γ`, and any values `x` of type `F (α → β)` and `y` of type `F α`, `map (λ hx => f ∘ hx) x >>= fun z => f <$ y = map (λ x => f ∘ x) x >>= fun x => x >>= fun y => f <$ y`.
|
Mathlib.Control.Basic._auxLemma.3
theorem Mathlib.Control.Basic._auxLemma.3 :
∀ {m : Type u → Type v} [inst : Monad m] [self : LawfulMonad m] {α β : Type u} (f : α → β) (x : m α),
f <$> x = do
let a ← x
pure (f a)
This theorem, `Mathlib.Control.Basic._auxLemma.3`, states that for any monad `m` (with the types `u` and `v`), which obeys the laws of monads (`LawfulMonad m`), and for any two types `α` and `β`, and a function `f` of type `α → β`, the operation of mapping `f` over `x` (denoted as `f <$> x`) is equivalent to first binding `x` to `a` using the `do` notation, and then applying `f` to `a` and wrapping the result in the monad using `pure`. It shows that these are two possible ways to apply a function to the value inside a monad: either by using the `fmap` operation (denoted by `<$>`), or by explicitly binding the value inside the monad to a variable and then applying the function to this variable.
More concisely: For any monad `m` and function `f`, the application of `f` to the value inside `m` using the `<$>` operator is equivalent to binding the value to a variable `x` using `do` notation and then applying `f` to `x` and wrapping the result in `m` using `pure`.
|
CommApplicative.commutative_prod
theorem CommApplicative.commutative_prod :
∀ {m : Type u → Type v} [inst : Applicative m] [self : CommApplicative m] {α β : Type u} (a : m α) (b : m β),
(Seq.seq (Prod.mk <$> a) fun x => b) = Seq.seq ((fun b a => (a, b)) <$> b) fun x => a
This theorem asserts that for any applicative functor `m`, under the condition that it also is a CommApplicative (which means that the order of effectful computations in `m` does not matter), given `a : m α` and `b : m β`, the computations performed first on `a` and then on `b` are the same as those performed in the reverse order. Specifically, this theorem states that `Seq.seq (Prod.mk <$> a) (fun x => b)` is equivalent to `Seq.seq ((fun b a => (a, b)) <$> b) (fun x => a)`. In other words, sequencing the effects of `a` and `b` and forming a pair is the same as doing it in reverse order and swapping the pair elements. The symbol `<$>` is the infix notation for the `fmap` function, which applies a function to a value in a context (for instance, a value within a functor).
More concisely: For any commutative applicative functor `m`, the sequence of computations `(a, b) <$> Seq.seq (fmap (x -> (x, b)) b) (fmap id a)` is equivalent to `Seq.seq (fmap (a -> (a, b)) a) (fmap id b)`, where `id` is the identity function.
|
seq_map_assoc
theorem seq_map_assoc :
∀ {α β γ : Type u} {F : Type u → Type v} [inst : Applicative F] [inst_1 : LawfulApplicative F] (x : F (α → β))
(f : γ → α) (y : F γ), (Seq.seq x fun x => f <$> y) = Seq.seq ((fun x => x ∘ f) <$> x) fun x => y
The theorem `seq_map_assoc` states that for any types `α`, `β`, `γ`, and applicative functor `F`, given an element `x` of type `F (α → β)`, a function `f` from `γ` to `α`, and an element `y` of type `F γ`, the operation of sequentially applying `x` to the result of mapping `f` over `y` (represented as `Seq.seq x fun x => f <$> y`) is equivalent to the operation of first mapping the function composition operator with `f` over `x`, and then sequentially applying this to `y` (represented as `Seq.seq ((fun x => x ∘ f) <$> x) fun x => y`). Here, `<$>` denotes the fmap operation of mapping a function over a functor. This theorem essentially expresses an associativity property of the `Seq.seq` operation in relation to the fmap operation.
More concisely: For any applicative functors `F`, types `α`, `β`, `γ`, functions `x : F (α → β)`, `f : γ → α`, and elements `y : F γ`, the sequential compositions `Seq.seq x (f <$> y)` and `Seq.seq ((λ x => x ∘ f) <$> x) y` are equivalent.
|
Functor.map_map
theorem Functor.map_map :
∀ {α β γ : Type u} {f : Type u → Type v} [inst : Functor f] [inst_1 : LawfulFunctor f] (m : α → β) (g : β → γ)
(x : f α), g <$> m <$> x = (g ∘ m) <$> x
The theorem `Functor.map_map` states that for any types `α`, `β`, and `γ`, and for a functor `f` of type `Type u → Type v` that obeys the laws of a `LawfulFunctor`, and given a function `m` from `α` to `β` and a function `g` from `β` to `γ`, and an instance `x` of functor `f` applied to `α`, the composition of applying function `m` then function `g` to `x` (denoted as `g <$> m <$> x`) is equivalent to applying the composed function `g ∘ m` to `x` (denoted as `(g ∘ m) <$> x`). In other words, the order of mapping functions over the functor does not change the final result, reflecting the law of composition in the context of functors.
More concisely: For any type maps `m : α → β` and `g : β → γ`, functor `f : Type u → Type v` (as a lawful functor), and `x : f α`, the application of `g` followed by `m` to `x` is equal to the composition of `g` and `m` applied to `x` (`(g ∘ m) <$> x` is equal to `g <$> m <$> x`).
|