Lemmas about List.range and List.zipIdx

Most of the results are deferred to Data.Init.List.Nat.Range, where more results about natural arithmetic are available.

Ranges and enumeration

range'

theorem List.range'_succ {s n step : Nat} : range' s (n + 1) step = s :: range' (s + step) n step

@[simp]

theorem List.length_range' {s step n : Nat} : (range' s n step).length = n

@[simp]

theorem List.range'_eq_nil_iff {s n step : Nat} : range' s n step = [] ↔ n = 0

@[reducible, inline, deprecated List.range'_eq_nil_iff (since := "2025-01-29")]

abbrev List.range'_eq_nil {s n step : Nat} : range' s n step = [] ↔ n = 0

theorem List.range'_ne_nil_iff (s : Nat) {n step : Nat} : range' s n step ≠ [] ↔ n ≠ 0

@[reducible, inline, deprecated List.range'_ne_nil_iff (since := "2025-01-29")]

abbrev List.range'_ne_nil (s : Nat) {n step : Nat} : range' s n step ≠ [] ↔ n ≠ 0

@[simp]

theorem List.range'_zero {s step : Nat} : range' s 0 step = []

@[simp]

theorem List.range'_one {s step : Nat} : range' s 1 step = [s]

@[simp]

theorem List.tail_range' {s n step : Nat} : (range' s n step).tail = range' (s + step) (n - 1) step

@[simp]

theorem List.range'_inj {s n s' n' : Nat} : range' s n = range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s')

theorem List.mem_range' {s step m n : Nat} : m ∈ range' s n step ↔ ∃ (i : Nat), i < n ∧ m = s + step * i

theorem List.getElem?_range' {s step i n : Nat} : i < n → (range' s n step)[i]? = some (s + step * i)

@[simp]

theorem List.getElem_range' {n m step i : Nat} (H : i < (range' n m step).length) : (range' n m step)[i] = n + step * i

theorem List.head?_range' {s n : Nat} : (range' s n).head? = if n = 0 then none else some s

@[simp]

theorem List.head_range' {s n : Nat} (h : range' s n ≠ []) : (range' s n).head h = s

theorem List.map_add_range' {a : Nat} (s n step : Nat) : map (fun (x : Nat) => a + x) (range' s n step) = range' (a + s) n step

theorem List.range'_succ_left {s n step : Nat} : range' (s + 1) n step = map (fun (x : Nat) => x + 1) (range' s n step)

theorem List.range'_append {s m n step : Nat} : range' s m step ++ range' (s + step * m) n step = range' s (m + n) step

@[simp]

theorem List.range'_append_1 {s m n : Nat} : range' s m ++ range' (s + m) n = range' s (m + n)

theorem List.range'_sublist_right {step s m n : Nat} : (range' s m step).Sublist (range' s n step) ↔ m ≤ n

theorem List.range'_subset_right {step s m n : Nat} (step0 : 0 < step) : range' s m step ⊆ range' s n step ↔ m ≤ n

theorem List.range'_subset_right_1 {s m n : Nat} : range' s m ⊆ range' s n ↔ m ≤ n

theorem List.range'_concat {step s n : Nat} : range' s (n + 1) step = range' s n step ++ [s + step * n]

theorem List.range'_1_concat {s n : Nat} : range' s (n + 1) = range' s n ++ [s + n]

theorem List.range'_eq_cons_iff {s n a : Nat} {xs : List Nat} : range' s n = a :: xs ↔ s = a ∧ 0 < n ∧ xs = range' (a + 1) (n - 1)

range

@[simp]

theorem List.range_one : range 1 = [0]

theorem List.range_loop_range' (s n : Nat) : range.loop s (range' s n) = range' 0 (n + s)

theorem List.range_eq_range' {n : Nat} : range n = range' 0 n

theorem List.getElem?_range {i n : Nat} (h : i < n) : (range n)[i]? = some i

@[simp]

theorem List.getElem_range {j n : Nat} (h : j < (range n).length) : (range n)[j] = j

theorem List.range_succ_eq_map {n : Nat} : range (n + 1) = 0 :: map Nat.succ (range n)

