feat: refactor of find functions on List/Array/Vector (leanprover#6833)

This PR makes the signatures of `find` functions across
`List`/`Array`/`Vector` consistent. Verification lemmas will follow in
subsequent PRs.

We were previously quite inconsistent about the signature of
`indexOf`/`findIdx` functions across `List` and `Array`. Moreover, there
are still quite large gaps in the verification lemma coverage for these
even at the `List` level.

My intention is to make the signatures consistent by providing:
`findIdx` / `findIdx?` / `findFinIdx?` (these all take a predicate, and
return respectively a `Nat`, `Option Nat`, `Option (Fin l.length)`) and
similarly `idxOf` / `idxOf?` / `finIdxOf?` (which look for an element)
for each of List/Array/Vector. I've seen enough examples by now where
each variant is genuinely the most convenient at the call-site, so I'm
going to accept the cost of having many closely related functions.
*Hopefully* for the verification lemmas we can simp all of these into
"projections" of the `Option (Fin l.length)` versions, and then only
have to specify that.

However, I will not plan on immediately either filling in the missing
verification lemmas (or even deciding what the simp normal forms
relating these operations are), and just reach parity amongst
List/Array/Vector for what is already there.

Author: kim-em

src/Init/Data/Array/Basic.lean

@@ -674,18 +674,30 @@ def findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   loop 0
 
+@[inline]
+def findIdx (p : α → Bool) (as : Array α) : Nat := (as.findIdx? p).getD as.size
+
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
+def idxOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
   if h : i < a.size then
     if a[i] == v then some ⟨i, h⟩
-    else indexOfAux a v (i+1)
+    else idxOfAux a v (i+1)
   else none
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
-def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
-  indexOfAux a v 0
+@[deprecated idxOfAux (since := "2025-01-29")]
+abbrev indexOfAux := @idxOfAux
+
+def finIdxOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
+  idxOfAux a v 0
 
-@[deprecated indexOf? (since := "2024-11-20")]
+@[deprecated "`Array.indexOf?` has been deprecated, use `idxOf?` or `finIdxOf?` instead." (since := "2025-01-29")]
+abbrev indexOf? := @finIdxOf?
+
+def idxOf? [BEq α] (a : Array α) (v : α) : Option Nat :=
+  (a.finIdxOf? v).map (·.val)
+
+@[deprecated idxOf? (since := "2024-11-20")]
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
   a.findIdx? fun a => a == v
 
@@ -884,7 +896,7 @@ def eraseIdx! (a : Array α) (i : Nat) : Array α :=
 This function takes worst case O(n) time because
 it has to backshift all later elements. -/
 def erase [BEq α] (as : Array α) (a : α) : Array α :=
-  match as.indexOf? a with
+  match as.finIdxOf? a with
   | none   => as
   | some i => as.eraseIdx i
 
@@ -893,9 +905,9 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
 This function takes worst case O(n) time because
 it has to backshift all later elements. -/
 def eraseP (as : Array α) (p : α → Bool) : Array α :=
-  match as.findIdx? p with
+  match as.findFinIdx? p with
   | none   => as
-  | some i => as.eraseIdxIfInBounds i
+  | some i => as.eraseIdx i
 
 /-- Insert element `a` at position `i`. -/
 @[inline] def insertIdx (as : Array α) (i : Nat) (a : α) (_ : i ≤ as.size := by get_elem_tactic) : Array α :=

src/Init/Data/List/Basic.lean

@@ -1269,21 +1269,58 @@ theorem findSome?_cons {f : α → Option β} :
 /-! ### indexOf -/
 
 /-- Returns the index of the first element equal to `a`, or the length of the list otherwise. -/
-def indexOf [BEq α] (a : α) : List α → Nat := findIdx (· == a)
+def idxOf [BEq α] (a : α) : List α → Nat := findIdx (· == a)
 
-@[simp] theorem indexOf_nil [BEq α] : ([] : List α).indexOf x = 0 := rfl
+/-- Returns the index of the first element equal to `a`, or the length of the list otherwise. -/
+@[deprecated idxOf (since := "2025-01-29")] abbrev indexOf := @idxOf
+
+@[simp] theorem idxOf_nil [BEq α] : ([] : List α).idxOf x = 0 := rfl
+
+@[deprecated idxOf_nil (since := "2025-01-29")]
+theorem indexOf_nil [BEq α] : ([] : List α).idxOf x = 0 := rfl
 
 /-! ### findIdx? -/
 
 /-- Return the index of the first occurrence of an element satisfying `p`. -/
-def findIdx? (p : α → Bool) : List α → (start : Nat := 0) → Option Nat
-| [], _ => none
-| a :: l, i => if p a then some i else findIdx? p l (i + 1)
+def findIdx? (p : α → Bool) (l : List α) : Option Nat :=
+  go l 0
+where
+  go : List α → Nat → Option Nat
+  | [], _ => none
+  | a :: l, i => if p a then some i else go l (i + 1)
 
 /-! ### indexOf? -/
 
 /-- Return the index of the first occurrence of `a` in the list. -/
-@[inline] def indexOf? [BEq α] (a : α) : List α → Option Nat := findIdx? (· == a)
+@[inline] def idxOf? [BEq α] (a : α) : List α → Option Nat := findIdx? (· == a)
+
+/-- Return the index of the first occurrence of `a` in the list. -/
+@[deprecated idxOf? (since := "2025-01-29")]
+abbrev indexOf? := @idxOf?
+
+/-! ### findFinIdx? -/
+
+/-- Return the index of the first occurrence of an element satisfying `p`, as a `Fin l.length`,
+or `none` if no such element is found. -/
+@[inline] def findFinIdx? (p : α → Bool) (l : List α) : Option (Fin l.length) :=
+  go l 0 (by simp)
+where
+  go : (l' : List α) → (i : Nat) → (h : l'.length + i = l.length) → Option (Fin l.length)
+  | [], _, _ => none
+  | a :: l, i, h =>
+    if p a then
+      some ⟨i, by
+        simp only [Nat.add_comm _ i, ← Nat.add_assoc] at h
+        exact Nat.lt_of_add_right_lt (Nat.lt_of_succ_le (Nat.le_of_eq h))⟩
+    else
+      go l (i + 1) (by simp at h; simpa [← Nat.add_assoc, Nat.add_right_comm] using h)
+
+/-! ### finIdxOf? -/
+
+/-- Return the index of the first occurrence of `a`, as a `Fin l.length`,
+or `none` if no such element is found. -/
+@[inline] def finIdxOf? [BEq α] (a : α) : (l : List α) → Option (Fin l.length) :=
+  findFinIdx? (· == a)
 
 /-! ### countP -/
 

src/Init/Data/List/Erase.lean

@@ -472,13 +472,13 @@ theorem getLast_erase_mem (xs : List α) (a : α) (h) : (xs.erase a).getLast h 
   (erase_sublist a xs).getLast_mem h
 
 theorem erase_eq_eraseIdx [LawfulBEq α] (l : List α) (a : α) :
-    l.erase a = match l.indexOf? a with
+    l.erase a = match l.idxOf? a with
     | none => l
     | some i => l.eraseIdx i := by
   induction l with
   | nil => simp
   | cons x xs ih =>
-    rw [erase_cons, indexOf?_cons]
+    rw [erase_cons, idxOf?_cons]
     split
     · simp
     · simp [ih]
@@ -600,20 +600,23 @@ protected theorem IsPrefix.eraseIdx {l l' : List α} (h : l <+: l') (k : Nat) :
 -- See also `mem_eraseIdx_iff_getElem` and `mem_eraseIdx_iff_getElem?` in
 -- `Init/Data/List/Nat/Basic.lean`.
 
-theorem erase_eq_eraseIdx_of_indexOf [BEq α] [LawfulBEq α]
-    (l : List α) (a : α) (i : Nat) (w : l.indexOf a = i) :
+theorem erase_eq_eraseIdx_of_idxOf [BEq α] [LawfulBEq α]
+    (l : List α) (a : α) (i : Nat) (w : l.idxOf a = i) :
     l.erase a = l.eraseIdx i := by
   subst w
   rw [erase_eq_iff]
   by_cases h : a ∈ l
   · right
     obtain ⟨as, bs, rfl, h'⟩ := eq_append_cons_of_mem h
     refine ⟨as, bs, h', by simp, ?_⟩
-    rw [indexOf_append, if_neg h', indexOf_cons_self, eraseIdx_append_of_length_le] <;>
+    rw [idxOf_append, if_neg h', idxOf_cons_self, eraseIdx_append_of_length_le] <;>
       simp
   · left
     refine ⟨h, ?_⟩
     rw [eq_comm, eraseIdx_eq_self]
-    exact Nat.le_of_eq (indexOf_eq_length h).symm
+    exact Nat.le_of_eq (idxOf_eq_length h).symm
+
+@[deprecated erase_eq_eraseIdx_of_idxOf (since := "2025-01-29")]
+abbrev erase_eq_eraseIdx_of_indexOf := @erase_eq_eraseIdx_of_idxOf
 
 end List