Theorems about List operations.

For each List operation, we would like theorems describing the following, when relevant:

• if it is a "convenience" function, a @[simp] lemma reducing it to more basic operations (e.g. List.partition_eq_filter_filter), and otherwise:
• any special cases of equational lemmas that require additional hypotheses
• lemmas for special cases of the arguments (e.g. List.map_id)
• the length of the result (f L).length
• the i-th element, described via (f L)[i] and/or (f L)[i]? (these should typically be @[simp])
• consequences for f L of the fact x ∈ L or x ∉ L
• conditions characterising x ∈ f L (often but not always @[simp])
• injectivity statements, or congruence statements of the form p L M → f L = f M.
• conditions characterising the result, i.e. of the form f L = M ↔ p M for some predicate p, along with special cases of M (e.g. List.append_eq_nil : L ++ M = [] ↔ L = [] ∧ M = [])
• negative characterisations are also useful, e.g. List.cons_ne_nil
• interactions with all previously described List operations where possible (some of these should be @[simp], particularly if the result can be described by a single operation)
• characterising (∀ (i) (_ : i ∈ f L), P i), for some predicate P

Of course for any individual operation, not all of these will be relevant or helpful, so some judgement is required.

General principles for simp normal forms for List operations:

• Conversion operations (e.g. toArray, or length) should be moved inwards aggressively, to make the conversion effective.
• Similarly, operations which work on elements should be moved inwards in preference to "structural" operations on the list, e.g. we prefer to simplify List.map f (L ++ M) ~> (List.map f L) ++ (List.map f M), List.map f L.reverse ~> (List.map f L).reverse, and List.map f (L.take n) ~> (List.map f L).take n.
• Arithmetic operations are "light", so e.g. we prefer to simplify drop i (drop j L) to drop (i + j) L, rather than the other way round.
• Function compositions are "light", so we prefer to simplify (L.map f).map g to L.map (g ∘ f).
• We try to avoid non-linear left hand sides (i.e. with subexpressions appearing multiple times), but this is only a weak preference.
• Generally, we prefer that the right hand side does not introduce duplication, however generally duplication of higher order arguments (functions, predicates, etc) is allowed, as we expect to be able to compute these once they reach ground terms.

See also

• Init.Data.List.Attach for definitions and lemmas about List.attach and List.pmap.
• Init.Data.List.Count for lemmas about List.countP and List.count.
• Init.Data.List.Erase for lemmas about List.eraseP and List.erase.
• Init.Data.List.Find for lemmas about List.find?, List.findSome?, List.findIdx, List.findIdx?, and List.indexOf
• Init.Data.List.MinMax for lemmas about List.min? and List.max?.
• Init.Data.List.Pairwise for lemmas about List.Pairwise and List.Nodup.
• Init.Data.List.Sublist for lemmas about List.Subset, List.Sublist, List.IsPrefix, List.IsSuffix, and List.IsInfix.
• Init.Data.List.TakeDrop for additional lemmas about List.take and List.drop.
• Init.Data.List.Zip for lemmas about List.zip, List.zipWith, List.zipWithAll, and List.unzip.

Further results, which first require developing further automation around Nat, appear in

• Init.Data.List.Nat.Basic: miscellaneous lemmas
• Init.Data.List.Nat.Range: List.range and List.enum
• Init.Data.List.Nat.TakeDrop: List.take and List.drop

Also

• Init.Data.List.Monadic for addiation lemmas about List.mapM and List.forM.

Preliminaries

nil

@[simp]

theorem List.nil_eq {α : Type u_1} {xs : List α} : [] = xs ↔ xs = []

cons

theorem List.cons_ne_nil {α : Type u_1} (a : α) (l : List α) : a :: l ≠ []

@[simp]

theorem List.cons_ne_self {α : Type u_1} (a : α) (l : List α) : a :: l ≠ l

@[simp]

theorem List.ne_cons_self {α : Type u_1} {a : α} {l : List α} : l ≠ a :: l

theorem List.head_eq_of_cons_eq : ∀ {α : Type u_1} {h₁ : α} {t₁ : List α} {h₂ : α} {t₂ : List α}, h₁ :: t₁ = h₂ :: t₂ → h₁ = h₂

theorem List.tail_eq_of_cons_eq : ∀ {α : Type u_1} {h₁ : α} {t₁ : List α} {h₂ : α} {t₂ : List α}, h₁ :: t₁ = h₂ :: t₂ → t₁ = t₂

