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

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

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

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

theorem Option.Mem.leftUnique {α : Type u_1} : Relator.LeftUnique fun (x : α) (x_1 : Option α) => x ∈ x_1

theorem Option.some_injective (α : Type u_5) : Function.Injective some

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.

@[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_some' {α : Type u_1} {β : Type u_2} {x : Option α} {f : α → Option β} {b : β} : Option.bind x f = some b ↔ ∃ (a : α), x = some a ∧ f a = some b

theorem Option.joinM_eq_join {α : Type u_1} : joinM = Option.join

theorem Option.bind_eq_bind' {α : Type u} {β : Type u} {f : α → Option β} {x : Option α} : x >>= f = Option.bind x 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} : Function.Injective Option.map

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

@[simp]

theorem Option.map_eq_id {α : Type u_1} {f : α → α} : Option.map 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 : α → Option β) (x : Option α) : (Option.pbind x fun (a : α) (x : 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 : a ∈ x) => 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 : 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 ∈ 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_1 : ∀ (a : α), a ∈ some x → p a) => 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 ⋯ ∈ 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 : 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) : 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 : Option α) (H : ∀ (a : α), a ∈ x → p a) : Option.pmap (fun (a : α) (x : p a) => 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) ⋯

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

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) : Option.pbind x f = none ↔ x = none

theorem Option.pbind_eq_some {α : Type u_1} {β : Type u_2} {x : Option α} {f : (a : α) → a ∈ x → Option β} {y : β} : Option.pbind x 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 : Option α} {h : ∀ (a : α), a ∈ x → p 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 : Option α} {hf : ∀ (a : α), a ∈ x → p 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 : 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) ⋯

@[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 : Option α) : (Option.orElse (some a) fun (x_1 : Unit) => x) = some a

@[simp]

theorem Option.none_orElse' {α : Type u_1} (x : Option α) : (Option.orElse none fun (x_1 : Unit) => x) = x

@[simp]

theorem Option.orElse_none' {α : Type u_1} (x : Option α) : (Option.orElse x fun (x : Unit) => none) = x

@[simp]

theorem Option.isSome_map {α : Type u_1} {β : Type u_2} (f : α → β) (o : Option α) : Option.isSome (Option.map f o) = Option.isSome o

@[simp]

theorem Option.get_map {α : Type u_1} {β : Type u_2} (f : α → β) {o : Option α} (h : Option.isSome (Option.map f o) = true) : Option.get (Option.map f o) h = f (Option.get o ⋯)

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

@[simp]

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

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₂

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

• Option.casesOn' x✝¹ x✝ x = match x✝¹, x✝, x with | none, n, x => n | some a, x, s => s a

@[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.casesOn'_eq_elim {α : Type u_1} {β : Type u_2} (b : β) (f : α → β) (a : Option α) : Option.casesOn' a b f = Option.elim a b f

theorem Option.orElse_eq_some {α : Type u_1} (o : Option α) (o' : Option α) (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 : Option α) (o' : Option α) (x : α) : (Option.orElse o fun (x : Unit) => o') = some x ↔ o = some x ∨ o = none ∧ o' = some x

@[simp]

theorem Option.orElse_eq_none {α : Type u_1} (o : Option α) (o' : Option α) : (HOrElse.hOrElse o fun (x : Unit) => o') = none ↔ o = none ∧ o' = none

@[simp]

theorem Option.orElse_eq_none' {α : Type u_1} (o : Option α) (o' : Option α) : (Option.orElse o fun (x : Unit) => o') = none ↔ o = none ∧ o' = none

theorem Option.choice_eq_none (α : Type u_5) [IsEmpty α] : Option.choice α = none

theorem Option.elim_none_some {α : Type u_1} {β : Type u_2} (f : Option α → β) : (fun (x : Option α) => 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