Documentation

Init.Data.List.Nat.Basic

Miscellaneous List lemmas, that require more Nat lemmas than are available in Init.Data.List.Lemmas. #

In particular, omega is available here.

dropLast #

source
theorem List.tail_dropLast {α : Type u_1} {l : List α} :
l.dropLast.tail = l.tail.dropLast
source
@[simp]
theorem List.dropLast_reverse {α : Type u_1} {l : List α} :
l.reverse.dropLast = l.tail.reverse

filter #

source
@[simp]
theorem List.length_filter_pos_iff {α : Type u_1} {l : List α} {p : α → Bool} :
0 < (filter p l).length ↔ ∃ (x : α), x ∈ l ∧ p x = true
source
@[simp]
theorem List.length_filter_lt_length_iff_exists {α✝ : Type u_1} {p : α✝ → Bool} {l : List α✝} :
(filter p l).length < l.length ↔ ∃ (x : α✝), x ∈ l ∧ ¬p x = true

filterMap #

source
@[simp]
theorem List.length_filterMap_pos_iff {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → Option β} :
0 < (filterMap f xs).length ↔ ∃ (x : α), ∃ (x_1 : x ∈ xs), ∃ (b : β), f x = some b
source
@[simp]
theorem List.length_filterMap_lt_length_iff_exists {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → Option β} :
(filterMap f xs).length < xs.length ↔ ∃ (x : α), ∃ (x_1 : x ∈ xs), f x = none

reverse #

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

leftpad #

source
theorem List.length_leftpad {α : Type u_1} {n : Nat} {a : α} {l : List α} :
(leftpad n a l).length = max n l.length

The length of the List returned by List.leftpad n a l is equal to the larger of n and l.length

source
@[reducible, inline, deprecated List.length_leftpad (since := "2025-02-24")]
abbrev List.leftpad_length {α : Type u_1} {n : Nat} {a : α} {l : List α} :
(leftpad n a l).length = max n l.length
Equations
Instances For
    source
    theorem List.length_rightpad {α : Type u_1} {n : Nat} {a : α} {l : List α} :
    (rightpad n a l).length = max n l.length

    intersperse #

    source
    @[simp]
    theorem List.length_intersperse {α : Type u_1} {l : List α} {sep : α} :
    (intersperse sep l).length = 2 * l.length - 1
    source
    @[simp]
    theorem List.getElem?_intersperse_two_mul {α : Type u_1} {l : List α} {sep : α} {i : Nat} :
    (intersperse sep l)[2 * i]? = l[i]?
    source
    theorem List.getElem?_intersperse_two_mul_add_one {α : Type u_1} {l : List α} {sep : α} {i : Nat} (h : i + 1 < l.length) :
    (intersperse sep l)[2 * i + 1]? = some sep
    source
    theorem List.getElem?_intersperse {α : Type u_1} {l : List α} {sep : α} {i : Nat} :
    (intersperse sep l)[i]? = if i % 2 = 0 then l[i / 2]? else if i < 2 * l.length - 1 then some sep else none
    source
    @[simp]
    theorem List.getElem_intersperse_two_mul {α : Type u_1} {l : List α} {sep : α} {i : Nat} (h : 2 * i < (intersperse sep l).length) :
    (intersperse sep l)[2 * i] = l[i]
    source
    @[simp]
    theorem List.getElem_intersperse_two_mul_add_one {α : Type u_1} {l : List α} {sep : α} {i : Nat} (h : 2 * i + 1 < (intersperse sep l).length) :
    (intersperse sep l)[2 * i + 1] = sep
    source
    theorem List.getElem_intersperse {α : Type u_1} {l : List α} {sep : α} {i : Nat} (h : i < (intersperse sep l).length) :
    (intersperse sep l)[i] = if i % 2 = 0 then l[i / 2] else sep
    source
    theorem List.getElem_eq_getElem_intersperse_two_mul {α : Type u_1} {l : List α} {sep : α} {i : Nat} (h : i < l.length) :
    l[i] = (intersperse sep l)[2 * i]

    eraseIdx #

    source
    theorem List.mem_eraseIdx_iff_getElem {α : Type u_1} {x : α} {l : List α} {k : Nat} :
    x ∈ l.eraseIdx k ↔ ∃ (i : Nat), ∃ (h : i < l.length), i ≠ k ∧ l[i] = x
    source
    theorem List.mem_eraseIdx_iff_getElem? {α : Type u_1} {x : α} {l : List α} {k : Nat} :
    x ∈ l.eraseIdx k ↔ ∃ (i : Nat), i ≠ k ∧ l[i]? = some x

    min? #

    source
    theorem List.min?_eq_some_iff' {a : Nat} {xs : List Nat} :
    xs.min? = some a ↔ a ∈ xs ∧ ∀ (b : Nat), b ∈ xs → a ≤ b
    source
    theorem List.min?_get_le_of_mem {l : List Nat} {a : Nat} (h : a ∈ l) :
    l.min?.get ⋯ ≤ a
    source
    theorem List.min?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
    l.min?.getD k ≤ a

    max? #

    source
    theorem List.max?_eq_some_iff' {a : Nat} {xs : List Nat} :
    xs.max? = some a ↔ a ∈ xs ∧ ∀ (b : Nat), b ∈ xs → b ≤ a
    source
    theorem List.le_max?_get_of_mem {l : List Nat} {a : Nat} (h : a ∈ l) :
    a ≤ l.max?.get ⋯
    source
    theorem List.le_max?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
    a ≤ l.max?.getD k