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, operation 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.

Preliminaries

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

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

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

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

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]

@[simp]

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

@[simp]

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?_len_le {α : Type u_1} {l : List α} {n : Nat} : l.length ≤ n → l[n]? = none

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

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

@[simp]

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

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

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

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

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

@[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.get_mk_zero {α : Type u_1} {l : List α} (h : 0 < l.length) : l.get ⟨0, h⟩ = 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.get!_of_get? {α : Type u_1} {a : α} [Inhabited α] {l : List α} {n : Nat} : l.get? n = some a → l.get! n = a

@[simp]

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

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} {a b : α} {l : List α}, a ∈ b :: l ↔ a = b ∨ a ∈ l

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

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} {a b : α}, 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.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

@[simp]

theorem List.decide_mem_cons {α : Type u_1} {y : α} {a : α} [BEq α] [LawfulBEq α] {l : List α} : decide (y ∈ a :: l) = (y == a || decide (y ∈ 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.set i a).length) : (l.set i a)[i]? = some a

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

@[simp]

theorem List.foldr_self_append {α : Type u_1} {l' : List α} (l : List α) : List.foldr List.cons l' l = l ++ 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)

getD

@[simp]

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

@[deprecated List.getD_eq_getElem?]

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

getLast

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₁ : a :: l ≠ []) (h₂ : l ≠ []) : (a :: l).getLast h₁ = l.getLast h₂

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

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

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?

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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)

tail

@[simp]

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

Basic operations

map

@[simp]

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

@[simp]

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} {b : α} {α_1 : Type u_2} {f : α_1 → α} {l : List α_1}, b ∈ List.map f l → ∃ (a : α_1), a ∈ l ∧ f a = b

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

@[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_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.headD_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) (a : α) : (List.map f l).headD (f a) = f (l.headD a)

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

@[simp]

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?

@[simp]

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

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

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

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

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

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

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

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 {α : Type u_1} (l : List α) : List.filterMap some l = l

theorem List.map_filterMap_some_eq_filter_map_is_some {α : 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.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'

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

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

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]

