Option.map₂_def
theorem Option.map₂_def :
∀ {α β γ : Type u} (f : α → β → γ) (a : Option α) (b : Option β),
Option.map₂ f a b = Seq.seq (f <$> a) fun x => b
The theorem `Option.map₂_def` is stating that, for all types `α`, `β`, and `γ`, and for any binary function `f : α → β → γ` and options `a : Option α` and `b : Option β`, the application of `Option.map₂` to `f`, `a`, and `b` is the same as applying the sequence operation `Seq.seq` to the function `f` mapped over `a` and a function that evaluates to `b`. Essentially, it provides an equivalency between the operations of mapping a binary function over two optional values and sequencing a functor of a function over an optional value with another optional value. Note that this theorem can't serve as the definition due to limitations in universe polymorphism.
More concisely: For all types α, β, γ, binary function f, and options a and b, Option.map₂(f) (a) (b) = Seq.seq (λ x y => f x y) (Option.map f a) b.
|
Option.map_map₂_distrib_left
theorem Option.map_map₂_distrib_left :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β → γ} {a : Option α} {b : Option β}
{α' : Type u_5} {g : γ → δ} {f' : α' → β → δ} {g' : α → α'},
(∀ (a : α) (b : β), g (f a b) = f' (g' a) b) →
Option.map g (Option.map₂ f a b) = Option.map₂ f' (Option.map g' a) b
The theorem `Option.map_map₂_distrib_left` states that for any types `α`, `β`, `γ`, `δ`, `α'`, and any binary function `f : α → β → γ`, unary function `g : γ → δ`, binary function `f' : α' → β → δ`, unary function `g' : α → α'`, and optional values `a : Option α` and `b : Option β`, if for every `a` in `α` and `b` in `β`, `g` applied to `f a b` is equal to `f'` applied to `g' a and b`, then applying `g` to the result of mapping `f` over `a` and `b` is equal to mapping `f'` over the result of applying `g'` to `a` and `b`. This theorem establishes a kind of distributivity of the `map` and `map₂` operations over options.
More concisely: If for all `a` in `α` and `b` in `β`, `g(f(a, b)) = f'(g'(a), g'(b))`, then `g(Option.map₂ f a b) = Option.map₂ f' (Option.map g' a) (Option.map g' b)`.
|
Option.map_map₂_distrib_right
theorem Option.map_map₂_distrib_right :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β → γ} {a : Option α} {b : Option β}
{β' : Type u_6} {g : γ → δ} {f' : α → β' → δ} {g' : β → β'},
(∀ (a : α) (b : β), g (f a b) = f' a (g' b)) →
Option.map g (Option.map₂ f a b) = Option.map₂ f' a (Option.map g' b)
The theorem `Option.map_map₂_distrib_right` states that for any types `α`, `β`, `γ`, and `δ`, any binary function `f` from `α` and `β` to `γ`, any unary function `g` from `γ` to `δ`, a new binary function `f'` from `α` and `β'` to `δ`, a unary function `g'` from `β` to `β'`, and options `a` of type `α` and `b` of type `β`, if for every `α` and `β`, the function `g` applied to `f a b` equals to `f' a (g' b)`, then the mapping of `g` over the "option mapping" of `f` over `a` and `b` is equal to the "option mapping" of `f'` over `a` and the mapping of `g'` over `b`.
Here the "option mapping" `Option.map₂` applies a binary function to the values contained in two options if they are both present, while `Option.map` applies a unary function to the value contained in an option if it is present.
More concisely: If for all `a` in `α` and `b` in `β`, `g(f(a, b)) = f'(a, g'(b))`, then `(Option.map g).(Option.map₂ f) (some a) (some b) = Option.map (λ b => f'(a, b)) (some a) (Option.map g' b)`.
|
Option.map₂_map_left_anticomm
theorem Option.map₂_map_left_anticomm :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {α' : Type u_5}
{f : α' → β → γ} {g : α → α'} {f' : β → α → δ} {g' : δ → γ},
(∀ (a : α) (b : β), f (g a) b = g' (f' b a)) →
Option.map₂ f (Option.map g a) b = Option.map g' (Option.map₂ f' b a)
The theorem `Option.map₂_map_left_anticomm` states that for any types `α`, `β`, `γ`, `δ`, `α'`, any options `a` of type `α` and `b` of type `β`, any binary function `f : α' → β → γ`, any functions `g : α → α'`, `f' : β → α → δ`, and `g' : δ → γ`, if for all `a` of type `α` and `b` of type `β` the binary function `f` applied to `g a` and `b` equals the function `g'` applied to the result of `f' b a`, then the image of the binary function `f` applied to the image of `g` over `a` and `b` equals the image of `g'` over the image of the binary function `f'` applied to `b` and `a`. This theorem is a statement about the commutation of mapping operations over optional values.
More concisely: If `f(g(a), b) = g'(f'(b, a))` for all `a` of type `α` and `b` of type `β`, then `Option.map₂ f g a b = Option.map₂ f' g' (f' b a)`.
|
Option.map₂_none_right
theorem Option.map₂_none_right :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : Option α), Option.map₂ f a none = none := by
sorry
This theorem states that for any types α, β, and γ, and any binary function `f` from α and β to γ, if you apply the function `Option.map₂` to `f` and an optional value of α, with the second optional value being `none`, the result will always be `none`. In other words, if the second argument of the `Option.map₂` function is a `none`, no matter what the other arguments are, the function will always return a `none`.
More concisely: For any types α, β, and γ, and any binary function f: α × β → γ, Option.map₂ f (some x) none = none, where Option is the option type.
|
Option.map₂_coe_right
theorem Option.map₂_coe_right :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : Option α) (b : β),
Option.map₂ f a (some b) = Option.map (fun a => f a b) a
This theorem, `Option.map₂_coe_right`, states that for any types `α`, `β`, and `γ`, any binary function `f : α → β → γ`, any optional value `a : Option α`, and any value `b : β`, applying the binary function `f` to the optional value `a` and the option-wrapped value `some b` using `Option.map₂` is equivalent to applying a function to `a` using `Option.map`, where the function applies `f` to its argument and `b`. Essentially, this theorem asserts that the process of mapping a binary function over an optional value and a certain value (wrapped in `Option`) can be rewritten as mapping a function over the optional value alone, where the function is the partial application of the binary function to the certain value.
More concisely: For any types `α`, `β`, and `γ`, and any binary function `f : α → β → γ`, `Option.map₂ f (some x) (some y) = Option.map (λ a, f a y) (some x)`.
|
Option.map₂_map_left_comm
theorem Option.map₂_map_left_comm :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {α' : Type u_5}
{f : α' → β → γ} {g : α → α'} {f' : α → β → δ} {g' : δ → γ},
(∀ (a : α) (b : β), f (g a) b = g' (f' a b)) →
Option.map₂ f (Option.map g a) b = Option.map g' (Option.map₂ f' a b)
The theorem `Option.map₂_map_left_comm` states that for any types `α`, `β`, `γ`, `δ`, and `α'`, and any optional values `a` of type `α` and `b` of type `β`, and functions: `f` mapping from `α'` and `β` to `γ`, `g` mapping from `α` to `α'`, `f'` mapping from `α` and `β` to `δ`, and `g'` mapping from `δ` to `γ`, if for every possible pairs `(a, b)` of type `(α, β)`, the composition of `f` after `g` applied to `a` and `b` equals to the composition of `g'` after `f'` applied to `a` and `b`, then the map of the binary function `f` over the map of `g` over `a` and `b` is equal to the map of `g'` over the map of the binary function `f'` over `a` and `b`. In other words, it asserts that the operations of mapping a function and mapping a binary function can be exchanged under certain conditions. The theorem is essentially about the commutativity of certain function mappings over optional values.
More concisely: If for all `(a, b)`, `f(g'(a, b)) = g'(f(a, b), b)` and `g` has a defined output for `a`, then `Option.map₂ f (Option.map g a) = Option.map (g') (Option.map₂ f' (a, b))`.
|
Option.map_map₂_right_anticomm
theorem Option.map_map₂_right_anticomm :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {β' : Type u_6}
{f : α → β' → γ} {g : β → β'} {f' : β → α → δ} {g' : δ → γ},
(∀ (a : α) (b : β), f a (g b) = g' (f' b a)) →
Option.map₂ f a (Option.map g b) = Option.map g' (Option.map₂ f' b a)
This theorem, `Option.map_map₂_right_anticomm`, asserts that for all types `α`, `β`, `γ`, `δ`, `β'`, options `a` of type `α` and `b` of type `β`, binary functions `f : α → β' → γ` and `f' : β → α → δ`, unary functions `g : β → β'` and `g' : δ → γ`, if `f a (g b) = g' (f' b a)` for all `a` of type `α` and `b` of type `β`, then mapping `f` over the option `a` and the mapped option of `g` over `b` is equivalent to mapping `g'` over the mapped option of `f'` over `b` and the option `a`. This can be seen as a statement about the commutativity of certain operations involving `map` and `map₂` on `Option` types under specific conditions.
More concisely: For all types `α`, `β`, `γ`, `δ`, `β'`, options `a : Option α` and `b : Option β`, binary functions `f : α → β' → γ` and `f' : β → α → δ`, unary functions `g : β → β'` and `g' : δ → γ`, if `f a (g b) = g' (f' b a)` for all `a` and `b`, then `Option.map f a = Option.map (g' . Option.map f' ) (Option.map g b)`.
|
Option.map₂_assoc
theorem Option.map₂_assoc :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {c : Option γ}
{ε : Type u_8} {ε' : Type u_9} {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε} {g' : β → γ → ε'},
(∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)) →
Option.map₂ f (Option.map₂ g a b) c = Option.map₂ f' a (Option.map₂ g' b c)
The theorem `Option.map₂_assoc` states that for any types `α`, `β`, `γ`, `δ`, `ε`, and `ε'`, any options of these types `a`, `b`, and `c`, and any binary functions `f: δ → γ → ε`, `g: α → β → δ`, `f': α → ε' → ε`, `g': β → γ → ε'`, if for all `a` in `α`, `b` in `β` and `c` in `γ`, the function `f` applied to the output of function `g` applied to `a` and `b` and then applied to `c` equals the function `f'` applied to `a` and the output of function `g'` applied to `b` and `c`, then mapping `f` onto the result of mapping `g` onto `a` and `b` and then onto `c` equals mapping `f'` onto `a` and the result of mapping `g'` onto `b` and `c`. This theorem essentially establishes an associativity property for the `Option.map₂` operation.
More concisely: For functions `f`, `g`, `f'`, and `g'` between types `α`, `β`, `γ`, `δ`, and `ε`, `ε'`, if `f(g(a, b) c) = f'(a, g'(b, c))` for all `a : α`, `b : β`, and `c : γ`, then `Option.map₂ f (Option.map₂ g a b) c = Option.map₂ f' a (Option.map₂ g' b c)`.
|
Option.map_map₂_right_comm
theorem Option.map_map₂_right_comm :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {β' : Type u_6}
{f : α → β' → γ} {g : β → β'} {f' : α → β → δ} {g' : δ → γ},
(∀ (a : α) (b : β), f a (g b) = g' (f' a b)) →
Option.map₂ f a (Option.map g b) = Option.map g' (Option.map₂ f' a b)
The theorem `Option.map_map₂_right_comm` states that for any types `α`, `β`, `γ`, `δ`, and `β'`, any options `a` of type `Option α` and `b` of type `Option β`, any binary function `f` of type `α → β' → γ`, any function `g` of type `β → β'`, any binary function `f'` of type `α → β → δ`, and any function `g'` of type `δ → γ`, if for all `a` of type `α` and `b` of type `β`, `f a (g b)` equals `g' (f' a b)`, then mapping the binary function `f` over the option `a` and the result of mapping function `g` over the option `b` equals mapping the function `g'` over the result of mapping the binary function `f'` over the options `a` and `b`. In other words, this theorem gives a condition under which we can swap the order of `map` and `map₂` operations involving options and functions.
More concisely: If for all `α`, `β`, `γ`, `δ`, `α → β' → γ` function `f`, `β → β'` function `g`, `α → β` binary function `f'`, and `δ → γ` function `g'`, `f (g x) (g' y) = g' (f' x y)` implies `(Option.map g a).map f = Option.map (g') (Option.map f a)`, then the statement is true.
|
Option.map₂_comm
theorem Option.map₂_comm :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : Option α} {b : Option β} {g : β → α → γ},
(∀ (a : α) (b : β), f a b = g b a) → Option.map₂ f a b = Option.map₂ g b a
This theorem asserts that for any types `α`, `β`, and `γ`, any binary functions `f : α → β → γ` and `g : β → α → γ`, and any optional values `a : Option α` and `b : Option β`, if `f` and `g` are commutative for all `α` and `β` (that is, `f a b` equals `g b a` for all `a` and `b`), then applying the function `Option.map₂` to `f`, `a`, and `b` will yield the same result as applying `Option.map₂` to `g`, `b`, and `a`. In other words, the theorem states the commutativity of `Option.map₂` under the condition that the binary functions are commutative.
More concisely: For commutative functions `f : α → β → γ` and `g : β → α → γ`, Option.map₂ preserves commutativity, that is, Option.map₂ `f` `a` `b` = Option.map₂ `g` `b` `a` for all optional values `a : Option α` and `b : Option β`.
|
Option.map₂_right_identity
theorem Option.map₂_right_identity :
∀ {α : Type u_1} {β : Type u_2} {f : α → β → α} {b : β},
(∀ (a : α), f a b = a) → ∀ (o : Option α), Option.map₂ f o (some b) = o
This theorem states that for any types `α` and `β`, and a binary function `f` from `α` and `β` to `α`, if there exists an element `b` of type `β` which is a right identity for `f` (i.e., for any `a` of `α`, `f a b = a`), then `some b` is also a right identity for `Option.map₂ f`. In other words, when the binary function `f` is applied to any optional value `o` of type `α` and `some b`, it results in the original optional value `o`. This can be understood as lifting the binary operation `f` and its right identity `b` to the optional context.
More concisely: For any types `α` and `β`, if `f : α -> α -> α` has a right identity `b : β`, then `Option.map₂ f (some a) (some b) = some a` for all `a : α`.
|
Option.map₂_left_identity
theorem Option.map₂_left_identity :
∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {a : α},
(∀ (b : β), f a b = b) → ∀ (o : Option β), Option.map₂ f (some a) o = o
This theorem states that if an element `a` from a type `α` acts as a left identity for a binary operation `f` (i.e., for any element `b` of type `β`, `f a b` equals `b`), then `some a` (the `Option` version of `a`) is a left identity for the `Option` version of the binary operation `f`, denoted as `Option.map₂ f`. In other words, given any `Option` of type `β` denoted as `o`, applying `Option.map₂ f` to `some a` and `o` results in `o`. In terms of functional programming, it basically says that if `f` returns the second argument when applied to `a` and any second argument, then applying the optionalized version of `f` to `some a` and any `Option` returns the same `Option`.
More concisely: If `a` is a left identity for binary operation `f` on types `α` and `β`, then `some a` is a left identity for the `Option.map₂ f` operation on `Option β`.
|
Option.map_map₂_antidistrib_left
theorem Option.map_map₂_antidistrib_left :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β → γ} {a : Option α} {b : Option β}
{β' : Type u_6} {g : γ → δ} {f' : β' → α → δ} {g' : β → β'},
(∀ (a : α) (b : β), g (f a b) = f' (g' b) a) →
Option.map g (Option.map₂ f a b) = Option.map₂ f' (Option.map g' b) a
This theorem, `Option.map_map₂_antidistrib_left`, states that for all types `α`, `β`, `γ`, and `δ`, and for all functions `f : α → β → γ`, `g : γ → δ`, `f' : β' → α → δ` and `g' : β → β'`, and for all optional values `a : Option α` and `b : Option β`, if for every pair of values `a : α` and `b : β`, the value of `g` applied to the result of `f` applied to `a` and `b` equals the result of `f'` applied to the result of `g'` applied to `b` and `a`, then the value of `Option.map` applied to `g` and the result of `Option.map₂` applied to `f`, `a`, and `b` equals the result of `Option.map₂` applied to `f'`, the result of `Option.map` applied to `g'` and `b`, and `a`.
In simpler terms, this theorem relates the mapping of functions over optional values with a particular form of associativity and commutativity, given a certain condition on the functions `f`, `g`, `f'` and `g'`.
More concisely: If for all `α β γ δ` and functions `f : α → β → γ`, `g : γ → δ`, `f' : β' → α → δ`, and `g' : β → β'`, with `a : Option α` and `b : Option β`, `g (f a b) = f' (g' b a)`, then `Option.map g (Option.map₂ f a b) = Option.map₂ f' (Option.map g' b) a`.
|
Option.map_map₂_antidistrib_right
theorem Option.map_map₂_antidistrib_right :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β → γ} {a : Option α} {b : Option β}
{α' : Type u_5} {g : γ → δ} {f' : β → α' → δ} {g' : α → α'},
(∀ (a : α) (b : β), g (f a b) = f' b (g' a)) →
Option.map g (Option.map₂ f a b) = Option.map₂ f' b (Option.map g' a)
The theorem `Option.map_map₂_antidistrib_right` states that for any types `α`, `β`, `γ`, `δ`, `α'`, two functions `f` of type `α → β → γ` and `g` of type `γ → δ`, an option type `a` of `Option α`, an option type `b` of `Option β`, a function `f'` of type `β → α' → δ`, and a function `g'` of type `α → α'`, if for all values `a` of type `α` and `b` of type `β`, the function composition `g (f a b)` equals `f' b (g' a)`, then mapping `g` over the result of applying `Option.map₂` with `f` to `a` and `b` is equal to the result of applying `Option.map₂` with `f'` to `b` and the result of mapping `g'` over `a`. In other words, this theorem asserts a specific distributive property of `Option.map` and `Option.map₂` under certain conditions.
More concisely: If for all `a : α` and `b : β`, `g (f a b) = f' b (g' a)`, then `Option.map₂ g (Option.map₂ f a b) = Option.map₂ f' b (Option.map₁ g' a)`.
|
Option.mem_map₂_iff
theorem Option.mem_map₂_iff :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : Option α} {b : Option β} {c : γ},
c ∈ Option.map₂ f a b ↔ ∃ a' b', a' ∈ a ∧ b' ∈ b ∧ f a' b' = c
This theorem asserts that for any types α, β, and γ, and for any binary function `f : α → β → γ`, an element `c : γ` is in the image of `f` applied to two options `a : Option α` and `b : Option β` if and only if there exist elements `a' : α` and `b' : β` such that `a'` is in `a`, `b'` is in `b`, and `f a' b'` equals `c`. In other words, this is about when an element is in the result of applying a binary function to two optional values.
More concisely: For any types α, β, γ and binary function f : α → β → γ, an element c is in the image of f applied to optional values a : Option α and b : Option β if and only if there exist a' : α and b' : β in a and b, respectively, such that f a' b' = c.
|
Option.map₂_eq_none_iff
theorem Option.map₂_eq_none_iff :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : Option α} {b : Option β},
Option.map₂ f a b = none ↔ a = none ∨ b = none
This theorem states that for any types `α`, `β`, and `γ` and any binary function `f : α → β → γ` applied to `Option α` and `Option β`, `Option.map₂ f a b` results in `none` if and only if either `a` is `none` or `b` is `none`. This means that in the context of option types, the failure of the binary function `f` to produce a result equates to the absence of a value in either of the input options.
More concisely: For any functions `f : α → β → γ` and `a : Option α`, `b : Option β`, `Option.map₂ f a b = none` if and only if `a = none` or `b = none`.
|