Documentation

Init.Data.List.Nat.Range

Lemmas about List.range and List.enum #

Ranges and enumeration #

range' #

@[simp]
theorem List.mem_range'_1 {s n m : Nat} :
m range' s n s m m < s + n
theorem List.getLast?_range' {s : Nat} (n : Nat) :
(range' s n).getLast? = if n = 0 then none else some (s + n - 1)
@[simp]
theorem List.getLast_range' {s : Nat} (n : Nat) (h : range' s n []) :
(range' s n).getLast h = s + n - 1
theorem List.pairwise_lt_range' (s n : Nat) (step : Nat := 1) (pos : 0 < step := by simp) :
Pairwise (fun (x1 x2 : Nat) => x1 < x2) (range' s n step)
theorem List.pairwise_le_range' (s n : Nat) (step : Nat := 1) :
Pairwise (fun (x1 x2 : Nat) => x1 x2) (range' s n step)
theorem List.nodup_range' (s n : Nat) (step : Nat := 1) (h : 0 < step := by simp) :
(range' s n step).Nodup
theorem List.map_sub_range' {step : Nat} (a s n : Nat) (h : a s) :
map (fun (x : Nat) => x - a) (range' s n step) = range' (s - a) n step
@[simp]
theorem List.range'_eq_singleton_iff {s n a : Nat} :
range' s n = [a] s = a n = 1
@[reducible, inline, deprecated List.range'_eq_singleton_iff (since := "2025-01-29")]
abbrev List.range'_eq_singleton {s n a : Nat} :
range' s n = [a] s = a n = 1
Equations
Instances For
    theorem List.range'_eq_append_iff {s n : Nat} {xs ys : List Nat} :
    range' s n = xs ++ ys (k : Nat), k n xs = range' s k ys = range' (s + k) (n - k)
    @[simp]
    theorem List.find?_range'_eq_some {s n i : Nat} {p : NatBool} :
    find? p (range' s n) = some i p i = true i range' s n ∀ (j : Nat), s jj < i → (!p j) = true
    theorem List.find?_range'_eq_none {s n : Nat} {p : NatBool} :
    find? p (range' s n) = none ∀ (i : Nat), s ii < s + n → (!p i) = true
    theorem List.erase_range' {s n i : Nat} :
    (range' s n).erase i = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

    range #

    theorem List.reverse_range' (s n : Nat) :
    (range' s n).reverse = map (fun (x : Nat) => s + n - 1 - x) (range n)
    @[simp]
    theorem List.mem_range {m n : Nat} :
    m range n m < n
    theorem List.pairwise_lt_range (n : Nat) :
    Pairwise (fun (x1 x2 : Nat) => x1 < x2) (range n)
    theorem List.pairwise_le_range (n : Nat) :
    Pairwise (fun (x1 x2 : Nat) => x1 x2) (range n)
    @[simp]
    theorem List.take_range (m n : Nat) :
    take m (range n) = range (min m n)
    @[simp]
    theorem List.find?_range_eq_some {n i : Nat} {p : NatBool} :
    find? p (range n) = some i p i = true i range n ∀ (j : Nat), j < i → (!p j) = true
    theorem List.find?_range_eq_none {n : Nat} {p : NatBool} :
    find? p (range n) = none ∀ (i : Nat), i < n → (!p i) = true
    theorem List.erase_range {n i : Nat} :
    (range n).erase i = range (min n i) ++ range' (i + 1) (n - (i + 1))

    iota #

    @[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
    @[simp, deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
    theorem List.length_iota (n : Nat) :
    (iota n).length = n
    @[simp, deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
    theorem List.iota_eq_nil {n : Nat} :
    iota n = [] n = 0
    @[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
    theorem List.iota_ne_nil {n : Nat} :
    iota n [] n 0
    @[simp, deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
    theorem List.mem_iota {m n : Nat} :
    m iota n 0 < m m n
    @[simp, deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
    theorem List.iota_inj {n n' : Nat} :
    iota n = iota n' n = n'
    @[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
    theorem List.iota_eq_cons_iff {n a : Nat} {xs : List Nat} :
    iota n = a :: xs n = a 0 < n xs = iota (n - 1)
    @[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
    theorem List.iota_eq_append_iff {n : Nat} {xs ys : List Nat} :
    iota n = xs ++ ys (k : Nat), k n xs = (range' (k + 1) (n - k)).reverse ys = iota k
    @[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
    theorem List.pairwise_gt_iota (n : Nat) :
    Pairwise (fun (x1 x2 : Nat) => x1 > x2) (iota n)
    @[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
    theorem List.nodup_iota (n : Nat) :
    @[simp, deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
    theorem List.head?_iota (n : Nat) :
    @[simp, deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
    theorem List.head_iota (n : Nat) (h : iota n []) :
    (iota n).head h = n
    @[simp, deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
    theorem List.tail_iota (n : Nat) :
    (iota n).tail = iota (n - 1)
    @[simp, deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
    theorem List.reverse_iota {n : Nat} :
    @[simp, deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
    @[simp, deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
    theorem List.getLast_iota (n : Nat) (h : iota n []) :
    (iota n).getLast h = 1
    @[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
    theorem List.find?_iota_eq_none {n : Nat} {p : NatBool} :
    find? p (iota n) = none ∀ (i : Nat), 0 < ii n → (!p i) = true
    @[simp, deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
    theorem List.find?_iota_eq_some {n i : Nat} {p : NatBool} :
    find? p (iota n) = some i p i = true i iota n ∀ (j : Nat), i < jj n → (!p j) = true

    zipIdx #

    @[simp]
    theorem List.zipIdx_singleton {α : Type u_1} (x : α) (k : Nat) :
    @[simp]
    theorem List.head?_zipIdx {α : Type u_1} (l : List α) (k : Nat) :
    (l.zipIdx k).head? = Option.map (fun (a : α) => (a, k)) l.head?
    @[simp]
    theorem List.getLast?_zipIdx {α : Type u_1} (l : List α) (k : Nat) :
    (l.zipIdx k).getLast? = Option.map (fun (a : α) => (a, k + l.length - 1)) l.getLast?
    theorem List.mk_add_mem_zipIdx_iff_getElem? {α : Type u_1} {k i : Nat} {x : α} {l : List α} :
    (x, k + i) l.zipIdx k l[i]? = some x
    theorem List.mk_mem_zipIdx_iff_le_and_getElem?_sub {α : Type u_1} {k i : Nat} {x : α} {l : List α} :
    (x, i) l.zipIdx k k i l[i - k]? = some x
    theorem List.mk_mem_zipIdx_iff_getElem? {α : Type u_1} {i : Nat} {x : α} {l : List α} :

    Variant of mk_mem_zipIdx_iff_le_and_getElem?_sub specialized at k = 0, to avoid the inequality and the subtraction.

    theorem List.mem_zipIdx_iff_le_and_getElem?_sub {α : Type u_1} {x : α × Nat} {l : List α} {k : Nat} :
    x l.zipIdx k k x.snd l[x.snd - k]? = some x.fst
    theorem List.mem_zipIdx_iff_getElem? {α : Type u_1} {x : α × Nat} {l : List α} :

    Variant of mem_zipIdx_iff_le_and_getElem?_sub specialized at k = 0, to avoid the inequality and the subtraction.

    theorem List.le_snd_of_mem_zipIdx {α : Type u_1} {x : α × Nat} {k : Nat} {l : List α} (h : x l.zipIdx k) :
    k x.snd
    theorem List.snd_lt_add_of_mem_zipIdx {α : Type u_1} {x : α × Nat} {l : List α} {k : Nat} (h : x l.zipIdx k) :
    x.snd < k + l.length
    theorem List.snd_lt_of_mem_zipIdx {α : Type u_1} {x : α × Nat} {l : List α} {k : Nat} (h : x l.zipIdx k) :
    x.snd < l.length + k
    theorem List.map_zipIdx {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) (k : Nat) :
    map (Prod.map f id) (l.zipIdx k) = (map f l).zipIdx k
    theorem List.fst_mem_of_mem_zipIdx {α : Type u_1} {x : α × Nat} {l : List α} {k : Nat} (h : x l.zipIdx k) :
    x.fst l
    theorem List.fst_eq_of_mem_zipIdx {α : Type u_1} {x : α × Nat} {l : List α} {k : Nat} (h : x l.zipIdx k) :
    x.fst = l[x.snd - k]
    theorem List.mem_zipIdx {α : Type u_1} {x : α} {i : Nat} {xs : List α} {k : Nat} (h : (x, i) xs.zipIdx k) :
    k i i < k + xs.length x = xs[i - k]
    theorem List.mem_zipIdx' {α : Type u_1} {x : α} {i : Nat} {xs : List α} (h : (x, i) xs.zipIdx) :
    i < xs.length x = xs[i]

    Variant of mem_zipIdx specialized at k = 0.

    theorem List.zipIdx_map {α : Type u_1} {β : Type u_2} (l : List α) (k : Nat) (f : αβ) :
    (map f l).zipIdx k = map (Prod.map f id) (l.zipIdx k)
    theorem List.zipIdx_append {α : Type u_1} (xs ys : List α) (k : Nat) :
    (xs ++ ys).zipIdx k = xs.zipIdx k ++ ys.zipIdx (k + xs.length)
    theorem List.zipIdx_eq_cons_iff {α : Type u_1} {x : α × Nat} {l' : List (α × Nat)} {l : List α} {k : Nat} :
    l.zipIdx k = x :: l' (a : α), (as : List α), l = a :: as x = (a, k) l' = as.zipIdx (k + 1)
    theorem List.zipIdx_eq_append_iff {α : Type u_1} {l₁ l₂ : List (α × Nat)} {l : List α} {k : Nat} :
    l.zipIdx k = l₁ ++ l₂ (l₁' : List α), (l₂' : List α), l = l₁' ++ l₂' l₁ = l₁'.zipIdx k l₂ = l₂'.zipIdx (k + l₁'.length)

    enumFrom #

    @[simp, deprecated List.zipIdx_singleton (since := "2025-01-21")]
    theorem List.enumFrom_singleton {α : Type u_1} (x : α) (n : Nat) :
    @[simp, deprecated List.head?_zipIdx (since := "2025-01-21")]
    theorem List.head?_enumFrom {α : Type u_1} (n : Nat) (l : List α) :
    (enumFrom n l).head? = Option.map (fun (a : α) => (n, a)) l.head?
    @[simp, deprecated List.getLast?_zipIdx (since := "2025-01-21")]
    theorem List.getLast?_enumFrom {α : Type u_1} (n : Nat) (l : List α) :
    (enumFrom n l).getLast? = Option.map (fun (a : α) => (n + l.length - 1, a)) l.getLast?
    @[deprecated List.mk_add_mem_zipIdx_iff_getElem? (since := "2025-01-21")]
    theorem List.mk_add_mem_enumFrom_iff_getElem? {α : Type u_1} {n i : Nat} {x : α} {l : List α} :
    (n + i, x) enumFrom n l l[i]? = some x
    @[deprecated List.mk_mem_zipIdx_iff_le_and_getElem?_sub (since := "2025-01-21")]
    theorem List.mk_mem_enumFrom_iff_le_and_getElem?_sub {α : Type u_1} {n i : Nat} {x : α} {l : List α} :
    (i, x) enumFrom n l n i l[i - n]? = some x
    @[deprecated List.le_snd_of_mem_zipIdx (since := "2025-01-21")]
    theorem List.le_fst_of_mem_enumFrom {α : Type u_1} {x : Nat × α} {n : Nat} {l : List α} (h : x enumFrom n l) :
    n x.fst
    @[deprecated List.snd_lt_add_of_mem_zipIdx (since := "2025-01-21")]
    theorem List.fst_lt_add_of_mem_enumFrom {α : Type u_1} {x : Nat × α} {n : Nat} {l : List α} (h : x enumFrom n l) :
    x.fst < n + l.length
    @[deprecated List.map_zipIdx (since := "2025-01-21")]
    theorem List.map_enumFrom {α : Type u_1} {β : Type u_2} (f : αβ) (n : Nat) (l : List α) :
    map (Prod.map id f) (enumFrom n l) = enumFrom n (map f l)
    @[deprecated List.fst_mem_of_mem_zipIdx (since := "2025-01-21")]
    theorem List.snd_mem_of_mem_enumFrom {α : Type u_1} {x : Nat × α} {n : Nat} {l : List α} (h : x enumFrom n l) :
    x.snd l
    @[deprecated List.fst_eq_of_mem_zipIdx (since := "2025-01-21")]
    theorem List.snd_eq_of_mem_enumFrom {α : Type u_1} {x : Nat × α} {n : Nat} {l : List α} (h : x enumFrom n l) :
    x.snd = l[x.fst - n]
    @[deprecated List.mem_zipIdx (since := "2025-01-21")]
    theorem List.mem_enumFrom {α : Type u_1} {x : α} {i j : Nat} {xs : List α} (h : (i, x) enumFrom j xs) :
    j i i < j + xs.length x = xs[i - j]
    @[deprecated List.zipIdx_map (since := "2025-01-21")]
    theorem List.enumFrom_map {α : Type u_1} {β : Type u_2} (n : Nat) (l : List α) (f : αβ) :
    enumFrom n (map f l) = map (Prod.map id f) (enumFrom n l)
    @[deprecated List.zipIdx_append (since := "2025-01-21")]
    theorem List.enumFrom_append {α : Type u_1} (xs ys : List α) (n : Nat) :
    enumFrom n (xs ++ ys) = enumFrom n xs ++ enumFrom (n + xs.length) ys
    @[deprecated List.zipIdx_eq_cons_iff (since := "2025-01-21")]
    theorem List.enumFrom_eq_cons_iff {α : Type u_1} {x : Nat × α} {l' : List (Nat × α)} {l : List α} {n : Nat} :
    enumFrom n l = x :: l' (a : α), (as : List α), l = a :: as x = (n, a) l' = enumFrom (n + 1) as
    @[deprecated List.zipIdx_eq_append_iff (since := "2025-01-21")]
    theorem List.enumFrom_eq_append_iff {α : Type u_1} {l₁ l₂ : List (Nat × α)} {l : List α} {n : Nat} :
    enumFrom n l = l₁ ++ l₂ (l₁' : List α), (l₂' : List α), l = l₁' ++ l₂' l₁ = enumFrom n l₁' l₂ = enumFrom (n + l₁'.length) l₂'

    enum #

    @[simp, deprecated List.zipIdx_eq_nil_iff (since := "2025-01-21")]
    theorem List.enum_eq_nil_iff {α : Type u_1} {l : List α} :
    l.enum = [] l = []
    @[deprecated List.zipIdx_eq_nil_iff (since := "2024-11-04")]
    theorem List.enum_eq_nil {α : Type u_1} {l : List α} :
    l.enum = [] l = []
    @[simp, deprecated List.zipIdx_singleton (since := "2025-01-21")]
    theorem List.enum_singleton {α : Type u_1} (x : α) :
    @[simp, deprecated List.length_zipIdx (since := "2025-01-21")]
    theorem List.enum_length {α✝ : Type u_1} {l : List α✝} :
    @[simp, deprecated List.getElem?_zipIdx (since := "2025-01-21")]
    theorem List.getElem?_enum {α : Type u_1} (l : List α) (n : Nat) :
    l.enum[n]? = Option.map (fun (a : α) => (n, a)) l[n]?
    @[simp, deprecated List.getElem_zipIdx (since := "2025-01-21")]
    theorem List.getElem_enum {α : Type u_1} (l : List α) (i : Nat) (h : i < l.enum.length) :
    l.enum[i] = (i, l[i])
    @[simp, deprecated List.head?_zipIdx (since := "2025-01-21")]
    theorem List.head?_enum {α : Type u_1} (l : List α) :
    l.enum.head? = Option.map (fun (a : α) => (0, a)) l.head?
    @[simp, deprecated List.getLast?_zipIdx (since := "2025-01-21")]
    theorem List.getLast?_enum {α : Type u_1} (l : List α) :
    l.enum.getLast? = Option.map (fun (a : α) => (l.length - 1, a)) l.getLast?
    @[simp, deprecated List.tail_zipIdx (since := "2025-01-21")]
    theorem List.tail_enum {α : Type u_1} (l : List α) :
    @[deprecated List.mk_mem_zipIdx_iff_getElem? (since := "2025-01-21")]
    theorem List.mk_mem_enum_iff_getElem? {α : Type u_1} {i : Nat} {x : α} {l : List α} :
    (i, x) l.enum l[i]? = some x
    @[deprecated List.mem_zipIdx_iff_getElem? (since := "2025-01-21")]
    theorem List.mem_enum_iff_getElem? {α : Type u_1} {x : Nat × α} {l : List α} :
    @[deprecated List.snd_lt_of_mem_zipIdx (since := "2025-01-21")]
    theorem List.fst_lt_of_mem_enum {α : Type u_1} {x : Nat × α} {l : List α} (h : x l.enum) :
    @[deprecated List.fst_mem_of_mem_zipIdx (since := "2025-01-21")]
    theorem List.snd_mem_of_mem_enum {α : Type u_1} {x : Nat × α} {l : List α} (h : x l.enum) :
    x.snd l
    @[deprecated List.fst_eq_of_mem_zipIdx (since := "2025-01-21")]
    theorem List.snd_eq_of_mem_enum {α : Type u_1} {x : Nat × α} {l : List α} (h : x l.enum) :
    x.snd = l[x.fst]
    @[deprecated List.mem_zipIdx (since := "2025-01-21")]
    theorem List.mem_enum {α : Type u_1} {x : α} {i : Nat} {xs : List α} (h : (i, x) xs.enum) :
    i < xs.length x = xs[i]
    @[deprecated List.map_zipIdx (since := "2025-01-21")]
    theorem List.map_enum {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) :
    map (Prod.map id f) l.enum = (map f l).enum
    @[simp, deprecated List.zipIdx_map_snd (since := "2025-01-21")]
    theorem List.enum_map_fst {α : Type u_1} (l : List α) :
    @[simp, deprecated List.zipIdx_map_fst (since := "2025-01-21")]
    theorem List.enum_map_snd {α : Type u_1} (l : List α) :
    @[deprecated List.zipIdx_map (since := "2025-01-21")]
    theorem List.enum_map {α : Type u_1} {β : Type u_2} (l : List α) (f : αβ) :
    (map f l).enum = map (Prod.map id f) l.enum
    @[deprecated List.zipIdx_append (since := "2025-01-21")]
    theorem List.enum_append {α : Type u_1} (xs ys : List α) :
    (xs ++ ys).enum = xs.enum ++ enumFrom xs.length ys
    @[deprecated List.zipIdx_eq_zip_range' (since := "2025-01-21")]
    theorem List.enum_eq_zip_range {α : Type u_1} (l : List α) :
    @[simp, deprecated List.unzip_zipIdx_eq_prod (since := "2025-01-21")]
    theorem List.unzip_enum_eq_prod {α : Type u_1} (l : List α) :
    @[deprecated List.zipIdx_eq_cons_iff (since := "2025-01-21")]
    theorem List.enum_eq_cons_iff {α : Type u_1} {x : Nat × α} {l' : List (Nat × α)} {l : List α} :
    l.enum = x :: l' (a : α), (as : List α), l = a :: as x = (0, a) l' = enumFrom 1 as
    @[deprecated List.zipIdx_eq_append_iff (since := "2025-01-21")]
    theorem List.enum_eq_append_iff {α : Type u_1} {l₁ l₂ : List (Nat × α)} {l : List α} :
    l.enum = l₁ ++ l₂ (l₁' : List α), (l₂' : List α), l = l₁' ++ l₂' l₁ = l₁'.enum l₂ = enumFrom l₁'.length l₂'