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 : o.isSome = true) :
some (o.get 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 (x1 : α) (x2 : Option α) => x1 x2
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 β) :
none.bind f = none
@[simp]
theorem Option.some_bind' {α : Type u_1} {β : Type u_2} (a : α) (f : αOption β) :
(some a).bind f = f a
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
theorem Option.bind_congr {α : Type u_1} {β : Type u_2} {f : αOption β} {g : αOption β} {x : Option α} (h : ∀ (a : α), a xf a = g a) :
x.bind f = x.bind g
theorem Option.bind_congr' {α : Type u_1} {β : Type u_2} {f : αOption β} {g : αOption β} {x : Option α} {y : Option α} (hx : x = y) (hf : ∀ (a : α), a yf a = g a) :
x.bind f = y.bind g
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 = x.bind 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 α) :
(x.pbind fun (a : α) (x : a x) => f a) = x.bind f
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)
theorem Option.pbind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (x : Option α) (g : (b : β) → b Option.map f xOption γ) :
(Option.map f x).pbind g = x.pbind fun (a : α) (h : a x) => g (f a)
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 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
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 ax 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 xp a) :
Option.pmap f x H >>= g = x.pbind fun (a : α) (h : a x) => g (f 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) :
x.pbind f = none x = none
theorem Option.pbind_eq_some {α : Type u_1} {β : Type u_2} {x : Option α} {f : (a : α) → a xOption β} {y : β} :
x.pbind f = some y ∃ (z : α), ∃ (H : z x), f z H = some 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.pmap (Option.pmap f) x H).join = Option.pmap f x.join
@[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 α) :
((some a).orElse fun (x_1 : Unit) => x) = some a
@[simp]
theorem Option.none_orElse' {α : Type u_1} (x : Option α) :
(none.orElse fun (x_1 : Unit) => x) = x
@[simp]
theorem Option.orElse_none' {α : Type u_1} (x : Option α) :
(x.orElse fun (x : Unit) => none) = x
theorem Option.exists_ne_none {α : Type u_1} {p : Option αProp} :
(∃ (x : Option α), x none p x) ∃ (x : α), p (some x)
theorem Option.iget_mem {α : Type u_1} [Inhabited α] {o : Option α} :
o.isSome = trueo.iget o
theorem Option.iget_of_mem {α : Type u_1} [Inhabited α] {a : α} {o : Option α} :
a oo.iget = a
theorem Option.getD_default_eq_iget {α : Type u_1} [Inhabited α] (o : Option α) :
o.getD default = o.iget
@[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
  • none.casesOn' x✝ x = x✝
  • (some a).casesOn' x✝ x = x a
Instances For
    @[simp]
    theorem Option.casesOn'_none {α : Type u_1} {β : Type u_2} (x : β) (f : αβ) :
    none.casesOn' x f = x
    @[simp]
    theorem Option.casesOn'_some {α : Type u_1} {β : Type u_2} (x : β) (f : αβ) (a : α) :
    (some a).casesOn' x f = f a
    @[simp]
    theorem Option.casesOn'_coe {α : Type u_1} {β : Type u_2} (x : β) (f : αβ) (a : α) :
    (some a).casesOn' x f = f a
    theorem Option.casesOn'_none_coe {α : Type u_1} {β : Type u_2} (f : Option αβ) (o : Option α) :
    o.casesOn' (f none) (f fun (a : α) => some a) = f o
    theorem Option.casesOn'_eq_elim {α : Type u_1} {β : Type u_2} (b : β) (f : αβ) (a : Option α) :
    a.casesOn' b f = a.elim 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 : α) :
    (o.orElse 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 α) :
    (o.orElse 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 α) => x.elim (f none) (f some)) = f
    theorem Option.elim_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : αβ) {f : γα} {x : α} {i : Option γ} :
    (i.elim (h x) fun (j : γ) => h (f j)) = h (i.elim x f)
    theorem Option.elim_comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : αβγ) {f : γα} {x : α} {g : γβ} {y : β} {i : Option γ} :
    (i.elim (h x y) fun (j : γ) => h (f j) (g j)) = h (i.elim x f) (i.elim y g)
    theorem Option.elim_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : γαβ} {x : αβ} {i : Option γ} {y : α} :
    i.elim x f y = i.elim (x y) fun (j : γ) => f j y
    @[simp]
    theorem Option.bnot_isSome {α : Type u_1} (a : Option α) :
    (!a.isSome) = a.isNone
    @[simp]
    theorem Option.bnot_comp_isSome {α : Type u_1} :
    (fun (x : Bool) => !x) Option.isSome = Option.isNone
    @[simp]
    theorem Option.bnot_isNone {α : Type u_1} (a : Option α) :
    (!a.isNone) = a.isSome
    @[simp]
    theorem Option.bnot_comp_isNone {α : Type u_1} :
    (fun (x : Bool) => !x) Option.isNone = Option.isSome
    @[simp]
    theorem Option.isNone_eq_false_iff {α : Type u_1} (a : Option α) :
    a.isNone = false a.isSome = true
    theorem Option.eq_none_or_eq_some {α : Type u_1} (a : Option α) :
    a = none ∃ (x : α), a = some x
    theorem Option.forall_some_ne_iff_eq_none {α : Type u_1} {o : Option α} :
    (∀ (x : α), some x o) o = none