# mathlib3documentation

data.option.basic

# Option of a type #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 with_bot α 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.

## Implementation notes #

option is currently defined in core Lean, but this will change in Lean 4.

theorem option.coe_def {α : Type u_1} :
theorem option.some_eq_coe {α : Type u_1} (a : α) :
theorem option.some_ne_none {α : Type u_1} (x : α) :
@[simp]
theorem option.coe_ne_none {α : Type u_1} (a : α) :
@[protected]
theorem option.forall {α : Type u_1} {p : Prop} :
( (x : option α), p x) (x : α), p (option.some x)
@[protected]
theorem option.exists {α : Type u_1} {p : Prop} :
( (x : option α), p x) (x : α), p (option.some x)
@[simp]
theorem option.get_mem {α : Type u_1} {o : option α} (h : (o.is_some)) :
o
theorem option.get_of_mem {α : Type u_1} {a : α} {o : option α} (h : (o.is_some)) :
a o = a
@[simp]
theorem option.not_mem_none {α : Type u_1} (a : α) :
@[simp]
theorem option.some_get {α : Type u_1} {x : option α} (h : (x.is_some)) :
= x
@[simp]
theorem option.get_some {α : Type u_1} (x : α) (h : ((option.some x).is_some)) :
= x
@[simp]
theorem option.get_or_else_some {α : Type u_1} (x y : α) :
y = x
@[simp]
theorem option.get_or_else_none {α : Type u_1} (x : α) :
@[simp]
theorem option.get_or_else_coe {α : Type u_1} (x y : α) :
theorem option.get_or_else_of_ne_none {α : Type u_1} {x : option α} (hx : x option.none) (y : α) :
@[simp]
theorem option.coe_get {α : Type u_1} {o : option α} (h : (o.is_some)) :
theorem option.mem_unique {α : Type u_1} {o : option α} {a b : α} (ha : a o) (hb : b o) :
a = b
theorem option.eq_of_mem_of_mem {α : Type u_1} {a : α} {o1 o2 : option α} (h1 : a o1) (h2 : a o2) :
o1 = o2
theorem option.mem.left_unique {α : Type u_1} :
theorem option.some_injective (α : Type u_1) :
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 : α β) :
@[ext]
theorem option.ext {α : Type u_1} {o₁ o₂ : option α} :
( (a : α), a o₁ a o₂) o₁ = o₂
theorem option.eq_none_iff_forall_not_mem {α : Type u_1} {o : option α} :
(a : α), a o
@[simp]
theorem option.none_bind {α β : Type u_1} (f : α ) :
@[simp]
theorem option.some_bind {α β : Type u_1} (a : α) (f : α ) :
= f a
@[simp]
theorem option.none_bind' {α : Type u_1} {β : Type u_2} (f : α ) :
@[simp]
theorem option.some_bind' {α : Type u_1} {β : Type u_2} (a : α) (f : α ) :
(option.some a).bind f = f a
@[simp]
theorem option.bind_some {α : Type u_1} (x : option α) :
= x
@[simp]
theorem option.bind_some' {α : Type u_1} (x : option α) :
= x
@[simp]
theorem option.bind_eq_some {α β : Type u_1} {x : option α} {f : α } {b : β} :
x >>= f = (a : α), x = f a =
@[simp]
theorem option.bind_eq_some' {α : Type u_1} {β : Type u_2} {x : option α} {f : α } {b : β} :
x.bind f = (a : α), x = f a =
@[simp]
theorem option.bind_eq_none' {α : Type u_1} {β : Type u_2} {o : option α} {f : α } :
o.bind f = option.none (b : β) (a : α), a o b f a
@[simp]
theorem option.bind_eq_none {α β : Type u_1} {o : option α} {f : α } :
o >>= f = option.none (b : β) (a : α), a o b f a
theorem option.bind_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β } (a : option α) (b : option β) :
a.bind (λ (x : α), b.bind (f x)) = b.bind (λ (y : β), a.bind (λ (x : α), f x y))
theorem option.bind_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (x : option α) (f : α ) (g : β ) :
(x.bind f).bind g = x.bind (λ (y : α), (f y).bind g)
theorem option.join_eq_some {α : Type u_1} {x : option (option α)} {a : α} :
x.join = x =
theorem option.join_ne_none {α : Type u_1} {x : option (option α)} :
(z : α), x =
theorem option.join_ne_none' {α : Type u_1} {x : option (option α)} :
(z : α), x =
theorem option.join_eq_none {α : Type u_1} {o : option (option α)} :
theorem option.bind_id_eq_join {α : Type u_1} {x : option (option α)} :
= x.join
theorem option.join_eq_join {α : Type u_1} :
theorem option.bind_eq_bind {α β : Type u_1} {f : α } {x : option α} :
x >>= f = x.bind f
@[simp]
theorem option.map_eq_map {α β : Type u_1} {f : α β} :
theorem option.map_none {α β : Type u_1} {f : α β} :
theorem option.map_some {α β : Type u_1} {a : α} {f : α β} :
= option.some (f a)
theorem option.map_coe {α β : Type u_1} {a : α} {f : α β} :
f <$> a = (f a) @[simp] theorem option.map_none' {α : Type u_1} {β : Type u_2} {f : α β} : @[simp] theorem option.map_some' {α : Type u_1} {β : Type u_2} {a : α} {f : α β} : @[simp] theorem option.map_coe' {α : Type u_1} {β : Type u_2} {a : α} {f : α β} : a = (f a) theorem option.map_eq_some {α β : Type u_1} {x : option α} {f : α β} {b : β} : f <$> x = (a : α), x = f a = b
@[simp]
theorem option.map_eq_some' {α : Type u_1} {β : Type u_2} {x : option α} {f : α β} {b : β} :
x = (a : α), x = f a = b
theorem option.map_eq_none {α β : Type u_1} {x : option α} {f : α β} :
@[simp]
theorem option.map_eq_none' {α : Type u_1} {β : Type u_2} {x : option α} {f : α β} :
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
theorem option.map_congr {α : Type u_1} {β : Type u_2} {f g : α β} {x : option α} (h : (a : α), a x f a = g a) :
x = x
@[simp]
theorem option.map_eq_id {α : Type u_1} {f : α α} :
f = id
@[simp]
theorem option.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : β γ) (g : α β) (x : option α) :
x) = option.map (h g) x
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 f₁ a) = (option.map f₂ a)
theorem option.comp_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : β γ) (g : α β) (x : option α) :
option.map (h g) x = x)
@[simp]
theorem option.map_comp_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β) (g : β γ) :
theorem option.mem_map_of_mem {α : Type u_1} {β : Type u_2} {a : α} {x : option α} (g : α β) (h : a x) :
g a x
theorem option.mem_map {α : Type u_1} {β : Type u_2} {f : α β} {y : β} {o : option α} :
y o (x : α) (H : x o), f x = y
theorem option.forall_mem_map {α : Type u_1} {β : Type u_2} {f : α β} {o : option α} {p : β Prop} :
( (y : β), y o p y) (x : α), x o p (f x)
theorem option.exists_mem_map {α : Type u_1} {β : Type u_2} {f : α β} {o : option α} {p : β Prop} :
( (y : β) (H : y o), p y) (x : α) (H : x o), p (f x)
theorem option.bind_map_comm {α β : Type u_1} {x : option (option α)} {f : α β} :
= x >>= id
theorem option.join_map_eq_map_join {α : Type u_1} {β : Type u_2} {f : α β} {x : option (option α)} :
theorem option.join_join {α : Type u_1} {x : option (option (option α))} :
theorem option.mem_of_mem_join {α : Type u_1} {a : α} {x : option (option α)} (h : a x.join) :
x
@[simp]
theorem option.pbind_eq_bind {α : Type u_1} {β : Type u_2} (f : α ) (x : option α) :
x.pbind (λ (a : α) (_x : a x), f a) = x.bind f
theorem option.map_bind {α β γ : Type u_1} (f : β γ) (x : option α) (g : α ) :
(x >>= g) = x >>= λ (a : α), (g a)
theorem option.map_bind' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β γ) (x : option α) (g : α ) :
(x.bind g) = x.bind (λ (a : α), (g a))
theorem option.map_pbind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β γ) (x : option α) (g : Π (a : α), a x ) :
(x.pbind g) = x.pbind (λ (a : α) (H : a x), (g a H))
theorem option.pbind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β) (x : option α) (g : Π (b : β), b x ) :
x).pbind g = x.pbind (λ (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 : α), p a} :
@[simp]
theorem option.pmap_some {α : Type u_1} {β : Type u_2} {p : α Prop} (f : Π (a : α), p a β) {x : α} (h : p x) :
(option.some x) = λ (_x : (a : α), a p a), option.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 _ 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 x p a) :
x) H = option.pmap (λ (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) :
x H) = option.pmap (λ (a : α) (h : p a), g (f a h)) x H
@[simp]
theorem option.pmap_eq_map {α : Type u_1} {β : Type u_2} (p : α Prop) (f : α β) (x : option α) (H : (a : α), a x p a) :
option.pmap (λ (a : α) (_x : p a), f a) x H = x
theorem option.pmap_bind {α β γ : Type u_1} {x : option α} {g : α } {p : β Prop} {f : Π (b : β), p b γ} (H : (a : β), a x >>= g p a) (H' : (a : α) (b : β), b g a b x >>= g) :
(x >>= g) H = x >>= λ (a : α), (g a) _
theorem option.bind_pmap {α : Type u_1} {β γ : Type u_2} {p : α Prop} (f : Π (a : α), p a β) (x : option α) (g : β ) (H : (a : α), a x p a) :
x H >>= g = x.pbind (λ (a : α) (h : a x), g (f a _))
theorem option.pbind_eq_none {α : Type u_1} {β : Type u_2} {x : option α} {f : Π (a : α), a x } (h' : (a : α) (H : a x), f a H = option.none ) :
theorem option.pbind_eq_some {α : Type u_1} {β : Type u_2} {x : option α} {f : Π (a : α), a x } {y : β} :
x.pbind f = (z : α) (H : z x), f z H =
@[simp]
theorem option.pmap_eq_none_iff {α : Type u_1} {β : Type u_2} {p : α Prop} {f : Π (a : α), p a β} {x : option α} {h : (a : α), a x p a} :
@[simp]
theorem option.pmap_eq_some_iff {α : Type u_1} {β : Type u_2} {p : α Prop} {f : Π (a : α), p a β} {x : option α} {hf : (a : α), a x p a} {y : β} :
x hf = (a : α) (H : x = , f a _ = y
@[simp]
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_1 : α), a_1 a p a_1) :
x H).join = x.join _
@[simp]
theorem option.seq_some {α β : Type u_1} {a : α} {f : α β} :
= option.some (f a)
@[simp]
theorem option.some_orelse' {α : Type u_1} (a : α) (x : option α) :
@[simp]
theorem option.some_orelse {α : Type u_1} (a : α) (x : option α) :
<|> x) =
@[simp]
theorem option.none_orelse' {α : Type u_1} (x : option α) :
@[simp]
theorem option.none_orelse {α : Type u_1} (x : option α) :
= x
@[simp]
theorem option.orelse_none' {α : Type u_1} (x : option α) :
@[simp]
theorem option.orelse_none {α : Type u_1} (x : option α) :
= x
@[simp]
theorem option.is_some_none {α : Type u_1} :
@[simp]
theorem option.is_some_some {α : Type u_1} {a : α} :
theorem option.is_some_iff_exists {α : Type u_1} {x : option α} :
(x.is_some) (a : α), x =
@[simp]
theorem option.is_none_none {α : Type u_1} :
@[simp]
theorem option.is_none_some {α : Type u_1} {a : α} :
@[simp]
theorem option.not_is_some {α : Type u_1} {a : option α} :
theorem option.eq_some_iff_get_eq {α : Type u_1} {o : option α} {a : α} :
o = (h : (o.is_some)), = a
theorem option.not_is_some_iff_eq_none {α : Type u_1} {o : option α} :
theorem option.ne_none_iff_is_some {α : Type u_1} {o : option α} :
theorem option.ne_none_iff_exists {α : Type u_1} {o : option α} :
(x : α), = o
theorem option.ne_none_iff_exists' {α : Type u_1} {o : option α} :
(x : α), o =
theorem option.bex_ne_none {α : Type u_1} {p : Prop} :
( (x : option α) (H : , p x) (x : α), p (option.some x)
theorem option.ball_ne_none {α : Type u_1} {p : Prop} :
( (x : option α), p x) (x : α), p (option.some x)
theorem option.iget_mem {α : Type u_1} [inhabited α] {o : option α} :
theorem option.iget_of_mem {α : Type u_1} [inhabited α] {a : α} {o : option α} :
a o o.iget = a
theorem option.get_or_else_default_eq_iget {α : Type u_1} [inhabited α] (o : option α) :
@[simp]
theorem option.guard_eq_some {α : Type u_1} {p : α Prop} {a b : α} :
a = a = b p a
@[simp]
theorem option.guard_eq_some' {p : Prop} [decidable p] (u : unit) :
p
theorem option.lift_or_get_choice {α : Type u_1} {f : α α α} (h : (a b : α), f a b = a f a b = b) (o₁ o₂ : option α) :
o₂ = o₁ o₂ = o₂
@[simp]
theorem option.lift_or_get_none_left {α : Type u_1} {f : α α α} {b : option α} :
@[simp]
theorem option.lift_or_get_none_right {α : Type u_1} {f : α α α} {a : option α} :
@[simp]
theorem option.lift_or_get_some_some {α : Type u_1} {f : α α α} {a b : α} :
(option.some b) = (f a b)
def option.cases_on' {α : 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
@[simp]
theorem option.cases_on'_none {α : Type u_1} {β : Type u_2} (x : β) (f : α β) :
= x
@[simp]
theorem option.cases_on'_some {α : Type u_1} {β : Type u_2} (x : β) (f : α β) (a : α) :
(option.some a).cases_on' x f = f a
@[simp]
theorem option.cases_on'_coe {α : Type u_1} {β : Type u_2} (x : β) (f : α β) (a : α) :
a.cases_on' x f = f a
@[simp]
theorem option.cases_on'_none_coe {α : Type u_1} {β : Type u_2} (f : β) (o : option α) :
o.cases_on' (f option.none) (f coe) = f o
@[simp]
theorem option.get_or_else_map {α : Type u_1} {β : Type u_2} (f : α β) (x : α) (o : option α) :
o).get_or_else (f x) = f (o.get_or_else x)
theorem option.orelse_eq_some {α : Type u_1} (o o' : option α) (x : α) :
(o <|> o') = o = o' =
theorem option.orelse_eq_some' {α : Type u_1} (o o' : option α) (x : α) :
o.orelse o' = o = o' =
@[simp]
theorem option.orelse_eq_none {α : Type u_1} (o o' : option α) :
@[simp]
theorem option.orelse_eq_none' {α : Type u_1} (o o' : option α) :
noncomputable def option.choice (α : Type u_1) :

An arbitrary some a with a : α if α is nonempty, and otherwise none.

Equations
theorem option.choice_eq {α : Type u_1} [subsingleton α] (a : α) :
theorem option.choice_eq_none (α : Type u_1) [is_empty α] :
@[simp]
theorem option.to_list_some {α : Type u_1} (a : α) :
@[simp]
theorem option.to_list_none (α : Type u_1) :
@[simp]
theorem option.elim_none_some {α : Type u_1} {β : Type u_2} (f : β) :