Option of a type #
This file develops the basic theory of option types.
If α is a type, then Option α can be understood as the type with one more element than α.
Option α has terms some a, where a : α, and none, which is the added element.
This is useful in multiple ways:
- It is the prototype of addition of terms to a type. See for example
WithBot αwhich usesnoneas an element smaller than all others. - It can be used to define failsafe partial functions, which return
some the_result_we_expectif we can findthe_result_we_expect, andnoneif there is no meaningful result. This forces any subsequent use of the partial function to explicitly deal with the exceptions that make it returnnone. Optionis a monad. We love monads.
Part is an alternative to Option that can be seen as the type of True/False values
along with a term a : α if the value is True.
@[simp]
theorem
Option.mem_map_of_injective
{α : Type u_1}
{β : Type u_2}
{f : α → β}
(H : Function.Injective f)
{a : α}
{o : Option α}
:
f a ∈ Option.map f o ↔ a ∈ o
theorem
Option.forall_mem_map
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{o : Option α}
{p : β → Prop}
:
(∀ (y : β), y ∈ Option.map f o → p y) ↔ ∀ (x : α), x ∈ o → p (f x)
theorem
Option.Mem.leftUnique
{α : Type u_1}
:
Relator.LeftUnique fun (x1 : α) (x2 : Option α) => x1 ∈ x2
theorem
Option.map_injective
{α : Type u_1}
{β : Type u_2}
{f : α → β}
(Hf : Function.Injective f)
:
Option.map f is injective if f is injective.
@[simp]
theorem
Option.map_comp_some
{α : Type u_1}
{β : Type u_2}
(f : α → β)
:
Option.map f ∘ some = some ∘ f
@[simp]
theorem
Option.map_coe'
{α : Type u_1}
{β : Type u_2}
{a : α}
{f : α → β}
:
Option.map f (some a) = some (f a)
Option.map as a function between functions is injective.
@[simp]
theorem
Option.map_inj
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{g : α → β}
:
Option.map f = Option.map g ↔ f = g
theorem
Option.map_comm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{f₁ : α → β}
{f₂ : α → γ}
{g₁ : β → δ}
{g₂ : γ → δ}
(h : g₁ ∘ f₁ = g₂ ∘ f₂)
(a : α)
:
Option.map g₁ (Option.map f₁ (some a)) = Option.map g₂ (Option.map f₂ (some a))
theorem
Option.map_bind'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : β → γ)
(x : Option α)
(g : α → Option β)
:
Option.map f (x.bind g) = x.bind fun (a : α) => Option.map f (g a)
theorem
Option.pbind_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β)
(x : Option α)
(g : (b : β) → b ∈ Option.map f x → Option γ)
:
(Option.map f x).pbind g = x.pbind fun (a : α) (h : a ∈ x) => g (f a) ⋯
theorem
Option.mem_pmem
{α : Type u_1}
{β : Type u_2}
{p : α → Prop}
(f : (a : α) → p a → β)
(x : Option α)
{a : α}
(h : ∀ (a : α), a ∈ x → p a)
(ha : a ∈ x)
:
f a ⋯ ∈ Option.pmap f x h
theorem
Option.pmap_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{p : α → Prop}
(f : (a : α) → p a → β)
(g : γ → α)
(x : Option γ)
(H : ∀ (a : α), a ∈ Option.map g x → p a)
:
Option.pmap f (Option.map g x) H = Option.pmap (fun (a : γ) (h : p (g a)) => f (g a) h) x ⋯
theorem
Option.map_pmap
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{p : α → Prop}
(g : β → γ)
(f : (a : α) → p a → β)
(x : Option α)
(H : ∀ (a : α), a ∈ x → p a)
:
Option.map g (Option.pmap f x H) = Option.pmap (fun (a : α) (h : p a) => g (f a h)) x H
theorem
Option.pmap_eq_map
{α : Type u_1}
{β : Type u_2}
(p : α → Prop)
(f : α → β)
(x : Option α)
(H : ∀ (a : α), a ∈ x → p a)
:
Option.pmap (fun (a : α) (x : p a) => f a) x H = Option.map f x
theorem
Option.join_pmap_eq_pmap_join
{α : Type u_1}
{β : Type u_2}
{p : α → Prop}
{f : (a : α) → p a → β}
{x : Option (Option α)}
(H : ∀ (a : Option α), a ∈ x → ∀ (a_2 : α), a_2 ∈ a → p a_2)
:
(Option.pmap (Option.pmap f) x H).join = Option.pmap f x.join ⋯
theorem
Option.liftOrGet_choice
{α : Type u_1}
{f : α → α → α}
(h : ∀ (a b : α), f a b = a ∨ f a b = b)
(o₁ : Option α)
(o₂ : Option α)
:
Option.liftOrGet f o₁ o₂ = o₁ ∨ Option.liftOrGet f o₁ o₂ = o₂
Given an element of a : Option α, a default element b : β and a function α → β, apply this
function to a if it comes from α, and return b otherwise.
Instances For
@[simp]
theorem
Option.casesOn'_none
{α : Type u_1}
{β : Type u_2}
(x : β)
(f : α → β)
:
none.casesOn' x f = x