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.

source

theorem option.coe_def {α : Type u_1} :

coe = option.some

source

theorem option.some_eq_coe {α : Type u_1} (a : α) :

option.some a = ↑a

source

theorem option.some_ne_none {α : Type u_1} (x : α) :

option.some x ≠ option.none

source

@[simp]

theorem option.coe_ne_none {α : Type u_1} (a : α) :

↑a ≠ option.none

source

@[protected]

theorem option.forall {α : Type u_1} {p : option α → Prop} :

(∀ (x : option α), p x) ↔ p option.none ∧ ∀ (x : α), p (option.some x)

source

@[protected]

theorem option.exists {α : Type u_1} {p : option α → Prop} :

(∃ (x : option α), p x) ↔ p option.none ∨ ∃ (x : α), p (option.some x)

source

@[simp]

theorem option.get_mem {α : Type u_1} {o : option α} (h : ↥(o.is_some)) :

option.get h ∈ o

source

theorem option.get_of_mem {α : Type u_1} {a : α} {o : option α} (h : ↥(o.is_some)) :

a ∈ o → option.get h = a

source

@[simp]

theorem option.not_mem_none {α : Type u_1} (a : α) :

a ∉ option.none

source

@[simp]

theorem option.some_get {α : Type u_1} {x : option α} (h : ↥(x.is_some)) :

option.some (option.get h) = x

source

@[simp]

theorem option.get_some {α : Type u_1} (x : α) (h : ↥((option.some x).is_some)) :

option.get h = x

source

@[simp]

theorem option.get_or_else_some {α : Type u_1} (x y : α) :

(option.some x).get_or_else y = x

source

@[simp]

theorem option.get_or_else_none {α : Type u_1} (x : α) :

option.none.get_or_else x = x

source

@[simp]

theorem option.get_or_else_coe {α : Type u_1} (x y : α) :

↑x.get_or_else y = x

source

theorem option.get_or_else_of_ne_none {α : Type u_1} {x : option α} (hx : x ≠ option.none) (y : α) :

option.some (x.get_or_else y) = x

source

@[simp]

theorem option.coe_get {α : Type u_1} {o : option α} (h : ↥(o.is_some)) :

↑(option.get h) = o

source

theorem option.mem_unique {α : Type u_1} {o : option α} {a b : α} (ha : a ∈ o) (hb : b ∈ o) :

a = b

source

theorem option.eq_of_mem_of_mem {α : Type u_1} {a : α} {o1 o2 : option α} (h1 : a ∈ o1) (h2 : a ∈ o2) :

o1 = o2

source

theorem option.mem.left_unique {α : Type u_1} :

relator.left_unique has_mem.mem

source

theorem option.some_injective (α : Type u_1) :

function.injective option.some

source

theorem option.map_injective {α : Type u_1} {β : Type u_2} {f : α → β} (Hf : function.injective f) :

function.injective (option.map f)

option.map f is injective if f is injective.

source

@[simp]

theorem option.map_comp_some {α : Type u_1} {β : Type u_2} (f : α → β) :

option.map f ∘ option.some = option.some ∘ f

source

@[ext]

theorem option.ext {α : Type u_1} {o₁ o₂ : option α} :

(∀ (a : α), a ∈ o₁ ↔ a ∈ o₂) → o₁ = o₂

source

theorem option.eq_none_iff_forall_not_mem {α : Type u_1} {o : option α} :

o = option.none ↔ ∀ (a : α), a ∉ o

source

@[simp]

theorem option.none_bind {α β : Type u_1} (f : α → option β) :

option.none >>= f = option.none

source

@[simp]

theorem option.some_bind {α β : Type u_1} (a : α) (f : α → option β) :

option.some a >>= f = f a

source

@[simp]

theorem option.none_bind' {α : Type u_1} {β : Type u_2} (f : α → option β) :

option.none.bind f = option.none

source

@[simp]

theorem option.some_bind' {α : Type u_1} {β : Type u_2} (a : α) (f : α → option β) :

(option.some a).bind f = f a

source

@[simp]

theorem option.bind_some {α : Type u_1} (x : option α) :

x >>= option.some = x

source

@[simp]

theorem option.bind_some' {α : Type u_1} (x : option α) :

x.bind option.some = x

source

@[simp]

theorem option.bind_eq_some {α β : Type u_1} {x : option α} {f : α → option β} {b : β} :

x >>= f = option.some b ↔ ∃ (a : α), x = option.some a ∧ f a = option.some b

