Mathlib.Data.Option.Defs

Option.traverse definition

{F : Type u → Type v} [Applicative F] {α : Type*} {β : Type u} (f : α → F β) : Option α → F (Option β)

Full source

/-- Traverse an object of `Option α` with a function `f : α → F β` for an applicative `F`. -/
protected def traverse.{u, v}
    {F : Type u → Type v} [Applicative F] {α : Type*} {β : Type u} (f : α → F β) :
    Option α → F (Option β)
  | none => pure none
  | some x => some <$> f x

Traversal of an optional value under an applicative functor

Informal description

Given an applicative functor $F$, a function $f : \alpha \to F \beta$, and an optional value of type $\text{Option } \alpha$, the function $\text{Option.traverse}$ applies $f$ to the contained value (if any) and wraps the result in $\text{Option } \beta$ within the applicative context $F$. Specifically: - If the input is $\text{none}$, it returns $\text{pure none}$. - If the input is $\text{some } x$, it applies $f$ to $x$ and maps the result to $\text{some}$ within $F$.

Option.elim' definition

(b : β) (f : α → β) : Option α → β

Full source

/-- An elimination principle for `Option`. It is a nondependent version of `Option.rec`. -/
protected def elim' (b : β) (f : α → β) : Option α → β
  | some a => f a
  | none => b

Elimination principle for optional values

Informal description

The function `Option.elim'` takes a default value $b$ of type $\beta$, a function $f : \alpha \to \beta$, and an optional value of type `Option α`. It returns $f(a)$ when the input is `some a`, and returns the default value $b$ when the input is `none`.

Option.elim'_none theorem

(b : β) (f : α → β) : Option.elim' b f none = b

Full source

@[simp]
theorem elim'_none (b : β) (f : α → β) : Option.elim' b f none = b := rfl

Elimination of `none` in Optional Values Yields Default Value

Informal description

