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.

source

theorem Option.coe_def {α : Type u_1} :

(fun (a : α) => some a) = some

source

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

y ∈ Option.map f o ↔ ∃ (x : α), x ∈ o ∧ f x = y

source

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

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 : β), y ∈ Option.map f o ∧ p y) ↔ ∃ (x : α), x ∈ o ∧ p (f x)

source

theorem Option.coe_get {α : Type u_1} {o : Option α} (h : o.isSome = true) :

some (o.get h) = o

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.leftUnique {α : Type u_1} :

Relator.LeftUnique fun (x1 : α) (x2 : Option α) => x1 ∈ x2

source

theorem Option.some_injective (α : Type u_5) :

Function.Injective 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 ∘ some = some ∘ f

source

@[simp]

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

none.bind f = none

source

@[simp]

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

(some a).bind f = f a

source

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

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

source

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

x.bind f = x.bind g

source

theorem Option.bind_congr' {α : Type u_1} {β : Type u_2} {f g : α → Option β} {x y : Option α} (hx : x = y) (hf : ∀ (a : α), a ∈ y → f a = g a) :

x.bind f = y.bind g

source

theorem Option.joinM_eq_join {α : Type u_1} :

joinM = join

source

theorem Option.bind_eq_bind' {α β : Type u} {f : α → Option β} {x : Option α} :

x >>= f = x.bind f

source

theorem Option.map_coe {α β : Type u_5} {a : α} {f : α → β} :

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

source

@[simp]

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

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

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

@[simp]

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

Option.map f = id ↔ f = id

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

source

@[simp]

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

(x.pbind fun (a : α) (x : a ∈ x) => f a) = x.bind f

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 fun (a : α) => Option.map f (g a)

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 fun (a : α) (h : a ∈ x) => g (f a) ⋯

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 ⋯ ∈ pmap f x h

source

theorem Option.pmap_bind {α β γ : 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) :

pmap f (x >>= g) H = do let a ← x pmap f (g a) ⋯

source

theorem Option.bind_pmap {α : Type u_5} {β γ : Type u_6} {p : α → Prop} (f : (a : α) → p a → β) (x : Option α) (g : β → Option γ) (H : ∀ (a : α), a ∈ x → p a) :

pmap f x H >>= g = x.pbind fun (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 = none → x = none) :

x.pbind f = none ↔ x = none

source

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

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

source

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

(pmap (pmap f) x H).join = pmap f x.join ⋯

source

@[simp]

theorem Option.pmap_bind_id_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) :

((pmap (pmap f) x H).bind fun (a : Option β) => a) = pmap f x.join ⋯

simp-normal form of join_pmap_eq_pmap_join

source

@[simp]

theorem Option.seq_some {α β : Type u_5} {a : α} {f : α → β} :

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

source

@[simp]

theorem Option.some_orElse' {α : Type u_1} (a : α) (x : Option α) :

((some a).orElse fun (x_1 : Unit) => x) = some a

source

@[simp]

theorem Option.none_orElse' {α : Type u_1} (x : Option α) :

(none.orElse fun (x_1 : Unit) => x) = x

source

@[simp]

theorem Option.orElse_none' {α : Type u_1} (x : Option α) :

(x.orElse fun (x : Unit) => none) = x

source

theorem Option.exists_ne_none {α : Type u_1} {p : Option α → Prop} :

(∃ (x : Option α), x ≠ none ∧ p x) ↔ ∃ (x : α), p (some x)

source

theorem Option.iget_mem {α : Type u_1} [Inhabited α] {o : Option α} :

o.isSome = true → o.iget ∈ o

source

theorem Option.iget_of_mem {α : Type u_1} [Inhabited α] {a : α} {o : Option α} :

a ∈ o → o.iget = a

source

theorem Option.getD_default_eq_iget {α : Type u_1} [Inhabited α] (o : Option α) :

o.getD default = o.iget

source

@[simp]

theorem Option.guard_eq_some' {p : Prop} [Decidable p] (u : Unit) :

_root_.guard p = some u ↔ p

source

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₁ ∨ liftOrGet f o₁ o₂ = o₂

source

def Option.casesOn' {α : 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