theorem List.cons_inj_right {α : Type u_1} (a : α) {l : List α} {l' : List α} : a :: l = a :: l' ↔ l = l'

@[reducible, inline, deprecated]

abbrev List.cons_inj {α : Type u_1} (a : α) {l : List α} {l' : List α} : a :: l = a :: l' ↔ l = l'

Equations

• @List.cons_inj = @List.cons_inj_right

theorem List.cons_eq_cons {α : Type u_1} {a : α} {b : α} {l : List α} {l' : List α} : a :: l = b :: l' ↔ a = b ∧ l = l'

theorem List.exists_cons_of_ne_nil {α : Type u_1} {l : List α} : l ≠ [] → ∃ (b : α), ∃ (L : List α), l = b :: L

theorem List.singleton_inj {α : Type u_1} {a : α} {b : α} : [a] = [b] ↔ a = b

length

theorem List.eq_nil_of_length_eq_zero : ∀ {α : Type u_1} {l : List α}, l.length = 0 → l = []

theorem List.ne_nil_of_length_eq_add_one : ∀ {α : Type u_1} {l : List α} {n : Nat}, l.length = n + 1 → l ≠ []

@[reducible, inline, deprecated List.ne_nil_of_length_eq_add_one]

abbrev List.ne_nil_of_length_eq_succ : ∀ {α : Type u_1} {l : List α} {n : Nat}, l.length = n + 1 → l ≠ []

Equations

• @List.ne_nil_of_length_eq_succ = @List.ne_nil_of_length_eq_add_one

theorem List.ne_nil_of_length_pos : ∀ {α : Type u_1} {l : List α}, 0 < l.length → l ≠ []

@[simp]

theorem List.length_eq_zero : ∀ {α : Type u_1} {l : List α}, l.length = 0 ↔ l = []

theorem List.length_pos_of_mem {α : Type u_1} {a : α} {l : List α} : a ∈ l → 0 < l.length

theorem List.exists_mem_of_length_pos {α : Type u_1} {l : List α} : 0 < l.length → ∃ (a : α), a ∈ l

theorem List.length_pos_iff_exists_mem {α : Type u_1} {l : List α} : 0 < l.length ↔ ∃ (a : α), a ∈ l

theorem List.exists_mem_of_length_eq_add_one {α : Type u_1} {n : Nat} {l : List α} : l.length = n + 1 → ∃ (a : α), a ∈ l

theorem List.exists_cons_of_length_pos {α : Type u_1} {l : List α} : 0 < l.length → ∃ (h : α), ∃ (t : List α), l = h :: t

theorem List.length_pos_iff_exists_cons {α : Type u_1} {l : List α} : 0 < l.length ↔ ∃ (h : α), ∃ (t : List α), l = h :: t

theorem List.exists_cons_of_length_eq_add_one {α : Type u_1} {n : Nat} {l : List α} : l.length = n + 1 → ∃ (h : α), ∃ (t : List α), l = h :: t

theorem List.length_pos {α : Type u_1} {l : List α} : 0 < l.length ↔ l ≠ []

theorem List.length_eq_one {α : Type u_1} {l : List α} : l.length = 1 ↔ ∃ (a : α), l = [a]

L[i] and L[i]?

get and get?.

We simplify l.get i to l[i.1]'i.2 and l.get? i to l[i]?.

theorem List.get_cons_zero : ∀ {α : Type u_1} {a : α} {l : List α}, (a :: l).get 0 = a

theorem List.get_cons_succ {α : Type u_1} {i : Nat} {a : α} {as : List α} {h : i + 1 < (a :: as).length} : (a :: as).get ⟨i + 1, h⟩ = as.get ⟨i, ⋯⟩

theorem List.get_cons_succ' {α : Type u_1} {a : α} {as : List α} {i : Fin as.length} : (a :: as).get i.succ = as.get i

@[deprecated]

theorem List.get_cons_cons_one : ∀ {α : Type u_1} {a₁ a₂ : α} {as : List α}, (a₁ :: a₂ :: as).get 1 = a₂

theorem List.get_mk_zero {α : Type u_1} {l : List α} (h : 0 < l.length) : l.get ⟨0, h⟩ = l.head ⋯

theorem List.get?_zero {α : Type u_1} (l : List α) : l.get? 0 = l.head?

theorem List.get?_len_le {α : Type u_1} {l : List α} {n : Nat} : l.length ≤ n → l.get? n = none

theorem List.get?_eq_get {α : Type u_1} {l : List α} {n : Nat} (h : n < l.length) : l.get? n = some (l.get ⟨n, h⟩)

theorem List.get?_eq_some : ∀ {α : Type u_1} {a : α} {l : List α} {n : Nat}, l.get? n = some a ↔ ∃ (h : n < l.length), l.get ⟨n, h⟩ = a

theorem List.get?_eq_none : ∀ {α : Type u_1} {l : List α} {n : Nat}, l.get? n = none ↔ l.length ≤ n

@[simp]

theorem List.get?_eq_getElem? {α : Type u_1} (l : List α) (i : Nat) : l.get? i = l[i]?

@[simp]

theorem List.get_eq_getElem {α : Type u_1} (l : List α) (i : Fin l.length) : l.get i = l[↑i]

theorem List.getElem?_eq_some {α : Type u_1} {i : Nat} {a : α} {l : List α} : l[i]? = some a ↔ ∃ (h : i < l.length), l[i] = a

theorem List.get_of_eq {α : Type u_1} {l : List α} {l' : List α} (h : l = l') (i : Fin l.length) : l.get i = l'.get ⟨↑i, ⋯⟩

If one has l.get i in an expression (with i : Fin l.length) and h : l = l', rw [h] will give a "motive it not type correct" error, as it cannot rewrite the i : Fin l.length to Fin l'.length directly. The theorem get_of_eq can be used to make such a rewrite, with rw [get_of_eq h].

getD

We simplify away getD, replacing getD l n a with (l[n]?).getD a. Because of this, there is only minimal API for getD.

@[simp]

theorem List.getD_eq_getElem?_getD {α : Type u_1} (l : List α) (n : Nat) (a : α) : l.getD n a = l[n]?.getD a

@[deprecated List.getD_eq_getElem?_getD]

theorem List.getD_eq_get? {α : Type u_1} (l : List α) (n : Nat) (a : α) : l.getD n a = (l.get? n).getD a

get!

We simplify l.get! n to l[n]!.

theorem List.get!_of_get? {α : Type u_1} {a : α} [Inhabited α] {l : List α} {n : Nat} : l.get? n = some a → l.get! n = a

theorem List.get!_eq_getD {α : Type u_1} [Inhabited α] (l : List α) (n : Nat) : l.get! n = l.getD n default

theorem List.get!_len_le {α : Type u_1} [Inhabited α] {l : List α} {n : Nat} : l.length ≤ n → l.get! n = default

@[simp]

theorem List.get!_eq_getElem! {α : Type u_1} [Inhabited α] (l : List α) (n : Nat) : l.get! n = l[n]!

getElem!

@[simp]

theorem List.getElem!_nil {α : Type u_1} [Inhabited α] {n : Nat} : [][n]! = default

@[simp]

theorem List.getElem!_cons_zero {α : Type u_1} {a : α} [Inhabited α] {l : List α} : (a :: l)[0]! = a

@[simp]

theorem List.getElem!_cons_succ {α : Type u_1} {a : α} {n : Nat} [Inhabited α] {l : List α} : (a :: l)[n + 1]! = l[n]!

getElem? and getElem

@[simp]

theorem List.getElem?_eq_getElem {α : Type u_1} {l : List α} {n : Nat} (h : n < l.length) : l[n]? = some l[n]

theorem List.getElem?_eq_some_iff {α : Type u_1} {n : Nat} {a : α} {l : List α} : l[n]? = some a ↔ ∃ (h : n < l.length), l[n] = a

theorem List.some_eq_getElem?_iff {α : Type u_1} {a : α} {n : Nat} {l : List α} : some a = l[n]? ↔ ∃ (h : n < l.length), l[n] = a

@[simp]

theorem List.getElem?_eq_none_iff : ∀ {α : Type u_1} {l : List α} {n : Nat}, l[n]? = none ↔ l.length ≤ n

@[simp]

theorem List.none_eq_getElem?_iff {α : Type u_1} {l : List α} {n : Nat} : none = l[n]? ↔ l.length ≤ n

theorem List.getElem?_eq_none : ∀ {α : Type u_1} {l : List α} {n : Nat}, l.length ≤ n → l[n]? = none

theorem List.getElem?_eq {α : Type u_1} (l : List α) (i : Nat) : l[i]? = if h : i < l.length then some l[i] else none

@[simp]

theorem List.some_getElem_eq_getElem?_iff {α : Type u_1} (xs : List α) (i : Nat) (h : i < xs.length) : some xs[i] = xs[i]? ↔ True

@[simp]

theorem List.getElem?_eq_some_getElem_iff {α : Type u_1} (xs : List α) (i : Nat) (h : i < xs.length) : xs[i]? = some xs[i] ↔ True

theorem List.getElem_eq_iff {α : Type u_1} {x : α} {l : List α} {n : Nat} {h : n < l.length} : l[n] = x ↔ l[n]? = some x

theorem List.getElem_eq_getElem?_get {α : Type u_1} (l : List α) (i : Nat) (h : i < l.length) : l[i] = l[i]?.get ⋯

@[reducible, inline, deprecated List.getElem_eq_getElem?_get]

abbrev List.getElem_eq_getElem? {α : Type u_1} (l : List α) (i : Nat) (h : i < l.length) : l[i] = l[i]?.get ⋯

Equations

• @List.getElem_eq_getElem? = @List.getElem_eq_getElem?_get

@[simp]

theorem List.getElem?_nil {α : Type u_1} {n : Nat} : [][n]? = none

theorem List.getElem?_cons_zero {α : Type u_1} {a : α} {l : List α} : (a :: l)[0]? = some a

@[simp]

theorem List.getElem?_cons_succ {α : Type u_1} {a : α} {n : Nat} {l : List α} : (a :: l)[n + 1]? = l[n]?

theorem List.getElem?_cons : ∀ {α : outParam (Type u_1)} {a : α} {l : List α} {i : Nat}, (a :: l)[i]? = if i = 0 then some a else l[i - 1]?

theorem List.getElem?_len_le {α : Type u_1} {l : List α} {n : Nat} : l.length ≤ n → l[n]? = none

theorem List.getElem_of_eq {α : Type u_1} {l : List α} {l' : List α} (h : l = l') {i : Nat} (w : i < l.length) : l[i] = l'[i]

If one has l[i] in an expression and h : l = l', rw [h] will give a "motive it not type correct" error, as it cannot rewrite the implicit i < l.length to i < l'.length directly. The theorem getElem_of_eq can be used to make such a rewrite, with rw [getElem_of_eq h].

@[simp]

theorem List.getElem_singleton {α : Type u_1} {i : Nat} (a : α) (h : i < 1) : [a][i] = a

@[deprecated List.getElem_singleton]

theorem List.get_singleton {α : Type u_1} (a : α) (n : Fin 1) : [a].get n = a

theorem List.getElem_zero {α : Type u_1} {l : List α} (h : 0 < l.length) : l[0] = l.head ⋯

theorem List.getElem!_of_getElem? {α : Type u_1} {a : α} [Inhabited α] {l : List α} {n : Nat} : l[n]? = some a → l[n]! = a

theorem List.ext_getElem?_iff {α : Type u_1} {l₁ : List α} {l₂ : List α} : l₁ = l₂ ↔ ∀ (n : Nat), l₁[n]? = l₂[n]?

theorem List.ext_getElem? {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : ∀ (n : Nat), l₁[n]? = l₂[n]?) : l₁ = l₂

theorem List.ext_getElem {α : Type u_1} {l₁ : List α} {l₂ : List α} (hl : l₁.length = l₂.length) (h : ∀ (n : Nat) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁[n] = l₂[n]) : l₁ = l₂

theorem List.ext_get {α : Type u_1} {l₁ : List α} {l₂ : List α} (hl : l₁.length = l₂.length) (h : ∀ (n : Nat) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩) : l₁ = l₂

@[simp]

theorem List.getElem_concat_length {α : Type u_1} (l : List α) (a : α) (i : Nat) : i = l.length → ∀ (w : i < (l ++ [a]).length), (l ++ [a])[i] = a

theorem List.getElem?_concat_length {α : Type u_1} (l : List α) (a : α) : (l ++ [a])[l.length]? = some a

@[deprecated List.getElem?_concat_length]

theorem List.get?_concat_length {α : Type u_1} (l : List α) (a : α) : (l ++ [a]).get? l.length = some a

mem

@[simp]

theorem List.not_mem_nil {α : Type u_1} (a : α) : ¬a ∈ []

@[simp]

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

theorem List.mem_cons_self {α : Type u_1} (a : α) (l : List α) : a ∈ a :: l

theorem List.mem_concat_self {α : Type u_1} (xs : List α) (a : α) : a ∈ xs ++ [a]

theorem List.mem_append_cons_self : ∀ {α : Type u_1} {xs : List α} {a : α} {ys : List α}, a ∈ xs ++ a :: ys

theorem List.eq_append_cons_of_mem {α : Type u_1} {a : α} {xs : List α} (h : a ∈ xs) : ∃ (as : List α), ∃ (bs : List α), xs = as ++ a :: bs ∧ ¬a ∈ as

theorem List.mem_cons_of_mem {α : Type u_1} (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y :: l

theorem List.exists_mem_of_ne_nil {α : Type u_1} (l : List α) (h : l ≠ []) : ∃ (x : α), x ∈ l

theorem List.eq_nil_iff_forall_not_mem {α : Type u_1} {l : List α} : l = [] ↔ ∀ (a : α), ¬a ∈ l

@[simp]

theorem List.mem_dite_nil_left {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : ¬p → List α} : (x ∈ if h : p then [] else l h) ↔ ∃ (h : ¬p), x ∈ l h

@[simp]

theorem List.mem_dite_nil_right {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : p → List α} : (x ∈ if h : p then l h else []) ↔ ∃ (h : p), x ∈ l h

@[simp]

theorem List.mem_ite_nil_left {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : List α} : (x ∈ if p then [] else l) ↔ ¬p ∧ x ∈ l

@[simp]

theorem List.mem_ite_nil_right {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : List α} : (x ∈ if p then l else []) ↔ p ∧ x ∈ l

theorem List.eq_of_mem_singleton : ∀ {α : Type u_1} {b a : α}, a ∈ [b] → a = b

@[simp]

theorem List.mem_singleton {α : Type u_1} {a : α} {b : α} : a ∈ [b] ↔ a = b

theorem List.forall_mem_cons {α : Type u_1} {p : α → Prop} {a : α} {l : List α} : (∀ (x : α), x ∈ a :: l → p x) ↔ p a ∧ ∀ (x : α), x ∈ l → p x

theorem List.forall_mem_ne {α : Type u_1} {a : α} {l : List α} : (∀ (a' : α), a' ∈ l → ¬a = a') ↔ ¬a ∈ l

theorem List.forall_mem_ne' {α : Type u_1} {a : α} {l : List α} : (∀ (a' : α), a' ∈ l → ¬a' = a) ↔ ¬a ∈ l

theorem List.exists_mem_nil {α : Type u_1} (p : α → Prop) : ¬∃ (x : α), ∃ (x_1 : x ∈ []), p x

theorem List.forall_mem_nil {α : Type u_1} (p : α → Prop) (x : α) : x ∈ [] → p x

theorem List.exists_mem_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

theorem List.forall_mem_singleton {α : Type u_1} {p : α → Prop} {a : α} : (∀ (x : α), x ∈ [a] → p x) ↔ p a

theorem List.mem_nil_iff {α : Type u_1} (a : α) : a ∈ [] ↔ False

theorem List.mem_singleton_self {α : Type u_1} (a : α) : a ∈ [a]

theorem List.mem_of_mem_cons_of_mem {α : Type u_1} {a : α} {b : α} {l : List α} : a ∈ b :: l → b ∈ l → a ∈ l

theorem List.eq_or_ne_mem_of_mem {α : Type u_1} {a : α} {b : α} {l : List α} (h' : a ∈ b :: l) : a = b ∨ a ≠ b ∧ a ∈ l

theorem List.ne_nil_of_mem {α : Type u_1} {a : α} {l : List α} (h : a ∈ l) : l ≠ []

theorem List.mem_of_ne_of_mem {α : Type u_1} {a : α} {y : α} {l : List α} (h₁ : a ≠ y) (h₂ : a ∈ y :: l) : a ∈ l

theorem List.ne_of_not_mem_cons {α : Type u_1} {a : α} {b : α} {l : List α} : ¬a ∈ b :: l → a ≠ b

theorem List.not_mem_of_not_mem_cons {α : Type u_1} {a : α} {b : α} {l : List α} : ¬a ∈ b :: l → ¬a ∈ l

theorem List.not_mem_cons_of_ne_of_not_mem {α : Type u_1} {a : α} {y : α} {l : List α} : a ≠ y → ¬a ∈ l → ¬a ∈ y :: l

theorem List.ne_and_not_mem_of_not_mem_cons {α : Type u_1} {a : α} {y : α} {l : List α} : ¬a ∈ y :: l → a ≠ y ∧ ¬a ∈ l

theorem List.getElem_of_mem {α : Type u_1} {a : α} {l : List α} : a ∈ l → ∃ (n : Nat), ∃ (h : n < l.length), l[n] = a

theorem List.get_of_mem {α : Type u_1} {a : α} {l : List α} (h : a ∈ l) : ∃ (n : Fin l.length), l.get n = a

theorem List.getElem?_of_mem {α : Type u_1} {a : α} {l : List α} (h : a ∈ l) : ∃ (n : Nat), l[n]? = some a

theorem List.get?_of_mem {α : Type u_1} {a : α} {l : List α} (h : a ∈ l) : ∃ (n : Nat), l.get? n = some a

@[simp]

theorem List.getElem_mem {α : Type u_1} {l : List α} {n : Nat} (h : n < l.length) : l[n] ∈ l

theorem List.get_mem {α : Type u_1} (l : List α) (n : Nat) (h : n < l.length) : l.get ⟨n, h⟩ ∈ l

theorem List.getElem?_mem {α : Type u_1} {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) : a ∈ l

theorem List.get?_mem {α : Type u_1} {l : List α} {n : Nat} {a : α} (e : l.get? n = some a) : a ∈ l

theorem List.mem_iff_getElem {α : Type u_1} {a : α} {l : List α} : a ∈ l ↔ ∃ (n : Nat), ∃ (h : n < l.length), l[n] = a

theorem List.mem_iff_get {α : Type u_1} {a : α} {l : List α} : a ∈ l ↔ ∃ (n : Fin l.length), l.get n = a

theorem List.mem_iff_getElem? {α : Type u_1} {a : α} {l : List α} : a ∈ l ↔ ∃ (n : Nat), l[n]? = some a

theorem List.mem_iff_get? {α : Type u_1} {a : α} {l : List α} : a ∈ l ↔ ∃ (n : Nat), l.get? n = some a

theorem List.forall_getElem {α : Type u_1} {l : List α} {p : α → Prop} : (∀ (n : Nat) (h : n < l.length), p l[n]) ↔ ∀ (a : α), a ∈ l → p a

@[simp]

theorem List.decide_mem_cons {α : Type u_1} {a : α} {y : α} [BEq α] [LawfulBEq α] {l : List α} : decide (y ∈ a :: l) = (y == a || decide (y ∈ l))

theorem List.elem_iff {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {as : List α} : List.elem a as = true ↔ a ∈ as

@[simp]

theorem List.elem_eq_mem {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (as : List α) : List.elem a as = decide (a ∈ as)

isEmpty

theorem List.isEmpty_iff {α : Type u_1} {l : List α} : l.isEmpty = true ↔ l = []

theorem List.isEmpty_eq_false_iff_exists_mem {α : Type u_1} {xs : List α} : xs.isEmpty = false ↔ ∃ (x : α), x ∈ xs

theorem List.isEmpty_iff_length_eq_zero {α : Type u_1} {l : List α} : l.isEmpty = true ↔ l.length = 0

@[simp]

theorem List.isEmpty_eq_true {α : Type u_1} {l : List α} : l.isEmpty = true ↔ l = []

@[simp]

theorem List.isEmpty_eq_false {α : Type u_1} {l : List α} : l.isEmpty = false ↔ l ≠ []

any / all

theorem List.any_beq {α : Type u_1} {a : α} [BEq α] [LawfulBEq α] {l : List α} : (l.any fun (x : α) => a == x) = true ↔ a ∈ l

theorem List.any_beq' {α : Type u_1} {a : α} [BEq α] [LawfulBEq α] {l : List α} : (l.any fun (x : α) => x == a) = true ↔ a ∈ l

theorem List.all_bne {α : Type u_1} {a : α} [BEq α] [LawfulBEq α] {l : List α} : (l.all fun (x : α) => a != x) = true ↔ ¬a ∈ l

theorem List.all_bne' {α : Type u_1} {a : α} [BEq α] [LawfulBEq α] {l : List α} : (l.all fun (x : α) => x != a) = true ↔ ¬a ∈ l

theorem List.any_eq {α : Type u_1} {p : α → Bool} {l : List α} : l.any p = decide (∃ (x : α), x ∈ l ∧ p x = true)

theorem List.all_eq {α : Type u_1} {p : α → Bool} {l : List α} : l.all p = decide (∀ (x : α), x ∈ l → p x = true)

theorem List.decide_exists_mem {α : Type u_1} {l : List α} {p : α → Prop} [DecidablePred p] : decide (∃ (x : α), x ∈ l ∧ p x) = l.any fun (b : α) => decide (p b)

theorem List.decide_forall_mem {α : Type u_1} {l : List α} {p : α → Prop} [DecidablePred p] : decide (∀ (x : α), x ∈ l → p x) = l.all fun (b : α) => decide (p b)

@[simp]

theorem List.any_eq_true {α : Type u_1} {p : α → Bool} {l : List α} : l.any p = true ↔ ∃ (x : α), x ∈ l ∧ p x = true

@[simp]

theorem List.all_eq_true {α : Type u_1} {p : α → Bool} {l : List α} : l.all p = true ↔ ∀ (x : α), x ∈ l → p x = true

@[simp]

theorem List.any_eq_false {α : Type u_1} {p : α → Bool} {l : List α} : l.any p = false ↔ ∀ (x : α), x ∈ l → ¬p x = true

@[simp]

theorem List.all_eq_false {α : Type u_1} {p : α → Bool} {l : List α} : l.all p = false ↔ ∃ (x : α), x ∈ l ∧ ¬p x = true

set

@[simp]

theorem List.set_nil {α : Type u_1} (n : Nat) (a : α) : [].set n a = []

@[simp]

theorem List.set_cons_zero {α : Type u_1} (x : α) (xs : List α) (a : α) : (x :: xs).set 0 a = a :: xs

@[simp]

theorem List.set_cons_succ {α : Type u_1} (x : α) (xs : List α) (n : Nat) (a : α) : (x :: xs).set (n + 1) a = x :: xs.set n a

@[simp]

theorem List.getElem_set_self {α : Type u_1} {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) : (l.set i a)[i] = a

@[reducible, inline, deprecated List.getElem_set_self]

abbrev List.getElem_set_eq {α : Type u_1} {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) : (l.set i a)[i] = a

Equations

• @List.getElem_set_eq = @List.getElem_set_self

@[deprecated List.getElem_set_self]

theorem List.get_set_eq {α : Type u_1} {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) : (l.set i a).get ⟨i, h⟩ = a

@[simp]

theorem List.getElem?_set_self {α : Type u_1} {l : List α} {i : Nat} {a : α} (h : i < l.length) : (l.set i a)[i]? = some a

@[reducible, inline, deprecated List.getElem?_set_self]

abbrev List.getElem?_set_eq {α : Type u_1} {l : List α} {i : Nat} {a : α} (h : i < l.length) : (l.set i a)[i]? = some a

Equations

• @List.getElem?_set_eq = @List.getElem?_set_self

theorem List.getElem?_set_self' {α : Type u_1} {l : List α} {i : Nat} {a : α} : (l.set i a)[i]? = Function.const α a <$> l[i]?

This differs from getElem?_set_self by monadically mapping Function.const _ a over the Option returned by l[i]?.

@[simp]

theorem List.getElem_set_ne {α : Type u_1} {l : List α} {i : Nat} {j : Nat} (h : i ≠ j) {a : α} (hj : j < (l.set i a).length) : (l.set i a)[j] = l[j]

@[deprecated List.getElem_set_ne]

theorem List.get_set_ne {α : Type u_1} {l : List α} {i : Nat} {j : Nat} (h : i ≠ j) {a : α} (hj : j < (l.set i a).length) : (l.set i a).get ⟨j, hj⟩ = l.get ⟨j, ⋯⟩

@[simp]

theorem List.getElem?_set_ne {α : Type u_1} {l : List α} {i : Nat} {j : Nat} (h : i ≠ j) {a : α} : (l.set i a)[j]? = l[j]?

theorem List.getElem_set {α : Type u_1} {l : List α} {m : Nat} {n : Nat} {a : α} (h : n < (l.set m a).length) : (l.set m a)[n] = if m = n then a else l[n]

@[deprecated List.getElem_set]

theorem List.get_set {α : Type u_1} {l : List α} {m : Nat} {n : Nat} {a : α} (h : n < (l.set m a).length) : (l.set m a).get ⟨n, h⟩ = if m = n then a else l.get ⟨n, ⋯⟩

theorem List.getElem?_set {α : Type u_1} {l : List α} {i : Nat} {j : Nat} {a : α} : (l.set i a)[j]? = if i = j then if i < l.length then some a else none else l[j]?

theorem List.getElem?_set' {α : Type u_1} {l : List α} {i : Nat} {j : Nat} {a : α} : (l.set i a)[j]? = if i = j then Function.const α a <$> l[j]? else l[j]?

This differs from getElem?_set by monadically mapping Function.const _ a over the Option returned by l[j]?

theorem List.set_eq_of_length_le {α : Type u_1} {l : List α} {n : Nat} (h : l.length ≤ n) {a : α} : l.set n a = l

@[simp]

theorem List.set_eq_nil_iff {α : Type u_1} {l : List α} (n : Nat) (a : α) : l.set n a = [] ↔ l = []

@[reducible, inline, deprecated List.set_eq_nil_iff]

abbrev List.set_eq_nil {α : Type u_1} {l : List α} (n : Nat) (a : α) : l.set n a = [] ↔ l = []

Equations

• @List.set_eq_nil = @List.set_eq_nil_iff

theorem List.set_comm {α : Type u_1} (a : α) (b : α) {n : Nat} {m : Nat} (l : List α) : n ≠ m → (l.set n a).set m b = (l.set m b).set n a

@[simp]

theorem List.set_set {α : Type u_1} (a : α) (b : α) (l : List α) (n : Nat) : (l.set n a).set n b = l.set n b

theorem List.mem_set {α : Type u_1} (l : List α) (n : Nat) (h : n < l.length) (a : α) : a ∈ l.set n a

theorem List.mem_or_eq_of_mem_set {α : Type u_1} {l : List α} {n : Nat} {a : α} {b : α} : a ∈ l.set n b → a ∈ l ∨ a = b

BEq

@[simp]

theorem List.reflBEq_iff {α : Type u_1} [BEq α] : ReflBEq (List α) ↔ ReflBEq α

@[simp]

theorem List.lawfulBEq_iff {α : Type u_1} [BEq α] : LawfulBEq (List α) ↔ LawfulBEq α

Lexicographic ordering

theorem List.lt_irrefl {α : Type u_1} [LT α] (lt_irrefl : ∀ (x : α), ¬x < x) (l : List α) : ¬l < l

theorem List.lt_trans {α : Type u_1} [LT α] [DecidableRel LT.lt] (lt_trans : ∀ {x y z : α}, x < y → y < z → x < z) (le_trans : ∀ {x y z : α}, ¬x < y → ¬y < z → ¬x < z) {l₁ : List α} {l₂ : List α} {l₃ : List α} (h₁ : l₁ < l₂) (h₂ : l₂ < l₃) : l₁ < l₃

theorem List.lt_antisymm {α : Type u_1} [LT α] (lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y) {l₁ : List α} {l₂ : List α} (h₁ : ¬l₁ < l₂) (h₂ : ¬l₂ < l₁) : l₁ = l₂

foldlM and foldrM

@[simp]

theorem List.foldlM_reverse {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (l : List α) (f : β → α → m β) (b : β) : List.foldlM f b l.reverse = List.foldrM (fun (x : α) (y : β) => f y x) b l

@[simp]

theorem List.foldlM_append {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] [LawfulMonad m] (f : β → α → m β) (b : β) (l : List α) (l' : List α) : List.foldlM f b (l ++ l') = do let init ← List.foldlM f b l List.foldlM f init l'

@[simp]

theorem List.foldrM_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (a : α) (l : List α) (f : α → β → m β) (b : β) : List.foldrM f b (a :: l) = List.foldrM f b l >>= f a

theorem List.foldl_eq_foldlM {β : Type u_1} {α : Type u_2} (f : β → α → β) (b : β) (l : List α) : List.foldl f b l = List.foldlM f b l

theorem List.foldr_eq_foldrM {α : Type u_1} {β : Type u_2} (f : α → β → β) (b : β) (l : List α) : List.foldr f b l = List.foldrM f b l

foldl and foldr

@[simp]

theorem List.foldr_cons_eq_append {α : Type u_1} {l' : List α} (l : List α) : List.foldr List.cons l' l = l ++ l'

@[reducible, inline, deprecated List.foldr_cons_eq_append]

abbrev List.foldr_self_append {α : Type u_1} {l' : List α} (l : List α) : List.foldr List.cons l' l = l ++ l'

Equations

• @List.foldr_self_append = @List.foldr_cons_eq_append

@[simp]

theorem List.foldl_flip_cons_eq_append {α : Type u_1} {l' : List α} (l : List α) : List.foldl (fun (x : List α) (y : α) => y :: x) l' l = l.reverse ++ l'

theorem List.foldr_cons_nil {α : Type u_1} (l : List α) : List.foldr List.cons [] l = l

@[reducible, inline, deprecated List.foldr_cons_nil]

abbrev List.foldr_self {α : Type u_1} (l : List α) : List.foldr List.cons [] l = l

Equations

• @List.foldr_self = @List.foldr_cons_nil

theorem List.foldl_map {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} (f : β₁ → β₂) (g : α → β₂ → α) (l : List β₁) (init : α) : List.foldl g init (List.map f l) = List.foldl (fun (x : α) (y : β₁) => g x (f y)) init l

theorem List.foldr_map {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁ → α₂) (g : α₂ → β → β) (l : List α₁) (init : β) : List.foldr g init (List.map f l) = List.foldr (fun (x : α₁) (y : β) => g (f x) y) init l

theorem List.foldl_map' {α : Type u} {β : Type u} (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α) (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : List.foldl f' (g a) (List.map g l) = g (List.foldl f a l)

theorem List.foldr_map' {α : Type u} {β : Type u} (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α) (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : List.foldr f' (g a) (List.map g l) = g (List.foldr f a l)

theorem List.foldl_assoc {α : Type u_1} {op : α → α → α} [ha : Std.Associative op] {l : List α} {a₁ : α} {a₂ : α} : List.foldl op (op a₁ a₂) l = op a₁ (List.foldl op a₂ l)

theorem List.foldr_assoc {α : Type u_1} {op : α → α → α} [ha : Std.Associative op] {l : List α} {a₁ : α} {a₂ : α} : List.foldr op (op a₁ a₂) l = op (List.foldr op a₁ l) a₂

theorem List.foldl_hom {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (l : List β) (init : α₁) (H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)) : List.foldl g₂ (f init) l = f (List.foldl g₁ init l)

theorem List.foldr_hom {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ : α → β₂ → β₂) (l : List α) (init : β₁) (H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)) : List.foldr g₂ (f init) l = f (List.foldr g₁ init l)

def List.foldlRecOn {β : Type u_1} {α : Type u_2} {motive : β → Sort u_3} (l : List α) (op : β → α → β) (b : β) : motive b → ((b : β) → motive b → (a : α) → a ∈ l → motive (op b a)) → motive (List.foldl op b l)

Prove a proposition about the result of List.foldl, by proving it for the initial data, and the implication that the operation applied to any element of the list preserves the property.

The motive can take values in Sort _, so this may be used to construct data, as well as to prove propositions.

Equations

• List.foldlRecOn [] x✝² x✝¹ x✝ x = x✝
• List.foldlRecOn (hd :: tl) x✝² x✝¹ x✝ x = List.foldlRecOn tl x✝² (x✝² x✝¹ hd) (x x✝¹ x✝ hd ⋯) fun (y : β) (hy : motive y) (x_1 : α) (hx : x_1 ∈ tl) => x y hy x_1 ⋯

@[simp]

theorem List.foldlRecOn_nil {β : Type u_1} {b : β} {α : Type u_2} {op : β → α → β} {motive : β → Sort u_3} (hb : motive b) (hl : (b : β) → motive b → (a : α) → a ∈ [] → motive (op b a)) : List.foldlRecOn [] op b hb hl = hb

@[simp]

theorem List.foldlRecOn_cons {β : Type u_1} {b : β} {α : Type u_2} {x : α} {l : List α} {op : β → α → β} {motive : β → Sort u_3} (hb : motive b) (hl : (b : β) → motive b → (a : α) → a ∈ x :: l → motive (op b a)) : List.foldlRecOn (x :: l) op b hb hl = List.foldlRecOn l op (op b x) (hl b hb x ⋯) fun (b : β) (c : motive b) (a : α) (m : a ∈ l) => hl b c a ⋯

def List.foldrRecOn {β : Type u_1} {α : Type u_2} {motive : β → Sort u_3} (l : List α) (op : α → β → β) (b : β) : motive b → ((b : β) → motive b → (a : α) → a ∈ l → motive (op a b)) → motive (List.foldr op b l)

Prove a proposition about the result of List.foldr, by proving it for the initial data, and the implication that the operation applied to any element of the list preserves the property.

The motive can take values in Sort _, so this may be used to construct data, as well as to prove propositions.

Equations

• List.foldrRecOn [] x✝² x✝¹ x✝ x = x✝
• List.foldrRecOn (x_5 :: l) x✝² x✝¹ x✝ x = x (List.foldr x✝² x✝¹ l) (List.foldrRecOn l x✝² x✝¹ x✝ fun (b : β) (c : motive b) (a : α) (m : a ∈ l) => x b c a ⋯) x_5 ⋯

@[simp]

theorem List.foldrRecOn_nil {β : Type u_1} {b : β} {α : Type u_2} {op : α → β → β} {motive : β → Sort u_3} (hb : motive b) (hl : (b : β) → motive b → (a : α) → a ∈ [] → motive (op a b)) : List.foldrRecOn [] op b hb hl = hb

@[simp]

theorem List.foldrRecOn_cons {β : Type u_1} {b : β} {α : Type u_2} {x : α} {l : List α} {op : α → β → β} {motive : β → Sort u_3} (hb : motive b) (hl : (b : β) → motive b → (a : α) → a ∈ x :: l → motive (op a b)) : List.foldrRecOn (x :: l) op b hb hl = hl (List.foldr op b l) (List.foldrRecOn l op b hb fun (b : β) (c : motive b) (a : α) (m : a ∈ l) => hl b c a ⋯) x ⋯

theorem List.foldl_rel {α : Type u_1} {β : Type u_2} {l : List α} {f : β → α → β} {g : β → α → β} {a : β} {b : β} (r : β → β → Prop) (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) : r (List.foldl (fun (acc : β) (a : α) => f acc a) a l) (List.foldl (fun (acc : β) (a : α) => g acc a) b l)

We can prove that two folds over the same list are related (by some arbitrary relation) if we know that the initial elements are related and the folding function, for each element of the list, preserves the relation.

theorem List.foldr_rel {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β → β} {g : α → β → β} {a : β} {b : β} (r : β → β → Prop) (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) : r (List.foldr (fun (a : α) (acc : β) => f a acc) a l) (List.foldr (fun (a : α) (acc : β) => g a acc) b l)

We can prove that two folds over the same list are related (by some arbitrary relation) if we know that the initial elements are related and the folding function, for each element of the list, preserves the relation.

getLast

theorem List.getLast_eq_getElem {α : Type u_1} (l : List α) (h : l ≠ []) : l.getLast h = l[l.length - 1]

@[deprecated List.getLast_eq_getElem]

theorem List.getLast_eq_get {α : Type u_1} (l : List α) (h : l ≠ []) : l.getLast h = l.get ⟨l.length - 1, ⋯⟩

theorem List.getLast_cons {α : Type u_1} {a : α} {l : List α} (h : l ≠ []) : (a :: l).getLast ⋯ = l.getLast h

theorem List.getLast_eq_getLastD {α : Type u_1} (a : α) (l : List α) (h : a :: l ≠ []) : (a :: l).getLast h = l.getLastD a

@[simp]

theorem List.getLastD_eq_getLast? {α : Type u_1} (a : α) (l : List α) : l.getLastD a = l.getLast?.getD a

@[simp]

theorem List.getLast_singleton {α : Type u_1} (a : α) (h : [a] ≠ []) : [a].getLast h = a

theorem List.getLast!_cons {α : Type u_1} {a : α} {l : List α} [Inhabited α] : (a :: l).getLast! = l.getLastD a

@[simp]

theorem List.getLast_mem {α : Type u_1} {l : List α} (h : l ≠ []) : l.getLast h ∈ l

theorem List.getLast_mem_getLast? {α : Type u_1} {l : List α} (h : l ≠ []) : l.getLast h ∈ l.getLast?

theorem List.getLastD_mem_cons {α : Type u_1} (l : List α) (a : α) : l.getLastD a ∈ a :: l

theorem List.getElem_cons_length {α : Type u_1} (x : α) (xs : List α) (n : Nat) (h : n = xs.length) : (x :: xs)[n] = (x :: xs).getLast ⋯

@[deprecated List.getElem_cons_length]

theorem List.get_cons_length {α : Type u_1} (x : α) (xs : List α) (n : Nat) (h : n = xs.length) : (x :: xs).get ⟨n, ⋯⟩ = (x :: xs).getLast ⋯

getLast?

@[simp]

theorem List.getLast?_singleton {α : Type u_1} (a : α) : [a].getLast? = some a

theorem List.getLast!_of_getLast? {α : Type u_1} {a : α} [Inhabited α] {l : List α} : l.getLast? = some a → l.getLast! = a

theorem List.getLast?_eq_getLast {α : Type u_1} (l : List α) (h : l ≠ []) : l.getLast? = some (l.getLast h)

theorem List.getLast?_eq_getElem? {α : Type u_1} (l : List α) : l.getLast? = l[l.length - 1]?

theorem List.getLast_eq_iff_getLast?_eq_some {α : Type u_1} {a : α} {xs : List α} (h : xs ≠ []) : xs.getLast h = a ↔ xs.getLast? = some a

theorem List.getLast?_cons {α : Type u_1} {l : List α} {a : α} : (a :: l).getLast? = some (l.getLast?.getD a)

@[simp]

theorem List.getLast?_cons_cons : ∀ {α : Type u_1} {a b : α} {l : List α}, (a :: b :: l).getLast? = (b :: l).getLast?

@[deprecated List.getLast?_eq_getElem?]

theorem List.getLast?_eq_get? {α : Type u_1} (l : List α) : l.getLast? = l.get? (l.length - 1)

theorem List.getLast?_concat {α : Type u_1} {a : α} (l : List α) : (l ++ [a]).getLast? = some a

theorem List.getLastD_concat {α : Type u_1} (a : α) (b : α) (l : List α) : (l ++ [b]).getLastD a = b

Head and tail

head

theorem List.head?_singleton {α : Type u_1} (a : α) : [a].head? = some a

theorem List.head!_of_head? {α : Type u_1} {a : α} [Inhabited α] {l : List α} : l.head? = some a → l.head! = a

theorem List.head?_eq_head {α : Type u_1} {l : List α} (h : l ≠ []) : l.head? = some (l.head h)

theorem List.head?_eq_getElem? {α : Type u_1} (l : List α) : l.head? = l[0]?

theorem List.head_eq_getElem {α : Type u_1} (l : List α) (h : l ≠ []) : l.head h = l[0]

theorem List.head_eq_iff_head?_eq_some {α : Type u_1} {a : α} {xs : List α} (h : xs ≠ []) : xs.head h = a ↔ xs.head? = some a

@[simp]

theorem List.head?_eq_none_iff : ∀ {α : Type u_1} {l : List α}, l.head? = none ↔ l = []

theorem List.head?_eq_some_iff {α : Type u_1} {xs : List α} {a : α} : xs.head? = some a ↔ ∃ (ys : List α), xs = a :: ys

@[simp]

theorem List.head?_isSome : ∀ {α : Type u_1} {l : List α}, l.head?.isSome = true ↔ l ≠ []

@[simp]

theorem List.head_mem {α : Type u_1} {l : List α} (h : l ≠ []) : l.head h ∈ l

theorem List.mem_of_mem_head? {α : Type u_1} {l : List α} {a : α} : a ∈ l.head? → a ∈ l

theorem List.head_mem_head? {α : Type u_1} {l : List α} (h : l ≠ []) : l.head h ∈ l.head?

theorem List.head?_concat {α : Type u_1} {l : List α} {a : α} : (l ++ [a]).head? = some (l.head?.getD a)

theorem List.head?_concat_concat : ∀ {α : Type u_1} {l : List α} {a b : α}, (l ++ [a, b]).head? = (l ++ [a]).head?

headD

@[simp]

theorem List.headD_eq_head?_getD {α : Type u_1} {a : α} {l : List α} : l.headD a = l.head?.getD a

simp unfolds headD in terms of head? and Option.getD.

tailD

@[simp]

theorem List.tailD_eq_tail? {α : Type u_1} (l : List α) (l' : List α) : l.tailD l' = l.tail?.getD l'

simp unfolds tailD in terms of tail? and Option.getD.

tail

@[simp]

theorem List.length_tail {α : Type u_1} (l : List α) : l.tail.length = l.length - 1

theorem List.tail_eq_tailD {α : Type u_1} (l : List α) : l.tail = l.tailD []

theorem List.tail_eq_tail? {α : Type u_1} (l : List α) : l.tail = l.tail?.getD []

theorem List.mem_of_mem_tail {α : Type u_1} {a : α} {l : List α} (h : a ∈ l.tail) : a ∈ l

theorem List.ne_nil_of_tail_ne_nil {α : Type u_1} {l : List α} : l.tail ≠ [] → l ≠ []

@[simp]

theorem List.getElem_tail {α : Type u_1} (l : List α) (i : Nat) (h : i < l.tail.length) : l.tail[i] = l[i + 1]

@[simp]

theorem List.getElem?_tail {α : Type u_1} (l : List α) (i : Nat) : l.tail[i]? = l[i + 1]?

@[simp]

theorem List.set_tail {α : Type u_1} (l : List α) (i : Nat) (a : α) : l.tail.set i a = (l.set (i + 1) a).tail

theorem List.one_lt_length_of_tail_ne_nil {α : Type u_1} {l : List α} (h : l.tail ≠ []) : 1 < l.length

@[simp]

theorem List.head_tail {α : Type u_1} (l : List α) (h : l.tail ≠ []) : l.tail.head h = l[1]

@[simp]

theorem List.head?_tail {α : Type u_1} (l : List α) : l.tail.head? = l[1]?

@[simp]

theorem List.getLast_tail {α : Type u_1} (l : List α) (h : l.tail ≠ []) : l.tail.getLast h = l.getLast ⋯

theorem List.getLast?_tail {α : Type u_1} (l : List α) : l.tail.getLast? = if l.length = 1 then none else l.getLast?

Basic operations

map

@[simp]

theorem List.map_id_fun {α : Type u_1} : List.map id = id

@[simp]

theorem List.map_id_fun' {α : Type u_1} : (List.map fun (a : α) => a) = id

map_id_fun' differs from map_id_fun by representing the identity function as a lambda, rather than id.

theorem List.map_id {α : Type u_1} (l : List α) : List.map id l = l

theorem List.map_id' {α : Type u_1} (l : List α) : List.map (fun (a : α) => a) l = l

map_id' differs from map_id by representing the identity function as a lambda, rather than id.

theorem List.map_id'' {α : Type u_1} {f : α → α} (h : ∀ (x : α), f x = x) (l : List α) : List.map f l = l

Variant of map_id, with a side condition that the function is pointwise the identity.

theorem List.map_singleton {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : List.map f [a] = [f a]

@[simp]

theorem List.length_map {α : Type u_1} {β : Type u_2} (as : List α) (f : α → β) : (List.map f as).length = as.length

@[simp]

theorem List.getElem?_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) (n : Nat) : (List.map f l)[n]? = Option.map f l[n]?

@[deprecated List.getElem?_map]

theorem List.get?_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) (n : Nat) : (List.map f l).get? n = Option.map f (l.get? n)

@[simp]

theorem List.getElem_map {α : Type u_1} {β : Type u_2} (f : α → β) {l : List α} {n : Nat} {h : n < (List.map f l).length} : (List.map f l)[n] = f l[n]

@[deprecated List.getElem_map]

theorem List.get_map {α : Type u_1} {β : Type u_2} (f : α → β) {l : List α} {n : Fin (List.map f l).length} : (List.map f l).get n = f (l.get ⟨↑n, ⋯⟩)

@[simp]

theorem List.mem_map {α : Type u_1} {β : Type u_2} {b : β} {f : α → β} {l : List α} : b ∈ List.map f l ↔ ∃ (a : α), a ∈ l ∧ f a = b

theorem List.exists_of_mem_map : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {l : List α} {b : α_1}, b ∈ List.map f l → ∃ (a : α), a ∈ l ∧ f a = b

theorem List.mem_map_of_mem {α : Type u_1} {β : Type u_2} {l : List α} {a : α} (f : α → β) (h : a ∈ l) : f a ∈ List.map f l

theorem List.forall_mem_map {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {P : β → Prop} : (∀ (i : β), i ∈ List.map f l → P i) ↔ ∀ (j : α), j ∈ l → P (f j)

@[reducible, inline, deprecated List.forall_mem_map]

abbrev List.forall_mem_map_iff {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {P : β → Prop} : (∀ (i : β), i ∈ List.map f l → P i) ↔ ∀ (j : α), j ∈ l → P (f j)

Equations

• @List.forall_mem_map_iff = @List.forall_mem_map

@[simp]

theorem List.map_inj_left {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} {g : α → β} : List.map f l = List.map g l ↔ ∀ (a : α), a ∈ l → f a = g a

theorem List.map_congr_left : ∀ {α : Type u_1} {l : List α} {α_1 : Type u_2} {f g : α → α_1}, (∀ (a : α), a ∈ l → f a = g a) → List.map f l = List.map g l

theorem List.map_inj : ∀ {α : Type u_1} {α_1 : Type u_2} {f g : α → α_1}, List.map f = List.map g ↔ f = g

@[simp]

theorem List.map_eq_nil_iff {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : List.map f l = [] ↔ l = []

@[reducible, inline, deprecated List.map_eq_nil_iff]

abbrev List.map_eq_nil {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : List.map f l = [] ↔ l = []

Equations

• @List.map_eq_nil = @List.map_eq_nil_iff

theorem List.eq_nil_of_map_eq_nil {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} (h : List.map f l = []) : l = []

theorem List.map_eq_cons_iff {α : Type u_1} {β : Type u_2} {b : β} {l₂ : List β} {f : α → β} {l : List α} : List.map f l = b :: l₂ ↔ ∃ (a : α), ∃ (l₁ : List α), l = a :: l₁ ∧ f a = b ∧ List.map f l₁ = l₂

@[reducible, inline, deprecated List.map_eq_cons_iff]

abbrev List.map_eq_cons {α : Type u_1} {β : Type u_2} {b : β} {l₂ : List β} {f : α → β} {l : List α} : List.map f l = b :: l₂ ↔ ∃ (a : α), ∃ (l₁ : List α), l = a :: l₁ ∧ f a = b ∧ List.map f l₁ = l₂

Equations

• @List.map_eq_cons = @List.map_eq_cons_iff

theorem List.map_eq_cons_iff' {α : Type u_1} {β : Type u_2} {b : β} {l₂ : List β} {f : α → β} {l : List α} : List.map f l = b :: l₂ ↔ Option.map f l.head? = some b ∧ Option.map (List.map f) l.tail? = some l₂

@[reducible, inline, deprecated List.map_eq_cons']

abbrev List.map_eq_cons' {α : Type u_1} {β : Type u_2} {b : β} {l₂ : List β} {f : α → β} {l : List α} : List.map f l = b :: l₂ ↔ Option.map f l.head? = some b ∧ Option.map (List.map f) l.tail? = some l₂

Equations

• @List.map_eq_cons' = @List.map_eq_cons_iff'

theorem List.map_eq_map_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {l : List α} {g : α → α_1}, List.map f l = List.map g l ↔ ∀ (a : α), a ∈ l → f a = g a

theorem List.map_eq_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {l : List α} {l' : List α_1}, List.map f l = l' ↔ ∀ (i : Nat), l'[i]? = Option.map f l[i]?

theorem List.map_eq_foldr {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : List.map f l = List.foldr (fun (a : α) (bs : List β) => f a :: bs) [] l

@[simp]

theorem List.map_set {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {i : Nat} {a : α} : List.map f (l.set i a) = (List.map f l).set i (f a)

@[deprecated]

theorem List.set_map {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {n : Nat} {a : α} : (List.map f l).set n (f a) = List.map f (l.set n a)

@[simp]

theorem List.head_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) (w : List.map f l ≠ []) : (List.map f l).head w = f (l.head ⋯)

@[simp]

theorem List.head?_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : (List.map f l).head? = Option.map f l.head?

@[simp]

theorem List.map_tail? {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : Option.map (List.map f) l.tail? = (List.map f l).tail?

@[simp]

theorem List.map_tail {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : List.map f l.tail = (List.map f l).tail

theorem List.headD_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) (a : α) : (List.map f l).headD (f a) = f (l.headD a)

theorem List.tailD_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) (l' : List α) : (List.map f l).tailD (List.map f l') = List.map f (l.tailD l')

@[simp]

theorem List.getLast_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) (h : List.map f l ≠ []) : (List.map f l).getLast h = f (l.getLast ⋯)

@[simp]

theorem List.getLast?_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : (List.map f l).getLast? = Option.map f l.getLast?

theorem List.getLastD_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) (a : α) : (List.map f l).getLastD (f a) = f (l.getLastD a)

@[simp]

theorem List.map_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} (g : β → γ) (f : α → β) (l : List α) : List.map g (List.map f l) = List.map (g ∘ f) l

filter

@[simp]

theorem List.filter_cons_of_pos {α : Type u_1} {p : α → Bool} {a : α} {l : List α} (pa : p a = true) : List.filter p (a :: l) = a :: List.filter p l

@[simp]

theorem List.filter_cons_of_neg {α : Type u_1} {p : α → Bool} {a : α} {l : List α} (pa : ¬p a = true) : List.filter p (a :: l) = List.filter p l

theorem List.filter_cons {α : Type u_1} {x : α} {xs : List α} {p : α → Bool} : List.filter p (x :: xs) = if p x = true then x :: List.filter p xs else List.filter p xs

theorem List.length_filter_le {α : Type u_1} (p : α → Bool) (l : List α) : (List.filter p l).length ≤ l.length

@[simp]

theorem List.filter_eq_self : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.filter p l = l ↔ ∀ (a : α), a ∈ l → p a = true

@[simp]

theorem List.filter_length_eq_length : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, (List.filter p l).length = l.length ↔ ∀ (a : α), a ∈ l → p a = true

@[simp]

theorem List.mem_filter : ∀ {α : Type u_1} {p : α → Bool} {as : List α} {x : α}, x ∈ List.filter p as ↔ x ∈ as ∧ p x = true

@[simp]

theorem List.filter_eq_nil_iff : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.filter p l = [] ↔ ∀ (a : α), a ∈ l → ¬p a = true

@[reducible, inline, deprecated List.filter_eq_nil_iff]

abbrev List.filter_eq_nil : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.filter p l = [] ↔ ∀ (a : α), a ∈ l → ¬p a = true

Equations

• @List.filter_eq_nil = @List.filter_eq_nil_iff

theorem List.forall_mem_filter {α : Type u_1} {l : List α} {p : α → Bool} {P : α → Prop} : (∀ (i : α), i ∈ List.filter p l → P i) ↔ ∀ (j : α), j ∈ l → p j = true → P j

@[reducible, inline, deprecated List.forall_mem_filter]

abbrev List.forall_mem_filter_iff {α : Type u_1} {l : List α} {p : α → Bool} {P : α → Prop} : (∀ (i : α), i ∈ List.filter p l → P i) ↔ ∀ (j : α), j ∈ l → p j = true → P j

Equations

• @List.forall_mem_filter_iff = @List.forall_mem_filter

@[simp]

theorem List.filter_filter : ∀ {α : Type u_1} {p : α → Bool} (q : α → Bool) (l : List α), List.filter p (List.filter q l) = List.filter (fun (a : α) => p a && q a) l

theorem List.filter_map {β : Type u_1} {α : Type u_2} {p : α → Bool} (f : β → α) (l : List β) : List.filter p (List.map f l) = List.map f (List.filter (p ∘ f) l)

@[reducible, inline, deprecated List.filter_map]

abbrev List.map_filter {β : Type u_1} {α : Type u_2} {p : α → Bool} (f : β → α) (l : List β) : List.filter p (List.map f l) = List.map f (List.filter (p ∘ f) l)

Equations

• @List.map_filter = @List.filter_map

theorem List.map_filter_eq_foldr {α : Type u_1} {β : Type u_2} (f : α → β) (p : α → Bool) (as : List α) : List.map f (List.filter p as) = List.foldr (fun (a : α) (bs : List β) => bif p a then f a :: bs else bs) [] as

@[simp]

theorem List.filter_append {α : Type u_1} {p : α → Bool} (l₁ : List α) (l₂ : List α) : List.filter p (l₁ ++ l₂) = List.filter p l₁ ++ List.filter p l₂

theorem List.filter_eq_cons_iff : ∀ {α : Type u_1} {p : α → Bool} {l : List α} {a : α} {as : List α}, List.filter p l = a :: as ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ List.filter p l₂ = as

@[reducible, inline, deprecated List.filter_eq_cons_iff]

abbrev List.filter_eq_cons : ∀ {α : Type u_1} {p : α → Bool} {l : List α} {a : α} {as : List α}, List.filter p l = a :: as ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ List.filter p l₂ = as

Equations

• @List.filter_eq_cons = @List.filter_eq_cons_iff

theorem List.filter_congr {α : Type u_1} {p : α → Bool} {q : α → Bool} {l : List α} : (∀ (x : α), x ∈ l → p x = q x) → List.filter p l = List.filter q l

@[reducible, inline, deprecated List.filter_congr]

abbrev List.filter_congr' {α : Type u_1} {p : α → Bool} {q : α → Bool} {l : List α} : (∀ (x : α), x ∈ l → p x = q x) → List.filter p l = List.filter q l

Equations

• @List.filter_congr' = @List.filter_congr

theorem List.head_filter_of_pos {α : Type u_1} {p : α → Bool} {l : List α} (w : l ≠ []) (h : p (l.head w) = true) : (List.filter p l).head ⋯ = l.head w

@[simp]

theorem List.filter_sublist {α : Type u_1} {p : α → Bool} (l : List α) : (List.filter p l).Sublist l

filterMap

@[simp]

theorem List.filterMap_cons_none {α : Type u_1} {β : Type u_2} {f : α → Option β} {a : α} {l : List α} (h : f a = none) : List.filterMap f (a :: l) = List.filterMap f l

@[simp]

theorem List.filterMap_cons_some {α : Type u_1} {β : Type u_2} {f : α → Option β} {a : α} {l : List α} {b : β} (h : f a = some b) : List.filterMap f (a :: l) = b :: List.filterMap f l

@[simp]

theorem List.filterMap_eq_map {α : Type u_1} {β : Type u_2} (f : α → β) : List.filterMap (some ∘ f) = List.map f

@[simp]

theorem List.filterMap_some_fun {α : Type u_1} : List.filterMap some = id

theorem List.filterMap_some {α : Type u_1} (l : List α) : List.filterMap some l = l

theorem List.map_filterMap_some_eq_filter_map_isSome {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) : List.map some (List.filterMap f l) = List.filter (fun (b : Option β) => b.isSome) (List.map f l)

theorem List.length_filterMap_le {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) : (List.filterMap f l).length ≤ l.length

@[simp]

theorem List.filterMap_length_eq_length : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {l : List α}, (List.filterMap f l).length = l.length ↔ ∀ (a : α), a ∈ l → (f a).isSome = true

@[simp]

theorem List.filterMap_eq_filter {α : Type u_1} (p : α → Bool) : List.filterMap (Option.guard fun (x : α) => p x = true) = List.filter p

theorem List.filterMap_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β) (g : β → Option γ) (l : List α) : List.filterMap g (List.filterMap f l) = List.filterMap (fun (x : α) => (f x).bind g) l

theorem List.map_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β) (g : β → γ) (l : List α) : List.map g (List.filterMap f l) = List.filterMap (fun (x : α) => Option.map g (f x)) l

@[simp]

theorem List.filterMap_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → Option γ) (l : List α) : List.filterMap g (List.map f l) = List.filterMap (g ∘ f) l

theorem List.filter_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (p : β → Bool) (l : List α) : List.filter p (List.filterMap f l) = List.filterMap (fun (x : α) => Option.filter p (f x)) l

theorem List.filterMap_filter {α : Type u_1} {β : Type u_2} (p : α → Bool) (f : α → Option β) (l : List α) : List.filterMap f (List.filter p l) = List.filterMap (fun (x : α) => if p x = true then f x else none) l

@[simp]

theorem List.mem_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} {b : β} : b ∈ List.filterMap f l ↔ ∃ (a : α), a ∈ l ∧ f a = some b

theorem List.forall_mem_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} {P : β → Prop} : (∀ (i : β), i ∈ List.filterMap f l → P i) ↔ ∀ (j : α), j ∈ l → ∀ (b : β), f j = some b → P b

@[reducible, inline, deprecated List.forall_mem_filterMap]

abbrev List.forall_mem_filterMap_iff {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} {P : β → Prop} : (∀ (i : β), i ∈ List.filterMap f l → P i) ↔ ∀ (j : α), j ∈ l → ∀ (b : β), f j = some b → P b

Equations

• @List.forall_mem_filterMap_iff = @List.forall_mem_filterMap

@[simp]

theorem List.filterMap_append {α : Type u_1} {β : Type u_2} (l : List α) (l' : List α) (f : α → Option β) : List.filterMap f (l ++ l') = List.filterMap f l ++ List.filterMap f l'

theorem List.map_filterMap_of_inv {α : Type u_1} {β : Type u_2} (f : α → Option β) (g : β → α) (H : ∀ (x : α), Option.map g (f x) = some x) (l : List α) : List.map g (List.filterMap f l) = l

theorem List.head_filterMap_of_eq_some {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} (w : l ≠ []) {b : β} (h : f (l.head w) = some b) : (List.filterMap f l).head ⋯ = b

theorem List.forall_none_of_filterMap_eq_nil : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {xs : List α}, List.filterMap f xs = [] → ∀ (x : α), x ∈ xs → f x = none

@[simp]

theorem List.filterMap_eq_nil_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {l : List α}, List.filterMap f l = [] ↔ ∀ (a : α), a ∈ l → f a = none

@[reducible, inline, deprecated List.filterMap_eq_nil_iff]

abbrev List.filterMap_eq_nil : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {l : List α}, List.filterMap f l = [] ↔ ∀ (a : α), a ∈ l → f a = none

Equations

• @List.filterMap_eq_nil = @List.filterMap_eq_nil_iff

theorem List.filterMap_eq_cons_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {l : List α} {b : α_1} {bs : List α_1}, List.filterMap f l = b :: bs ↔ ∃ (l₁ : List α), ∃ (a : α), ∃ (l₂ : List α), l = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → f x = none) ∧ f a = some b ∧ List.filterMap f l₂ = bs

@[reducible, inline, deprecated List.filterMap_eq_cons_iff]

abbrev List.filterMap_eq_cons : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {l : List α} {b : α_1} {bs : List α_1}, List.filterMap f l = b :: bs ↔ ∃ (l₁ : List α), ∃ (a : α), ∃ (l₂ : List α), l = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → f x = none) ∧ f a = some b ∧ List.filterMap f l₂ = bs

Equations

• @List.filterMap_eq_cons = @List.filterMap_eq_cons_iff

append

@[simp]

theorem List.nil_append_fun {α : Type u_1} : (fun (x : List α) => [] ++ x) = id

@[simp]

theorem List.cons_append_fun {α : Type u_1} (a : α) (as : List α) : (fun (bs : List α) => a :: as ++ bs) = fun (bs : List α) => a :: (as ++ bs)

theorem List.getElem_append {α : Type u_1} {l₁ : List α} {l₂ : List α} (n : Nat) (h : n < (l₁ ++ l₂).length) : (l₁ ++ l₂)[n] = if h' : n < l₁.length then l₁[n] else l₂[n - l₁.length]

theorem List.getElem?_append_left {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (hn : n < l₁.length) : (l₁ ++ l₂)[n]? = l₁[n]?

theorem List.getElem?_append_right {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} : l₁.length ≤ n → (l₁ ++ l₂)[n]? = l₂[n - l₁.length]?

theorem List.getElem?_append {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} : (l₁ ++ l₂)[n]? = if n < l₁.length then l₁[n]? else l₂[n - l₁.length]?

@[deprecated List.getElem?_append_right]

theorem List.get?_append_right {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h : l₁.length ≤ n) : (l₁ ++ l₂).get? n = l₂.get? (n - l₁.length)

theorem List.getElem_append_left' {α : Type u_1} (l₂ : List α) {l₁ : List α} {n : Nat} (hn : n < l₁.length) : l₁[n] = (l₁ ++ l₂)[n]

Variant of getElem_append_left useful for rewriting from the small list to the big list.

theorem List.getElem_append_right' {α : Type u_1} (l₁ : List α) {l₂ : List α} {n : Nat} (hn : n < l₂.length) : l₂[n] = (l₁ ++ l₂)[n + l₁.length]

Variant of getElem_append_right useful for rewriting from the small list to the big list.

@[deprecated]

theorem List.get_append_right_aux {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h₁ : l₁.length ≤ n) (h₂ : n < (l₁ ++ l₂).length) : n - l₁.length < l₂.length

@[deprecated List.getElem_append_right]

theorem List.get_append_right' {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h₁ : l₁.length ≤ n) (h₂ : n < (l₁ ++ l₂).length) : (l₁ ++ l₂).get ⟨n, h₂⟩ = l₂.get ⟨n - l₁.length, ⋯⟩

theorem List.getElem_of_append {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α} {n : Nat} {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) : l[n] = a

@[deprecated]

theorem List.get_of_append_proof {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α} {n : Nat} {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) : n < l.length

@[deprecated List.getElem_of_append]

theorem List.get_of_append {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α} {n : Nat} {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) : l.get ⟨n, ⋯⟩ = a

theorem List.append_of_mem {α : Type u_1} {a : α} {l : List α} : a ∈ l → ∃ (s : List α), ∃ (t : List α), l = s ++ a :: t

See also eq_append_cons_of_mem, which proves a stronger version in which the initial list must not contain the element.

@[simp]

theorem List.singleton_append : ∀ {α : Type u_1} {x : α} {l : List α}, [x] ++ l = x :: l

theorem List.append_inj {α : Type u_1} {s₁ : List α} {s₂ : List α} {t₁ : List α} {t₂ : List α} : s₁ ++ t₁ = s₂ ++ t₂ → s₁.length = s₂.length → s₁ = s₂ ∧ t₁ = t₂

theorem List.append_inj_right : ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → s₁.length = s₂.length → t₁ = t₂

theorem List.append_inj_left : ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → s₁.length = s₂.length → s₁ = s₂

theorem List.append_inj' : ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → t₁.length = t₂.length → s₁ = s₂ ∧ t₁ = t₂

Variant of append_inj instead requiring equality of the lengths of the second lists.

theorem List.append_inj_right' : ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → t₁.length = t₂.length → t₁ = t₂

Variant of append_inj_right instead requiring equality of the lengths of the second lists.

theorem List.append_inj_left' : ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → t₁.length = t₂.length → s₁ = s₂

Variant of append_inj_left instead requiring equality of the lengths of the second lists.

theorem List.append_right_inj {α : Type u_1} {t₁ : List α} {t₂ : List α} (s : List α) : s ++ t₁ = s ++ t₂ ↔ t₁ = t₂

theorem List.append_left_inj {α : Type u_1} {s₁ : List α} {s₂ : List α} (t : List α) : s₁ ++ t = s₂ ++ t ↔ s₁ = s₂

@[simp]

theorem List.append_left_eq_self {α : Type u_1} {x : List α} {y : List α} : x ++ y = y ↔ x = []

@[simp]

theorem List.self_eq_append_left {α : Type u_1} {x : List α} {y : List α} : y = x ++ y ↔ x = []

@[simp]

theorem List.append_right_eq_self {α : Type u_1} {x : List α} {y : List α} : x ++ y = x ↔ y = []

@[simp]

theorem List.self_eq_append_right {α : Type u_1} {x : List α} {y : List α} : x = x ++ y ↔ y = []

@[simp]

theorem List.append_eq_nil : ∀ {α : Type u_1} {p q : List α}, p ++ q = [] ↔ p = [] ∧ q = []

theorem List.getLast_concat {α : Type u_1} {a : α} (l : List α) : (l ++ [a]).getLast ⋯ = a

@[deprecated List.getElem_append]

theorem List.get_append {α : Type u_1} {l₁ : List α} {l₂ : List α} (n : Nat) (h : n < l₁.length) : (l₁ ++ l₂).get ⟨n, ⋯⟩ = l₁.get ⟨n, h⟩

@[deprecated List.getElem_append_left]

theorem List.get_append_left {α : Type u_1} {i : Nat} (as : List α) (bs : List α) (h : i < as.length) {h' : i < (as ++ bs).length} : (as ++ bs).get ⟨i, h'⟩ = as.get ⟨i, h⟩

@[deprecated List.getElem_append_right]

theorem List.get_append_right {α : Type u_1} {i : Nat} (as : List α) (bs : List α) (h : as.length ≤ i) {h' : i < (as ++ bs).length} {h'' : i - as.length < bs.length} : (as ++ bs).get ⟨i, h'⟩ = bs.get ⟨i - as.length, h''⟩

@[deprecated List.getElem?_append_left]

theorem List.get?_append {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (hn : n < l₁.length) : (l₁ ++ l₂).get? n = l₁.get? n

@[simp]

theorem List.head_append_of_ne_nil {α : Type u_1} {l' : List α} {l : List α} {w₁ : l ++ l' ≠ []} (w₂ : l ≠ []) : (l ++ l').head w₁ = l.head w₂

theorem List.head_append {α : Type u_1} {l₁ : List α} {l₂ : List α} (w : l₁ ++ l₂ ≠ []) : (l₁ ++ l₂).head w = if h : l₁.isEmpty = true then l₂.head ⋯ else l₁.head ⋯

theorem List.head_append_left {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : l₁ ≠ []) : (l₁ ++ l₂).head ⋯ = l₁.head h

theorem List.head_append_right {α : Type u_1} {l₁ : List α} {l₂ : List α} (w : l₁ ++ l₂ ≠ []) (h : l₁ = []) : (l₁ ++ l₂).head w = l₂.head ⋯

@[simp]

theorem List.head?_append {α : Type u_1} {l' : List α} {l : List α} : (l ++ l').head? = l.head?.or l'.head?

theorem List.tail?_append {α : Type u_1} {l : List α} {l' : List α} : (l ++ l').tail? = (Option.map (fun (x : List α) => x ++ l') l.tail?).or l'.tail?

theorem List.tail?_append_of_ne_nil {α : Type u_1} {l : List α} {l' : List α} : l ≠ [] → (l ++ l').tail? = some (l.tail ++ l')

theorem List.tail_append {α : Type u_1} {l : List α} {l' : List α} : (l ++ l').tail = if l.isEmpty = true then l'.tail else l.tail ++ l'

@[simp]

theorem List.tail_append_of_ne_nil {α : Type u_1} {xs : List α} {ys : List α} (h : xs ≠ []) : (xs ++ ys).tail = xs.tail ++ ys

@[reducible, inline, deprecated List.tail_append_of_ne_nil]

abbrev List.tail_append_left {α : Type u_1} {xs : List α} {ys : List α} (h : xs ≠ []) : (xs ++ ys).tail = xs.tail ++ ys

Equations

• @List.tail_append_left = @List.tail_append_of_ne_nil

theorem List.nil_eq_append_iff : ∀ {α : Type u_1} {a b : List α}, [] = a ++ b ↔ a = [] ∧ b = []

@[reducible, inline, deprecated List.nil_eq_append_iff]

abbrev List.nil_eq_append : ∀ {α : Type u_1} {a b : List α}, [] = a ++ b ↔ a = [] ∧ b = []

Equations

• @List.nil_eq_append = @List.nil_eq_append_iff

theorem List.append_ne_nil_of_left_ne_nil {α : Type u_1} {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ []

theorem List.append_ne_nil_of_right_ne_nil {α : Type u_1} {t : List α} (s : List α) : t ≠ [] → s ++ t ≠ []

@[deprecated List.append_ne_nil_of_left_ne_nil]

theorem List.append_ne_nil_of_ne_nil_left {α : Type u_1} {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ []

@[deprecated List.append_ne_nil_of_right_ne_nil]

theorem List.append_ne_nil_of_ne_nil_right {α : Type u_1} {t : List α} (s : List α) : t ≠ [] → s ++ t ≠ []

theorem List.append_eq_cons_iff : ∀ {α : Type u_1} {a b : List α} {x : α} {c : List α}, a ++ b = x :: c ↔ a = [] ∧ b = x :: c ∨ ∃ (a' : List α), a = x :: a' ∧ c = a' ++ b

@[reducible, inline, deprecated List.append_eq_cons_iff]

abbrev List.append_eq_cons : ∀ {α : Type u_1} {a b : List α} {x : α} {c : List α}, a ++ b = x :: c ↔ a = [] ∧ b = x :: c ∨ ∃ (a' : List α), a = x :: a' ∧ c = a' ++ b

Equations

• @List.append_eq_cons = @List.append_eq_cons_iff

theorem List.cons_eq_append_iff : ∀ {α : Type u_1} {x : α} {c a b : List α}, x :: c = a ++ b ↔ a = [] ∧ b = x :: c ∨ ∃ (a' : List α), a = x :: a' ∧ c = a' ++ b

@[reducible, inline, deprecated List.cons_eq_append_iff]

abbrev List.cons_eq_append : ∀ {α : Type u_1} {x : α} {c a b : List α}, x :: c = a ++ b ↔ a = [] ∧ b = x :: c ∨ ∃ (a' : List α), a = x :: a' ∧ c = a' ++ b

Equations

• @List.cons_eq_append = @List.cons_eq_append_iff

theorem List.append_eq_append_iff {α : Type u_1} {a : List α} {b : List α} {c : List α} {d : List α} : a ++ b = c ++ d ↔ (∃ (a' : List α), c = a ++ a' ∧ b = a' ++ d) ∨ ∃ (c' : List α), a = c ++ c' ∧ d = c' ++ b

@[reducible, inline, deprecated List.append_inj]

abbrev List.append_inj_of_length_left {α : Type u_1} {s₁ : List α} {s₂ : List α} {t₁ : List α} {t₂ : List α} : s₁ ++ t₁ = s₂ ++ t₂ → s₁.length = s₂.length → s₁ = s₂ ∧ t₁ = t₂

Equations

• @List.append_inj_of_length_left = @List.append_inj

@[reducible, inline, deprecated List.append_inj']

abbrev List.append_inj_of_length_right : ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → t₁.length = t₂.length → s₁ = s₂ ∧ t₁ = t₂

Equations

• @List.append_inj_of_length_right = @List.append_inj'

@[simp]

theorem List.mem_append {α : Type u_1} {a : α} {s : List α} {t : List α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t

theorem List.not_mem_append {α : Type u_1} {a : α} {s : List α} {t : List α} (h₁ : ¬a ∈ s) (h₂ : ¬a ∈ t) : ¬a ∈ s ++ t

theorem List.mem_append_eq {α : Type u_1} (a : α) (s : List α) (t : List α) : (a ∈ s ++ t) = (a ∈ s ∨ a ∈ t)

theorem List.mem_append_left {α : Type u_1} {a : α} {l₁ : List α} (l₂ : List α) (h : a ∈ l₁) : a ∈ l₁ ++ l₂

theorem List.mem_append_right {α : Type u_1} {a : α} (l₁ : List α) {l₂ : List α} (h : a ∈ l₂) : a ∈ l₁ ++ l₂

theorem List.mem_iff_append {α : Type u_1} {a : α} {l : List α} : a ∈ l ↔ ∃ (s : List α), ∃ (t : List α), l = s ++ a :: t

theorem List.forall_mem_append {α : Type u_1} {p : α → Prop} {l₁ : List α} {l₂ : List α} : (∀ (x : α), x ∈ l₁ ++ l₂ → p x) ↔ (∀ (x : α), x ∈ l₁ → p x) ∧ ∀ (x : α), x ∈ l₂ → p x

theorem List.set_append {α : Type u_1} {i : Nat} {x : α} {s : List α} {t : List α} : (s ++ t).set i x = if i < s.length then s.set i x ++ t else s ++ t.set (i - s.length) x

@[simp]

theorem List.set_append_left {α : Type u_1} {s : List α} {t : List α} (i : Nat) (x : α) (h : i < s.length) : (s ++ t).set i x = s.set i x ++ t

@[simp]

theorem List.set_append_right {α : Type u_1} {s : List α} {t : List α} (i : Nat) (x : α) (h : s.length ≤ i) : (s ++ t).set i x = s ++ t.set (i - s.length) x

@[simp]

theorem List.foldrM_append {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → β → m β) (b : β) (l : List α) (l' : List α) : List.foldrM f b (l ++ l') = do let init ← List.foldrM f b l' List.foldrM f init l

@[simp]

theorem List.foldl_append {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (l : List α) (l' : List α) : List.foldl f b (l ++ l') = List.foldl f (List.foldl f b l) l'

@[simp]

theorem List.foldr_append {α : Type u_1} {β : Type u_2} (f : α → β → β) (b : β) (l : List α) (l' : List α) : List.foldr f b (l ++ l') = List.foldr f (List.foldr f b l') l

theorem List.filterMap_eq_append_iff {α : Type u_1} {β : Type u_2} {l : List α} {L₁ : List β} {L₂ : List β} {f : α → Option β} : List.filterMap f l = L₁ ++ L₂ ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ List.filterMap f l₁ = L₁ ∧ List.filterMap f l₂ = L₂

@[reducible, inline, deprecated List.filterMap_eq_append_iff]

abbrev List.filterMap_eq_append {α : Type u_1} {β : Type u_2} {l : List α} {L₁ : List β} {L₂ : List β} {f : α → Option β} : List.filterMap f l = L₁ ++ L₂ ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ List.filterMap f l₁ = L₁ ∧ List.filterMap f l₂ = L₂

Equations

• @List.filterMap_eq_append = @List.filterMap_eq_append_iff

theorem List.append_eq_filterMap_iff {α : Type u_1} {β : Type u_2} {L₁ : List β} {L₂ : List β} {l : List α} {f : α → Option β} : L₁ ++ L₂ = List.filterMap f l ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ List.filterMap f l₁ = L₁ ∧ List.filterMap f l₂ = L₂

@[reducible, inline, deprecated List.append_eq_filterMap]

abbrev List.append_eq_filterMap {α : Type u_1} {β : Type u_2} {L₁ : List β} {L₂ : List β} {l : List α} {f : α → Option β} : L₁ ++ L₂ = List.filterMap f l ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ List.filterMap f l₁ = L₁ ∧ List.filterMap f l₂ = L₂

Equations

• @List.append_eq_filterMap = @List.append_eq_filterMap_iff

theorem List.filter_eq_append_iff {α : Type u_1} {l : List α} {L₁ : List α} {L₂ : List α} {p : α → Bool} : List.filter p l = L₁ ++ L₂ ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ List.filter p l₁ = L₁ ∧ List.filter p l₂ = L₂

theorem List.append_eq_filter_iff {α : Type u_1} {L₁ : List α} {L₂ : List α} {l : List α} {p : α → Bool} : L₁ ++ L₂ = List.filter p l ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ List.filter p l₁ = L₁ ∧ List.filter p l₂ = L₂

@[reducible, inline, deprecated List.append_eq_filter_iff]

abbrev List.append_eq_filter {α : Type u_1} {L₁ : List α} {L₂ : List α} {l : List α} {p : α → Bool} : L₁ ++ L₂ = List.filter p l ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ List.filter p l₁ = L₁ ∧ List.filter p l₂ = L₂

Equations

• @List.append_eq_filter = @List.append_eq_filter_iff

@[simp]

theorem List.map_append {α : Type u_1} {β : Type u_2} (f : α → β) (l₁ : List α) (l₂ : List α) : List.map f (l₁ ++ l₂) = List.map f l₁ ++ List.map f l₂

theorem List.map_eq_append_iff {α : Type u_1} {β : Type u_2} {l : List α} {L₁ : List β} {L₂ : List β} {f : α → β} : List.map f l = L₁ ++ L₂ ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ List.map f l₁ = L₁ ∧ List.map f l₂ = L₂

theorem List.append_eq_map_iff {α : Type u_1} {β : Type u_2} {L₁ : List β} {L₂ : List β} {l : List α} {f : α → β} : L₁ ++ L₂ = List.map f l ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ List.map f l₁ = L₁ ∧ List.map f l₂ = L₂

@[reducible, inline, deprecated List.map_eq_append_iff]

abbrev List.map_eq_append {α : Type u_1} {β : Type u_2} {l : List α} {L₁ : List β} {L₂ : List β} {f : α → β} : List.map f l = L₁ ++ L₂ ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ List.map f l₁ = L₁ ∧ List.map f l₂ = L₂

Equations

• @List.map_eq_append = @List.map_eq_append_iff

@[reducible, inline, deprecated List.append_eq_map_iff]

abbrev List.append_eq_map {α : Type u_1} {β : Type u_2} {L₁ : List β} {L₂ : List β} {l : List α} {f : α → β} : L₁ ++ L₂ = List.map f l ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ List.map f l₁ = L₁ ∧ List.map f l₂ = L₂

Equations

• @List.append_eq_map = @List.append_eq_map_iff

concat

Note that concat_eq_append is a @[simp] lemma, so concat should usually not appear in goals. As such there's no need for a thorough set of lemmas describing concat.

theorem List.concat_nil {α : Type u_1} (a : α) : [].concat a = [a]

theorem List.concat_cons {α : Type u_1} (a : α) (b : α) (l : List α) : (a :: l).concat b = a :: l.concat b

theorem List.init_eq_of_concat_eq {α : Type u_1} {a : α} {b : α} {l₁ : List α} {l₂ : List α} : l₁.concat a = l₂.concat b → l₁ = l₂

theorem List.last_eq_of_concat_eq {α : Type u_1} {a : α} {b : α} {l₁ : List α} {l₂ : List α} : l₁.concat a = l₂.concat b → a = b

theorem List.concat_inj {α : Type u_1} {a : α} {b : α} {l : List α} {l' : List α} : l.concat a = l'.concat b ↔ l = l' ∧ a = b

theorem List.concat_inj_left {α : Type u_1} {l : List α} {l' : List α} (a : α) : l.concat a = l'.concat a ↔ l = l'

theorem List.concat_inj_right {α : Type u_1} {l : List α} {a : α} {a' : α} : l.concat a = l.concat a' ↔ a = a'

@[reducible, inline, deprecated List.concat_inj]

abbrev List.concat_eq_concat {α : Type u_1} {a : α} {b : α} {l : List α} {l' : List α} : l.concat a = l'.concat b ↔ l = l' ∧ a = b

Equations

• @List.concat_eq_concat = @List.concat_inj

theorem List.concat_ne_nil {α : Type u_1} (a : α) (l : List α) : l.concat a ≠ []

theorem List.concat_append {α : Type u_1} (a : α) (l₁ : List α) (l₂ : List α) : l₁.concat a ++ l₂ = l₁ ++ a :: l₂

theorem List.append_concat {α : Type u_1} (a : α) (l₁ : List α) (l₂ : List α) : l₁ ++ l₂.concat a = (l₁ ++ l₂).concat a

theorem List.map_concat {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) (l : List α) : List.map f (l.concat a) = (List.map f l).concat (f a)

theorem List.eq_nil_or_concat {α : Type u_1} (l : List α) : l = [] ∨ ∃ (L : List α), ∃ (b : α), l = L.concat b

join

@[simp]

theorem List.length_join {α : Type u_1} (L : List (List α)) : L.join.length = Nat.sum (List.map List.length L)

theorem List.join_singleton {α : Type u_1} (l : List α) : [l].join = l

@[simp]

theorem List.mem_join {α : Type u_1} {a : α} {L : List (List α)} : a ∈ L.join ↔ ∃ (l : List α), l ∈ L ∧ a ∈ l

@[simp]

theorem List.join_eq_nil_iff {α : Type u_1} {L : List (List α)} : L.join = [] ↔ ∀ (l : List α), l ∈ L → l = []

@[reducible, inline, deprecated List.join_eq_nil_iff]

abbrev List.join_eq_nil {α : Type u_1} {L : List (List α)} : L.join = [] ↔ ∀ (l : List α), l ∈ L → l = []

Equations

• @List.join_eq_nil = @List.join_eq_nil_iff

theorem List.join_ne_nil_iff {α : Type u_1} {xs : List (List α)} : xs.join ≠ [] ↔ ∃ (x : List α), x ∈ xs ∧ x ≠ []

@[reducible, inline, deprecated List.join_ne_nil_iff]

abbrev List.join_ne_nil {α : Type u_1} {xs : List (List α)} : xs.join ≠ [] ↔ ∃ (x : List α), x ∈ xs ∧ x ≠ []

Equations

• @List.join_ne_nil = @List.join_ne_nil_iff

theorem List.exists_of_mem_join : ∀ {α : Type u_1} {L : List (List α)} {a : α}, a ∈ L.join → ∃ (l : List α), l ∈ L ∧ a ∈ l

theorem List.mem_join_of_mem : ∀ {α : Type u_1} {L : List (List α)} {l : List α} {a : α}, l ∈ L → a ∈ l → a ∈ L.join

theorem List.forall_mem_join {α : Type u_1} {p : α → Prop} {L : List (List α)} : (∀ (x : α), x ∈ L.join → p x) ↔ ∀ (l : List α), l ∈ L → ∀ (x : α), x ∈ l → p x

theorem List.join_eq_bind {α : Type u_1} {L : List (List α)} : L.join = L.bind id

theorem List.head?_join {α : Type u_1} {L : List (List α)} : L.join.head? = List.findSome? (fun (l : List α) => l.head?) L

theorem List.foldl_join {β : Type u_1} {α : Type u_2} (f : β → α → β) (b : β) (L : List (List α)) : List.foldl f b L.join = List.foldl (fun (b : β) (l : List α) => List.foldl f b l) b L

theorem List.foldr_join {α : Type u_1} {β : Type u_2} (f : α → β → β) (b : β) (L : List (List α)) : List.foldr f b L.join = List.foldr (fun (l : List α) (b : β) => List.foldr f b l) b L

@[simp]

theorem List.map_join {α : Type u_1} {β : Type u_2} (f : α → β) (L : List (List α)) : List.map f L.join = (List.map (List.map f) L).join

@[simp]

theorem List.filterMap_join {α : Type u_1} {β : Type u_2} (f : α → Option β) (L : List (List α)) : List.filterMap f L.join = (List.map (List.filterMap f) L).join

@[simp]

theorem List.filter_join {α : Type u_1} (p : α → Bool) (L : List (List α)) : List.filter p L.join = (List.map (List.filter p) L).join

theorem List.join_filter_not_isEmpty {α : Type u_1} {L : List (List α)} : (List.filter (fun (l : List α) => !l.isEmpty) L).join = L.join

theorem List.join_filter_ne_nil {α : Type u_1} [DecidablePred fun (l : List α) => l ≠ []] {L : List (List α)} : (List.filter (fun (l : List α) => decide (l ≠ [])) L).join = L.join

@[deprecated List.filter_join]

theorem List.join_map_filter {α : Type u_1} (p : α → Bool) (l : List (List α)) : (List.map (List.filter p) l).join = List.filter p l.join

@[simp]

theorem List.join_append {α : Type u_1} (L₁ : List (List α)) (L₂ : List (List α)) : (L₁ ++ L₂).join = L₁.join ++ L₂.join

theorem List.join_concat {α : Type u_1} (L : List (List α)) (l : List α) : (L ++ [l]).join = L.join ++ l

theorem List.join_join {α : Type u_1} {L : List (List (List α))} : L.join.join = (List.map List.join L).join

theorem List.join_eq_cons_iff {α : Type u_1} {xs : List (List α)} {y : α} {ys : List α} : xs.join = y :: ys ↔ ∃ (as : List (List α)), ∃ (bs : List α), ∃ (cs : List (List α)), xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.join

theorem List.join_eq_append_iff {α : Type u_1} {xs : List (List α)} {ys : List α} {zs : List α} : xs.join = ys ++ zs ↔ (∃ (as : List (List α)), ∃ (bs : List (List α)), xs = as ++ bs ∧ ys = as.join ∧ zs = bs.join) ∨ ∃ (as : List (List α)), ∃ (bs : List α), ∃ (c : α), ∃ (cs : List α), ∃ (ds : List (List α)), xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.join ++ bs ∧ zs = c :: cs ++ ds.join

@[reducible, inline, deprecated List.join_eq_cons_iff]

abbrev List.join_eq_cons {α : Type u_1} {xs : List (List α)} {y : α} {ys : List α} : xs.join = y :: ys ↔ ∃ (as : List (List α)), ∃ (bs : List α), ∃ (cs : List (List α)), xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.join

Equations

• @List.join_eq_cons = @List.join_eq_cons_iff

@[reducible, inline, deprecated List.join_eq_append_iff]

abbrev List.join_eq_append {α : Type u_1} {xs : List (List α)} {ys : List α} {zs : List α} : xs.join = ys ++ zs ↔ (∃ (as : List (List α)), ∃ (bs : List (List α)), xs = as ++ bs ∧ ys = as.join ∧ zs = bs.join) ∨ ∃ (as : List (List α)), ∃ (bs : List α), ∃ (c : α), ∃ (cs : List α), ∃ (ds : List (List α)), xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.join ++ bs ∧ zs = c :: cs ++ ds.join

Equations

• @List.join_eq_append = @List.join_eq_append_iff

theorem List.eq_iff_join_eq {α : Type u_1} {L : List (List α)} {L' : List (List α)} : L = L' ↔ L.join = L'.join ∧ List.map List.length L = List.map List.length L'

Two lists of sublists are equal iff their joins coincide, as well as the lengths of the sublists.

bind

theorem List.bind_def {α : Type u_1} {β : Type u_2} (l : List α) (f : α → List β) : l.bind f = (List.map f l).join

@[simp]

theorem List.bind_id {α : Type u_1} (l : List (List α)) : l.bind id = l.join

@[simp]

theorem List.mem_bind {α : Type u_1} {β : Type u_2} {f : α → List β} {b : β} {l : List α} : b ∈ l.bind f ↔ ∃ (a : α), a ∈ l ∧ b ∈ f a

theorem List.exists_of_mem_bind {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : α → List β} : b ∈ l.bind f → ∃ (a : α), a ∈ l ∧ b ∈ f a

theorem List.mem_bind_of_mem {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : α → List β} {a : α} (al : a ∈ l) (h : b ∈ f a) : b ∈ l.bind f

@[simp]

theorem List.bind_eq_nil_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} : l.bind f = [] ↔ ∀ (x : α), x ∈ l → f x = []

@[reducible, inline, deprecated List.bind_eq_nil_iff]

abbrev List.bind_eq_nil {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} : l.bind f = [] ↔ ∀ (x : α), x ∈ l → f x = []

Equations

• @List.bind_eq_nil = @List.bind_eq_nil_iff

theorem List.forall_mem_bind {β : Type u_1} {α : Type u_2} {p : β → Prop} {l : List α} {f : α → List β} : (∀ (x : β), x ∈ l.bind f → p x) ↔ ∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b

theorem List.bind_singleton {α : Type u_1} {β : Type u_2} (f : α → List β) (x : α) : [x].bind f = f x

@[simp]

theorem List.bind_singleton' {α : Type u_1} (l : List α) : (l.bind fun (x : α) => [x]) = l

theorem List.head?_bind {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} : (l.bind f).head? = List.findSome? (fun (a : α) => (f a).head?) l

@[simp]

theorem List.bind_append {α : Type u_1} {β : Type u_2} (xs : List α) (ys : List α) (f : α → List β) : (xs ++ ys).bind f = xs.bind f ++ ys.bind f

@[reducible, inline, deprecated List.bind_append]

abbrev List.append_bind {α : Type u_1} {β : Type u_2} (xs : List α) (ys : List α) (f : α → List β) : (xs ++ ys).bind f = xs.bind f ++ ys.bind f

Equations

• @List.append_bind = @List.bind_append

theorem List.bind_assoc {γ : Type u_1} {α : Type u_2} {β : Type u_3} (l : List α) (f : α → List β) (g : β → List γ) : (l.bind f).bind g = l.bind fun (x : α) => (f x).bind g

theorem List.map_bind {β : Type u_1} {γ : Type u_2} {α : Type u_3} (f : β → γ) (g : α → List β) (l : List α) : List.map f (l.bind g) = l.bind fun (a : α) => List.map f (g a)

theorem List.bind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → List γ) (l : List α) : (List.map f l).bind g = l.bind fun (a : α) => g (f a)

theorem List.map_eq_bind {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : List.map f l = l.bind fun (x : α) => [f x]

theorem List.filterMap_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (l : List α) (g : α → List β) (f : β → Option γ) : List.filterMap f (l.bind g) = l.bind fun (a : α) => List.filterMap f (g a)

theorem List.filter_bind {α : Type u_1} {β : Type u_2} (l : List α) (g : α → List β) (f : β → Bool) : List.filter f (l.bind g) = l.bind fun (a : α) => List.filter f (g a)

theorem List.bind_eq_foldl {α : Type u_1} {β : Type u_2} (f : α → List β) (l : List α) : l.bind f = List.foldl (fun (acc : List β) (a : α) => acc ++ f a) [] l

replicate

@[simp]

theorem List.replicate_one : ∀ {α : Type u_1} {a : α}, List.replicate 1 a = [a]

@[simp]

theorem List.mem_replicate {α : Type u_1} {a : α} {b : α} {n : Nat} : b ∈ List.replicate n a ↔ n ≠ 0 ∧ b = a

@[simp, deprecated List.mem_replicate]

theorem List.contains_replicate {α : Type u_1} [BEq α] {n : Nat} {a : α} {b : α} : (List.replicate n b).contains a = (a == b && !n == 0)

@[simp, deprecated List.mem_replicate]

theorem List.decide_mem_replicate {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} {n : Nat} : decide (b ∈ List.replicate n a) = (decide ¬(n == 0) = true && b == a)

theorem List.eq_of_mem_replicate {α : Type u_1} {a : α} {b : α} {n : Nat} (h : b ∈ List.replicate n a) : b = a

theorem List.forall_mem_replicate {α : Type u_1} {p : α → Prop} {a : α} {n : Nat} : (∀ (b : α), b ∈ List.replicate n a → p b) ↔ n = 0 ∨ p a

@[simp]

theorem List.replicate_succ_ne_nil {α : Type u_1} (n : Nat) (a : α) : List.replicate (n + 1) a ≠ []

@[simp]

theorem List.replicate_eq_nil_iff {α : Type u_1} {n : Nat} (a : α) : List.replicate n a = [] ↔ n = 0

@[reducible, inline, deprecated List.replicate_eq_nil_iff]

abbrev List.replicate_eq_nil {α : Type u_1} {n : Nat} (a : α) : List.replicate n a = [] ↔ n = 0

Equations

• @List.replicate_eq_nil = @List.replicate_eq_nil_iff

@[simp]

theorem List.getElem_replicate {α : Type u_1} (a : α) {n : Nat} {m : Nat} (h : m < (List.replicate n a).length) : (List.replicate n a)[m] = a

@[deprecated List.getElem_replicate]

theorem List.get_replicate {α : Type u_1} (a : α) {n : Nat} (m : Fin (List.replicate n a).length) : (List.replicate n a).get m = a

theorem List.getElem?_replicate {n : Nat} : ∀ {α : Type u_1} {a : α} {m : Nat}, (List.replicate n a)[m]? = if m < n then some a else none

@[simp]

theorem List.getElem?_replicate_of_lt : ∀ {α : Type u_1} {a : α} {n m : Nat}, m < n → (List.replicate n a)[m]? = some a

theorem List.head?_replicate {α : Type u_1} (a : α) (n : Nat) : (List.replicate n a).head? = if n = 0 then none else some a

@[simp]

theorem List.head_replicate {n : Nat} : ∀ {α : Type u_1} {a : α} (w : List.replicate n a ≠ []), (List.replicate n a).head w = a

@[simp]

theorem List.tail_replicate {α : Type u_1} (n : Nat) (a : α) : (List.replicate n a).tail = List.replicate (n - 1) a

@[simp]

theorem List.replicate_inj {n : Nat} : ∀ {α : Type u_1} {a : α} {m : Nat} {b : α}, List.replicate n a = List.replicate m b ↔ n = m ∧ (n = 0 ∨ a = b)

theorem List.eq_replicate_of_mem {α : Type u_1} {a : α} {l : List α} : (∀ (b : α), b ∈ l → b = a) → l = List.replicate l.length a

theorem List.eq_replicate_iff {α : Type u_1} {a : α} {n : Nat} {l : List α} : l = List.replicate n a ↔ l.length = n ∧ ∀ (b : α), b ∈ l → b = a

@[reducible, inline, deprecated List.eq_replicate_iff]

abbrev List.eq_replicate {α : Type u_1} {a : α} {n : Nat} {l : List α} : l = List.replicate n a ↔ l.length = n ∧ ∀ (b : α), b ∈ l → b = a

Equations

• @List.eq_replicate = @List.eq_replicate_iff

theorem List.map_eq_replicate_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} {b : β} : List.map f l = List.replicate l.length b ↔ ∀ (x : α), x ∈ l → f x = b

@[simp]

theorem List.map_const {α : Type u_1} {β : Type u_2} (l : List α) (b : β) : List.map (Function.const α b) l = List.replicate l.length b

@[simp]

theorem List.map_const_fun {β : Type u_1} {α : Type u_2} (x : β) : List.map (Function.const α x) = fun (x_1 : List α) => List.replicate x_1.length x

theorem List.map_const' {α : Type u_1} {β : Type u_2} (l : List α) (b : β) : List.map (fun (x : α) => b) l = List.replicate l.length b

Variant of map_const using a lambda rather than Function.const.

@[simp]

theorem List.set_replicate_self {n : Nat} : ∀ {α : Type u_1} {a : α} {i : Nat}, (List.replicate n a).set i a = List.replicate n a

@[simp]

theorem List.append_replicate_replicate {n : Nat} : ∀ {α : Type u_1} {a : α} {m : Nat}, List.replicate n a ++ List.replicate m a = List.replicate (n + m) a

theorem List.append_eq_replicate_iff {α : Type u_1} {n : Nat} {l₁ : List α} {l₂ : List α} {a : α} : l₁ ++ l₂ = List.replicate n a ↔ l₁.length + l₂.length = n ∧ l₁ = List.replicate l₁.length a ∧ l₂ = List.replicate l₂.length a

@[reducible, inline, deprecated List.append_eq_replicate_iff]

abbrev List.append_eq_replicate {α : Type u_1} {n : Nat} {l₁ : List α} {l₂ : List α} {a : α} : l₁ ++ l₂ = List.replicate n a ↔ l₁.length + l₂.length = n ∧ l₁ = List.replicate l₁.length a ∧ l₂ = List.replicate l₂.length a

Equations

• @List.append_eq_replicate = @List.append_eq_replicate_iff

@[simp]

theorem List.map_replicate {n : Nat} : ∀ {α : Type u_1} {a : α} {α_1 : Type u_2} {f : α → α_1}, List.map f (List.replicate n a) = List.replicate n (f a)

theorem List.filter_replicate {n : Nat} : ∀ {α : Type u_1} {a : α} {p : α → Bool}, List.filter p (List.replicate n a) = if p a = true then List.replicate n a else []

@[simp]

theorem List.filter_replicate_of_pos : ∀ {α : Type u_1} {p : α → Bool} {n : Nat} {a : α}, p a = true → List.filter p (List.replicate n a) = List.replicate n a

@[simp]

theorem List.filter_replicate_of_neg : ∀ {α : Type u_1} {p : α → Bool} {n : Nat} {a : α}, ¬p a = true → List.filter p (List.replicate n a) = []

theorem List.filterMap_replicate {α : Type u_1} {β : Type u_2} {n : Nat} {a : α} {f : α → Option β} : List.filterMap f (List.replicate n a) = match f a with | none => [] | some b => List.replicate n b

theorem List.filterMap_replicate_of_some {α : Type u_1} {β : Type u_2} {a : α} {b : β} {n : Nat} {f : α → Option β} (h : f a = some b) : List.filterMap f (List.replicate n a) = List.replicate n b

@[simp]

theorem List.filterMap_replicate_of_isSome {α : Type u_1} {β : Type u_2} {a : α} {n : Nat} {f : α → Option β} (h : (f a).isSome = true) : List.filterMap f (List.replicate n a) = List.replicate n ((f a).get h)

@[simp]

theorem List.filterMap_replicate_of_none {α : Type u_1} {β : Type u_2} {a : α} {n : Nat} {f : α → Option β} (h : f a = none) : List.filterMap f (List.replicate n a) = []

@[simp]

theorem List.join_replicate_nil {n : Nat} {α : Type u_1} : (List.replicate n []).join = []

@[simp]

theorem List.join_replicate_singleton {n : Nat} : ∀ {α : Type u_1} {a : α}, (List.replicate n [a]).join = List.replicate n a

@[simp]

theorem List.join_replicate_replicate {n : Nat} {m : Nat} : ∀ {α : Type u_1} {a : α}, (List.replicate n (List.replicate m a)).join = List.replicate (n * m) a

theorem List.bind_replicate {α : Type u_1} {n : Nat} {a : α} {β : Type u_2} (f : α → List β) : (List.replicate n a).bind f = (List.replicate n (f a)).join

@[simp]

theorem List.isEmpty_replicate {n : Nat} : ∀ {α : Type u_1} {a : α}, (List.replicate n a).isEmpty = decide (n = 0)

theorem List.eq_replicate_or_eq_replicate_append_cons {α : Type u_1} (l : List α) : l = [] ∨ (∃ (n : Nat), ∃ (a : α), l = List.replicate n a ∧ 0 < n) ∨ ∃ (n : Nat), ∃ (a : α), ∃ (b : α), ∃ (l' : List α), l = List.replicate n a ++ b :: l' ∧ 0 < n ∧ a ≠ b

Every list is either empty, a non-empty replicate, or begins with a non-empty replicate followed by a different element.

@[irreducible]

theorem List.replicateRecOn {α : Type u_1} {p : List α → Prop} (m : List α) (h0 : p []) (hr : ∀ (a : α) (n : Nat), 0 < n → p (List.replicate n a)) (hi : ∀ (a b : α) (n : Nat) (l : List α), a ≠ b → 0 < n → p (b :: l) → p (List.replicate n a ++ b :: l)) : p m

An induction principle for lists based on contiguous runs of identical elements.

reverse

@[simp]

theorem List.length_reverse {α : Type u_1} (as : List α) : as.reverse.length = as.length

theorem List.mem_reverseAux {α : Type u_1} {x : α} {as : List α} {bs : List α} : x ∈ as.reverseAux bs ↔ x ∈ as ∨ x ∈ bs

@[simp]

theorem List.mem_reverse {α : Type u_1} {x : α} {as : List α} : x ∈ as.reverse ↔ x ∈ as

@[simp]

theorem List.reverse_eq_nil_iff {α : Type u_1} {xs : List α} : xs.reverse = [] ↔ xs = []

theorem List.reverse_ne_nil_iff {α : Type u_1} {xs : List α} : xs.reverse ≠ [] ↔ xs ≠ []

theorem List.getElem?_reverse' {α : Type u_1} {l : List α} (i : Nat) (j : Nat) : i + j + 1 = l.length → l.reverse[i]? = l[j]?

Variant of getElem?_reverse with a hypothesis giving the linear relation between the indices.

@[deprecated List.getElem?_reverse']

theorem List.get?_reverse' {α : Type u_1} {l : List α} (i : Nat) (j : Nat) (h : i + j + 1 = l.length) : l.reverse.get? i = l.get? j

@[simp]

theorem List.getElem?_reverse {α : Type u_1} {l : List α} {i : Nat} (h : i < l.length) : l.reverse[i]? = l[l.length - 1 - i]?

@[simp]

theorem List.getElem_reverse {α : Type u_1} {l : List α} {i : Nat} (h : i < l.reverse.length) : l.reverse[i] = l[l.length - 1 - i]

@[deprecated List.getElem?_reverse]

theorem List.get?_reverse {α : Type u_1} {l : List α} {i : Nat} (h : i < l.length) : l.reverse.get? i = l.get? (l.length - 1 - i)

theorem List.reverseAux_reverseAux_nil {α : Type u_1} (as : List α) (bs : List α) : (as.reverseAux bs).reverseAux [] = bs.reverseAux as

@[simp]

theorem List.reverse_reverse {α : Type u_1} (as : List α) : as.reverse.reverse = as

theorem List.reverse_eq_iff {α : Type u_1} {as : List α} {bs : List α} : as.reverse = bs ↔ as = bs.reverse

@[simp]

theorem List.reverse_inj {α : Type u_1} {xs : List α} {ys : List α} : xs.reverse = ys.reverse ↔ xs = ys

@[simp]

theorem List.reverse_eq_cons_iff {α : Type u_1} {xs : List α} {a : α} {ys : List α} : xs.reverse = a :: ys ↔ xs = ys.reverse ++ [a]

@[reducible, inline, deprecated List.reverse_eq_cons_iff]

abbrev List.reverse_eq_cons {α : Type u_1} {xs : List α} {a : α} {ys : List α} : xs.reverse = a :: ys ↔ xs = ys.reverse ++ [a]

Equations

• @List.reverse_eq_cons = @List.reverse_eq_cons_iff

@[simp]

theorem List.getLast?_reverse {α : Type u_1} (l : List α) : l.reverse.getLast? = l.head?

@[simp]

theorem List.head?_reverse {α : Type u_1} (l : List α) : l.reverse.head? = l.getLast?

theorem List.getLast?_eq_head?_reverse {α : Type u_1} {xs : List α} : xs.getLast? = xs.reverse.head?

theorem List.head?_eq_getLast?_reverse {α : Type u_1} {xs : List α} : xs.head? = xs.reverse.getLast?

theorem List.mem_of_mem_getLast? {α : Type u_1} {l : List α} {a : α} (h : a ∈ l.getLast?) : a ∈ l

@[simp]

theorem List.map_reverse {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : List.map f l.reverse = (List.map f l).reverse

@[deprecated List.map_reverse]

theorem List.reverse_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : (List.map f l).reverse = List.map f l.reverse

@[simp]

theorem List.filter_reverse {α : Type u_1} (p : α → Bool) (l : List α) : List.filter p l.reverse = (List.filter p l).reverse

@[simp]

theorem List.filterMap_reverse {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) : List.filterMap f l.reverse = (List.filterMap f l).reverse

@[simp]

theorem List.reverse_append {α : Type u_1} (as : List α) (bs : List α) : (as ++ bs).reverse = bs.reverse ++ as.reverse

@[simp]

theorem List.reverse_eq_append_iff {α : Type u_1} {xs : List α} {ys : List α} {zs : List α} : xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse

@[reducible, inline, deprecated List.reverse_eq_append_iff]

abbrev List.reverse_eq_append {α : Type u_1} {xs : List α} {ys : List α} {zs : List α} : xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse

Equations

• @List.reverse_eq_append = @List.reverse_eq_append_iff

theorem List.reverse_concat {α : Type u_1} (l : List α) (a : α) : (l ++ [a]).reverse = a :: l.reverse

theorem List.reverse_eq_concat {α : Type u_1} {xs : List α} {ys : List α} {a : α} : xs.reverse = ys ++ [a] ↔ xs = a :: ys.reverse

theorem List.reverse_join {α : Type u_1} (L : List (List α)) : L.join.reverse = (List.map List.reverse L).reverse.join

Reversing a join is the same as reversing the order of parts and reversing all parts.

theorem List.join_reverse {α : Type u_1} (L : List (List α)) : L.reverse.join = (List.map List.reverse L).join.reverse

Joining a reverse is the same as reversing all parts and reversing the joined result.

theorem List.reverse_bind {α : Type u_1} {β : Type u_2} (l : List α) (f : α → List β) : (l.bind f).reverse = l.reverse.bind (List.reverse ∘ f)

theorem List.bind_reverse {α : Type u_1} {β : Type u_2} (l : List α) (f : α → List β) : l.reverse.bind f = (l.bind (List.reverse ∘ f)).reverse

@[simp]

theorem List.reverseAux_eq {α : Type u_1} (as : List α) (bs : List α) : as.reverseAux bs = as.reverse ++ bs

@[simp]

theorem List.foldrM_reverse {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (l : List α) (f : α → β → m β) (b : β) : List.foldrM f b l.reverse = List.foldlM (fun (x : β) (y : α) => f y x) b l

@[simp]

theorem List.foldl_reverse {α : Type u_1} {β : Type u_2} (l : List α) (f : β → α → β) (b : β) : List.foldl f b l.reverse = List.foldr (fun (x : α) (y : β) => f y x) b l

@[simp]

theorem List.foldr_reverse {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β → β) (b : β) : List.foldr f b l.reverse = List.foldl (fun (x : β) (y : α) => f y x) b l

@[simp]

theorem List.reverse_replicate {α : Type u_1} (n : Nat) (a : α) : (List.replicate n a).reverse = List.replicate n a

Further results about getLast and getLast?

@[simp]

theorem List.head_reverse {α : Type u_1} {l : List α} (h : l.reverse ≠ []) : l.reverse.head h = l.getLast ⋯

theorem List.getLast_eq_head_reverse {α : Type u_1} {l : List α} (h : l ≠ []) : l.getLast h = l.reverse.head ⋯

theorem List.getLast_eq_iff_getLast_eq_some {α : Type u_1} {a : α} {xs : List α} (h : xs ≠ []) : xs.getLast h = a ↔ xs.getLast? = some a

@[simp]

theorem List.getLast?_eq_none_iff {α : Type u_1} {xs : List α} : xs.getLast? = none ↔ xs = []

theorem List.getLast?_eq_some_iff {α : Type u_1} {xs : List α} {a : α} : xs.getLast? = some a ↔ ∃ (ys : List α), xs = ys ++ [a]

@[simp]

theorem List.getLast?_isSome : ∀ {α : Type u_1} {l : List α}, l.getLast?.isSome = true ↔ l ≠ []

theorem List.mem_of_getLast?_eq_some {α : Type u_1} {xs : List α} {a : α} (h : xs.getLast? = some a) : a ∈ xs

@[simp]

theorem List.getLast_reverse {α : Type u_1} {l : List α} (h : l.reverse ≠ []) : l.reverse.getLast h = l.head ⋯

theorem List.head_eq_getLast_reverse {α : Type u_1} {l : List α} (h : l ≠ []) : l.head h = l.reverse.getLast ⋯

@[simp]

theorem List.getLast_append_of_ne_nil {α : Type u_1} {l' : List α} {l : List α} {h₁ : l ++ l' ≠ []} (h₂ : l' ≠ []) : (l ++ l').getLast h₁ = l'.getLast h₂

theorem List.getLast_append {α : Type u_1} {l' : List α} {l : List α} (h : l ++ l' ≠ []) : (l ++ l').getLast h = if h' : l'.isEmpty = true then l.getLast ⋯ else l'.getLast ⋯

theorem List.getLast_append_right {α : Type u_1} {l' : List α} {l : List α} (h : l' ≠ []) : (l ++ l').getLast ⋯ = l'.getLast h

theorem List.getLast_append_left {α : Type u_1} {l' : List α} {l : List α} (w : l ++ l' ≠ []) (h : l' = []) : (l ++ l').getLast w = l.getLast ⋯

@[simp]

theorem List.getLast?_append {α : Type u_1} {l : List α} {l' : List α} : (l ++ l').getLast? = l'.getLast?.or l.getLast?

theorem List.getLast_filter_of_pos {α : Type u_1} {p : α → Bool} {l : List α} (w : l ≠ []) (h : p (l.getLast w) = true) : (List.filter p l).getLast ⋯ = l.getLast w

theorem List.getLast_filterMap_of_eq_some {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} {w : l ≠ []} {b : β} (h : f (l.getLast w) = some b) : (List.filterMap f l).getLast ⋯ = b

theorem List.getLast?_bind {α : Type u_1} {β : Type u_2} {L : List α} {f : α → List β} : (L.bind f).getLast? = List.findSome? (fun (a : α) => (f a).getLast?) L.reverse

theorem List.getLast?_join {α : Type u_1} {L : List (List α)} : L.join.getLast? = List.findSome? (fun (l : List α) => l.getLast?) L.reverse

theorem List.getLast?_replicate {α : Type u_1} (a : α) (n : Nat) : (List.replicate n a).getLast? = if n = 0 then none else some a

@[simp]

theorem List.getLast_replicate {n : Nat} : ∀ {α : Type u_1} {a : α} (w : List.replicate n a ≠ []), (List.replicate n a).getLast w = a

Additional operations

leftpad

theorem List.leftpad_prefix {α : Type u_1} (n : Nat) (a : α) (l : List α) : List.replicate (n - l.length) a <+: List.leftpad n a l

theorem List.leftpad_suffix {α : Type u_1} (n : Nat) (a : α) (l : List α) : l <:+ List.leftpad n a l

List membership

elem / contains

theorem List.elem_cons_self {α : Type u_1} {as : List α} [BEq α] [LawfulBEq α] {a : α} : List.elem a (a :: as) = true

@[simp]

theorem List.contains_cons {α : Type u_1} {a : α} {as : List α} {x : α} [BEq α] : (a :: as).contains x = (x == a || as.contains x)

theorem List.contains_eq_any_beq {α : Type u_1} [BEq α] (l : List α) (a : α) : l.contains a = l.any fun (x : α) => a == x

theorem List.contains_iff_exists_mem_beq {α : Type u_1} [BEq α] {l : List α} {a : α} : l.contains a = true ↔ ∃ (a' : α), a' ∈ l ∧ (a == a') = true

Sublists

partition

Because we immediately simplify partition into two filters for verification purposes, we do not separately develop much theory about it.

@[simp]

theorem List.partition_eq_filter_filter {α : Type u_1} (p : α → Bool) (l : List α) : List.partition p l = (List.filter p l, List.filter (not ∘ p) l)

theorem List.partition_eq_filter_filter.aux {α : Type u_1} (p : α → Bool) (l : List α) {as : List α} {bs : List α} : List.partition.loop p l (as, bs) = (as.reverse ++ List.filter p l, bs.reverse ++ List.filter (not ∘ p) l)

theorem List.mem_partition : ∀ {α : Type u_1} {l : List α} {a : α} {p : α → Bool}, a ∈ l ↔ a ∈ (List.partition p l).fst ∨ a ∈ (List.partition p l).snd

dropLast

dropLast is the specification for Array.pop, so theorems about List.dropLast are often used for theorems about Array.pop.

@[simp]

theorem List.length_dropLast {α : Type u_1} (xs : List α) : xs.dropLast.length = xs.length - 1

@[simp]

theorem List.getElem_dropLast {α : Type u_1} (xs : List α) (i : Nat) (h : i < xs.dropLast.length) : xs.dropLast[i] = xs[i]

@[deprecated List.getElem_dropLast]

theorem List.get_dropLast {α : Type u_1} (xs : List α) (i : Fin xs.dropLast.length) : xs.dropLast.get i = xs.get ⟨↑i, ⋯⟩

theorem List.getElem?_dropLast {α : Type u_1} (xs : List α) (i : Nat) : xs.dropLast[i]? = if i < xs.length - 1 then xs[i]? else none

theorem List.head_dropLast {α : Type u_1} (xs : List α) (h : xs.dropLast ≠ []) : xs.dropLast.head h = xs.head ⋯

theorem List.head?_dropLast {α : Type u_1} (xs : List α) : xs.dropLast.head? = if 1 < xs.length then xs.head? else none

theorem List.getLast_dropLast {α : Type u_1} {xs : List α} (h : xs.dropLast ≠ []) : xs.dropLast.getLast h = xs[xs.length - 2]

theorem List.getLast?_dropLast {α : Type u_1} {xs : List α} : xs.dropLast.getLast? = if xs.length ≤ 1 then none else xs[xs.length - 2]?

theorem List.dropLast_cons_of_ne_nil {α : Type u} {x : α} {l : List α} (h : l ≠ []) : (x :: l).dropLast = x :: l.dropLast

theorem List.dropLast_concat_getLast {α : Type u_1} {l : List α} (h : l ≠ []) : l.dropLast ++ [l.getLast h] = l

@[simp]

theorem List.map_dropLast {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : List.map f l.dropLast = (List.map f l).dropLast

@[simp]

theorem List.dropLast_append_of_ne_nil {α : Type u} {l : List α} (l' : List α) : l ≠ [] → (l' ++ l).dropLast = l' ++ l.dropLast

theorem List.dropLast_append {α : Type u_1} {l₁ : List α} {l₂ : List α} : (l₁ ++ l₂).dropLast = if l₂.isEmpty = true then l₁.dropLast else l₁ ++ l₂.dropLast

theorem List.dropLast_append_cons : ∀ {α : Type u_1} {l₁ : List α} {b : α} {l₂ : List α}, (l₁ ++ b :: l₂).dropLast = l₁ ++ (b :: l₂).dropLast

@[simp]

theorem List.dropLast_concat : ∀ {α : Type u_1} {l₁ : List α} {b : α}, (l₁ ++ [b]).dropLast = l₁

@[simp]

theorem List.dropLast_replicate {α : Type u_1} (n : Nat) (a : α) : (List.replicate n a).dropLast = List.replicate (n - 1) a

@[simp]

theorem List.dropLast_cons_self_replicate {α : Type u_1} (n : Nat) (a : α) : (a :: List.replicate n a).dropLast = List.replicate n a

@[simp]

theorem List.tail_reverse {α : Type u_1} (l : List α) : l.reverse.tail = l.dropLast.reverse

splitAt

We don't provide any API for splitAt, beyond the @[simp] lemma splitAt n l = (l.take n, l.drop n), which is proved in Init.Data.List.TakeDrop.

theorem List.splitAt_go {α : Type u_1} {xs : List α} (n : Nat) (l : List α) (acc : List α) : List.splitAt.go l xs n acc = if n < xs.length then (acc.reverse ++ List.take n xs, List.drop n xs) else (l, [])

Manipulating elements

replace

@[simp]

theorem List.replace_cons_self {α : Type u_1} [BEq α] {as : List α} {b : α} [LawfulBEq α] {a : α} : (a :: as).replace a b = b :: as

@[simp]

theorem List.replace_of_not_mem {α : Type u_1} [BEq α] {a : α} {b : α} {l : List α} (h : (!List.elem a l) = true) : l.replace a b = l

@[simp]

theorem List.length_replace {α : Type u_1} [BEq α] {a : α} {b : α} {l : List α} : (l.replace a b).length = l.length

theorem List.getElem?_replace {α : Type u_1} [BEq α] {a : α} {b : α} [LawfulBEq α] {l : List α} {i : Nat} : (l.replace a b)[i]? = if (l[i]? == some a) = true then if a ∈ List.take i l then some a else some b else l[i]?

theorem List.getElem?_replace_of_ne {α : Type u_1} [BEq α] {a : α} {b : α} [LawfulBEq α] {l : List α} {i : Nat} (h : l[i]? ≠ some a) : (l.replace a b)[i]? = l[i]?

theorem List.getElem_replace {α : Type u_1} [BEq α] {a : α} {b : α} [LawfulBEq α] {l : List α} {i : Nat} (h : i < l.length) : (l.replace a b)[i] = if (l[i] == a) = true then if a ∈ List.take i l then a else b else l[i]

theorem List.getElem_replace_of_ne {α : Type u_1} [BEq α] {a : α} {b : α} [LawfulBEq α] {l : List α} {i : Nat} {h : i < l.length} (h' : l[i] ≠ a) : (l.replace a b)[i] = l[i]

theorem List.head?_replace {α : Type u_1} [BEq α] (l : List α) (a : α) (b : α) : (l.replace a b).head? = match l.head? with | none => none | some x => some (if (a == x) = true then b else x)

theorem List.head_replace {α : Type u_1} [BEq α] (l : List α) (a : α) (b : α) (w : l.replace a b ≠ []) : (l.replace a b).head w = if (a == l.head ⋯) = true then b else l.head ⋯

theorem List.replace_append {α : Type u_1} [BEq α] {a : α} {b : α} [LawfulBEq α] {l₁ : List α} {l₂ : List α} : (l₁ ++ l₂).replace a b = if a ∈ l₁ then l₁.replace a b ++ l₂ else l₁ ++ l₂.replace a b

theorem List.replace_append_left {α : Type u_1} [BEq α] {a : α} {b : α} [LawfulBEq α] {l₁ : List α} {l₂ : List α} (h : a ∈ l₁) : (l₁ ++ l₂).replace a b = l₁.replace a b ++ l₂

theorem List.replace_append_right {α : Type u_1} [BEq α] {a : α} {b : α} [LawfulBEq α] {l₁ : List α} {l₂ : List α} (h : ¬a ∈ l₁) : (l₁ ++ l₂).replace a b = l₁ ++ l₂.replace a b

theorem List.replace_take {α : Type u_1} [BEq α] {a : α} {b : α} {l : List α} {n : Nat} : (List.take n l).replace a b = List.take n (l.replace a b)

@[simp]

theorem List.replace_replicate_self {α : Type u_1} [BEq α] {n : Nat} {b : α} [LawfulBEq α] {a : α} (h : 0 < n) : (List.replicate n a).replace a b = b :: List.replicate (n - 1) a

@[simp]

theorem List.replace_replicate_ne {α : Type u_1} [BEq α] {n : Nat} {a : α} {b : α} {c : α} (h : (!b == a) = true) : (List.replicate n a).replace b c = List.replicate n a

insert

@[simp]

theorem List.insert_nil {α : Type u_1} [BEq α] (a : α) : List.insert a [] = [a]

@[simp]

theorem List.insert_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) : List.insert a l = l

@[simp]

theorem List.insert_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : ¬a ∈ l) : List.insert a l = a :: l

@[simp]

theorem List.mem_insert_iff {α : Type u_1} [BEq α] [LawfulBEq α] {b : α} {a : α} {l : List α} : a ∈ List.insert b l ↔ a = b ∨ a ∈ l

@[simp]

theorem List.mem_insert_self {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) : a ∈ List.insert a l

theorem List.mem_insert_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} {l : List α} (h : a ∈ l) : a ∈ List.insert b l

theorem List.eq_or_mem_of_mem_insert {α : Type u_1} [BEq α] [LawfulBEq α] {b : α} {a : α} {l : List α} (h : a ∈ List.insert b l) : a = b ∨ a ∈ l

@[simp]

theorem List.length_insert_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) : (List.insert a l).length = l.length

@[simp]

theorem List.length_insert_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : ¬a ∈ l) : (List.insert a l).length = l.length + 1

theorem List.length_le_length_insert {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} : l.length ≤ (List.insert a l).length

theorem List.length_insert_pos {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} : 0 < (List.insert a l).length

theorem List.insert_eq {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} : List.insert a l = if a ∈ l then l else a :: l

theorem List.getElem?_insert_zero {α : Type u_1} [BEq α] [LawfulBEq α] (l : List α) (a : α) : (List.insert a l)[0]? = if a ∈ l then l[0]? else some a

theorem List.getElem?_insert_succ {α : Type u_1} [BEq α] [LawfulBEq α] (l : List α) (a : α) (i : Nat) : (List.insert a l)[i + 1]? = if a ∈ l then l[i + 1]? else l[i]?

theorem List.getElem?_insert {α : Type u_1} [BEq α] [LawfulBEq α] (l : List α) (a : α) (i : Nat) : (List.insert a l)[i]? = if a ∈ l then l[i]? else if i = 0 then some a else l[i - 1]?

theorem List.getElem_insert {α : Type u_1} [BEq α] [LawfulBEq α] (l : List α) (a : α) (i : Nat) (h : i < l.length) : (List.insert a l)[i] = if a ∈ l then l[i] else if i = 0 then a else l[i - 1]

theorem List.head?_insert {α : Type u_1} [BEq α] [LawfulBEq α] (l : List α) (a : α) : (List.insert a l).head? = some (if h : a ∈ l then l.head ⋯ else a)

theorem List.head_insert {α : Type u_1} [BEq α] [LawfulBEq α] (l : List α) (a : α) (w : List.insert a l ≠ []) : (List.insert a l).head w = if h : a ∈ l then l.head ⋯ else a

theorem List.insert_append {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ : List α} {l₂ : List α} {a : α} : List.insert a (l₁ ++ l₂) = if a ∈ l₂ then l₁ ++ l₂ else List.insert a l₁ ++ l₂

theorem List.insert_append_of_mem_left {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ : List α} {l₂ : List α} (h : a ∈ l₂) : List.insert a (l₁ ++ l₂) = l₁ ++ l₂

theorem List.insert_append_of_not_mem_left {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ : List α} {l₂ : List α} (h : ¬a ∈ l₂) : List.insert a (l₁ ++ l₂) = List.insert a l₁ ++ l₂

@[simp]

theorem List.insert_replicate_self {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {a : α} (h : 0 < n) : List.insert a (List.replicate n a) = List.replicate n a

@[simp]

theorem List.insert_replicate_ne {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {a : α} {b : α} (h : (!b == a) = true) : List.insert b (List.replicate n a) = b :: List.replicate n a

Logic

any / all

theorem List.not_any_eq_all_not {α : Type u_1} (l : List α) (p : α → Bool) : (!l.any p) = l.all fun (a : α) => !p a

theorem List.not_all_eq_any_not {α : Type u_1} (l : List α) (p : α → Bool) : (!l.all p) = l.any fun (a : α) => !p a

theorem List.and_any_distrib_left {α : Type u_1} (l : List α) (p : α → Bool) (q : Bool) : (q && l.any p) = l.any fun (a : α) => q && p a

theorem List.and_any_distrib_right {α : Type u_1} (l : List α) (p : α → Bool) (q : Bool) : (l.any p && q) = l.any fun (a : α) => p a && q

theorem List.or_all_distrib_left {α : Type u_1} (l : List α) (p : α → Bool) (q : Bool) : (q || l.all p) = l.all fun (a : α) => q || p a

theorem List.or_all_distrib_right {α : Type u_1} (l : List α) (p : α → Bool) (q : Bool) : (l.all p || q) = l.all fun (a : α) => p a || q

theorem List.any_eq_not_all_not {α : Type u_1} (l : List α) (p : α → Bool) : l.any p = !l.all fun (x : α) => !p x

theorem List.all_eq_not_any_not {α : Type u_1} (l : List α) (p : α → Bool) : l.all p = !l.any fun (x : α) => !p x

@[simp]

theorem List.any_map {α : Type u_1} {f : α → α} {l : List α} {p : α → Bool} : (List.map f l).any p = l.any (p ∘ f)

@[simp]

theorem List.all_map {α : Type u_1} {f : α → α} {l : List α} {p : α → Bool} : (List.map f l).all p = l.all (p ∘ f)

@[simp]

theorem List.any_filter {α : Type u_1} {l : List α} {p : α → Bool} {q : α → Bool} : (List.filter p l).any q = l.any fun (a : α) => p a && q a

@[simp]

theorem List.all_filter {α : Type u_1} {l : List α} {p : α → Bool} {q : α → Bool} : (List.filter p l).all q = l.all fun (a : α) => decide (p a = true → q a = true)

@[simp]

theorem List.any_filterMap {α : Type u_1} {β : Type u_2} {l : List α} {f : α → Option β} {p : β → Bool} : (List.filterMap f l).any p = l.any fun (a : α) => match f a with | some b => p b | none => false

@[simp]

theorem List.all_filterMap {α : Type u_1} {β : Type u_2} {l : List α} {f : α → Option β} {p : β → Bool} : (List.filterMap f l).all p = l.all fun (a : α) => match f a with | some b => p b | none => true

@[simp]

theorem List.any_append {α : Type u_1} {f : α → Bool} {x : List α} {y : List α} : (x ++ y).any f = (x.any f || y.any f)

@[simp]

theorem List.all_append {α : Type u_1} {f : α → Bool} {x : List α} {y : List α} : (x ++ y).all f = (x.all f && y.all f)

@[simp]

theorem List.any_join {α : Type u_1} {f : α → Bool} {l : List (List α)} : l.join.any f = l.any fun (x : List α) => x.any f

@[simp]

theorem List.all_join {α : Type u_1} {f : α → Bool} {l : List (List α)} : l.join.all f = l.all fun (x : List α) => x.all f

@[simp]

theorem List.any_bind {α : Type u_1} {β : Type u_2} {p : β → Bool} {l : List α} {f : α → List β} : (l.bind f).any p = l.any fun (a : α) => (f a).any p

@[simp]

theorem List.all_bind {α : Type u_1} {β : Type u_2} {p : β → Bool} {l : List α} {f : α → List β} : (l.bind f).all p = l.all fun (a : α) => (f a).all p

@[simp]

theorem List.any_reverse {α : Type u_1} {f : α → Bool} {l : List α} : l.reverse.any f = l.any f

@[simp]

theorem List.all_reverse {α : Type u_1} {f : α → Bool} {l : List α} : l.reverse.all f = l.all f

@[simp]

theorem List.any_replicate {α : Type u_1} {f : α → Bool} {n : Nat} {a : α} : (List.replicate n a).any f = if n = 0 then false else f a

@[simp]

theorem List.all_replicate {α : Type u_1} {f : α → Bool} {n : Nat} {a : α} : (List.replicate n a).all f = if n = 0 then true else f a

@[simp]

theorem List.any_insert {α : Type u_1} {f : α → Bool} [BEq α] [LawfulBEq α] {l : List α} {a : α} : (List.insert a l).any f = (f a || l.any f)

@[simp]

theorem List.all_insert {α : Type u_1} {f : α → Bool} [BEq α] [LawfulBEq α] {l : List α} {a : α} : (List.insert a l).all f = (f a && l.all f)