feat: grind annotations for List/Array/Vector.ofFn theorems and List.Impl (#8749)

This PR adds grind annotations for `List/Array/Vector.ofFn` theorems and
additional `List.Impl` find operations.

The annotations are added to theorems that correspond to those already
annotated in the List implementation, ensuring consistency across all
three container types (List, Array, Vector) for ofFn operations and
related functionality.

Key theorems annotated include:
- Element access theorems (`getElem_ofFn`, `getElem?_ofFn`)
- Construction and conversion theorems (`ofFn_zero`, `toList_ofFn`,
`toArray_ofFn`)
- Membership theorems (`mem_ofFn`)
- Head/tail operations (`back_ofFn`)
- Monadic operations (`ofFnM_zero`, `toList_ofFnM`, `toArray_ofFnM`,
`idRun_ofFnM`)
- List.Impl find operations (`find?_singleton`, `find?_append`,
`findSome?_singleton`, `findSome?_append`)

Author: kim-em

src/Init/Data/Array/OfFn.lean

@@ -23,7 +23,7 @@ namespace Array
 
 /-! ### ofFn -/
 
-@[simp] theorem ofFn_zero {f : Fin 0 → α} : ofFn f = #[] := by
+@[simp, grind =] theorem ofFn_zero {f : Fin 0 → α} : ofFn f = #[] := by
   simp [ofFn, ofFn.go]
 
 theorem ofFn_succ {f : Fin (n+1) → α} :
@@ -42,10 +42,10 @@ theorem ofFn_add {n m} {f : Fin (n + m) → α} :
   | zero => simp
   | succ m ih => simp [ofFn_succ, ih]
 
-@[simp] theorem _root_.List.toArray_ofFn {f : Fin n → α} : (List.ofFn f).toArray = Array.ofFn f := by
+@[simp, grind =] theorem _root_.List.toArray_ofFn {f : Fin n → α} : (List.ofFn f).toArray = Array.ofFn f := by
   ext <;> simp
 
-@[simp] theorem toList_ofFn {f : Fin n → α} : (Array.ofFn f).toList = List.ofFn f := by
+@[simp, grind =] theorem toList_ofFn {f : Fin n → α} : (Array.ofFn f).toList = List.ofFn f := by
   apply List.ext_getElem <;> simp
 
 theorem ofFn_succ' {f : Fin (n+1) → α} :
@@ -58,7 +58,7 @@ theorem ofFn_eq_empty_iff {f : Fin n → α} : ofFn f = #[] ↔ n = 0 := by
   rw [← Array.toList_inj]
   simp
 
-@[simp 500]
+@[simp 500, grind =]
 theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i = a := by
   constructor
   · intro w
@@ -73,7 +73,7 @@ theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i =
 def ofFnM {n} [Monad m] (f : Fin n → m α) : m (Array α) :=
   Fin.foldlM n (fun xs i => xs.push <$> f i) (Array.emptyWithCapacity n)
 
-@[simp]
+@[simp, grind =]
 theorem ofFnM_zero [Monad m] {f : Fin 0 → m α} : ofFnM f = pure #[] := by
   simp [ofFnM]
 
@@ -109,7 +109,7 @@ theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} :
     funext x
     simp
 
-@[simp] theorem toList_ofFnM [Monad m] [LawfulMonad m] {f : Fin n → m α} :
+@[simp, grind =] theorem toList_ofFnM [Monad m] [LawfulMonad m] {f : Fin n → m α} :
     toList <$> ofFnM f = List.ofFnM f := by
   induction n with
   | zero => simp

src/Init/Data/List/Impl.lean

@@ -261,7 +261,7 @@ Examples:
 /-- Tail recursive implementation of `findRev?`. This is only used at runtime. -/
 def findRev?TR (p : α → Bool) (l : List α) : Option α := l.reverse.find? p
 
-@[simp] theorem find?_singleton {a : α} : [a].find? p = if p a then some a else none := by
+@[simp, grind =] theorem find?_singleton {a : α} : [a].find? p = if p a then some a else none := by
   simp only [find?]
   split <;> simp_all
 
@@ -287,12 +287,12 @@ def findRev?TR (p : α → Bool) (l : List α) : Option α := l.reverse.find? p
 /-- Tail recursive implementation of `finSomedRev?`. This is only used at runtime. -/
 def findSomeRev?TR (f : α → Option β) (l : List α) : Option β := l.reverse.findSome? f
 
-@[simp] theorem findSome?_singleton {a : α} :
+@[simp, grind =] theorem findSome?_singleton {a : α} :
     [a].findSome? f = f a := by
   simp only [findSome?_cons, findSome?_nil]
   split <;> simp_all
 
-@[simp] theorem findSome?_append {xs ys : List α} : (xs ++ ys).findSome? f = (xs.findSome? f).or (ys.findSome? f) := by
+@[simp, grind =] theorem findSome?_append {xs ys : List α} : (xs ++ ys).findSome? f = (xs.findSome? f).or (ys.findSome? f) := by
   induction xs with
   | nil => simp [findSome?]
   | cons x xs ih =>

src/Init/Data/List/OfFn.lean

@@ -34,14 +34,14 @@ to each potential index in order, starting at `0`.
 def ofFnM {n} [Monad m] (f : Fin n → m α) : m (List α) :=
   List.reverse <$> Fin.foldlM n (fun xs i => (· :: xs) <$> f i) []
 
-@[simp]
+@[simp, grind =]
 theorem length_ofFn {f : Fin n → α} : (ofFn f).length = n := by
   simp only [ofFn]
   induction n with
   | zero => simp
   | succ n ih => simp [Fin.foldr_succ, ih]
 
