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.coe_get
{α : Type u_1}
{o : Option α}
(h : Option.isSome o = true)
:
some (Option.get o h) = o
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.none_bind'
{α : Type u_1}
{β : Type u_2}
(f : α → Option β)
:
Option.bind none f = none
@[simp]
theorem
Option.some_bind'
{α : Type u_1}
{β : Type u_2}
(a : α)
(f : α → Option β)
:
Option.bind (some a) f = f a
theorem
Option.bind_eq_bind
{α : Type u_5}
{β : Type u_5}
{f : α → Option β}
{x : Option α}
:
x >>= f = Option.bind x 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.pbind_eq_bind
{α : Type u_1}
{β : Type u_2}
(f : α → Option β)
(x : Option α)
:
(Option.pbind x fun a x => f a) = Option.bind x f
theorem
Option.map_bind
{α : Type u_5}
{β : Type u_5}
{γ : Type u_5}
(f : β → γ)
(x : Option α)
(g : α → Option β)
:
Option.map f (x >>= g) = do
let a ← x
Option.map f (g a)
theorem
Option.map_bind'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : β → γ)
(x : Option α)
(g : α → Option β)
:
Option.map f (Option.bind x g) = Option.bind x fun a => Option.map f (g a)
theorem
Option.map_pbind
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : β → γ)
(x : Option α)
(g : (a : α) → a ∈ x → Option β)
:
Option.map f (Option.pbind x g) = Option.pbind x fun a H => Option.map f (g a H)
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.pbind (Option.map f x) g = Option.pbind x fun a h => g (f a) (_ : f a ∈ Option.map f x)
@[simp]
theorem
Option.pmap_none
{α : Type u_1}
{β : Type u_2}
{p : α → Prop}
(f : (a : α) → p a → β)
{H : (a : α) → a ∈ none → p a}
:
Option.pmap f none H = none
@[simp]
theorem
Option.pmap_some
{α : Type u_1}
{β : Type u_2}
{p : α → Prop}
(f : (a : α) → p a → β)
{x : α}
(h : p x)
:
Option.pmap f (some x) = fun x => some (f x h)
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 (h a ha) ∈ 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 => f (g a) h) x fun a h => H (g a) (_ : g a ∈ Option.map g 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 => 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 => f a) x H = Option.map f x
theorem
Option.pmap_bind
{α : Type u_5}
{β : Type u_5}
{γ : Type u_5}
{x : Option α}
{g : α → Option β}
{p : β → Prop}
{f : (b : β) → p b → γ}
(H : (a : β) → a ∈ x >>= g → p a)
(H' : ∀ (a : α) (b : β), b ∈ g a → b ∈ x >>= g)
:
Option.pmap f (x >>= g) H = do
let a ← x
Option.pmap f (g a) fun b h => H b (H' a b h)
theorem
Option.bind_pmap
{α : Type u_5}
{β : Type u_6}
{γ : Type u_6}
{p : α → Prop}
(f : (a : α) → p a → β)
(x : Option α)
(g : β → Option γ)
(H : (a : α) → a ∈ x → p a)
:
Option.pmap f x H >>= g = Option.pbind x fun a h => g (f a (H a h))
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.join (Option.pmap (Option.pmap f) x H) = Option.pmap f (Option.join x) fun a h => H (some a) (_ : some a ∈ x) a (_ : some a = some a)
@[simp]
theorem
Option.some_orElse'
{α : Type u_1}
(a : α)
(x : Option α)
:
(Option.orElse (some a) fun x => x) = some a
@[simp]
@[simp]
theorem
Option.iget_mem
{α : Type u_1}
[Inhabited α]
{o : Option α}
:
Option.isSome o = true → Option.iget o ∈ o
theorem
Option.iget_of_mem
{α : Type u_1}
[Inhabited α]
{a : α}
{o : Option α}
:
a ∈ o → Option.iget o = a
theorem
Option.getD_default_eq_iget
{α : Type u_1}
[Inhabited α]
(o : Option α)
:
Option.getD o default = Option.iget o
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.
Equations
- Option.casesOn' x x x = match x, x, x with | none, n, x => n | some a, x, s => s a
Instances For
@[simp]
theorem
Option.casesOn'_none
{α : Type u_1}
{β : Type u_2}
(x : β)
(f : α → β)
:
Option.casesOn' none x f = x
@[simp]
theorem
Option.casesOn'_some
{α : Type u_1}
{β : Type u_2}
(x : β)
(f : α → β)
(a : α)
:
Option.casesOn' (some a) x f = f a
@[simp]
theorem
Option.casesOn'_coe
{α : Type u_1}
{β : Type u_2}
(x : β)
(f : α → β)
(a : α)
:
Option.casesOn' (some a) x f = f a
theorem
Option.casesOn'_none_coe
{α : Type u_1}
{β : Type u_2}
(f : Option α → β)
(o : Option α)
:
Option.casesOn' o (f none) (f ∘ fun a => some a) = f o
theorem
Option.elim_none_some
{α : Type u_1}
{β : Type u_2}
(f : Option α → β)
:
(fun x => Option.elim x (f none) (f ∘ some)) = f
theorem
Option.elim_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(h : α → β)
{f : γ → α}
{x : α}
{i : Option γ}
:
(Option.elim i (h x) fun j => h (f j)) = h (Option.elim i x f)
theorem
Option.elim_comp₂
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(h : α → β → γ)
{f : γ → α}
{x : α}
{g : γ → β}
{y : β}
{i : Option γ}
:
(Option.elim i (h x y) fun j => h (f j) (g j)) = h (Option.elim i x f) (Option.elim i y g)
theorem
Option.elim_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : γ → α → β}
{x : α → β}
{i : Option γ}
{y : α}
:
Option.elim γ (α → β) i x f y = Option.elim i (x y) fun j => f j y