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
with_bot α
which usesnone
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 findthe_result_we_expect
, andnone
if there is no meaningful result. This forces any subsequent use of the partial function to explicitly deal with the exceptions that make it returnnone
. 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
.
Implementation notes #
option
is currently defined in core Lean, but this will change in Lean 4.
@[protected]
theorem
option.forall
{α : Type u_1}
{p : option α → Prop} :
(∀ (x : option α), p x) ↔ p option.none ∧ ∀ (x : α), p (option.some x)
@[protected]
theorem
option.exists
{α : Type u_1}
{p : option α → Prop} :
(∃ (x : option α), p x) ↔ p option.none ∨ ∃ (x : α), p (option.some x)
@[simp]
theorem
option.get_of_mem
{α : Type u_1}
{a : α}
{o : option α}
(h : ↥(o.is_some)) :
a ∈ o → option.get h = a
@[simp]
theorem
option.some_get
{α : Type u_1}
{x : option α}
(h : ↥(x.is_some)) :
option.some (option.get h) = x
@[simp]
@[simp]
@[simp]
theorem
option.get_or_else_of_ne_none
{α : Type u_1}
{x : option α}
(hx : x ≠ option.none)
(y : α) :
option.some (x.get_or_else y) = x
@[simp]
theorem
option.map_injective
{α : Type u_1}
{β : Type u_2}
{f : α → β}
(Hf : function.injective f) :
option.map f
is injective if f
is injective.
theorem
option.eq_none_iff_forall_not_mem
{α : Type u_1}
{o : option α} :
o = option.none ↔ ∀ (a : α), a ∉ o
@[simp]
@[simp]
@[simp]
@[simp]
theorem
option.some_bind'
{α : Type u_1}
{β : Type u_2}
(a : α)
(f : α → option β) :
(option.some a).bind f = f a
@[simp]
theorem
option.bind_eq_some
{α β : Type u_1}
{x : option α}
{f : α → option β}
{b : β} :
x >>= f = option.some b ↔ ∃ (a : α), x = option.some a ∧ f a = option.some b
@[simp]
theorem
option.bind_eq_some'
{α : Type u_1}
{β : Type u_2}
{x : option α}
{f : α → option β}
{b : β} :
x.bind f = option.some b ↔ ∃ (a : α), x = option.some a ∧ f a = option.some b
@[simp]
@[simp]
theorem
option.join_eq_some
{α : Type u_1}
{x : option (option α)}
{a : α} :
x.join = option.some a ↔ x = option.some (option.some a)
theorem
option.join_ne_none
{α : Type u_1}
{x : option (option α)} :
x.join ≠ option.none ↔ ∃ (z : α), x = option.some (option.some z)
theorem
option.join_ne_none'
{α : Type u_1}
{x : option (option α)} :
¬x.join = option.none ↔ ∃ (z : α), x = option.some (option.some z)
theorem
option.join_eq_none
{α : Type u_1}
{o : option (option α)} :
o.join = option.none ↔ o = option.none ∨ o = option.some option.none
@[simp]
theorem
option.map_some
{α β : Type u_1}
{a : α}
{f : α → β} :
f <$> option.some a = option.some (f a)
@[simp]
@[simp]
theorem
option.map_some'
{α : Type u_1}
{β : Type u_2}
{a : α}
{f : α → β} :
option.map f (option.some a) = option.some (f a)
@[simp]
theorem
option.map_coe'
{α : Type u_1}
{β : Type u_2}
{a : α}
{f : α → β} :
option.map f ↑a = ↑(f a)
theorem
option.map_eq_some
{α β : Type u_1}
{x : option α}
{f : α → β}
{b : β} :
f <$> x = option.some b ↔ ∃ (a : α), x = option.some a ∧ f a = b
@[simp]
theorem
option.map_eq_some'
{α : Type u_1}
{β : Type u_2}
{x : option α}
{f : α → β}
{b : β} :
option.map f x = option.some b ↔ ∃ (a : α), x = option.some a ∧ f a = b
theorem
option.map_eq_none
{α β : Type u_1}
{x : option α}
{f : α → β} :
f <$> x = option.none ↔ x = option.none
@[simp]
theorem
option.map_eq_none'
{α : Type u_1}
{β : Type u_2}
{x : option α}
{f : α → β} :
option.map f x = option.none ↔ x = option.none
theorem
option.map_congr
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{x : option α}
(h : ∀ (a : α), a ∈ x → f a = g a) :
option.map f x = option.map g x
@[simp]
theorem
option.map_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(h : β → γ)
(g : α → β)
(x : option α) :
option.map h (option.map g x) = option.map (h ∘ g) x
theorem
option.comp_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(h : β → γ)
(g : α → β)
(x : option α) :
option.map (h ∘ g) x = option.map h (option.map g x)
@[simp]
theorem
option.map_comp_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β)
(g : β → γ) :
option.map g ∘ option.map f = option.map (g ∘ f)
theorem
option.mem_map_of_mem
{α : Type u_1}
{β : Type u_2}
{a : α}
{x : option α}
(g : α → β)
(h : a ∈ x) :
g a ∈ option.map g x
theorem
option.bind_map_comm
{α β : Type u_1}
{x : option (option α)}
{f : α → β} :
x >>= option.map f = option.map (option.map f) x >>= id
theorem
option.join_map_eq_map_join
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{x : option (option α)} :
(option.map (option.map f) x).join = option.map f x.join
theorem
option.join_join
{α : Type u_1}
{x : option (option (option α))} :
x.join.join = (option.map option.join x).join
theorem
option.mem_of_mem_join
{α : Type u_1}
{a : α}
{x : option (option α)}
(h : a ∈ x.join) :
option.some a ∈ x
theorem
option.map_bind
{α β γ : Type u_1}
(f : β → γ)
(x : option α)
(g : α → option β) :
option.map f (x >>= g) = x >>= λ (a : α), 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 (x.bind g) = x.bind (λ (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 (x.pbind g) = x.pbind (λ (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.map f x).pbind g = x.pbind (λ (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 ∈ option.none → p a} :
@[simp]
theorem
option.pmap_some
{α : Type u_1}
{β : Type u_2}
{p : α → Prop}
(f : Π (a : α), p a → β)
{x : α}
(h : p x) :
option.pmap f (option.some x) = λ (_x : ∀ (a : α), a ∈ option.some x → p a), option.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 (λ (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 (λ (a : α) (h : p a), g (f a h)) x H
@[simp]
theorem
option.pmap_eq_map
{α : Type u_1}
{β : Type u_2}
(p : α → Prop)
(f : α → β)
(x : option α)
(H : ∀ (a : α), a ∈ x → p a) :
option.pmap (λ (a : α) (_x : p a), f a) x H = option.map f x
theorem
option.pmap_bind
{α β γ : Type u_1}
{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 = x >>= λ (a : α), option.pmap f (g a) _
theorem
option.bind_pmap
{α : Type u_1}
{β γ : Type u_2}
{p : α → Prop}
(f : Π (a : α), p a → β)
(x : option α)
(g : β → option γ)
(H : ∀ (a : α), a ∈ x → p a) :
option.pmap f x H >>= g = x.pbind (λ (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 = option.none → x = option.none) :
x.pbind f = option.none ↔ x = option.none
theorem
option.pbind_eq_some
{α : Type u_1}
{β : Type u_2}
{x : option α}
{f : Π (a : α), a ∈ x → option β}
{y : β} :
x.pbind f = option.some y ↔ ∃ (z : α) (H : z ∈ x), f z H = option.some y
@[simp]
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 = option.none ↔ x = option.none
@[simp]
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 = option.some y ↔ ∃ (a : α) (H : x = option.some a), f a _ = y
@[simp]
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_1 : α), a_1 ∈ a → p a_1) :
(option.pmap (option.pmap f) x H).join = option.pmap f x.join _
@[simp]
theorem
option.seq_some
{α β : Type u_1}
{a : α}
{f : α → β} :
option.some f <*> option.some a = option.some (f a)
@[simp]
theorem
option.some_orelse'
{α : Type u_1}
(a : α)
(x : option α) :
(option.some a).orelse x = option.some a
@[simp]
theorem
option.some_orelse
{α : Type u_1}
(a : α)
(x : option α) :
(option.some a <|> x) = option.some a
@[simp]
theorem
option.is_some_iff_exists
{α : Type u_1}
{x : option α} :
↥(x.is_some) ↔ ∃ (a : α), x = option.some a
@[simp]
theorem
option.eq_some_iff_get_eq
{α : Type u_1}
{o : option α}
{a : α} :
o = option.some a ↔ ∃ (h : ↥(o.is_some)), option.get h = a
theorem
option.ne_none_iff_exists
{α : Type u_1}
{o : option α} :
o ≠ option.none ↔ ∃ (x : α), option.some x = o
theorem
option.ne_none_iff_exists'
{α : Type u_1}
{o : option α} :
o ≠ option.none ↔ ∃ (x : α), o = option.some x
theorem
option.bex_ne_none
{α : Type u_1}
{p : option α → Prop} :
(∃ (x : option α) (H : x ≠ option.none), p x) ↔ ∃ (x : α), p (option.some x)
theorem
option.ball_ne_none
{α : Type u_1}
{p : option α → Prop} :
(∀ (x : option α), x ≠ option.none → p x) ↔ ∀ (x : α), p (option.some x)
@[simp]
theorem
option.guard_eq_some
{α : Type u_1}
{p : α → Prop}
[decidable_pred p]
{a b : α} :
option.guard p a = option.some b ↔ a = b ∧ p a
@[simp]
theorem
option.lift_or_get_choice
{α : Type u_1}
{f : α → α → α}
(h : ∀ (a b : α), f a b = a ∨ f a b = b)
(o₁ o₂ : option α) :
option.lift_or_get f o₁ o₂ = o₁ ∨ option.lift_or_get f o₁ o₂ = o₂
@[simp]
theorem
option.lift_or_get_none_left
{α : Type u_1}
{f : α → α → α}
{b : option α} :
option.lift_or_get f option.none b = b
@[simp]
theorem
option.lift_or_get_none_right
{α : Type u_1}
{f : α → α → α}
{a : option α} :
option.lift_or_get f a option.none = a
@[simp]
theorem
option.lift_or_get_some_some
{α : Type u_1}
{f : α → α → α}
{a b : α} :
option.lift_or_get f (option.some a) (option.some b) = ↑(f a b)
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.some a).cases_on' n s = s a
- option.none.cases_on' n s = n
@[simp]
theorem
option.cases_on'_none
{α : Type u_1}
{β : Type u_2}
(x : β)
(f : α → β) :
option.none.cases_on' x f = x
@[simp]
theorem
option.cases_on'_some
{α : Type u_1}
{β : Type u_2}
(x : β)
(f : α → β)
(a : α) :
(option.some a).cases_on' x f = f a
@[simp]
@[simp]
theorem
option.cases_on'_none_coe
{α : Type u_1}
{β : Type u_2}
(f : option α → β)
(o : option α) :
o.cases_on' (f option.none) (f ∘ coe) = f o
@[simp]
theorem
option.get_or_else_map
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(x : α)
(o : option α) :
(option.map f o).get_or_else (f x) = f (o.get_or_else x)
theorem
option.orelse_eq_some
{α : Type u_1}
(o o' : option α)
(x : α) :
(o <|> o') = option.some x ↔ o = option.some x ∨ o = option.none ∧ o' = option.some x
theorem
option.orelse_eq_some'
{α : Type u_1}
(o o' : option α)
(x : α) :
o.orelse o' = option.some x ↔ o = option.some x ∨ o = option.none ∧ o' = option.some x
@[simp]
theorem
option.orelse_eq_none
{α : Type u_1}
(o o' : option α) :
(o <|> o') = option.none ↔ o = option.none ∧ o' = option.none
@[simp]
theorem
option.orelse_eq_none'
{α : Type u_1}
(o o' : option α) :
o.orelse o' = option.none ↔ o = option.none ∧ o' = option.none
An arbitrary some a
with a : α
if α
is nonempty, and otherwise none
.
Equations
- option.choice α = dite (nonempty α) (λ (h : nonempty α), option.some h.some) (λ (h : ¬nonempty α), option.none)
theorem
option.choice_is_some_iff_nonempty
{α : Type u_1} :
↥((option.choice α).is_some) ↔ nonempty α
@[simp]
theorem
option.elim_none_some
{α : Type u_1}
{β : Type u_2}
(f : option α → β) :
option.elim (f option.none) (f ∘ option.some) = f