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.minimum? and List.maximum?.
• 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

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_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]?.

@[simp]

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

@[simp]

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, ⋯⟩

@[simp]

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_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].

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]

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 {α : Type u_1} {n : Nat} {a : α} {l : List α} : l[n]? = some a ↔ ∃ (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

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? {α : Type u_1} (xs : List α) (i : Nat) (h : i < xs.length) : some xs[i] = xs[i]? ↔ True

@[simp]

theorem List.getElem?_eq_some_getElem {α : 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? {α : Type u_1} (l : List α) (i : Nat) (h : i < l.length) : l[i] = l[i]?.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

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.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.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.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)

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_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.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.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

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), 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))

isEmpty

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

theorem List.isEmpty_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_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)

@[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

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_eq {α : Type u_1} {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) : (l.set i a)[i] = a

@[deprecated List.getElem_set_eq]

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_eq {α : Type u_1} {l : List α} {i : Nat} {a : α} (h : i < l.length) : (l.set i a)[i]? = some a

theorem List.getElem?_set_eq' {α : Type u_1} {l : List α} {i : Nat} {a : α} : (l.set i a)[i]? = Function.const α a <$> 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 (fun (x : α) => a) <$> l[j]? else 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 {α : Type u_1} (l : List α) (n : Nat) (a : α) : l.set n a = [] ↔ l = []

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

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_self {α : Type u_1} (l : List α) : List.foldr List.cons [] l = l

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_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 ⋯

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.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?_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?

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]?

@[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!_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_iff_head?_eq_some {α : Type u_1} {a : α} {xs : List α} (h : xs ≠ []) : xs.head h = a ↔ xs.head? = some a

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

@[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_mem {α : Type u_1} {l : List α} (h : l ≠ []) : l.head h ∈ l

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 []

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

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

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

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 {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : List.map f l = [] ↔ l = []

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 {α : 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₂

theorem 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₂

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.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.tail?_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : (List.map f l).tail? = Option.map (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 : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.filter p l = [] ↔ ∀ (a : α), a ∈ l → ¬p a = true

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 : α) => decide (p a = true ∧ q a = true)) 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 : ∀ {α : 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

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 : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {l : List α}, List.filterMap f l = [] ↔ ∀ (a : α), a ∈ l → f a = none

theorem 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

append

theorem List.getElem?_append_right {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} : l₁.length ≤ n → (l₁ ++ l₂)[n]? = 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_right' {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h₁ : l₁.length ≤ n) (h₂ : n < (l₁ ++ l₂).length) : (l₁ ++ l₂)[n] = l₂[n - l₁.length]

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]

@[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

@[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₂

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

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

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

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

@[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 : ¬i < as.length) {h' : i < (as ++ bs).length} {h'' : i - as.length < bs.length} : (as ++ bs).get ⟨i, h'⟩ = bs.get ⟨i - as.length, h''⟩

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

@[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

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]?

@[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 ⋯

@[simp]

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

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

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.tail_append {α : Type u_1} (xs : List α) (ys : List α) : (xs ++ ys).tail = if xs.isEmpty = true then ys.tail else xs.tail ++ ys

@[simp]

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

theorem 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

theorem 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

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

theorem List.append_inj_of_length_left {α : Type u_1} {a : List α} {b : List α} {c : List α} {d : List α} (h : a ++ b = c ++ d) (hl : a.length = c.length) : a = c ∧ b = d

theorem List.append_inj_of_length_right {α : Type u_1} {a : List α} {b : List α} {c : List α} {d : List α} (h : a ++ b = c ++ d) (hl : b.length = d.length) : a = c ∧ b = d

@[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 : ¬i < s.length) : (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 {α : 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₂

theorem 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₂

theorem List.filter_eq_append {α : 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 {α : 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₂

@[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 {α : 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 {α : 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₂

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_left {α : Type u_1} {l : List α} {l' : List α} (a : α) : l.concat a = l'.concat a ↔ l = l'

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

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 {α : Type u_1} {L : List (List α)} : L.join = [] ↔ ∀ (l : List α), l ∈ L → l = []

@[deprecated List.join_eq_nil]

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

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

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

@[simp]

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

@[simp]

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 {α : 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 {α : 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

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 {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} : l.bind f = [] ↔ ∀ (x : α), x ∈ l → f x = []

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.contains_replicate {α : Type u_1} [BEq α] {n : Nat} {a : α} {b : α} : (List.replicate n b).contains a = (a == b && !n == 0)

@[simp]

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)

@[simp]

theorem List.mem_replicate {α : Type u_1} {a : α} {b : α} {n : Nat} : b ∈ List.replicate n a ↔ n ≠ 0 ∧ 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 {α : Type u_1} (n : Nat) (a : α) : List.replicate n a = [] ↔ n = 0

@[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 {α : Type u_1} {a : α} {n : Nat} {l : List α} : l = List.replicate n a ↔ l.length = n ∧ ∀ (b : α), b ∈ l → b = a

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

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

@[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 {α : 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

@[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)

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]?

@[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 {α : Type u_1} {xs : List α} {a : α} {ys : List α} : xs.reverse = a :: ys ↔ xs = ys.reverse ++ [a]

@[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?

@[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 {α : Type u_1} {xs : List α} {ys : List α} {zs : List α} : xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse

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]

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 ⋯

@[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.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

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_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₂

@[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

lookup

@[simp]

theorem List.lookup_cons_self {α : Type u_2} [BEq α] [LawfulBEq α] : ∀ {β : Type u_1} {b : β} {es : List (α × β)} {k : α}, List.lookup k ((k, b) :: es) = some b

theorem List.lookup_replicate {α : Type u_2} [BEq α] [LawfulBEq α] {n : Nat} {a : α} : ∀ {α_1 : Type u_1} {b : α_1} {k : α}, List.lookup k (List.replicate n (a, b)) = if n = 0 then none else if (k == a) = true then some b else none

theorem List.lookup_replicate_of_pos {α : Type u_2} [BEq α] [LawfulBEq α] {n : Nat} {a : α} : ∀ {α_1 : Type u_1} {b : α_1} {k : α}, 0 < n → List.lookup k (List.replicate n (a, b)) = if (k == a) = true then some b else none

theorem List.lookup_replicate_self {α : Type u_2} [BEq α] [LawfulBEq α] {n : Nat} : ∀ {α_1 : Type u_1} {b : α_1} {a : α}, List.lookup a (List.replicate n (a, b)) = if n = 0 then none else some b

@[simp]

theorem List.lookup_replicate_self_of_pos {α : Type u_2} [BEq α] [LawfulBEq α] {n : Nat} : ∀ {α_1 : Type u_1} {b : α_1} {a : α}, 0 < n → List.lookup a (List.replicate n (a, b)) = some b

@[simp]

theorem List.lookup_replicate_ne {α : Type u_2} [BEq α] [LawfulBEq α] {a : α} {n : Nat} : ∀ {α_1 : Type u_1} {b : α_1} {k : α}, (!k == a) = true → List.lookup k (List.replicate n (a, b)) = none

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)