@[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_eq_nil : ∀ {α : Type u_1} {p q : List α}, p ++ q = [] ↔ p = [] ∧ q = []

@[simp]

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

theorem List.getLast_concat : ∀ {α : Type u_1} {l : List α} {a : α} {h : l.concat a ≠ []}, (l.concat a).getLast h = 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 {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (hn : n < l₁.length) : (l₁ ++ l₂)[n]? = l₁[n]?

@[deprecated]

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.append_eq_append : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.append l₂ = l₁ ++ l₂

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

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

@[simp]

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} (a : List α) (b : List α) (h0 : a ≠ []) : a ++ b ≠ []

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

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

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.mem_join {α : Type u_1} {a : α} {L : List (List α)} : a ∈ L.join ↔ ∃ (l : List α), l ∈ L ∧ a ∈ l

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

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

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

bind

@[simp]

theorem 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

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

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

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

@[simp]

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

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

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

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

theorem List.getElem?_reverse {α : Type u_1} {l : List α} {i : Nat} (h : i < l.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

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

@[simp]

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

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

@[simp]

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

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

List membership

elem / contains

@[simp]

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

Sublists

take and drop

Further results on List.take and List.drop, which rely on stronger automation in Nat, are given in Init.Data.List.TakeDrop.

@[simp]

theorem List.take_append_drop {α : Type u_1} (n : Nat) (l : List α) : List.take n l ++ List.drop n l = l

@[simp]

theorem List.length_drop {α : Type u_1} (i : Nat) (l : List α) : (List.drop i l).length = l.length - i

theorem List.drop_length_le {α : Type u_1} {i : Nat} {l : List α} (h : l.length ≤ i) : List.drop i l = []

theorem List.take_length_le {α : Type u_1} {i : Nat} {l : List α} (h : l.length ≤ i) : List.take i l = l

@[simp]

theorem List.drop_length {α : Type u_1} (l : List α) : List.drop l.length l = []

@[simp]

theorem List.take_length {α : Type u_1} (l : List α) : List.take l.length l = l

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

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

@[reducible, inline]

abbrev List.take_succ_cons : ∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, List.take (i + 1) (a :: as) = a :: List.take i as

Equations

• @List.take_succ_cons = @List.take_cons_succ

theorem List.take_all_of_le {α : Type u_1} {n : Nat} {l : List α} (h : l.length ≤ n) : List.take n l = l

@[simp]

theorem List.take_left {α : Type u_1} (l₁ : List α) (l₂ : List α) : List.take l₁.length (l₁ ++ l₂) = l₁

theorem List.take_left' {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h : l₁.length = n) : List.take n (l₁ ++ l₂) = l₁

@[simp]

theorem List.map_take {α : Type u_1} {β : Type u_2} (f : α → β) (L : List α) (i : Nat) : List.map f (List.take i L) = List.take i (List.map f L)

theorem List.getElem?_take {α : Type u_1} {l : List α} {n : Nat} {m : Nat} (h : m < n) : (List.take n l)[m]? = l[m]?

@[deprecated List.getElem?_take]

theorem List.get?_take {α : Type u_1} {l : List α} {n : Nat} {m : Nat} (h : m < n) : (List.take n l).get? m = l.get? m

@[simp]

theorem List.get?_take_of_succ {α : Type u_1} {l : List α} {n : Nat} : (List.take (n + 1) l)[n]? = l[n]?

theorem List.take_succ {α : Type u_1} {l : List α} {n : Nat} : List.take (n + 1) l = List.take n l ++ l[n]?.toList

@[simp]

theorem List.take_eq_nil_iff {α : Type u_1} {l : List α} {k : Nat} : List.take k l = [] ↔ l = [] ∨ k = 0

theorem List.take_eq_nil_of_eq_nil {α : Type u_1} {as : List α} {i : Nat} : as = [] → List.take i as = []

theorem List.ne_nil_of_take_ne_nil {α : Type u_1} {as : List α} {i : Nat} (h : List.take i as ≠ []) : as ≠ []

theorem List.dropLast_eq_take {α : Type u_1} (l : List α) : l.dropLast = List.take l.length.pred l

@[simp]

theorem List.drop_eq_nil_iff_le {α : Type u_1} {l : List α} {k : Nat} : List.drop k l = [] ↔ l.length ≤ k

theorem List.drop_sizeOf_le {α : Type u_1} [SizeOf α] (l : List α) (n : Nat) : sizeOf (List.drop n l) ≤ sizeOf l

@[simp]

theorem List.drop_drop {α : Type u_1} (n : Nat) (m : Nat) (l : List α) : List.drop n (List.drop m l) = List.drop (n + m) l

theorem List.take_drop {α : Type u_1} (m : Nat) (n : Nat) (l : List α) : List.take n (List.drop m l) = List.drop m (List.take (m + n) l)

@[simp]

theorem List.map_drop {α : Type u_1} {β : Type u_2} (f : α → β) (L : List α) (i : Nat) : List.map f (List.drop i L) = List.drop i (List.map f L)

@[simp]

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

@[deprecated List.getElem_cons_drop]

theorem List.get_cons_drop {α : Type u_1} (l : List α) (i : Fin l.length) : l.get i :: List.drop (↑i + 1) l = List.drop (↑i) l

theorem List.drop_eq_getElem_cons {α : Type u_1} {n : Nat} {l : List α} (h : n < l.length) : List.drop n l = l[n] :: List.drop (n + 1) l

@[deprecated List.drop_eq_getElem_cons]

theorem List.drop_eq_get_cons {α : Type u_1} {n : Nat} {l : List α} (h : n < l.length) : List.drop n l = l.get ⟨n, h⟩ :: List.drop (n + 1) l

theorem List.drop_eq_nil_of_eq_nil {α : Type u_1} {as : List α} {i : Nat} : as = [] → List.drop i as = []

theorem List.ne_nil_of_drop_ne_nil {α : Type u_1} {as : List α} {i : Nat} (h : List.drop i as ≠ []) : as ≠ []

@[deprecated List.drop_drop]

theorem List.drop_add {α : Type u_1} (m : Nat) (n : Nat) (l : List α) : List.drop (m + n) l = List.drop m (List.drop n l)

@[simp]

theorem List.drop_left {α : Type u_1} (l₁ : List α) (l₂ : List α) : List.drop l₁.length (l₁ ++ l₂) = l₂

theorem List.drop_left' {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h : l₁.length = n) : List.drop n (l₁ ++ l₂) = l₂

takeWhile and dropWhile

theorem List.takeWhile_cons {α : Type u_1} (p : α → Bool) (a : α) (l : List α) : List.takeWhile p (a :: l) = if p a = true then a :: List.takeWhile p l else []

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

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

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

@[simp]

theorem List.takeWhile_append_dropWhile {α : Type u_1} (p : α → Bool) (l : List α) : List.takeWhile p l ++ List.dropWhile p l = l

theorem List.dropWhile_append {α : Type u_1} {p : α → Bool} {xs : List α} {ys : List α} : List.dropWhile p (xs ++ ys) = if (List.dropWhile p xs).isEmpty = true then List.dropWhile p ys else List.dropWhile p xs ++ ys

@[simp]

theorem List.takeWhile_replicate_eq_filter {α : Type u_1} {n : Nat} {a : α} (p : α → Bool) : List.takeWhile p (List.replicate n a) = List.filter p (List.replicate n a)

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

@[simp]

theorem List.dropWhile_replicate_eq_filter_not {α : Type u_1} {n : Nat} {a : α} (p : α → Bool) : List.dropWhile p (List.replicate n a) = List.filter (fun (a : α) => !p a) (List.replicate n a)

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

partition

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

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.dropLast_cons_of_ne_nil {α : Type u} {x : α} {l : List α} (h : l ≠ []) : (x :: l).dropLast = x :: 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_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.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_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

isPrefixOf

@[simp]

theorem List.isPrefixOf_cons₂_self {α : Type u_1} [BEq α] {as : List α} {bs : List α} [LawfulBEq α] {a : α} : (a :: as).isPrefixOf (a :: bs) = as.isPrefixOf bs

@[simp]

theorem List.isPrefixOf_length_pos_nil {α : Type u_1} [BEq α] {L : List α} (h : 0 < L.length) : L.isPrefixOf [] = false

@[simp]

theorem List.isPrefixOf_replicate {α : Type u_1} [BEq α] {l : List α} {n : Nat} {a : α} : l.isPrefixOf (List.replicate n a) = (decide (l.length ≤ n) && l.all fun (x : α) => x == a)

isSuffixOf

@[simp]

theorem List.isSuffixOf_cons_nil {α : Type u_1} [BEq α] {a : α} {as : List α} : (a :: as).isSuffixOf [] = false

@[simp]

theorem List.isSuffixOf_replicate {α : Type u_1} [BEq α] {l : List α} {n : Nat} {a : α} : l.isSuffixOf (List.replicate n a) = (decide (l.length ≤ n) && l.all fun (x : α) => x == a)

rotateLeft

@[simp]

theorem List.rotateLeft_zero {α : Type u_1} (l : List α) : l.rotateLeft 0 = l

rotateRight

@[simp]

theorem List.rotateRight_zero {α : Type u_1} (l : List α) : l.rotateRight 0 = 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.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 α] [LawfulBEq α] (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 α] {a : α} {b : α} {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 α] {a : α} {b : α} {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

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

erase

@[simp]

theorem List.erase_cons_head {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) : (a :: l).erase a = l

@[simp]

theorem List.erase_cons_tail {α : Type u_1} [BEq α] {a : α} {b : α} (l : List α) (h : ¬(b == a) = true) : (b :: l).erase a = b :: l.erase a

theorem List.erase_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} : ¬a ∈ l → l.erase a = l

@[simp]

theorem List.erase_replicate_self {α : Type u_1} [BEq α] {n : Nat} [LawfulBEq α] {a : α} : (List.replicate n a).erase a = List.replicate (n - 1) a

@[simp]

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

find?

@[simp]

theorem List.find?_cons_of_pos : ∀ {α : Type u_1} {p : α → Bool} {a : α} (l : List α), p a = true → List.find? p (a :: l) = some a

@[simp]

theorem List.find?_cons_of_neg : ∀ {α : Type u_1} {p : α → Bool} {a : α} (l : List α), ¬p a = true → List.find? p (a :: l) = List.find? p l

@[simp]

theorem List.find?_eq_none : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.find? p l = none ↔ ∀ (x : α), x ∈ l → ¬p x = true

theorem List.find?_some : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, List.find? p l = some a → p a = true

@[simp]

theorem List.mem_of_find?_eq_some : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, List.find? p l = some a → a ∈ l

@[simp]

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

theorem List.find?_replicate : ∀ {α : Type u_1} {p : α → Bool} {n : Nat} {a : α}, List.find? p (List.replicate n a) = if n = 0 then none else if p a = true then some a else none

@[simp]

theorem List.find?_replicate_of_length_pos {n : Nat} : ∀ {α : Type u_1} {p : α → Bool} {a : α}, 0 < n → List.find? p (List.replicate n a) = if p a = true then some a else none

@[simp]

theorem List.find?_replicate_of_pos : ∀ {α : Type u_1} {p : α → Bool} {n : Nat} {a : α}, p a = true → List.find? p (List.replicate n a) = if n = 0 then none else some a

@[simp]

theorem List.find?_replicate_of_neg : ∀ {α : Type u_1} {p : α → Bool} {n : Nat} {a : α}, ¬p a = true → List.find? p (List.replicate n a) = none

findSome?

@[simp]

theorem List.findSome?_cons_of_isSome : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {a : α} (l : List α), (f a).isSome = true → List.findSome? f (a :: l) = f a

@[simp]

theorem List.findSome?_cons_of_isNone : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {a : α} (l : List α), (f a).isNone = true → List.findSome? f (a :: l) = List.findSome? f l

theorem List.exists_of_findSome?_eq_some {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → Option β} (w : List.findSome? f l = some b) : ∃ (a : α), a ∈ l ∧ f a = some b

@[simp]

theorem List.findSome?_map {β : Type u_1} {γ : Type u_2} : ∀ {α : Type u_3} {p : γ → Option α} (f : β → γ) (l : List β), List.findSome? p (List.map f l) = List.findSome? (p ∘ f) l

theorem List.findSome?_replicate : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : Nat} {a : α}, List.findSome? f (List.replicate n a) = if n = 0 then none else f a

