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 usesnoneas an element smaller than all others. - It can be used to define failsafe partial functions, which return
some the_result_we_expectif we can findthe_result_we_expect, andnoneif there is no meaningful result. This forces any subsequent use of the partial function to explicitly deal with the exceptions that make it returnnone. Optionis 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.
@[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.coe_get
{α : Type u_1}
{o : Option α}
(h : Option.isSome o = true)
:
some (Option.get o h) = o
theorem
Option.Mem.leftUnique
{α : Type u_1}
:
Relator.LeftUnique fun (x : α) (x_1 : Option α) => x ∈ x_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 : α → β)
:
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_bind'
{α : Type u}
{β : Type u}
{f : α → Option β}
{x : Option α}
:
x >>= f = Option.bind x f
@[simp]
theorem
Option.map_coe'
{α : Type u_1}
{β : Type u_2}
{a : α}
{f : α → β}
:
Option.map f (some a) = some (f a)
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
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) (_ : f a ∈ Option.map f x)
@[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
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 (_ : p 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 (_ : ∀ (a : γ), a ∈ x → p (g a))
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) (_ : ∀ (b : β), b ∈ g a → p b)
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 (_ : p a))
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) (_ : ∀ (a : α), a ∈ Option.join x → p 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
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
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₂
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
Instances For
@[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.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