Init.Data.Option.List

Option.mem_toList theorem

{a : α} {o : Option α} : a ∈ o.toList ↔ a ∈ o

Full source

@[simp] theorem mem_toList {a : α} {o : Option α} : a ∈ o.toLista ∈ o.toList ↔ a ∈ o := by
  cases o <;> simp [eq_comm]

Membership Preservation in Option-to-List Conversion: $a \in o.\text{toList} \leftrightarrow a \in o$

Informal description

For any element $a$ of type $\alpha$ and any optional value $o$ of type $\text{Option}\ \alpha$, the element $a$ belongs to the list obtained by converting $o$ to a list if and only if $a$ belongs to $o$ itself. In other words, $a \in o.\text{toList} \leftrightarrow a \in o$.

Option.forIn'_none theorem

[Monad m] (b : β) (f : (a : α) → a ∈ none → β → m (ForInStep β)) : forIn' none b f = pure b

Full source

@[simp] theorem forIn'_none [Monad m] (b : β) (f : (a : α) → a ∈ none → β → m (ForInStep β)) :
    forIn' none b f = pure b := by
  rfl

Monadic Iteration over Empty Option Yields Initial State

Informal description

For any monad `m`, initial state `b : β`, and function `f` that takes an element `a : α`, a proof that `a` is in the empty option `none`, and a state `β`, the monadic iteration `forIn'` over `none` with initial state `b` and function `f` returns the pure monadic value `pure b`.