@[simp]

theorem List.findSome?_replicate_of_pos {n : Nat} : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {a : α}, 0 < n → List.findSome? f (List.replicate n a) = f a

@[simp]

theorem List.find?_replicate_of_isSome : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : Nat} {a : α}, (f a).isSome = true → List.findSome? f (List.replicate n a) = if n = 0 then none else f a

@[simp]

theorem List.find?_replicate_of_isNone : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : Nat} {a : α}, (f a).isNone = true → List.findSome? f (List.replicate n a) = none

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

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

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

Zippers

zip

theorem List.zip_map {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) (l₁ : List α) (l₂ : List β) : (List.map f l₁).zip (List.map g l₂) = List.map (Prod.map f g) (l₁.zip l₂)

theorem List.zip_map_left {α : Type u_1} {γ : Type u_2} {β : Type u_3} (f : α → γ) (l₁ : List α) (l₂ : List β) : (List.map f l₁).zip l₂ = List.map (Prod.map f id) (l₁.zip l₂)

theorem List.zip_map_right {β : Type u_1} {γ : Type u_2} {α : Type u_3} (f : β → γ) (l₁ : List α) (l₂ : List β) : l₁.zip (List.map f l₂) = List.map (Prod.map id f) (l₁.zip l₂)

theorem List.zip_append {α : Type u_1} {β : Type u_2} {l₁ : List α} {r₁ : List α} {l₂ : List β} {r₂ : List β} (_h : l₁.length = l₂.length) : (l₁ ++ r₁).zip (l₂ ++ r₂) = l₁.zip l₂ ++ r₁.zip r₂

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

