Documentation

Mathlib.Data.Option.Basic

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:

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 op y) ∀ (x : α), x op (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.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_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} :

Option.map as a function between functions is injective.

@[simp]
theorem Option.map_inj {α : Type u_1} {β : Type u_2} {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 xOption β) :
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 xOption γ) :
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 nonep 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 xp 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 xp 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 xp a) :
Option.pmap f (Option.map g x) H = Option.pmap (fun (a : γ) (h : p (g a)) => f (g a) h) x (_ : ∀ (a : γ), a xp (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 xp 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 xp 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 >>= gp a) (H' : ∀ (a : α) (b : β), b g ab x >>= g) :
Option.pmap f (x >>= g) H = do let a ← x Option.pmap f (g a) (_ : ∀ (b : β), b g ap 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 xp a) :
Option.pmap f x H >>= g = Option.pbind x fun (a : α) (h : a x) => g (f a (_ : p a))
theorem Option.pbind_eq_none {α : Type u_1} {β : Type u_2} {x : Option α} {f : (a : α) → a xOption β} (h' : ∀ (a : α) (H : a x), f a H = nonex = none) :
Option.pbind x f = none x = none
theorem Option.pbind_eq_some {α : Type u_1} {β : Type u_2} {x : Option α} {f : (a : α) → a xOption β} {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 xp 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 xp a} {y : β} :
Option.pmap f x hf = some y ∃ (a : α), ∃ (H : x = some a), f a (_ : p 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 ap a_2) :
Option.join (Option.pmap (Option.pmap f) x H) = Option.pmap f (Option.join x) (_ : ∀ (a : α), a Option.join xp a)
@[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
theorem Option.iget_mem {α : Type u_1} [Inhabited α] {o : Option α} :
theorem Option.iget_of_mem {α : Type u_1} [Inhabited α] {a : α} {o : Option α} :
a oOption.iget o = a
theorem Option.getD_default_eq_iget {α : Type u_1} [Inhabited α] (o : Option α) :
@[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
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.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 α] :
    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