Lemmas for List not (yet) in Batteries

append

length

map

bind

mem

theorem List.mem_cons_eq {α : Type u} (a : α) (y : α) (l : List α) : (a ∈ y :: l) = (a = y ∨ a ∈ l)

theorem List.eq_or_mem_of_mem_cons : ∀ {α : Type u_1} {a b : α} {l : List α}, a ∈ b :: l → a = b ∨ a ∈ l

Alias of the forward direction of List.mem_cons.

theorem List.not_exists_mem_nil {α : Type u} (p : α → Prop) : ¬∃ (x : α), x ∈ [] ∧ p x

@[deprecated List.not_exists_mem_nil]

theorem List.not_bex_nil {α : Type u} (p : α → Prop) : ¬∃ (x : α), x ∈ [] ∧ p x

Alias of List.not_exists_mem_nil.

@[deprecated List.exists_mem_cons]

theorem List.bex_cons {α : Type u_1} {p : α → Prop} {a : α} {l : List α} : (∃ (x : α), ∃ (x_1 : x ∈ a :: l), p x) ↔ p a ∨ ∃ (x : α), ∃ (x_1 : x ∈ l), p x

Alias of List.exists_mem_cons.

list subset

sublists

theorem List.length_le_of_sublist : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.length ≤ l₂.length

Alias of List.Sublist.length_le.

filter

map_accumr

def List.mapAccumr {α : Type u} {β : Type v} {σ : Type w₂} (f : α → σ → σ × β) : List α → σ → σ × List β

Runs a function over a list returning the intermediate results and a final result.

Equations

• List.mapAccumr f [] x = (x, [])
• List.mapAccumr f (y :: yr) x = let r := List.mapAccumr f yr x; let z := f y r.fst; (z.fst, z.snd :: r.snd)

@[simp]

theorem List.length_mapAccumr {α : Type u} {β : Type v} {σ : Type w₂} (f : α → σ → σ × β) (x : List α) (s : σ) : (List.mapAccumr f x s).snd.length = x.length

Length of the list obtained by mapAccumr.

def List.mapAccumr₂ {α : Type u} {β : Type v} {φ : Type w₁} {σ : Type w₂} (f : α → β → σ → σ × φ) : List α → List β → σ → σ × List φ

Runs a function over two lists returning the intermediate results and a final result.

Equations

• List.mapAccumr₂ f [] x✝ x = (x, [])
• List.mapAccumr₂ f x✝ [] x = (x, [])
• List.mapAccumr₂ f (x_3 :: xr) (y :: yr) x = let r := List.mapAccumr₂ f xr yr x; let q := f x_3 y r.fst; (q.fst, q.snd :: r.snd)

@[simp]

theorem List.length_mapAccumr₂ {α : Type u} {β : Type v} {φ : Type w₁} {σ : Type w₂} (f : α → β → σ → σ × φ) (x : List α) (y : List β) (c : σ) : (List.mapAccumr₂ f x y c).snd.length = min x.length y.length

Length of a list obtained using mapAccumr₂.