theorem List.of_mem_zip {α : Type u_1} {β : Type u_2} {a : α} {b : β} {l₁ : List α} {l₂ : List β} : (a, b) ∈ l₁.zip l₂ → a ∈ l₁ ∧ b ∈ l₂

theorem List.map_fst_zip {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) : l₁.length ≤ l₂.length → List.map Prod.fst (l₁.zip l₂) = l₁

theorem List.map_snd_zip {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) : l₂.length ≤ l₁.length → List.map Prod.snd (l₁.zip l₂) = l₂

@[simp]

theorem List.zip_replicate' {α : Type u_1} {β : Type u_2} {a : α} {b : β} {n : Nat} : (List.replicate n a).zip (List.replicate n b) = List.replicate n (a, b)

See also List.zip_replicate in Init.Data.List.TakeDrop for a generalization with different lengths.

zipWith

theorem List.getElem?_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : α → β → γ} {i : Nat} : (List.zipWith f as bs)[i]? = match as[i]?, bs[i]? with | some a, some b => some (f a b) | x, x_1 => none

@[deprecated List.getElem?_zipWith]

theorem List.get?_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {i : Nat} {f : α → β → γ} : (List.zipWith f as bs).get? i = match as.get? i, bs.get? i with | some a, some b => some (f a b) | x, x_1 => none

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

