Lemmas for List not (yet) in Std

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_bex_nil {α : Type u} (p : α → Prop) : ¬∃ (x : α), x ∈ [] ∧ p x

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

list subset

sublists

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

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.length (List.mapAccumr f x s).snd = List.length x

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.length (List.mapAccumr₂ f x y c).snd = min (List.length x) (List.length y)

Length of a list obtained using mapAccumr₂.