source

@[simp]

theorem option.bind_eq_some' {α : Type u_1} {β : Type u_2} {x : option α} {f : α → option β} {b : β} :

x.bind f = option.some b ↔ ∃ (a : α), x = option.some a ∧ f a = option.some b

source

@[simp]

theorem option.bind_eq_none' {α : Type u_1} {β : Type u_2} {o : option α} {f : α → option β} :

o.bind f = option.none ↔ ∀ (b : β) (a : α), a ∈ o → b ∉ f a

source

@[simp]

theorem option.bind_eq_none {α β : Type u_1} {o : option α} {f : α → option β} :

o >>= f = option.none ↔ ∀ (b : β) (a : α), a ∈ o → b ∉ f a

source

theorem option.bind_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → option γ} (a : option α) (b : option β) :

a.bind (λ (x : α), b.bind (f x)) = b.bind (λ (y : β), a.bind (λ (x : α), f x y))

source

theorem option.bind_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (x : option α) (f : α → option β) (g : β → option γ) :

(x.bind f).bind g = x.bind (λ (y : α), (f y).bind g)

source

theorem option.join_eq_some {α : Type u_1} {x : option (option α)} {a : α} :

x.join = option.some a ↔ x = option.some (option.some a)

source

theorem option.join_ne_none {α : Type u_1} {x : option (option α)} :

x.join ≠ option.none ↔ ∃ (z : α), x = option.some (option.some z)

source

theorem option.join_ne_none' {α : Type u_1} {x : option (option α)} :

¬x.join = option.none ↔ ∃ (z : α), x = option.some (option.some z)

source

theorem option.join_eq_none {α : Type u_1} {o : option (option α)} :

o.join = option.none ↔ o = option.none ∨ o = option.some option.none

source

theorem option.bind_id_eq_join {α : Type u_1} {x : option (option α)} :

x >>= id = x.join

source

theorem option.join_eq_join {α : Type u_1} :

mjoin = option.join

source

theorem option.bind_eq_bind {α β : Type u_1} {f : α → option β} {x : option α} :

x >>= f = x.bind f

source

@[simp]

theorem option.map_eq_map {α β : Type u_1} {f : α → β} :

functor.map f = option.map f

source

theorem option.map_none {α β : Type u_1} {f : α → β} :

f <$> option.none = option.none

source

theorem option.map_some {α β : Type u_1} {a : α} {f : α → β} :

f <$> option.some a = option.some (f a)

source

theorem option.map_coe {α β : Type u_1} {a : α} {f : α → β} :

f <$> ↑a = ↑(f a)

source

@[simp]

theorem option.map_none' {α : Type u_1} {β : Type u_2} {f : α → β} :

option.map f option.none = option.none

source

@[simp]

theorem option.map_some' {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} :

option.map f (option.some a) = option.some (f a)

source

@[simp]

theorem option.map_coe' {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} :

option.map f ↑a = ↑(f a)

source

theorem option.map_eq_some {α β : Type u_1} {x : option α} {f : α → β} {b : β} :

f <$> x = option.some b ↔ ∃ (a : α), x = option.some a ∧ f a = b

source

@[simp]

theorem option.map_eq_some' {α : Type u_1} {β : Type u_2} {x : option α} {f : α → β} {b : β} :

option.map f x = option.some b ↔ ∃ (a : α), x = option.some a ∧ f a = b

source

theorem option.map_eq_none {α β : Type u_1} {x : option α} {f : α → β} :

f <$> x = option.none ↔ x = option.none

source

@[simp]

theorem option.map_eq_none' {α : Type u_1} {β : Type u_2} {x : option α} {f : α → β} :

option.map f x = option.none ↔ x = option.none

source

theorem option.map_injective' {α : Type u_1} {β : Type u_2} :

function.injective option.map

option.map as a function between functions is injective.

source

@[simp]

theorem option.map_inj {α : Type u_1} {β : Type u_2} {f g : α → β} :

option.map f = option.map g ↔ f = g

source

theorem option.map_congr {α : Type u_1} {β : Type u_2} {f g : α → β} {x : option α} (h : ∀ (a : α), a ∈ x → f a = g a) :

option.map f x = option.map g x

source

@[simp]

theorem option.map_eq_id {α : Type u_1} {f : α → α} :

option.map f = id ↔ f = id

source

@[simp]

theorem option.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : β → γ) (g : α → β) (x : option α) :

option.map h (option.map g x) = option.map (h ∘ g) x