Option.forIn'_some theorem

 [Monad m] [LawfulMonad m] (a : α) (b : β) (f : (a' : α) → a' ∈ some a → β → m (ForInStep β)) :
  forIn' (some a) b f = bind (f a rfl b) (fun r => pure (ForInStep.value r))

Full source

@[simp] theorem forIn'_some [Monad m] [LawfulMonad m] (a : α) (b : β) (f : (a' : α) → a' ∈ some a → β → m (ForInStep β)) :
    forIn' (some a) b f = bind (f a rfl b) (fun r => pure (ForInStep.value r)) := by
  simp only [forIn', bind_pure_comp]
  rw [map_eq_pure_bind]
  congr
  funext x
  split <;> rfl

Monadic Iteration over Non-Empty Optional Value with Membership Proofs

Informal description

Let $m$ be a lawful monad, $\alpha$ and $\beta$ be types, $a \in \alpha$ be an element, $b \in \beta$ be an initial state, and $f : \alpha \to \beta \to m(\text{ForInStep}\ \beta)$ be a function that processes elements with membership proofs. Then the monadic iteration over the optional value $\text{some}\ a$ with initial state $b$ and processing function $f$ is equal to binding the result of applying $f$ to $a$ (with proof $\text{rfl}$ that $a \in \text{some}\ a$) and $b$, then mapping the result to its value component. In symbols: $$\text{forIn'}\ (\text{some}\ a)\ b\ f = \text{bind}\ (f\ a\ \text{rfl}\ b)\ (\lambda r.\ \text{pure}\ (\text{ForInStep.value}\ r))$$

Option.forIn_none theorem

[Monad m] (b : β) (f : α → β → m (ForInStep β)) : forIn none b f = pure b

Full source

@[simp] theorem forIn_none [Monad m] (b : β) (f : α → β → m (ForInStep β)) :
    forIn none b f = pure b := by
  rfl

Monadic Iteration over `none` Returns Initial State

Informal description

For any monad `m`, initial state `b : β`, and function `f : α → β → m (ForInStep β)`, iterating over the `none` option with `forIn` returns the initial state `b` wrapped in the monad, i.e., `pure b`.

Option.forIn_some theorem

 [Monad m] [LawfulMonad m] (a : α) (b : β) (f : α → β → m (ForInStep β)) :
  forIn (some a) b f = bind (f a b) (fun r => pure (ForInStep.value r))

Full source

@[simp] theorem forIn_some [Monad m] [LawfulMonad m] (a : α) (b : β) (f : α → β → m (ForInStep β)) :
    forIn (some a) b f = bind (f a b) (fun r => pure (ForInStep.value r)) := by
  simp only [forIn, forIn', bind_pure_comp]
  rw [map_eq_pure_bind]
  congr
  funext x
  split <;> rfl

Monadic Iteration over Non-Empty Optional Value

Informal description

For any monad `m` that is a lawful monad, any element `a : α`, any initial state `b : β`, and any step function `f : α → β → m (ForInStep β)`, the monadic iteration over the optional value `some a` with initial state `b` and step function `f` is equal to binding the result of `f a b` and then wrapping the resulting value in `ForInStep.value`. In mathematical notation: $$\text{forIn}\ (\text{some}\ a)\ b\ f = f(a, b) \gg= \lambda r.\ \text{pure}\ (\text{ForInStep.value}\ r)$$

Option.forIn'_toList theorem

 [Monad m] (o : Option α) (b : β) (f : (a : α) → a ∈ o.toList → β → m (ForInStep β)) :
  forIn' o.toList b f = forIn' o b fun a m b => f a (by simpa using m) b

Full source

@[simp] theorem forIn'_toList [Monad m] (o : Option α) (b : β) (f : (a : α) → a ∈ o.toList → β → m (ForInStep β)) :
    forIn' o.toList b f = forIn' o b fun a m b => f a (by simpa using m) b := by
  cases o <;> rfl

Equivalence of Monadic Iteration with Membership Proofs for Optional Value and Its List Conversion

Informal description

Let $m$ be a monad, $o$ an optional value of type $\text{Option } \alpha$, $b$ a value of type $\beta$, and $f$ a function that takes an element $a \in \alpha$ with a proof that $a$ belongs to the list obtained from converting $o$ to a list, and a value of type $\beta$, and returns a monadic step. Then the monadic iteration with membership proofs over the list obtained from converting $o$ to a list is equal to the monadic iteration with membership proofs over $o$ itself, where the membership proof is derived from the conversion. In other words: \[ \text{forIn' } (\text{toList } o) \ b \ f = \text{forIn' } o \ b \ (\lambda a \ m \ b, f \ a \ (\text{by simpa using } m) \ b) \]

Option.forIn_toList theorem

[Monad m] (o : Option α) (b : β) (f : α → β → m (ForInStep β)) : forIn o.toList b f = forIn o b f

Full source

@[simp] theorem forIn_toList [Monad m] (o : Option α) (b : β) (f : α → β → m (ForInStep β)) :
    forIn o.toList b f = forIn o b f := by
  cases o <;> rfl

Equivalence of Monadic Iteration Between Optional Value and Its List Conversion

Informal description

For any monad $m$, optional value $o : \text{Option } \alpha$, initial state $b : \beta$, and iteration function $f : \alpha \to \beta \to m (\text{ForInStep } \beta)$, the monadic iteration over the list obtained from converting $o$ to a list is equivalent to the monadic iteration over $o$ itself. That is, \[ \text{forIn } (\text{toList } o) \ b \ f = \text{forIn } o \ b \ f. \]

Option.foldlM_toList theorem

 [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : α → β → m α) :
  o.toList.foldlM f a = o.elim (pure a) (fun b => f a b)

Full source

@[simp] theorem foldlM_toList [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : α → β → m α) :
    o.toList.foldlM f a = o.elim (pure a) (fun b => f a b) := by
  cases o <;> simp

Monadic Left Fold over Optional Value as List Conversion

Informal description

Let $m$ be a monad with lawful monad operations, and let $o$ be an optional value of type $\text{Option } \beta$. For any initial value $a : \alpha$ and any function $f : \alpha \to \beta \to m \alpha$, the monadic left fold over the list obtained from converting $o$ to a list is equal to eliminating the optional value $o$: if $o$ is $\text{none}$, return $\text{pure } a$; if $o$ is $\text{some } b$, apply $f$ to $a$ and $b$. In other words: \[ \text{foldlM } f \ a \ (\text{toList } o) = \text{elim } o \ (\text{pure } a) \ (\lambda b, f \ a \ b) \]

Option.foldrM_toList theorem

 [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : β → α → m α) :
  o.toList.foldrM f a = o.elim (pure a) (fun b => f b a)

Full source

@[simp] theorem foldrM_toList [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : β → α → m α) :
    o.toList.foldrM f a = o.elim (pure a) (fun b => f b a) := by
  cases o <;> simp

Monadic Right Fold over Optional Value as List Conversion

Informal description

Let $m$ be a monad with lawful monad operations, and let $o$ be an optional value of type $\text{Option } \beta$. For any initial value $a : \alpha$ and any function $f : \beta \to \alpha \to m \alpha$, the monadic right fold over the list obtained from converting $o$ to a list is equal to eliminating the optional value $o$: if $o$ is $\text{none}$, return $\text{pure } a$; if $o$ is $\text{some } b$, apply $f$ to $b$ and $a$. In other words: \[ \text{foldrM } f \ a \ (\text{toList } o) = \text{elim } o \ (\text{pure } a) \ (\lambda b, f \ b \ a) \]

Option.foldl_toList theorem

(o : Option β) (a : α) (f : α → β → α) : o.toList.foldl f a = o.elim a (fun b => f a b)

Full source

@[simp] theorem foldl_toList (o : Option β) (a : α) (f : α → β → α) :
    o.toList.foldl f a = o.elim a (fun b => f a b) := by
  cases o <;> simp

Left Fold over Option-to-List Conversion Equals Option Elimination

Informal description

For any optional value $o$ of type $\text{Option } \beta$, initial value $a$ of type $\alpha$, and function $f : \alpha \to \beta \to \alpha$, the left fold of $f$ over the list obtained from converting $o$ to a list, starting with $a$, is equal to eliminating $o$ by returning $a$ if $o$ is $\text{none}$ or applying $f$ to $a$ and the contained value $b$ if $o$ is $\text{some } b$. In symbols: \[ \text{foldl } f \ a \ (\text{toList } o) = \text{elim } o \ a \ (\lambda b, f \ a \ b) \]

Option.foldr_toList theorem

(o : Option β) (a : α) (f : β → α → α) : o.toList.foldr f a = o.elim a (fun b => f b a)

Full source

@[simp] theorem foldr_toList (o : Option β) (a : α) (f : β → α → α) :
    o.toList.foldr f a = o.elim a (fun b => f b a) := by
  cases o <;> simp

Right Fold over Option-to-List Conversion Equals Option Elimination

Informal description

For any optional value $o$ of type $\text{Option } \beta$, initial value $a$ of type $\alpha$, and function $f : \beta \to \alpha \to \alpha$, the right fold of $f$ over the list obtained from converting $o$ to a list, starting with $a$, is equal to eliminating $o$ by returning $a$ if $o$ is $\text{none}$ or applying $f$ to the contained value $b$ and $a$ if $o$ is $\text{some } b$. In symbols: \[ \text{foldr } f \ a \ (\text{toList } o) = \text{elim } o \ a \ (\lambda b, f \ b \ a) \]

Option.pairwise_toList theorem

{P : α → α → Prop} {o : Option α} : o.toList.Pairwise P

Full source

@[simp]
theorem pairwise_toList {P : α → α → Prop} {o : Option α} : o.toList.Pairwise P := by
  cases o <;> simp

Pairwise Property Holds for Option-to-List Conversion

Informal description

For any binary relation $P$ on a type $\alpha$ and any optional value $o$ of type $\text{Option } \alpha$, the list obtained by converting $o$ to a list satisfies the pairwise property with respect to $P$. In other words, if $o$ is $\text{none}$, the empty list trivially satisfies $\text{Pairwise } P$, and if $o$ is $\text{some } a$, the singleton list $[a]$ also satisfies $\text{Pairwise } P$ since there are no distinct elements to compare.

Option.head?_toList theorem

{o : Option α} : o.toList.head? = o

Full source

@[simp]
theorem head?_toList {o : Option α} : o.toList.head? = o := by
  cases o <;> simp

Head of Option-to-List Conversion Preserves Option Value

Informal description

For any optional value $o$ of type $\text{Option } \alpha$, the head of the list obtained by converting $o$ to a list is equal to $o$ itself. In other words, if $o$ is $\text{none}$, then $\text{head?}(\text{none.toList}) = \text{none}$, and if $o$ is $\text{some } a$, then $\text{head?}([\text{some } a]) = \text{some } a$.