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_nil {α : Type u_1} : [].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_le {α : Type u_1} (l : List (Option α)) : l.reduceOption.length ≤ l.length

theorem List.reduceOption_length_eq_iff {α : Type u_1} {l : List (Option α)} : l.reduceOption.length = l.length ↔ ∀ (x : Option α), 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_singleton {α : Type u_1} (x : Option α) : [x].reduceOption = x.toList

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