theorem List.range'_eq_map_range {s n : Nat} : range' s n = map (fun (x : Nat) => s + x) (range n)

@[simp]

theorem List.length_range {n : Nat} : (range n).length = n

@[simp]

theorem List.range_eq_nil {n : Nat} : range n = [] ↔ n = 0

theorem List.range_ne_nil {n : Nat} : range n ≠ [] ↔ n ≠ 0

@[simp]

theorem List.tail_range {n : Nat} : (range n).tail = range' 1 (n - 1)

@[simp]

theorem List.range_sublist {m n : Nat} : (range m).Sublist (range n) ↔ m ≤ n

@[simp]

theorem List.range_subset {m n : Nat} : range m ⊆ range n ↔ m ≤ n

theorem List.range_succ {n : Nat} : range n.succ = range n ++ [n]

theorem List.range_add {n m : Nat} : range (n + m) = range n ++ map (fun (x : Nat) => n + x) (range m)

theorem List.head?_range {n : Nat} : (range n).head? = if n = 0 then none else some 0

@[simp]

theorem List.head_range {n : Nat} (h : range n ≠ []) : (range n).head h = 0

theorem List.getLast?_range {n : Nat} : (range n).getLast? = if n = 0 then none else some (n - 1)

@[simp]

theorem List.getLast_range {n : Nat} (h : range n ≠ []) : (range n).getLast h = n - 1

zipIdx

@[simp]

theorem List.zipIdx_eq_nil_iff {α : Type u_1} {l : List α} {i : Nat} : l.zipIdx i = [] ↔ l = []

@[simp]

theorem List.length_zipIdx {α : Type u_1} {l : List α} {i : Nat} : (l.zipIdx i).length = l.length

@[simp]

theorem List.getElem?_zipIdx {α : Type u_1} {l : List α} {i j : Nat} : (l.zipIdx i)[j]? = Option.map (fun (a : α) => (a, i + j)) l[j]?

@[simp]

theorem List.getElem_zipIdx {α : Type u_1} {i j : Nat} {l : List α} (h : i < (l.zipIdx j).length) : (l.zipIdx j)[i] = (l[i], j + i)

@[simp]

theorem List.tail_zipIdx {α : Type u_1} {l : List α} {i : Nat} : (l.zipIdx i).tail = l.tail.zipIdx (i + 1)

theorem List.map_snd_add_zipIdx_eq_zipIdx {α : Type u_1} {l : List α} {n k : Nat} : map (Prod.map id fun (x : Nat) => x + n) (l.zipIdx k) = l.zipIdx (n + k)

theorem List.zipIdx_cons' {α : Type u_1} {i : Nat} {x : α} {xs : List α} : (x :: xs).zipIdx i = (x, i) :: map (Prod.map id fun (x : Nat) => x + 1) (xs.zipIdx i)

@[simp]

theorem List.zipIdx_map_snd {α : Type u_1} (i : Nat) (l : List α) : map Prod.snd (l.zipIdx i) = range' i l.length

@[simp]

theorem List.zipIdx_map_fst {α : Type u_1} (i : Nat) (l : List α) : map Prod.fst (l.zipIdx i) = l

theorem List.zipIdx_eq_zip_range' {α : Type u_1} {l : List α} {i : Nat} : l.zipIdx i = l.zip (range' i l.length)

@[simp]

