# 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 uses none as an element smaller than all others.
• It can be used to define failsafe partial functions, which return some the_result_we_expect if we can find the_result_we_expect, and none if there is no meaningful result. This forces any subsequent use of the partial function to explicitly deal with the exceptions that make it return none.
• Option is 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.

theorem Option.coe_def {α : Type u_1} :
(fun (a : α) => some a) = some
theorem Option.mem_map {α : Type u_1} {β : Type u_2} {f : αβ} {y : β} {o : } :
y ∃ (x : α), x o f x = y
@[simp]
theorem Option.mem_map_of_injective {α : Type u_1} {β : Type u_2} {f : αβ} (H : ) {a : α} {o : } :
f a a o
theorem Option.forall_mem_map {α : Type u_1} {β : Type u_2} {f : αβ} {o : } {p : βProp} :
(∀ (y : β), y p y) ∀ (x : α), x op (f x)
theorem Option.exists_mem_map {α : Type u_1} {β : Type u_2} {f : αβ} {o : } {p : βProp} :
(∃ (y : β), y p y) ∃ (x : α), x o p (f x)
theorem Option.coe_get {α : Type u_1} {o : } (h : o.isSome = true) :
some (o.get h) = o
theorem Option.eq_of_mem_of_mem {α : Type u_1} {a : α} {o1 : } {o2 : } (h1 : a o1) (h2 : a o2) :
o1 = o2
theorem Option.Mem.leftUnique {α : Type u_1} :
Relator.LeftUnique fun (x1 : α) (x2 : ) => x1 x2
theorem Option.some_injective (α : Type u_5) :
theorem Option.map_injective {α : Type u_1} {β : Type u_2} {f : αβ} (Hf : ) :

Option.map f is injective if f is injective.

@[simp]
theorem Option.map_comp_some {α : Type u_1} {β : Type u_2} (f : αβ) :
some = some f
@[simp]
theorem Option.none_bind' {α : Type u_1} {β : Type u_2} (f : α) :
none.bind f = none
@[simp]
theorem Option.some_bind' {α : Type u_1} {β : Type u_2} (a : α) (f : α) :
(some a).bind f = f a
theorem Option.bind_eq_some' {α : Type u_1} {β : Type u_2} {x : } {f : α} {b : β} :
x.bind f = some b ∃ (a : α), x = some a f a = some b
theorem Option.bind_congr {α : Type u_1} {β : Type u_2} {f : α} {g : α} {x : } (h : ∀ (a : α), a xf a = g a) :
x.bind f = x.bind g
theorem Option.bind_congr' {α : Type u_1} {β : Type u_2} {f : α} {g : α} {x : } {y : } (hx : x = y) (hf : ∀ (a : α), a yf a = g a) :
x.bind f = y.bind g
theorem Option.joinM_eq_join {α : Type u_1} :
joinM = Option.join
theorem Option.bind_eq_bind' {α : Type u} {β : Type u} {f : α} {x : } :
x >>= f = x.bind f
theorem Option.map_coe {α : Type u_5} {β : Type u_5} {a : α} {f : αβ} :
f <\$> some a = some (f a)
@[simp]
theorem Option.map_coe' {α : Type u_1} {β : Type u_2} {a : α} {f : αβ} :
Option.map f (some a) = some (f a)
theorem Option.map_injective' {α : Type u_1} {β : Type u_2} :

Option.map as a function between functions is injective.