-@[simp]
+@[simp, grind =]
 protected theorem getElem_ofFn {f : Fin n → α} (h : i < (ofFn f).length) :
     (ofFn f)[i] = f ⟨i, by simp_all⟩ := by
   simp only [ofFn]
@@ -55,7 +55,7 @@ protected theorem getElem_ofFn {f : Fin n → α} (h : i < (ofFn f).length) :
       apply ih
       simp_all
 
-@[simp]
+@[simp, grind =]
 protected theorem getElem?_ofFn {f : Fin n → α} :
     (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none :=
   if h : i < (ofFn f).length
@@ -67,7 +67,7 @@ protected theorem getElem?_ofFn {f : Fin n → α} :
     simpa using h
 
 /-- `ofFn` on an empty domain is the empty list. -/
-@[simp]
+@[simp, grind =]
 theorem ofFn_zero {f : Fin 0 → α} : ofFn f = [] := by
   rw [ofFn, Fin.foldr_zero]
 
@@ -98,7 +98,7 @@ theorem ofFn_add {n m} {f : Fin (n + m) → α} :
 theorem ofFn_eq_nil_iff {f : Fin n → α} : ofFn f = [] ↔ n = 0 := by
   cases n <;> simp only [ofFn_zero, ofFn_succ, eq_self_iff_true, Nat.succ_ne_zero, reduceCtorEq]
 
-@[simp 500]
+@[simp 500, grind =]
 theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i = a := by
   constructor
   · intro w
@@ -107,17 +107,17 @@ theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i =
   · rintro ⟨i, rfl⟩
     apply mem_of_getElem (i := i) <;> simp
 
-theorem head_ofFn {n} {f : Fin n → α} (h : ofFn f ≠ []) :
+@[grind =] theorem head_ofFn {n} {f : Fin n → α} (h : ofFn f ≠ []) :
     (ofFn f).head h = f ⟨0, Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)⟩ := by
   rw [← getElem_zero (length_ofFn ▸ Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)),
     List.getElem_ofFn]
 
-theorem getLast_ofFn {n} {f : Fin n → α} (h : ofFn f ≠ []) :
+@[grind =]theorem getLast_ofFn {n} {f : Fin n → α} (h : ofFn f ≠ []) :
     (ofFn f).getLast h = f ⟨n - 1, Nat.sub_one_lt (mt ofFn_eq_nil_iff.2 h)⟩ := by
   simp [getLast_eq_getElem, length_ofFn, List.getElem_ofFn]
 
 /-- `ofFnM` on an empty domain is the empty list. -/
-@[simp]
+@[simp, grind =]
 theorem ofFnM_zero [Monad m] [LawfulMonad m] {f : Fin 0 → m α} : ofFnM f = pure [] := by
   simp [ofFnM]
 

src/Init/Data/Vector/OfFn.lean

@@ -20,15 +20,15 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va
 
 namespace Vector
 
-@[simp] theorem getElem_ofFn {α n} {f : Fin n → α} (h : i < n) :
+@[simp, grind =] theorem getElem_ofFn {α n} {f : Fin n → α} (h : i < n) :
     (Vector.ofFn f)[i] = f ⟨i, by simpa using h⟩ := by
   simp [ofFn]
 
-theorem getElem?_ofFn {α n} {f : Fin n → α} :
+@[simp, grind =] theorem getElem?_ofFn {α n} {f : Fin n → α} :
     (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none := by
   simp [getElem?_def]
 
-@[simp 500]
+@[simp 500, grind =]
 theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i = a := by
   constructor
   · intro w
@@ -37,7 +37,7 @@ theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i =
   · rintro ⟨i, rfl⟩
     apply mem_of_getElem (i := i) <;> simp
 
-theorem back_ofFn {n} [NeZero n] {f : Fin n → α} :
+@[grind =] theorem back_ofFn {n} [NeZero n] {f : Fin n → α} :
     (ofFn f).back = f ⟨n - 1, by have := NeZero.ne n; omega⟩ := by
   simp [back]
 
@@ -71,7 +71,7 @@ def ofFnM {n} [Monad m] (f : Fin n → m α) : m (Vector α n) :=
     else
       pure ⟨acc, by omega⟩
 
-@[simp]
+@[simp, grind =]
 theorem ofFnM_zero [Monad m] {f : Fin 0 → m α} : Vector.ofFnM f = pure #v[] := by
   simp [ofFnM, ofFnM.go]
 
@@ -114,13 +114,13 @@ theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} :
   | zero => simp
   | succ k ih => simp [ofFnM_succ, ih, ← push_append]
 
-@[simp, grind] theorem toArray_ofFnM [Monad m] [LawfulMonad m] {f : Fin n → m α} :
+@[simp, grind =] theorem toArray_ofFnM [Monad m] [LawfulMonad m] {f : Fin n → m α} :
     toArray <$> ofFnM f = Array.ofFnM f := by
   induction n with
   | zero => simp
   | succ n ih => simp [ofFnM_succ, Array.ofFnM_succ, ← ih]
 
-@[simp, grind] theorem toList_ofFnM [Monad m] [LawfulMonad m] {f : Fin n → m α} :
+@[simp, grind =] theorem toList_ofFnM [Monad m] [LawfulMonad m] {f : Fin n → m α} :
     toList <$> Vector.ofFnM f = List.ofFnM f := by
   unfold toList
   suffices Array.toList <$> (toArray <$> ofFnM f) = List.ofFnM f by