source

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₁ ↑a) = option.map g₂ (option.map f₂ ↑a)

source

theorem option.comp_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : β → γ) (g : α → β) (x : option α) :

option.map (h ∘ g) x = option.map h (option.map g x)

source

@[simp]

theorem option.map_comp_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) :

option.map g ∘ option.map f = option.map (g ∘ f)

source

theorem option.mem_map_of_mem {α : Type u_1} {β : Type u_2} {a : α} {x : option α} (g : α → β) (h : a ∈ x) :

g a ∈ option.map g x

source

theorem option.mem_map {α : Type u_1} {β : Type u_2} {f : α → β} {y : β} {o : option α} :

y ∈ option.map f o ↔ ∃ (x : α) (H : x ∈ o), f x = y

source

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)

source

theorem option.exists_mem_map {α : Type u_1} {β : Type u_2} {f : α → β} {o : option α} {p : β → Prop} :

(∃ (y : β) (H : y ∈ option.map f o), p y) ↔ ∃ (x : α) (H : x ∈ o), p (f x)

source

theorem option.bind_map_comm {α β : Type u_1} {x : option (option α)} {f : α → β} :

x >>= option.map f = option.map (option.map f) x >>= id

source

theorem option.join_map_eq_map_join {α : Type u_1} {β : Type u_2} {f : α → β} {x : option (option α)} :

(option.map (option.map f) x).join = option.map f x.join

source

theorem option.join_join {α : Type u_1} {x : option (option (option α))} :

x.join.join = (option.map option.join x).join

source

theorem option.mem_of_mem_join {α : Type u_1} {a : α} {x : option (option α)} (h : a ∈ x.join) :

option.some a ∈ x

source

@[simp]

theorem option.pbind_eq_bind {α : Type u_1} {β : Type u_2} (f : α → option β) (x : option α) :

x.pbind (λ (a : α) (_x : a ∈ x), f a) = x.bind f

source

theorem option.map_bind {α β γ : Type u_1} (f : β → γ) (x : option α) (g : α → option β) :

option.map f (x >>= g) = x >>= λ (a : α), option.map f (g a)

source

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 (λ (a : α), option.map f (g a))

source

theorem option.map_pbind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (x : option α) (g : Π (a : α), a ∈ x → option β) :

option.map f (x.pbind g) = x.pbind (λ (a : α) (H : a ∈ x), option.map f (g a H))

source

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 (λ (a : α) (h : a ∈ x), g (f a) _)

source

@[simp]

theorem option.pmap_none {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) {H : ∀ (a : α), a ∈ option.none → p a} :

option.pmap f option.none H = option.none

source

@[simp]

theorem option.pmap_some {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) {x : α} (h : p x) :

option.pmap f (option.some x) = λ (_x : ∀ (a : α), a ∈ option.some x → p a), option.some (f x h)

source

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

source

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 (λ (a : γ) (h : p (g a)), f (g a) h) x _

source

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 (λ (a : α) (h : p a), g (f a h)) x H

source

