Binary map of options #
This file defines the binary map of Option. This is mostly useful to define pointwise operations
on intervals.
Main declarations #
Option.map₂: Binary map of options.
Notes #
This file is very similar to the n-ary section of Mathlib.Data.Set.Basic, to
Mathlib.Data.Finset.NAry and to Mathlib.Order.Filter.NAry. Please keep them in sync.
(porting note - only some of these may exist right now!)
We do not define Option.map₃ as its only purpose so far would be to prove properties of
Option.map₂ and casing already fulfills this task.
def
Option.map₂
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(a : Option α)
(b : Option β)
:
Option γ
The image of a binary function f : α → β → γ as a function Option α → Option β → Option γ.
Mathematically this should be thought of as the image of the corresponding function α × β → γ.
Equations
- Option.map₂ f a b = Option.bind a fun (a : α) => Option.map (f a) b
Instances For
theorem
Option.map₂_def
{α : Type u}
{β : Type u}
{γ : Type u}
(f : α → β → γ)
(a : Option α)
(b : Option β)
:
Option.map₂ f a b = Seq.seq (f <$> a) fun (x : Unit) => b
Option.map₂ in terms of monadic operations. Note that this can't be taken as the definition
because of the lack of universe polymorphism.
theorem
Option.map₂_some_some
{α : Type u_2}
{β : Type u_3}
{γ : Type u_1}
(f : α → β → γ)
(a : α)
(b : β)
:
Option.map₂ f (some a) (some b) = some (f a b)
theorem
Option.map₂_coe_coe
{α : Type u_2}
{β : Type u_3}
{γ : Type u_1}
(f : α → β → γ)
(a : α)
(b : β)
:
Option.map₂ f (some a) (some b) = some (f a b)
@[simp]
theorem
Option.map₂_none_left
{α : Type u_3}
{β : Type u_1}
{γ : Type u_2}
(f : α → β → γ)
(b : Option β)
:
Option.map₂ f none b = none
@[simp]
theorem
Option.map₂_none_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_2}
(f : α → β → γ)
(a : Option α)
:
Option.map₂ f a none = none
@[simp]
theorem
Option.map₂_coe_left
{α : Type u_3}
{β : Type u_1}
{γ : Type u_2}
(f : α → β → γ)
(a : α)
(b : Option β)
:
Option.map₂ f (some a) b = Option.map (fun (b : β) => f a b) b
@[simp]
theorem
Option.map₂_coe_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_2}
(f : α → β → γ)
(a : Option α)
(b : β)
:
Option.map₂ f a (some b) = Option.map (fun (a : α) => f a b) a
theorem
Option.map₂_swap
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(a : Option α)
(b : Option β)
:
Option.map₂ f a b = Option.map₂ (fun (a : β) (b : α) => f b a) b a
theorem
Option.map_map₂
{α : Type u_3}
{β : Type u_4}
{γ : Type u_2}
{a : Option α}
{b : Option β}
{δ : Type u_1}
(f : α → β → γ)
(g : γ → δ)
:
Option.map g (Option.map₂ f a b) = Option.map₂ (fun (a : α) (b : β) => g (f a b)) a b
theorem
Option.map₂_map_left
{α : Type u_4}
{β : Type u_3}
{γ : Type u_2}
{a : Option α}
{b : Option β}
{δ : Type u_1}
(f : γ → β → δ)
(g : α → γ)
:
Option.map₂ f (Option.map g a) b = Option.map₂ (fun (a : α) (b : β) => f (g a) b) a b
theorem
Option.map₂_map_right
{α : Type u_2}
{β : Type u_4}
{γ : Type u_3}
{a : Option α}
{b : Option β}
{δ : Type u_1}
(f : α → γ → δ)
(g : β → γ)
:
Option.map₂ f a (Option.map g b) = Option.map₂ (fun (a : α) (b : β) => f a (g b)) a b
@[simp]
theorem
Option.map₂_curry
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α × β → γ)
(a : Option α)
(b : Option β)
:
Option.map₂ (Function.curry f) a b = Option.map f (Option.map₂ Prod.mk a b)
@[simp]
theorem
Option.map_uncurry
{α : Type u_2}
{β : Type u_1}
{γ : Type u_3}
(f : α → β → γ)
(x : Option (α × β))
:
Option.map (Function.uncurry f) x = Option.map₂ f (Option.map Prod.fst x) (Option.map Prod.snd x)
Algebraic replacement rules #
A collection of lemmas to transfer associativity, commutativity, distributivity, ... of operations
to the associativity, commutativity, distributivity, ... of Option.map₂ of those operations.
The proof pattern is map₂_lemma operation_lemma. For example, map₂_comm mul_comm proves that
map₂ (*) a b = map₂ (*) g f in a CommSemigroup.
theorem
Option.map₂_assoc
{α : Type u_5}
{β : Type u_6}
{γ : Type u_4}
{a : Option α}
{b : Option β}
{c : Option γ}
{δ : Type u_1}
{ε : Type u_2}
{ε' : Type u_3}
{f : δ → γ → ε}
{g : α → β → δ}
{f' : α → ε' → ε}
{g' : β → γ → ε'}
(h_assoc : ∀ (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)
theorem
Option.map₂_comm
{α : Type u_2}
{β : Type u_3}
{γ : Type u_1}
{f : α → β → γ}
{a : Option α}
{b : Option β}
{g : β → α → γ}
(h_comm : ∀ (a : α) (b : β), f a b = g b a)
:
Option.map₂ f a b = Option.map₂ g b a
theorem
Option.map₂_left_comm
{α : Type u_4}
{β : Type u_5}
{γ : Type u_6}
{a : Option α}
{b : Option β}
{c : Option γ}
{δ : Type u_1}
{ε : Type u_2}
{δ' : Type u_3}
{f : α → δ → ε}
{g : β → γ → δ}
{f' : α → γ → δ'}
{g' : β → δ' → ε}
(h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c))
:
Option.map₂ f a (Option.map₂ g b c) = Option.map₂ g' b (Option.map₂ f' a c)
theorem
Option.map₂_right_comm
{α : Type u_5}
{β : Type u_6}
{γ : Type u_4}
{a : Option α}
{b : Option β}
{c : Option γ}
{δ : Type u_1}
{ε : Type u_2}
{δ' : Type u_3}
{f : δ → γ → ε}
{g : α → β → δ}
{f' : α → γ → δ'}
{g' : δ' → β → ε}
(h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b)
:
Option.map₂ f (Option.map₂ g a b) c = Option.map₂ g' (Option.map₂ f' a c) b
theorem
Option.map_map₂_distrib
{α : Type u_5}
{β : Type u_6}
{γ : Type u_4}
{f : α → β → γ}
{a : Option α}
{b : Option β}
{δ : Type u_1}
{α' : Type u_2}
{β' : Type u_3}
{g : γ → δ}
{f' : α' → β' → δ}
{g₁ : α → α'}
{g₂ : β → β'}
(h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b))
:
Option.map g (Option.map₂ f a b) = Option.map₂ f' (Option.map g₁ a) (Option.map g₂ b)
The following symmetric restatement are needed because unification has a hard time figuring all the functions if you symmetrize on the spot. This is also how the other n-ary APIs do it.
theorem
Option.map_map₂_distrib_left
{α : Type u_4}
{β : Type u_5}
{γ : Type u_3}
{f : α → β → γ}
{a : Option α}
{b : Option β}
{δ : Type u_1}
{α' : Type u_2}
{g : γ → δ}
{f' : α' → β → δ}
{g' : α → α'}
(h_distrib : ∀ (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
Symmetric statement to Option.map₂_map_left_comm.
theorem
Option.map_map₂_distrib_right
{α : Type u_4}
{β : Type u_5}
{γ : Type u_3}
{f : α → β → γ}
{a : Option α}
{b : Option β}
{δ : Type u_1}
{β' : Type u_2}
{g : γ → δ}
{f' : α → β' → δ}
{g' : β → β'}
(h_distrib : ∀ (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)
Symmetric statement to Option.map_map₂_right_comm.
theorem
Option.map₂_map_left_comm
{α : Type u_5}
{β : Type u_4}
{γ : Type u_3}
{a : Option α}
{b : Option β}
{α' : Type u_1}
{δ : Type u_2}
{f : α' → β → γ}
{g : α → α'}
{f' : α → β → δ}
{g' : δ → γ}
(h_left_comm : ∀ (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)
Symmetric statement to Option.map_map₂_distrib_left.
theorem
Option.map_map₂_right_comm
{α : Type u_4}
{β : Type u_5}
{γ : Type u_3}
{a : Option α}
{b : Option β}
{β' : Type u_1}
{δ : Type u_2}
{f : α → β' → γ}
{g : β → β'}
{f' : α → β → δ}
{g' : δ → γ}
(h_right_comm : ∀ (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)
Symmetric statement to Option.map_map₂_distrib_right.
theorem
Option.map_map₂_antidistrib
{α : Type u_5}
{β : Type u_6}
{γ : Type u_4}
{f : α → β → γ}
{a : Option α}
{b : Option β}
{δ : Type u_1}
{β' : Type u_2}
{α' : Type u_3}
{g : γ → δ}
{f' : β' → α' → δ}
{g₁ : β → β'}
{g₂ : α → α'}
(h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a))
:
Option.map g (Option.map₂ f a b) = Option.map₂ f' (Option.map g₁ b) (Option.map g₂ a)
theorem
Option.map_map₂_antidistrib_left
{α : Type u_4}
{β : Type u_5}
{γ : Type u_3}
{f : α → β → γ}
{a : Option α}
{b : Option β}
{δ : Type u_1}
{β' : Type u_2}
{g : γ → δ}
{f' : β' → α → δ}
{g' : β → β'}
(h_antidistrib : ∀ (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
Symmetric statement to Option.map₂_map_left_anticomm.
theorem
Option.map_map₂_antidistrib_right
{α : Type u_4}
{β : Type u_5}
{γ : Type u_3}
{f : α → β → γ}
{a : Option α}
{b : Option β}
{δ : Type u_1}
{α' : Type u_2}
{g : γ → δ}
{f' : β → α' → δ}
{g' : α → α'}
(h_antidistrib : ∀ (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)
Symmetric statement to Option.map_map₂_right_anticomm.
theorem
Option.map₂_map_left_anticomm
{α : Type u_5}
{β : Type u_4}
{γ : Type u_3}
{a : Option α}
{b : Option β}
{α' : Type u_1}
{δ : Type u_2}
{f : α' → β → γ}
{g : α → α'}
{f' : β → α → δ}
{g' : δ → γ}
(h_left_anticomm : ∀ (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)
Symmetric statement to Option.map_map₂_antidistrib_left.
theorem
Option.map_map₂_right_anticomm
{α : Type u_4}
{β : Type u_5}
{γ : Type u_3}
{a : Option α}
{b : Option β}
{β' : Type u_1}
{δ : Type u_2}
{f : α → β' → γ}
{g : β → β'}
{f' : β → α → δ}
{g' : δ → γ}
(h_right_anticomm : ∀ (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)
Symmetric statement to Option.map_map₂_antidistrib_right.
theorem
Option.map₂_left_identity
{α : Type u_2}
{β : Type u_1}
{f : α → β → β}
{a : α}
(h : ∀ (b : β), f a b = b)
(o : Option β)
:
Option.map₂ f (some a) o = o
If a is a left identity for a binary operation f, then some a is a left identity for
Option.map₂ f.
theorem
Option.map₂_right_identity
{α : Type u_1}
{β : Type u_2}
{f : α → β → α}
{b : β}
(h : ∀ (a : α), f a b = a)
(o : Option α)
:
Option.map₂ f o (some b) = o
If b is a right identity for a binary operation f, then some b is a right identity for
Option.map₂ f.