feat: grind annotations for List/Array/Vector.ofFn theorems and List.Impl

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