@[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 = option.map f x

source

theorem option.pmap_bind {α β γ : Type u_1} {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 = x >>= λ (a : α), option.pmap f (g a) _

source

theorem option.bind_pmap {α : Type u_1} {β γ : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) (x : option α) (g : β → option γ) (H : ∀ (a : α), a ∈ x → p a) :

option.pmap f x H >>= g = x.pbind (λ (a : α) (h : a ∈ x), g (f a _))

source

theorem option.pbind_eq_none {α : Type u_1} {β : Type u_2} {x : option α} {f : Π (a : α), a ∈ x → option β} (h' : ∀ (a : α) (H : a ∈ x), f a H = option.none → x = option.none) :

x.pbind f = option.none ↔ x = option.none

source

theorem option.pbind_eq_some {α : Type u_1} {β : Type u_2} {x : option α} {f : Π (a : α), a ∈ x → option β} {y : β} :

x.pbind f = option.some y ↔ ∃ (z : α) (H : z ∈ x), f z H = option.some y

source

@[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} :

option.pmap f x h = option.none ↔ x = option.none

source

@[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 : β} :

option.pmap f x hf = option.some y ↔ ∃ (a : α) (H : x = option.some a), f a _ = y

source

@[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) :

(option.pmap (option.pmap f) x H).join = option.pmap f x.join _

source

@[simp]

theorem option.seq_some {α β : Type u_1} {a : α} {f : α → β} :

option.some f <*> option.some a = option.some (f a)

source

@[simp]

theorem option.some_orelse' {α : Type u_1} (a : α) (x : option α) :

(option.some a).orelse x = option.some a

source

@[simp]

theorem option.some_orelse {α : Type u_1} (a : α) (x : option α) :

(option.some a <|> x) = option.some a

source

@[simp]

theorem option.none_orelse' {α : Type u_1} (x : option α) :

option.none.orelse x = x

source

@[simp]

theorem option.none_orelse {α : Type u_1} (x : option α) :

(option.none <|> x) = x

source

@[simp]

theorem option.orelse_none' {α : Type u_1} (x : option α) :

x.orelse option.none = x

source

@[simp]

theorem option.orelse_none {α : Type u_1} (x : option α) :

(x <|> option.none) = x

source

@[simp]

theorem option.is_some_none {α : Type u_1} :

option.none.is_some = bool.ff

source

@[simp]

theorem option.is_some_some {α : Type u_1} {a : α} :

(option.some a).is_some = bool.tt

source

theorem option.is_some_iff_exists {α : Type u_1} {x : option α} :

↥(x.is_some) ↔ ∃ (a : α), x = option.some a

source

@[simp]

theorem option.is_none_none {α : Type u_1} :

option.none.is_none = bool.tt

source

@[simp]

theorem option.is_none_some {α : Type u_1} {a : α} :

(option.some a).is_none = bool.ff

source

@[simp]

theorem option.not_is_some {α : Type u_1} {a : option α} :

a.is_some = bool.ff ↔ a.is_none = bool.tt

source

theorem option.eq_some_iff_get_eq {α : Type u_1} {o : option α} {a : α} :

o = option.some a ↔ ∃ (h : ↥(o.is_some)), option.get h = a

source

theorem option.not_is_some_iff_eq_none {α : Type u_1} {o : option α} :

¬↥(o.is_some) ↔ o = option.none

source

theorem option.ne_none_iff_is_some {α : Type u_1} {o : option α} :

o ≠ option.none ↔ ↥(o.is_some)

source

theorem option.ne_none_iff_exists {α : Type u_1} {o : option α} :

o ≠ option.none ↔ ∃ (x : α), option.some x = o

source

theorem option.ne_none_iff_exists' {α : Type u_1} {o : option α} :

o ≠ option.none ↔ ∃ (x : α), o = option.some x

source

theorem option.bex_ne_none {α : Type u_1} {p : option α → Prop} :

(∃ (x : option α) (H : x ≠ option.none), p x) ↔ ∃ (x : α), p (option.some x)

source

theorem option.ball_ne_none {α : Type u_1} {p : option α → Prop} :

(∀ (x : option α), x ≠ option.none → p x) ↔ ∀ (x : α), p (option.some x)

source

theorem option.iget_mem {α : Type u_1} [inhabited α] {o : option α} :

↥(o.is_some) → o.iget ∈ o

source

theorem option.iget_of_mem {α : Type u_1} [inhabited α] {a : α} {o : option α} :

a ∈ o → o.iget = a

source

theorem option.get_or_else_default_eq_iget {α : Type u_1} [inhabited α] (o : option α) :

o.get_or_else inhabited.default = o.iget

source

@[simp]

theorem option.guard_eq_some {α : Type u_1} {p : α → Prop} [decidable_pred p] {a b : α} :

option.guard p a = option.some b ↔ a = b ∧ p a

source

@[simp]

theorem option.guard_eq_some' {p : Prop} [decidable p] (u : unit) :

guard p = option.some u ↔ p

source

theorem option.lift_or_get_choice {α : Type u_1} {f : α → α → α} (h : ∀ (a b : α), f a b = a ∨ f a b = b) (o₁ o₂ : option α) :

option.lift_or_get f o₁ o₂ = o₁ ∨ option.lift_or_get f o₁ o₂ = o₂

source

@[simp]

theorem option.lift_or_get_none_left {α : Type u_1} {f : α → α → α} {b : option α} :

option.lift_or_get f option.none b = b

source

@[simp]

theorem option.lift_or_get_none_right {α : Type u_1} {f : α → α → α} {a : option α} :

option.lift_or_get f a option.none = a

source

@[simp]

theorem option.lift_or_get_some_some {α : Type u_1} {f : α → α → α} {a b : α} :

option.lift_or_get f (option.some a) (option.some b) = ↑(f a b)

source

def option.cases_on' {α : Type u_1} {β : Type u_2} :

option α → β → (α → β) → β

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