theorem List.unzip_zipIdx_eq_prod {α : Type u_1} {l : List α} {i : Nat} : (l.zipIdx i).unzip = (l, range' i l.length)

theorem List.zipIdx_succ {α : Type u_1} {l : List α} {i : Nat} : l.zipIdx (i + 1) = map (fun (x : α × Nat) => match x with | (a, i) => (a, i + 1)) (l.zipIdx i)

Replace zipIdx with a starting index n+1 with zipIdx starting from n, followed by a map increasing the indices by one.

theorem List.zipIdx_eq_map_add {α : Type u_1} {l : List α} {i : Nat} : l.zipIdx i = map (fun (x : α × Nat) => match x with | (a, j) => (a, i + j)) l.zipIdx

Replace zipIdx with a starting index with zipIdx starting from 0, followed by a map increasing the indices.

enumFrom

@[simp, deprecated List.zipIdx_eq_nil_iff (since := "2025-01-21")]

theorem List.enumFrom_eq_nil {α : Type u_1} {n : Nat} {l : List α} : enumFrom n l = [] ↔ l = []

@[simp, deprecated List.length_zipIdx (since := "2025-01-21")]

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

@[simp, deprecated List.getElem?_zipIdx (since := "2025-01-21")]

theorem List.getElem?_enumFrom {α : Type u_1} (i : Nat) (l : List α) (j : Nat) : (enumFrom i l)[j]? = Option.map (fun (a : α) => (i + j, a)) l[j]?

@[simp, deprecated List.getElem_zipIdx (since := "2025-01-21")]

theorem List.getElem_enumFrom {α : Type u_1} (l : List α) (n i : Nat) (h : i < (enumFrom n l).length) : (enumFrom n l)[i] = (n + i, l[i])

@[simp, deprecated List.tail_zipIdx (since := "2025-01-21")]

theorem List.tail_enumFrom {α : Type u_1} (l : List α) (n : Nat) : (enumFrom n l).tail = enumFrom (n + 1) l.tail

@[simp, deprecated List.map_snd_add_zipIdx_eq_zipIdx (since := "2025-01-21")]

theorem List.map_fst_add_enumFrom_eq_enumFrom {α : Type u_1} (l : List α) (n k : Nat) : map (Prod.map (fun (x : Nat) => x + n) id) (enumFrom k l) = enumFrom (n + k) l

@[simp, deprecated List.map_snd_add_zipIdx_eq_zipIdx (since := "2025-01-21")]

theorem List.map_fst_add_enum_eq_enumFrom {α : Type u_1} (l : List α) (n : Nat) : map (Prod.map (fun (x : Nat) => x + n) id) l.enum = enumFrom n l

@[simp, deprecated List.zipIdx_cons' (since := "2025-01-21")]

theorem List.enumFrom_cons' {α : Type u_1} (n : Nat) (x : α) (xs : List α) : enumFrom n (x :: xs) = (n, x) :: map (Prod.map (fun (x : Nat) => x + 1) id) (enumFrom n xs)

@[simp, deprecated List.zipIdx_map_snd (since := "2025-01-21")]

theorem List.enumFrom_map_fst {α : Type u_1} (n : Nat) (l : List α) : map Prod.fst (enumFrom n l) = range' n l.length

@[simp, deprecated List.zipIdx_map_fst (since := "2025-01-21")]

theorem List.enumFrom_map_snd {α : Type u_1} (n : Nat) (l : List α) : map Prod.snd (enumFrom n l) = l

@[deprecated List.zipIdx_eq_zip_range' (since := "2025-01-21")]

theorem List.enumFrom_eq_zip_range' {α : Type u_1} (l : List α) {n : Nat} : enumFrom n l = (range' n l.length).zip l

@[simp, deprecated List.unzip_zipIdx_eq_prod (since := "2025-01-21")]

theorem List.unzip_enumFrom_eq_prod {α : Type u_1} (l : List α) {n : Nat} : (enumFrom n l).unzip = (range' n l.length, l)

enum

@[deprecated List.zipIdx_cons (since := "2025-01-21")]

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

@[deprecated List.zipIdx_cons (since := "2025-01-21")]

theorem List.enum_cons' {α : Type u_1} (x : α) (xs : List α) : (x :: xs).enum = (0, x) :: map (Prod.map (fun (x : Nat) => x + 1) id) xs.enum

@[deprecated "These are now both `l.zipIdx 0`" (since := "2025-01-21")]

theorem List.enum_eq_enumFrom {α : Type u_1} {l : List α} : l.enum = enumFrom 0 l

@[deprecated "Use the reverse direction of `map_snd_add_zipIdx_eq_zipIdx` instead" (since := "2025-01-21")]

theorem List.enumFrom_eq_map_enum {α : Type u_1} (l : List α) (n : Nat) : enumFrom n l = map (Prod.map (fun (x : Nat) => x + n) id) l.enum