feat: rename List.enum(From) to List.zipIdx, and `Array/Vector.zi…

…pWithIndex` to `zipIdx` (#6800)

This PR uniformizes the naming of `enum`/`enumFrom` (on `List`) and
`zipWithIndex` (on `Array` on `Vector`), replacing all with `zipIdx`. At
the same time, we generalize to add an optional `Nat` parameter for the
initial value of the index (which previously existed, only for `List`,
as the separate function `enumFrom`).

src/Init/Data/Array/Basic.lean

@@ -605,8 +605,10 @@ def mapIdx {α : Type u} {β : Type v} (f : Nat → α → β) (as : Array α) :
   Id.run <| as.mapIdxM f
 
 /-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/
-def zipWithIndex (arr : Array α) : Array (α × Nat) :=
-  arr.mapIdx fun i a => (a, i)
+def zipIdx (arr : Array α) (start := 0) : Array (α × Nat) :=
+  arr.mapIdx fun i a => (a, i + start)
+
+@[deprecated zipIdx (since := "2025-01-21")] abbrev zipWithIndex := @zipIdx
 
 @[inline]
 def find? {α : Type u} (p : α → Bool) (as : Array α) : Option α :=

src/Init/Data/Array/MapIdx.lean

@@ -48,9 +48,11 @@ theorem mapFinIdx_spec (as : Array α) (f : (i : Nat) → α → (h : i < as.siz
     (a.mapFinIdx f).size = a.size :=
   (mapFinIdx_spec (p := fun _ _ _ => True) (hs := fun _ _ => trivial)).1
 
-@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
+@[simp] theorem size_zipIdx (as : Array α) (k : Nat) : (as.zipIdx k).size = as.size :=
   Array.size_mapFinIdx _ _
 
+@[deprecated size_zipIdx (since := "2025-01-21")] abbrev size_zipWithIndex := @size_zipIdx
+
 @[simp] theorem getElem_mapFinIdx (a : Array α) (f : (i : Nat) → α → (h : i < a.size) → β) (i : Nat)
     (h : i < (mapFinIdx a f).size) :
     (a.mapFinIdx f)[i] = f i (a[i]'(by simp_all))  (by simp_all) :=
@@ -115,34 +117,58 @@ end List
 
 namespace Array
 
-/-! ### zipWithIndex -/
+/-! ### zipIdx -/
+
+@[simp] theorem getElem_zipIdx (a : Array α) (k : Nat) (i : Nat) (h : i < (a.zipIdx k).size) :
+    (a.zipIdx k)[i] = (a[i]'(by simp_all), i + k) := by
+  simp [zipIdx]
 
-@[simp] theorem getElem_zipWithIndex (a : Array α) (i : Nat) (h : i < a.zipWithIndex.size) :
-    (a.zipWithIndex)[i] = (a[i]'(by simp_all), i) := by
-  simp [zipWithIndex]
+@[deprecated getElem_zipIdx (since := "2025-01-21")]
+abbrev getElem_zipWithIndex := @getElem_zipIdx
 
-@[simp] theorem zipWithIndex_toArray {l : List α} :
-    l.toArray.zipWithIndex = (l.enum.map fun (i, x) => (x, i)).toArray := by
-  ext i hi₁ hi₂ <;> simp
+@[simp] theorem zipIdx_toArray {l : List α} {k : Nat} :
+    l.toArray.zipIdx k = (l.zipIdx k).toArray := by
+  ext i hi₁ hi₂ <;> simp [Nat.add_comm]
 
-@[simp] theorem toList_zipWithIndex (a : Array α) :
-    a.zipWithIndex.toList = a.toList.enum.map (fun (i, a) => (a, i)) := by
+@[deprecated zipIdx_toArray (since := "2025-01-21")]
+abbrev zipWithIndex_toArray := @zipIdx_toArray
+
+@[simp] theorem toList_zipIdx (a : Array α) (k : Nat) :
+    (a.zipIdx k).toList = a.toList.zipIdx k := by
   rcases a with ⟨a⟩
   simp
 
-theorem mk_mem_zipWithIndex_iff_getElem? {x : α} {i : Nat} {l : Array α} :
-    (x, i) ∈ l.zipWithIndex ↔ l[i]? = x := by
+@[deprecated toList_zipIdx (since := "2025-01-21")]
+abbrev toList_zipWithIndex := @toList_zipIdx
+
+theorem mk_mem_zipIdx_iff_le_and_getElem?_sub {k i : Nat} {x : α} {l : Array α} :
+    (x, i) ∈ zipIdx l k ↔ k ≤ i ∧ l[i - k]? = some x := by
   rcases l with ⟨l⟩
-  simp only [zipWithIndex_toArray, mem_toArray, List.mem_map, Prod.mk.injEq, Prod.exists,
-    List.mk_mem_enum_iff_getElem?, List.getElem?_toArray]
-  constructor
-  · rintro ⟨a, b, h, rfl, rfl⟩
-    exact h
-  · intro h
-    exact ⟨i, x, by simp [h]⟩
+  simp [List.mk_mem_zipIdx_iff_le_and_getElem?_sub]
 
-theorem mem_enum_iff_getElem? {x : α × Nat} {l : Array α} : x ∈ l.zipWithIndex ↔ l[x.2]? = some x.1 :=
-  mk_mem_zipWithIndex_iff_getElem?
+/-- Variant of `mk_mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
+to avoid the inequality and the subtraction. -/
+theorem mk_mem_zipIdx_iff_getElem? {x : α} {i : Nat} {l : Array α} :
+    (x, i) ∈ l.zipIdx ↔ l[i]? = x := by
+  rw [mk_mem_zipIdx_iff_le_and_getElem?_sub]
+  simp
+
+theorem mem_zipIdx_iff_le_and_getElem?_sub {x : α × Nat} {l : Array α} {k : Nat} :
+    x ∈ zipIdx l k ↔ k ≤ x.2 ∧ l[x.2 - k]? = some x.1 := by
+  cases x
+  simp [mk_mem_zipIdx_iff_le_and_getElem?_sub]
+
+/-- Variant of `mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
+to avoid the inequality and the subtraction. -/
+theorem mem_zipIdx_iff_getElem? {x : α × Nat} {l : Array α} :
+    x ∈ l.zipIdx ↔ l[x.2]? = some x.1 := by
+  rw [mk_mem_zipIdx_iff_getElem?]
+
+@[deprecated mk_mem_zipIdx_iff_getElem? (since := "2025-01-21")]
+abbrev mk_mem_zipWithIndex_iff_getElem? := @mk_mem_zipIdx_iff_getElem?
+
+@[deprecated mem_zipIdx_iff_getElem? (since := "2025-01-21")]
+abbrev mem_zipWithIndex_iff_getElem? := @mem_zipIdx_iff_getElem?
 
 /-! ### mapFinIdx -/
 
@@ -179,12 +205,15 @@ theorem mapFinIdx_singleton {a : α} {f : (i : Nat) → α → (h : i < 1) → 
     #[a].mapFinIdx f = #[f 0 a (by simp)] := by
   simp
 
-theorem mapFinIdx_eq_zipWithIndex_map {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} :
-    l.mapFinIdx f = l.zipWithIndex.attach.map
+theorem mapFinIdx_eq_zipIdx_map {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} :
+    l.mapFinIdx f = l.zipIdx.attach.map
       fun ⟨⟨x, i⟩, m⟩ =>
-        f i x (by simp [mk_mem_zipWithIndex_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1) := by
+        f i x (by simp [mk_mem_zipIdx_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1) := by
   ext <;> simp
 
+@[deprecated mapFinIdx_eq_zipIdx_map (since := "2025-01-21")]
+abbrev mapFinIdx_eq_zipWithIndex_map := @mapFinIdx_eq_zipIdx_map
+
 @[simp]
 theorem mapFinIdx_eq_empty_iff {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} :
     l.mapFinIdx f = #[] ↔ l = #[] := by
@@ -285,10 +314,13 @@ theorem mapIdx_eq_mapFinIdx {l : Array α} {f : Nat → α → β} :
     l.mapIdx f = l.mapFinIdx (fun i a _ => f i a) := by
   simp [mapFinIdx_eq_mapIdx]
 
-theorem mapIdx_eq_zipWithIndex_map {l : Array α} {f : Nat → α → β} :
-    l.mapIdx f = l.zipWithIndex.map fun ⟨a, i⟩ => f i a := by
+theorem mapIdx_eq_zipIdx_map {l : Array α} {f : Nat → α → β} :
+    l.mapIdx f = l.zipIdx.map fun ⟨a, i⟩ => f i a := by
   ext <;> simp
 
+@[deprecated mapIdx_eq_zipIdx_map (since := "2025-01-21")]
+abbrev mapIdx_eq_zipWithIndex_map := @mapIdx_eq_zipIdx_map
+
 theorem mapIdx_append {K L : Array α} :
     (K ++ L).mapIdx f = K.mapIdx f ++ L.mapIdx fun i => f (i + K.size) := by
   rcases K with ⟨K⟩

src/Init/Data/List/Basic.lean

@@ -43,7 +43,7 @@ The operations are organized as follow:
  `countP`, `count`, and `lookup`.
 * Logic: `any`, `all`, `or`, and `and`.
 * Zippers: `zipWith`, `zip`, `zipWithAll`, and `unzip`.
-* Ranges and enumeration: `range`, `iota`, `enumFrom`, and `enum`.
+* Ranges and enumeration: `range`, `zipIdx`.
 * Minima and maxima: `min?` and `max?`.
 * Other functions: `intersperse`, `intercalate`, `eraseDups`, `eraseReps`, `span`, `splitBy`,
   `removeAll`
@@ -1530,28 +1530,51 @@ set_option linter.deprecated false in
 set_option linter.deprecated false in
 @[simp] theorem iota_succ : iota (i+1) = (i+1) :: iota i := rfl
 
+/-! ### zipIdx -/
+
+/--
+`O(|l|)`. `zipIdx l` zips a list with its indices, optionally starting from a given index.
+* `zipIdx [a, b, c] = [(a, 0), (b, 1), (c, 2)]`
+* `zipIdx [a, b, c] 5 = [(a, 5), (b, 6), (c, 7)]`
+-/
+def zipIdx : List α → (n : Nat := 0) → List (α × Nat)
+  | [], _ => nil
+  | x :: xs, n => (x, n) :: zipIdx xs (n + 1)
+
+@[simp] theorem zipIdx_nil : ([] : List α).zipIdx i = [] := rfl
+@[simp] theorem zipIdx_cons : (a::as).zipIdx i = (a, i) :: as.zipIdx (i+1) := rfl
+
 /-! ### enumFrom -/
 
 /--
 `O(|l|)`. `enumFrom n l` is like `enum` but it allows you to specify the initial index.
 * `enumFrom 5 [a, b, c] = [(5, a), (6, b), (7, c)]`
 -/
+@[deprecated "Use `zipIdx` instead; note the signature change." (since := "2025-01-21")]
 def enumFrom : Nat → List α → List (Nat × α)
   | _, [] => nil
   | n, x :: xs   => (n, x) :: enumFrom (n + 1) xs
 
-@[simp] theorem enumFrom_nil : ([] : List α).enumFrom i = [] := rfl
-@[simp] theorem enumFrom_cons : (a::as).enumFrom i = (i, a) :: as.enumFrom (i+1) := rfl
+set_option linter.deprecated false in
+@[deprecated zipIdx_nil (since := "2025-01-21"), simp]
+theorem enumFrom_nil : ([] : List α).enumFrom i = [] := rfl
+set_option linter.deprecated false in
+@[deprecated zipIdx_cons (since := "2025-01-21"), simp]
+theorem enumFrom_cons : (a::as).enumFrom i = (i, a) :: as.enumFrom (i+1) := rfl
 
 /-! ### enum -/
 
+set_option linter.deprecated false in
 /--
 `O(|l|)`. `enum l` pairs up each element with its index in the list.
 * `enum [a, b, c] = [(0, a), (1, b), (2, c)]`
 -/
+@[deprecated "Use `zipIdx` instead; note the signature change." (since := "2025-01-21")]
 def enum : List α → List (Nat × α) := enumFrom 0
 
-@[simp] theorem enum_nil : ([] : List α).enum = [] := rfl
+set_option linter.deprecated false in
+@[deprecated zipIdx_nil (since := "2025-01-21"), simp]
+theorem enum_nil : ([] : List α).enum = [] := rfl
 
 /-! ## Minima and maxima -/
 

src/Init/Data/List/Find.lean

@@ -822,28 +822,28 @@ theorem findIdx?_flatten {l : List (List α)} {p : α → Bool} :
     simp only [replicate, findIdx?_cons, Nat.zero_add, findIdx?_succ, zero_lt_succ, true_and]
     split <;> simp_all
 
-theorem findIdx?_eq_findSome?_enum {xs : List α} {p : α → Bool} :
-    xs.findIdx? p = xs.enum.findSome? fun ⟨i, a⟩ => if p a then some i else none := by
+theorem findIdx?_eq_findSome?_zipIdx {xs : List α} {p : α → Bool} :
+    xs.findIdx? p = xs.zipIdx.findSome? fun ⟨a, i⟩ => if p a then some i else none := by
   induction xs with
   | nil => simp
   | cons x xs ih =>
-    simp only [findIdx?_cons, Nat.zero_add, findIdx?_succ, enum]
+    simp only [findIdx?_cons, Nat.zero_add, findIdx?_succ, zipIdx]
     split
     · simp_all
-    · simp_all only [enumFrom_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone, reduceCtorEq]
-      simp [Function.comp_def, ← map_fst_add_enum_eq_enumFrom, findSome?_map]
+    · simp_all only [zipIdx_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone, reduceCtorEq]
+      rw [← map_snd_add_zipIdx_eq_zipIdx (n := 1) (k := 0)]
+      simp [Function.comp_def, findSome?_map]
 
-theorem findIdx?_eq_fst_find?_enum {xs : List α} {p : α → Bool} :
-    xs.findIdx? p = (xs.enum.find? fun ⟨_, x⟩ => p x).map (·.1) := by
+theorem findIdx?_eq_fst_find?_zipIdx {xs : List α} {p : α → Bool} :
+    xs.findIdx? p = (xs.zipIdx.find? fun ⟨x, _⟩ => p x).map (·.2) := by
   induction xs with
   | nil => simp
   | cons x xs ih =>
-    simp only [findIdx?_cons, Nat.zero_add, findIdx?_start_succ, enum_cons]
+    simp only [findIdx?_cons, Nat.zero_add, findIdx?_start_succ, zipIdx_cons]
     split
     · simp_all
-    · simp only [Option.map_map, enumFrom_eq_map_enum, Bool.false_eq_true, not_false_eq_true,
-        find?_cons_of_neg, find?_map, *]
-      congr
+    · rw [ih, ← map_snd_add_zipIdx_eq_zipIdx (n := 1) (k := 0)]
+      simp [Function.comp_def, *]
 
 -- See also `findIdx_le_findIdx`.
 theorem findIdx?_eq_none_of_findIdx?_eq_none {xs : List α} {p q : α → Bool} (w : ∀ x ∈ xs, p x → q x) :

src/Init/Data/List/Impl.lean

@@ -316,14 +316,35 @@ theorem insertIdxTR_go_eq : ∀ n l, insertIdxTR.go a n l acc = acc.toList ++ in
 
 /-! ## Ranges and enumeration -/
 
+/-! ### zipIdx -/
+
+/-- Tail recursive version of `List.zipIdx`. -/
+def zipIdxTR (l : List α) (n : Nat := 0) : List (α × Nat) :=
+  let arr := l.toArray
+  (arr.foldr (fun a (n, acc) => (n-1, (a, n-1) :: acc)) (n + arr.size, [])).2
+
+@[csimp] theorem zipIdx_eq_zipIdxTR : @zipIdx = @zipIdxTR := by
+  funext α l n; simp [zipIdxTR, -Array.size_toArray]
+  let f := fun (a : α) (n, acc) => (n-1, (a, n-1) :: acc)
+  let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, zipIdx l n)
+    | [], n => rfl
+    | a::as, n => by
+      rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
+      simp [zipIdx, f]
+  rw [← Array.foldr_toList]
+  simp +zetaDelta [go]
+
 /-! ### enumFrom -/
 
 /-- Tail recursive version of `List.enumFrom`. -/
+@[deprecated zipIdxTR (since := "2025-01-21")]
 def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
   let arr := l.toArray
   (arr.foldr (fun a (n, acc) => (n-1, (n-1, a) :: acc)) (n + arr.size, [])).2
 
-@[csimp] theorem enumFrom_eq_enumFromTR : @enumFrom = @enumFromTR := by
+set_option linter.deprecated false in
+@[deprecated zipIdx_eq_zipIdxTR (since := "2025-01-21"), csimp]
+theorem enumFrom_eq_enumFromTR : @enumFrom = @enumFromTR := by
   funext α n l; simp [enumFromTR, -Array.size_toArray]
   let f := fun (a : α) (n, acc) => (n-1, (n-1, a) :: acc)
   let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, enumFrom n l)

src/Init/Data/List/MapIdx.lean

@@ -132,27 +132,30 @@ theorem mapFinIdx_singleton {a : α} {f : (i : Nat) → α → (h : i < 1) → 
     [a].mapFinIdx f = [f 0 a (by simp)] := by
   simp
 
-theorem mapFinIdx_eq_enum_map {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
-    l.mapFinIdx f = l.enum.attach.map
-      fun ⟨⟨i, x⟩, m⟩ =>
-        f i x (by rw [mk_mem_enum_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1) := by
+theorem mapFinIdx_eq_zipIdx_map {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
+    l.mapFinIdx f = l.zipIdx.attach.map
+      fun ⟨⟨x, i⟩, m⟩ =>
+        f i x (by rw [mk_mem_zipIdx_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1) := by
   apply ext_getElem <;> simp
 
+@[deprecated mapFinIdx_eq_zipIdx_map (since := "2025-01-21")]
+abbrev mapFinIdx_eq_zipWithIndex_map := @mapFinIdx_eq_zipIdx_map
+
 @[simp]
 theorem mapFinIdx_eq_nil_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
     l.mapFinIdx f = [] ↔ l = [] := by
-  rw [mapFinIdx_eq_enum_map, map_eq_nil_iff, attach_eq_nil_iff, enum_eq_nil_iff]
+  rw [mapFinIdx_eq_zipIdx_map, map_eq_nil_iff, attach_eq_nil_iff, zipIdx_eq_nil_iff]
 
 theorem mapFinIdx_ne_nil_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
     l.mapFinIdx f ≠ [] ↔ l ≠ [] := by
   simp
 
 theorem exists_of_mem_mapFinIdx {b : β} {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β}
     (h : b ∈ l.mapFinIdx f) : ∃ (i : Nat) (h : i < l.length), f i l[i] h = b := by
-  rw [mapFinIdx_eq_enum_map] at h
+  rw [mapFinIdx_eq_zipIdx_map] at h
   replace h := exists_of_mem_map h
-  simp only [mem_attach, true_and, Subtype.exists, Prod.exists, mk_mem_enum_iff_getElem?] at h
-  obtain ⟨i, b, h, rfl⟩ := h
+  simp only [mem_attach, true_and, Subtype.exists, Prod.exists, mk_mem_zipIdx_iff_getElem?] at h
+  obtain ⟨b, i, h, rfl⟩ := h
   rw [getElem?_eq_some_iff] at h
   obtain ⟨h', rfl⟩ := h
   exact ⟨i, h', rfl⟩
@@ -331,17 +334,19 @@ theorem mapIdx_eq_mapFinIdx {l : List α} {f : Nat → α → β} :
     l.mapIdx f = l.mapFinIdx (fun i a _ => f i a) := by
   simp [mapFinIdx_eq_mapIdx]
 
-theorem mapIdx_eq_enum_map {l : List α} :
-    l.mapIdx f = l.enum.map (Function.uncurry f) := by
+theorem mapIdx_eq_zipIdx_map {l : List α} {f : Nat → α → β} :
+    l.mapIdx f = l.zipIdx.map (fun ⟨a, i⟩ => f i a) := by
   ext1 i
-  simp only [getElem?_mapIdx, Option.map, getElem?_map, getElem?_enum]
+  simp only [getElem?_mapIdx, Option.map, getElem?_map, getElem?_zipIdx]
   split <;> simp
 
+@[deprecated mapIdx_eq_zipIdx_map (since := "2025-01-21")]
+abbrev mapIdx_eq_enum_map := @mapIdx_eq_zipIdx_map
+
 @[simp]
 theorem mapIdx_cons {l : List α} {a : α} :
     mapIdx f (a :: l) = f 0 a :: mapIdx (fun i => f (i + 1)) l := by
-  simp [mapIdx_eq_enum_map, enum_eq_zip_range, map_uncurry_zip_eq_zipWith,
-    range_succ_eq_map, zipWith_map_left]
+  simp [mapIdx_eq_zipIdx_map, List.zipIdx_succ]
 
 theorem mapIdx_append {K L : List α} :
     (K ++ L).mapIdx f = K.mapIdx f ++ L.mapIdx fun i => f (i + K.length) := by
@@ -358,7 +363,7 @@ theorem mapIdx_singleton {a : α} : mapIdx f [a] = [f 0 a] := by
 
 @[simp]
 theorem mapIdx_eq_nil_iff {l : List α} : List.mapIdx f l = [] ↔ l = [] := by
-  rw [List.mapIdx_eq_enum_map, List.map_eq_nil_iff, List.enum_eq_nil_iff]
+  rw [List.mapIdx_eq_zipIdx_map, List.map_eq_nil_iff, List.zipIdx_eq_nil_iff]
 
 theorem mapIdx_ne_nil_iff {l : List α} :
     List.mapIdx f l ≠ [] ↔ l ≠ [] := by

src/Init/Data/List/Nat/Find.lean

@@ -37,14 +37,14 @@ theorem find?_eq_some_iff_getElem {xs : List α} {p : α → Bool} {b : α} :
 
 theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : List α} {p q : α → Bool} (w : ∀ x ∈ xs, p x → q x) {i : Nat}
     (h : xs.findIdx? p = some i) : ∃ j, j ≤ i ∧ xs.findIdx? q = some j := by
-  simp only [findIdx?_eq_findSome?_enum] at h
+  simp only [findIdx?_eq_findSome?_zipIdx] at h
   rw [findSome?_eq_some_iff] at h
   simp only [Option.ite_none_right_eq_some, Option.some.injEq, ite_eq_right_iff, reduceCtorEq,
     imp_false, Bool.not_eq_true, Prod.forall, exists_and_right, Prod.exists] at h
   obtain ⟨h, h₁, b, ⟨es, h₂⟩, ⟨hb, rfl⟩, h₃⟩ := h
-  rw [enum_eq_enumFrom, enumFrom_eq_append_iff] at h₂
+  rw [zipIdx_eq_append_iff] at h₂
   obtain ⟨l₁', l₂', rfl, rfl, h₂⟩ := h₂
-  rw [eq_comm, enumFrom_eq_cons_iff] at h₂
+  rw [eq_comm, zipIdx_eq_cons_iff] at h₂
   obtain ⟨a, as, rfl, h₂, rfl⟩ := h₂
   simp only [Nat.zero_add, Prod.mk.injEq] at h₂
   obtain ⟨rfl, rfl⟩ := h₂