@[simp]
theorem Option.map_inj {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} :
f = g
@[simp]
theorem Option.map_eq_id {α : Type u_1} {f : αα} :
= id f = id
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 : α) (x : ) :
(x.pbind fun (a : α) (x : a x) => f a) = x.bind f
theorem Option.map_bind {α : Type u_5} {β : Type u_5} {γ : Type u_5} (f : βγ) (x : ) (g : α) :
Option.map f (x >>= g) = do let ax Option.map f (g a)
theorem Option.map_bind' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : βγ) (x : ) (g : α) :
Option.map f (x.bind g) = x.bind fun (a : α) => Option.map f (g a)
theorem Option.map_pbind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : βγ) (x : ) (g : (a : α) → a x) :
Option.map f (x.pbind g) = x.pbind fun (a : α) (H : a x) => Option.map f (g a H)
theorem Option.pbind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (x : ) (g : (b : β) → b ) :
(Option.map f x).pbind g = x.pbind fun (a : α) (h : a x) => g (f a)
@[simp]
theorem Option.pmap_none {α : Type u_1} {β : Type u_2} {p : αProp} (f : (a : α) → p aβ) {H : ∀ (a : α), a nonep 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_1 : ∀ (a : α), a some xp a) => some (f x h)
theorem Option.mem_pmem {α : Type u_1} {β : Type u_2} {p : αProp} (f : (a : α) → p aβ) (x : ) {a : α} (h : ∀ (a : α), a xp 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 : ) (H : ∀ (a : α), a 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 : ) (H : ∀ (a : α), a xp 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 : ) (H : ∀ (a : α), a xp a) :
Option.pmap (fun (a : α) (x : p a) => f a) x H =
theorem Option.pmap_bind {α : Type u_5} {β : Type u_5} {γ : Type u_5} {x : } {g : α} {p : βProp} {f : (b : β) → p bγ} (H : ∀ (a : β), a x >>= gp a) (H' : ∀ (a : α) (b : β), b g ab x >>= g) :
Option.pmap f (x >>= g) H = do let ax Option.pmap f (g a)
theorem Option.bind_pmap {α : Type u_5} {β : Type u_6} {γ : Type u_6} {p : αProp} (f : (a : α) → p aβ) (x : ) (g : β) (H : ∀ (a : α), a xp a) :
Option.pmap f x H >>= g = x.pbind fun (a : α) (h : a x) => g (f a )
theorem Option.pbind_eq_none {α : Type u_1} {β : Type u_2} {x : } {f : (a : α) → a x} (h' : ∀ (a : α) (H : a x), f a H = nonex = none) :
x.pbind f = none x = none
theorem Option.pbind_eq_some {α : Type u_1} {β : Type u_2} {x : } {f : (a : α) → a x} {y : β} :
x.pbind f = some y ∃ (z : α), ∃ (H : z x), f z H = some y
theorem Option.pmap_eq_none_iff {α : Type u_1} {β : Type u_2} {p : αProp} {f : (a : α) → p aβ} {x : } {h : ∀ (a : α), a xp a} :
Option.pmap f x h = none x = none
theorem Option.pmap_eq_some_iff {α : Type u_1} {β : Type u_2} {p : αProp} {f : (a : α) → p aβ} {x : } {hf : ∀ (a : α), a xp a} {y : β} :
Option.pmap f x hf = some y ∃ (a : α), ∃ (H : x = some a), f a = y
theorem Option.join_pmap_eq_pmap_join {α : Type u_1} {β : Type u_2} {p : αProp} {f : (a : α) → p aβ} {x : Option (Option α)} (H : ∀ (a : ), a x∀ (a_2 : α), a_2 ap a_2) :
(Option.pmap (Option.pmap f) x H).join = Option.pmap f x.join
@[simp]
theorem Option.seq_some {α : Type u_5} {β : Type u_5} {a : α} {f : αβ} :
(Seq.seq (some f) fun (x : Unit) => some a) = some (f a)
@[simp]
theorem Option.some_orElse' {α : Type u_1} (a : α) (x : ) :
((some a).orElse fun (x_1 : Unit) => x) = some a
@[simp]
theorem Option.none_orElse' {α : Type u_1} (x : ) :
(none.orElse fun (x_1 : Unit) => x) = x
@[simp]
theorem Option.orElse_none' {α : Type u_1} (x : ) :
(x.orElse fun (x : Unit) => none) = x
theorem Option.exists_ne_none {α : Type u_1} {p : Prop} :
(∃ (x : ), x none p x) ∃ (x : α), p (some x)
theorem Option.iget_mem {α : Type u_1} [] {o : } :
o.isSome = trueo.iget o
theorem Option.iget_of_mem {α : Type u_1} [] {a : α} {o : } :
a oo.iget = a
theorem Option.getD_default_eq_iget {α : Type u_1} [] (o : ) :
o.getD default = o.iget
@[simp]
theorem Option.guard_eq_some' {p : Prop} [] (u : Unit) :
= some u p
theorem Option.liftOrGet_choice {α : Type u_1} {f : ααα} (h : ∀ (a b : α), f a b = a f a b = b) (o₁ : ) (o₂ : ) :
Option.liftOrGet f o₁ o₂ = o₁ Option.liftOrGet f o₁ o₂ = o₂
def Option.casesOn' {α : Type u_1} {β : Type u_2} :
β(αβ)β

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
• none.casesOn' x✝ x = x✝
• (some a).casesOn' x✝ x = x a
Instances For
@[simp]
theorem Option.casesOn'_none {α : Type u_1} {β : Type u_2} (x : β) (f : αβ) :
none.casesOn' x f = x
@[simp]
theorem Option.casesOn'_some {α : Type u_1} {β : Type u_2} (x : β) (f : αβ) (a : α) :
(some a).casesOn' x f = f a
@[simp]
theorem Option.casesOn'_coe {α : Type u_1} {β : Type u_2} (x : β) (f : αβ) (a : α) :
(some a).casesOn' x f = f a
theorem Option.casesOn'_none_coe {α : Type u_1} {β : Type u_2} (f : β) (o : ) :
o.casesOn' (f none) (f fun (a : α) => some a) = f o
theorem Option.casesOn'_eq_elim {α : Type u_1} {β : Type u_2} (b : β) (f : αβ) (a : ) :
a.casesOn' b f = a.elim b f
theorem Option.orElse_eq_some {α : Type u_1} (o : ) (o' : ) (x : α) :
(HOrElse.hOrElse o fun (x : Unit) => o') = some x o = some x o = none o' = some x
theorem Option.orElse_eq_some' {α : Type u_1} (o : ) (o' : ) (x : α) :
(o.orElse fun (x : Unit) => o') = some x o = some x o = none o' = some x
@[simp]
theorem Option.orElse_eq_none {α : Type u_1} (o : ) (o' : ) :
(HOrElse.hOrElse o fun (x : Unit) => o') = none o = none o' = none
@[simp]
theorem Option.orElse_eq_none' {α : Type u_1} (o : ) (o' : ) :
(o.orElse fun (x : Unit) => o') = none o = none o' = none
theorem Option.choice_eq_none (α : Type u_5) [] :
= none
theorem Option.elim_none_some {α : Type u_1} {β : Type u_2} (f : β) :
(fun (x : ) => x.elim (f none) (f some)) = f
theorem Option.elim_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : αβ) {f : γα} {x : α} {i : } :
(i.elim (h x) fun (j : γ) => h (f j)) = h (i.elim x f)
theorem Option.elim_comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : αβγ) {f : γα} {x : α} {g : γβ} {y : β} {i : } :
(i.elim (h x y) fun (j : γ) => h (f j) (g j)) = h (i.elim x f) (i.elim y g)
theorem Option.elim_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : γαβ} {x : αβ} {i : } {y : α} :
i.elim x f y = i.elim (x y) fun (j : γ) => f j y
@[simp]
theorem Option.bnot_isSome {α : Type u_1} (a : ) :
(!a.isSome) = a.isNone
@[simp]
theorem Option.bnot_comp_isSome {α : Type u_1} :
(fun (x : Bool) => !x) Option.isSome = Option.isNone
@[simp]
theorem Option.bnot_isNone {α : Type u_1} (a : ) :
(!a.isNone) = a.isSome
@[simp]
theorem Option.bnot_comp_isNone {α : Type u_1} :
(fun (x : Bool) => !x) Option.isNone = Option.isSome
@[simp]
theorem Option.isNone_eq_false_iff {α : Type u_1} (a : ) :
a.isNone = false a.isSome = true
theorem Option.eq_none_or_eq_some {α : Type u_1} (a : ) :
a = none ∃ (x : α), a = some x
theorem Option.forall_some_ne_iff_eq_none {α : Type u_1} {o : } :
(∀ (x : α), some x o) o = none