Properties of List.reduceOption #
In this file we prove basic lemmas about List.reduceOption.
@[simp]
theorem
List.reduceOption_cons_of_some
{α : Type u_1}
(x : α)
(l : List (Option α))
:
(some x :: l).reduceOption = x :: l.reduceOption
@[simp]
theorem
List.reduceOption_cons_of_none
{α : Type u_1}
(l : List (Option α))
:
(none :: l).reduceOption = l.reduceOption
@[simp]
theorem
List.reduceOption_map
{α : Type u_1}
{β : Type u_2}
{l : List (Option α)}
{f : α → β}
:
(map (Option.map f) l).reduceOption = map f l.reduceOption
theorem
List.reduceOption_append
{α : Type u_1}
(l l' : List (Option α))
:
(l ++ l').reduceOption = l.reduceOption ++ l'.reduceOption
@[simp]
theorem
List.reduceOption_replicate_none
{α : Type u_1}
{n : ℕ}
:
(replicate n none).reduceOption = []
theorem
List.reduceOption_eq_nil_iff
{α : Type u_1}
(l : List (Option α))
:
l.reduceOption = [] ↔ ∃ (n : ℕ), l = replicate n none
theorem
List.reduceOption_eq_singleton_iff
{α : Type u_1}
(l : List (Option α))
(a : α)
:
l.reduceOption = [a] ↔ ∃ (m : ℕ) (n : ℕ), l = replicate m none ++ some a :: replicate n none
theorem
List.reduceOption_eq_append_iff
{α : Type u_1}
(l : List (Option α))
(l'₁ l'₂ : List α)
:
l.reduceOption = l'₁ ++ l'₂ ↔ ∃ (l₁ : List (Option α)) (l₂ : List (Option α)), l = l₁ ++ l₂ ∧ l₁.reduceOption = l'₁ ∧ l₂.reduceOption = l'₂
theorem
List.reduceOption_eq_concat_iff
{α : Type u_1}
(l : List (Option α))
(l' : List α)
(a : α)
:
l.reduceOption = l'.concat a ↔ ∃ (l₁ : List (Option α)) (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
theorem
List.reduceOption_length_eq
{α : Type u_1}
{l : List (Option α)}
:
l.reduceOption.length = (filter Option.isSome l).length
theorem
List.length_eq_reduceOption_length_add_filter_none
{α : Type u_1}
{l : List (Option α)}
:
l.length = l.reduceOption.length + (filter Option.isNone l).length
theorem
List.reduceOption_length_eq_iff
{α : Type u_1}
{l : List (Option α)}
:
l.reduceOption.length = l.length ↔ ∀ x ∈ l, x.isSome = true
theorem
List.reduceOption_length_lt_iff
{α : Type u_1}
{l : List (Option α)}
:
l.reduceOption.length < l.length ↔ none ∈ l
theorem
List.reduceOption_concat
{α : Type u_1}
(l : List (Option α))
(x : Option α)
:
(l.concat x).reduceOption = l.reduceOption ++ x.toList
theorem
List.reduceOption_concat_of_some
{α : Type u_1}
(l : List (Option α))
(x : α)
:
(l.concat (some x)).reduceOption = l.reduceOption.concat x
theorem
List.reduceOption_mem_iff
{α : Type u_1}
{l : List (Option α)}
{x : α}
:
x ∈ l.reduceOption ↔ some x ∈ l
theorem
List.reduceOption_getElem?_iff
{α : Type u_1}
{l : List (Option α)}
{x : α}
:
(∃ (i : ℕ), l[i]? = some (some x)) ↔ ∃ (i : ℕ), l.reduceOption[i]? = some x