abbrev List.zipWith_get? {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {i : Nat} {f : α → β → γ} : (List.zipWith f as bs).get? i = match as.get? i, bs.get? i with | some a, some b => some (f a b) | x, x_1 => none

Equations

• @List.zipWith_get? = @List.get?_zipWith

@[simp]

theorem List.zipWith_map {γ : Type u_1} {δ : Type u_2} {α : Type u_3} {β : Type u_4} {μ : Type u_5} (f : γ → δ → μ) (g : α → γ) (h : β → δ) (l₁ : List α) (l₂ : List β) : List.zipWith f (List.map g l₁) (List.map h l₂) = List.zipWith (fun (a : α) (b : β) => f (g a) (h b)) l₁ l₂

theorem List.zipWith_map_left {α : Type u_1} {β : Type u_2} {α' : Type u_3} {γ : Type u_4} (l₁ : List α) (l₂ : List β) (f : α → α') (g : α' → β → γ) : List.zipWith g (List.map f l₁) l₂ = List.zipWith (fun (a : α) (b : β) => g (f a) b) l₁ l₂

theorem List.zipWith_map_right {α : Type u_1} {β : Type u_2} {β' : Type u_3} {γ : Type u_4} (l₁ : List α) (l₂ : List β) (f : β → β') (g : α → β' → γ) : List.zipWith g l₁ (List.map f l₂) = List.zipWith (fun (a : α) (b : β) => g a (f b)) l₁ l₂

theorem List.zipWith_foldr_eq_zip_foldr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l₁ : List α} {l₂ : List β} {g : γ → δ → δ} {f : α → β → γ} (i : δ) : List.foldr g i (List.zipWith f l₁ l₂) = List.foldr (fun (p : α × β) (r : δ) => g (f p.fst p.snd) r) i (l₁.zip l₂)

theorem List.zipWith_foldl_eq_zip_foldl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l₁ : List α} {l₂ : List β} {g : δ → γ → δ} {f : α → β → γ} (i : δ) : List.foldl g i (List.zipWith f l₁ l₂) = List.foldl (fun (r : δ) (p : α × β) => g r (f p.fst p.snd)) i (l₁.zip l₂)

@[simp]

theorem List.zipWith_eq_nil_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {l : List α} {l' : List β} : List.zipWith f l l' = [] ↔ l = [] ∨ l' = []

theorem List.map_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ → α) (l : List γ) (l' : List δ) : List.map f (List.zipWith g l l') = List.zipWith (fun (x : γ) (y : δ) => f (g x y)) l l'

theorem List.zipWith_distrib_take : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {l : List α} {l' : List α_1} {n : Nat}, List.take n (List.zipWith f l l') = List.zipWith f (List.take n l) (List.take n l')

theorem List.zipWith_distrib_drop : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {l : List α} {l' : List α_1} {n : Nat}, List.drop n (List.zipWith f l l') = List.zipWith f (List.drop n l) (List.drop n l')

theorem List.zipWith_append {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (l : List α) (la : List α) (l' : List β) (lb : List β) (h : l.length = l'.length) : List.zipWith f (l ++ la) (l' ++ lb) = List.zipWith f l l' ++ List.zipWith f la lb

@[simp]

theorem List.zipWith_replicate' {α : Type u_1} {β : Type u_2} : ∀ {α_1 : Type u_3} {f : α → β → α_1} {a : α} {b : β} {n : Nat}, List.zipWith f (List.replicate n a) (List.replicate n b) = List.replicate n (f a b)

See also List.zipWith_replicate in Init.Data.List.TakeDrop for a generalization with different lengths.

zipWithAll

theorem List.getElem?_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : Option α → Option β → γ} {i : Nat} : (List.zipWithAll f as bs)[i]? = match as[i]?, bs[i]? with | none, none => none | a?, b? => some (f a? b?)

@[deprecated List.getElem?_zipWithAll]

theorem List.get?_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {i : Nat} {f : Option α → Option β → γ} : (List.zipWithAll f as bs).get? i = match as.get? i, bs.get? i with | none, none => none | a?, b? => some (f a? b?)

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

abbrev List.zipWithAll_get? {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {i : Nat} {f : Option α → Option β → γ} : (List.zipWithAll f as bs).get? i = match as.get? i, bs.get? i with | none, none => none | a?, b? => some (f a? b?)

Equations

• @List.zipWithAll_get? = @List.get?_zipWithAll

theorem List.zipWithAll_map {γ : Type u_1} {δ : Type u_2} {α : Type u_1} {β : Type u_2} {μ : Type u_3} (f : Option γ → Option δ → μ) (g : α → γ) (h : β → δ) (l₁ : List α) (l₂ : List β) : List.zipWithAll f (List.map g l₁) (List.map h l₂) = List.zipWithAll (fun (a : Option α) (b : Option β) => f (g <$> a) (h <$> b)) l₁ l₂

theorem List.zipWithAll_map_left {α : Type u_1} {β : Type u_2} {α' : Type u_1} {γ : Type u_3} (l₁ : List α) (l₂ : List β) (f : α → α') (g : Option α' → Option β → γ) : List.zipWithAll g (List.map f l₁) l₂ = List.zipWithAll (fun (a : Option α) (b : Option β) => g (f <$> a) b) l₁ l₂

theorem List.zipWithAll_map_right {α : Type u_1} {β : Type u_2} {β' : Type u_2} {γ : Type u_3} (l₁ : List α) (l₂ : List β) (f : β → β') (g : Option α → Option β' → γ) : List.zipWithAll g l₁ (List.map f l₂) = List.zipWithAll (fun (a : Option α) (b : Option β) => g a (f <$> b)) l₁ l₂

theorem List.map_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : Option γ → Option δ → α) (l : List γ) (l' : List δ) : List.map f (List.zipWithAll g l l') = List.zipWithAll (fun (x : Option γ) (y : Option δ) => f (g x y)) l l'

@[simp]

theorem List.zipWithAll_replicate {α : Type u_1} {β : Type u_2} : ∀ {α_1 : Type u_3} {f : Option α → Option β → α_1} {a : α} {b : β} {n : Nat}, List.zipWithAll f (List.replicate n a) (List.replicate n b) = List.replicate n (f (some a) (some b))

unzip

@[simp]

theorem List.unzip_replicate {α : Type u_1} {β : Type u_2} {n : Nat} {a : α} {b : β} : (List.replicate n (a, b)).unzip = (List.replicate n a, List.replicate n b)

Ranges and enumeration

enumFrom

@[simp]

theorem List.enumFrom_length {α : Type u_1} {n : Nat} {l : List α} : (List.enumFrom n l).length = l.length

theorem List.map_enumFrom {α : Type u_1} {β : Type u_2} (f : α → β) (n : Nat) (l : List α) : List.map (Prod.map id f) (List.enumFrom n l) = List.enumFrom n (List.map f l)

enum

@[simp]

theorem List.enum_length : ∀ {α : Type u_1} {l : List α}, l.enum.length = l.length

theorem List.enum_cons : ∀ {α : Type u_1} {a : α} {as : List α}, (a :: as).enum = (0, a) :: List.enumFrom 1 as

theorem List.map_enum {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : List.map (Prod.map id f) l.enum = (List.map f l).enum

Minima and maxima

minimum?

@[simp]

theorem List.minimum?_nil {α : Type u_1} [Min α] : [].minimum? = none

theorem List.minimum?_cons {α : Type u_1} {x : α} [Min α] {xs : List α} : (x :: xs).minimum? = some (List.foldl min x xs)

@[simp]

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

theorem List.minimum?_mem {α : Type u_1} {a : α} [Min α] (min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b) {xs : List α} : xs.minimum? = some a → a ∈ xs

theorem List.le_minimum?_iff {α : Type u_1} {a : α} [Min α] [LE α] (le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} : xs.minimum? = some a → ∀ (x : α), x ≤ a ↔ ∀ (b : α), b ∈ xs → x ≤ b

theorem List.minimum?_eq_some_iff {α : Type u_1} {a : α} [Min α] [LE α] [anti : Antisymm fun (x x_1 : α) => x ≤ x_1] (le_refl : ∀ (a : α), a ≤ a) (min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b) (le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} : xs.minimum? = some a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → a ≤ b

theorem List.minimum?_replicate {α : Type u_1} [Min α] {n : Nat} {a : α} (w : min a a = a) : (List.replicate n a).minimum? = if n = 0 then none else some a

@[simp]

theorem List.minimum?_replicate_of_pos {α : Type u_1} [Min α] {n : Nat} {a : α} (w : min a a = a) (h : 0 < n) : (List.replicate n a).minimum? = some a

maximum?

@[simp]

theorem List.maximum?_nil {α : Type u_1} [Max α] : [].maximum? = none

theorem List.maximum?_cons {α : Type u_1} {x : α} [Max α] {xs : List α} : (x :: xs).maximum? = some (List.foldl max x xs)

@[simp]

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

theorem List.maximum?_mem {α : Type u_1} {a : α} [Max α] (min_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b) {xs : List α} : xs.maximum? = some a → a ∈ xs

theorem List.maximum?_le_iff {α : Type u_1} {a : α} [Max α] [LE α] (max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} : xs.maximum? = some a → ∀ (x : α), a ≤ x ↔ ∀ (b : α), b ∈ xs → b ≤ x

theorem List.maximum?_eq_some_iff {α : Type u_1} {a : α} [Max α] [LE α] [anti : Antisymm fun (x x_1 : α) => x ≤ x_1] (le_refl : ∀ (a : α), a ≤ a) (max_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b) (max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} : xs.maximum? = some a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → b ≤ a

theorem List.maximum?_replicate {α : Type u_1} [Max α] {n : Nat} {a : α} (w : max a a = a) : (List.replicate n a).maximum? = if n = 0 then none else some a

@[simp]

theorem List.maximum?_replicate_of_pos {α : Type u_1} [Max α] {n : Nat} {a : α} (w : max a a = a) (h : 0 < n) : (List.replicate n a).maximum? = some a

Monadic operations

mapM

def List.mapM' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) : List α → m (List β)

Alternate (non-tail-recursive) form of mapM for proofs.

Equations

• List.mapM' f [] = pure []
• List.mapM' f (a :: l) = do let __do_lift ← f a let __do_lift_1 ← List.mapM' f l pure (__do_lift :: __do_lift_1)

@[simp]

theorem List.mapM'_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {f : α → m β} : List.mapM' f [] = pure []

@[simp]

theorem List.mapM'_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {a : α} {l : List α} [Monad m] {f : α → m β} : List.mapM' f (a :: l) = do let __do_lift ← f a let __do_lift_1 ← List.mapM' f l pure (__do_lift :: __do_lift_1)

theorem List.mapM'_eq_mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) : List.mapM' f l = List.mapM f l

theorem List.mapM'_eq_mapM.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) (acc : List β) : List.mapM.loop f l acc = do let __do_lift ← List.mapM' f l pure (acc.reverse ++ __do_lift)

@[simp]

theorem List.mapM_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) : List.mapM f [] = pure []

@[simp]

theorem List.mapM_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {a : α} {l : List α} [Monad m] [LawfulMonad m] (f : α → m β) : List.mapM f (a :: l) = do let __do_lift ← f a let __do_lift_1 ← List.mapM f l pure (__do_lift :: __do_lift_1)

@[simp]

theorem List.mapM_append {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) {l₁ : List α} {l₂ : List α} : List.mapM f (l₁ ++ l₂) = do let __do_lift ← List.mapM f l₁ let __do_lift_1 ← List.mapM f l₂ pure (__do_lift ++ __do_lift_1)

forM

@[simp]

theorem List.forM_nil' {m : Type u_1 → Type u_2} {α : Type u_3} {f : α → m PUnit} [Monad m] : [].forM f = pure PUnit.unit

@[simp]

theorem List.forM_cons' {m : Type u_1 → Type u_2} : ∀ {α : Type u_3} {a : α} {as : List α} {f : α → m PUnit} [inst : Monad m], (a :: as).forM f = do f a as.forM f