perf: make {Array,List}.findIdx e-matching less aggressive (#14182)

This PR stops automatically connected `findIdx` to `findIdx?` through
e-matching whenever `findIdx` is available and instead only does so when
`findIdx` and `findIdx?` are available.

Author: hargoniX

src/Init/Data/Array/Find.lean

@@ -595,12 +595,13 @@ theorem findIdx?_eq_none_of_findIdx?_eq_none {xs : Array α} {p q : α → Bool}
   rcases xs with ⟨xs⟩
   simpa using List.findIdx?_eq_none_of_findIdx?_eq_none (by simpa using w)
 
-@[grind =]
 theorem findIdx_eq_getD_findIdx? {xs : Array α} {p : α → Bool} :
     xs.findIdx p = (xs.findIdx? p).getD xs.size := by
   rcases xs with ⟨xs⟩
   simp [List.findIdx_eq_getD_findIdx?]
 
+grind_pattern findIdx_eq_getD_findIdx? => xs.findIdx p, xs.findIdx? p
+
 theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {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
   rcases xs with ⟨xs⟩

src/Init/Data/List/Basic.lean

@@ -1700,7 +1700,7 @@ Examples:
   | [], n => n
   | a :: l, n => bif p a then n else go l (n + 1)
 
-@[simp] theorem findIdx_nil {p : α → Bool} : [].findIdx p = 0 := rfl
+@[simp, grind =] theorem findIdx_nil {p : α → Bool} : [].findIdx p = 0 := rfl
 
 /-! ### idxOf -/
 

src/Init/Data/List/Find.lean

@@ -980,7 +980,6 @@ theorem IsInfix.findIdx?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l
 grind_pattern IsInfix.findIdx?_eq_none => l₁ <:+: l₂, l₁.findIdx? p
 grind_pattern IsInfix.findIdx?_eq_none => l₁ <:+: l₂, l₂.findIdx? p
 
-@[grind =]
 theorem findIdx_eq_getD_findIdx? {xs : List α} {p : α → Bool} :
     xs.findIdx p = (xs.findIdx? p).getD xs.length := by
   induction xs with
@@ -989,6 +988,8 @@ theorem findIdx_eq_getD_findIdx? {xs : List α} {p : α → Bool} :
     simp only [findIdx_cons, findIdx?_cons]
     split <;> simp_all
 
+grind_pattern findIdx_eq_getD_findIdx? => xs.findIdx p, xs.findIdx? p
+
 @[simp] theorem findIdx?_subtype {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.findIdx? f = l.unattach.findIdx? g := by

tests/elab/grind_lint_1.lean

@@ -103,16 +103,10 @@ info: instantiating `Array.back?_empty` triggers 17 additional `grind` theorem i
 ---
 info: instantiating `Array.count_empty` triggers 19 additional `grind` theorem instantiations
 ---
-info: instantiating `Array.findIdx_empty` triggers 20 additional `grind` theorem instantiations
----
-info: instantiating `Array.findIdx_singleton` triggers 16 additional `grind` theorem instantiations
----
 info: Try this:
   [apply] #grind_lint check  (min := 15) in Array
   #grind_lint inspect Array.back?_empty
   #grind_lint inspect Array.count_empty
-  #grind_lint inspect Array.findIdx_empty
-  #grind_lint inspect Array.findIdx_singleton
 -/
 #guard_msgs in
 #grind_lint check (min := 15) in Array