For any default value $b$ of type $\beta$ and any function $f : \alpha \to \beta$, applying the elimination function `Option.elim'` to $b$, $f$, and `none` yields the default value $b$, i.e., $\text{Option.elim'}\ b\ f\ \text{none} = b$.

Option.elim'_some theorem

{a : α} (b : β) (f : α → β) : Option.elim' b f (some a) = f a

Full source

@[simp]
theorem elim'_some {a : α} (b : β) (f : α → β) : Option.elim' b f (some a) = f a := rfl

Elimination of `some a` in Optional Values Yields Function Application

Informal description

For any element $a$ of type $\alpha$, any default value $b$ of type $\beta$, and any function $f : \alpha \to \beta$, applying the elimination function `Option.elim'` to $b$, $f$, and `some a` yields the result of applying $f$ to $a$, i.e., $\text{Option.elim'}\ b\ f\ (\text{some}\ a) = f(a)$.

Option.elim'_none_some theorem

(f : Option α → β) : (Option.elim' (f none) (f ∘ some)) = f

Full source

@[simp]
theorem elim'_none_some (f : Option α → β) : (Option.elim' (f none) (f ∘ some)) = f :=
  funext fun o ↦ by cases o <;> rfl

Elimination Principle for Option Type: $\text{Option.elim'}(f(\text{none}), f \circ \text{some}) = f$

Informal description

For any function $f : \text{Option } \alpha \to \beta$, the elimination function $\text{Option.elim'}$ applied to the default value $f(\text{none})$ and the composition $f \circ \text{some}$ is equal to $f$ itself, i.e., \[ \text{Option.elim'}(f(\text{none}), f \circ \text{some}) = f. \]

Option.elim'_eq_elim theorem

{α β : Type*} (b : β) (f : α → β) (a : Option α) : Option.elim' b f a = Option.elim a b f

Full source

lemma elim'_eq_elim {α β : Type*} (b : β) (f : α → β) (a : Option α) :
    Option.elim' b f a = Option.elim a b f := by
  cases a <;> rfl

Equivalence of Option Elimination Functions: `Option.elim'` and `Option.elim`

Informal description

For any types $\alpha$ and $\beta$, a default value $b : \beta$, a function $f : \alpha \to \beta$, and an optional value $a : \text{Option } \alpha$, the elimination function `Option.elim'` applied to $b$, $f$, and $a$ is equal to `Option.elim` applied to $a$, $b$, and $f$.

Option.mem_some_iff theorem

{α : Type*} {a b : α} : a ∈ some b ↔ b = a

Full source

theorem mem_some_iff {α : Type*} {a b : α} : a ∈ some ba ∈ some b ↔ b = a := by simp

Membership in `some` is equivalent to equality

Informal description

For any elements $a$ and $b$ of type $\alpha$, the element $a$ is a member of the `Option.some b` constructor if and only if $b = a$.

Option.decidableEqNone definition

{o : Option α} : Decidable (o = none)

Full source

/-- `o = none` is decidable even if the wrapped type does not have decidable equality.
This is not an instance because it is not definitionally equal to `Option.decidableEq`.
Try to use `o.isNone` or `o.isSome` instead.
-/
@[inline]
def decidableEqNone {o : Option α} : Decidable (o = none) :=
  decidable_of_decidable_of_iff isNone_iff_eq_none

Decidability of equality with `none` for optional values

Informal description

For any optional value `o : Option α`, the proposition `o = none` is decidable, even when the type `α` does not have decidable equality. This is not an instance because it is not definitionally equal to `Option.decidableEq`. It is recommended to use `o.isNone` or `o.isSome` instead for better definitional behavior.

Option.decidableForallMem instance

{p : α → Prop} [DecidablePred p] : ∀ o : Option α, Decidable (∀ a ∈ o, p a)

Full source

instance decidableForallMem {p : α → Prop} [DecidablePred p] :
    ∀ o : Option α, Decidable (∀ a ∈ o, p a)
  | none => isTrue (by simp [false_imp_iff])
  | some a =>
      if h : p a then isTrue fun _ e ↦ some_inj.1 e ▸ h
      else isFalse <| mt (fun H ↦ H _ rfl) h

Decidability of Universal Quantification over Option Types

Informal description

For any predicate $p$ on a type $\alpha$ with a decidable truth value, and for any optional value $o$ of type $\text{Option } \alpha$, it is decidable whether all elements $a$ in $o$ satisfy $p(a)$.

Option.decidableExistsMem instance

{p : α → Prop} [DecidablePred p] : ∀ o : Option α, Decidable (∃ a ∈ o, p a)

Full source

instance decidableExistsMem {p : α → Prop} [DecidablePred p] :
    ∀ o : Option α, Decidable (∃ a ∈ o, p a)
  | none => isFalse fun ⟨a, ⟨h, _⟩⟩ ↦ by cases h
  | some a => if h : p a then isTrue <| ⟨_, rfl, h⟩ else isFalse fun ⟨_, ⟨rfl, hn⟩⟩ ↦ h hn

Decidability of Existential Quantifier over Option Type

Informal description

For any predicate $p$ on a type $\alpha$ with a decidable truth value, and for any optional value $o$ of type $\alpha$, it is decidable whether there exists an element $a$ in $o$ such that $p(a)$ holds.

Option.iget abbrev

[Inhabited α] : Option α → α

Full source

/-- Inhabited `get` function. Returns `a` if the input is `some a`, otherwise returns `default`. -/
abbrev iget [Inhabited α] : Option α → α
  | some x => x
  | none => default

Default-valued extraction from Option type

Informal description

Given a type $\alpha$ with a distinguished default element (i.e., $\alpha$ is `Inhabited`), the function `iget` maps an `Option α` to an $\alpha$ by returning the contained value if the input is `some a`, and the default value otherwise.

Option.iget_some theorem

[Inhabited α] {a : α} : (some a).iget = a

Full source

theorem iget_some [Inhabited α] {a : α} : (some a).iget = a :=
  rfl

Default extraction from `some` returns the contained value

Informal description

For any element $a$ of an inhabited type $\alpha$, the function `iget` applied to the option `some a` returns $a$.

Option.liftOrGet_isCommutative instance

(f : α → α → α) [Std.Commutative f] : Std.Commutative (liftOrGet f)

Full source

instance liftOrGet_isCommutative (f : α → α → α) [Std.Commutative f] :
    Std.Commutative (liftOrGet f) :=
  ⟨fun a b ↦ by cases a <;> cases b <;> simp [liftOrGet, Std.Commutative.comm]⟩

Commutativity of Lifted Operation on Options

Informal description

For any binary operation $f : \alpha \to \alpha \to \alpha$ that is commutative, the lifted operation `liftOrGet f` on `Option α` is also commutative.

Option.liftOrGet_isAssociative instance

(f : α → α → α) [Std.Associative f] : Std.Associative (liftOrGet f)

Full source

instance liftOrGet_isAssociative (f : α → α → α) [Std.Associative f] :
    Std.Associative (liftOrGet f) :=
  ⟨fun a b c ↦ by cases a <;> cases b <;> cases c <;> simp [liftOrGet, Std.Associative.assoc]⟩

Associativity of `liftOrGet` for Associative Operations

Informal description

For any associative binary operation $f : \alpha \to \alpha \to \alpha$, the operation `liftOrGet f` on `Option α` is also associative.

Option.liftOrGet_isIdempotent instance

(f : α → α → α) [Std.IdempotentOp f] : Std.IdempotentOp (liftOrGet f)

Full source

instance liftOrGet_isIdempotent (f : α → α → α) [Std.IdempotentOp f] :
    Std.IdempotentOp (liftOrGet f) :=
  ⟨fun a ↦ by cases a <;> simp [liftOrGet, Std.IdempotentOp.idempotent]⟩

Idempotence of `liftOrGet` for Idempotent Operations

Informal description

For any idempotent binary operation $f$ on a type $\alpha$, the operation `liftOrGet f` on `Option α` is also idempotent.

Option.liftOrGet_isId instance

(f : α → α → α) : Std.LawfulIdentity (liftOrGet f) none

Full source

instance liftOrGet_isId (f : α → α → α) : Std.LawfulIdentity (liftOrGet f) none where
  left_id a := by cases a <;> simp [liftOrGet]
  right_id a := by cases a <;> simp [liftOrGet]

`none` is the identity for `liftOrGet f` on `Option α`

Informal description

For any binary operation $f$ on a type $\alpha$, the operation `liftOrGet f` on `Option α` has `none` as its identity element.

Option.lawfulIdentity_merge instance

(f : α → α → α) : Std.LawfulIdentity (merge f) none

Full source

instance lawfulIdentity_merge (f : α → α → α) : Std.LawfulIdentity (merge f) none :=
  liftOrGet_isId f

`none` is the identity for `merge f` on `Option α`

Informal description

For any binary operation $f$ on a type $\alpha$, the operation `merge f` on `Option α` has `none` as its identity element.

Lean.LOption.toOption definition

{α} : Lean.LOption α → Option α

Full source

/-- Convert `undef` to `none` to make an `LOption` into an `Option`. -/
def _root_.Lean.LOption.toOption {α} : Lean.LOption α → Option α
  | .some a => some a
  | _ => none

Conversion from `LOption` to `Option`

Informal description

The function converts a value of type `Lean.LOption α` to an `Option α` by mapping `Lean.LOption.some a` to `Option.some a` and all other cases (including `Lean.LOption.undef`) to `Option.none`.