feat: another grind_pattern for getElem?_pos

This PR activates `getElem?_pos` more aggressively, triggered by `c[i]`.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>

src/Init/GetElem.lean

@@ -172,6 +172,9 @@ instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (v
   rw [getElem?_def]
   exact dif_pos h
 
+grind_pattern getElem?_pos => c[i] where
+  guard dom c i
+
 @[simp, grind =] theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) (h : ¬dom c i) : c[i]? = none := by
   have : Decidable (dom c i) := .isFalse h

src/Lean/Elab/Tactic/Grind/LintExceptions.lean

@@ -7,6 +7,7 @@ module
 prelude
 import Init.Grind.Lint
 import Lean.Elab.Tactic.Grind.Lint
+import Std
 
 -- We allow these as grind lemmas even though they triggers >20 further instantiations.
 -- See tests/lean/run/grind_lint_*.lean for more details.
@@ -16,8 +17,18 @@ import Lean.Elab.Tactic.Grind.Lint
 #grind_lint skip List.Sublist.append
 #grind_lint skip List.Sublist.middle
 #grind_lint skip List.getLast?_pmap
+#grind_lint skip List.getLast_attach
+#grind_lint skip List.getLast_attachWith
+#grind_lint skip List.head_attachWith
+#grind_lint skip Array.back_singleton
 #grind_lint skip Array.count_singleton
 #grind_lint skip Array.foldl_empty
 #grind_lint skip Array.foldr_empty
+#grind_lint skip Array.getElem_zero_filter
+#grind_lint skip Array.getElem_zero_filterMap
+#grind_lint skip Std.ExtHashMap.getElem_filterMap'
+#grind_lint skip Std.ExtTreeMap.getElem_filterMap'
+#grind_lint skip Std.HashMap.getElem_filterMap'
+#grind_lint skip Std.TreeMap.getElem_filterMap'
 
 #grind_lint skip suffix sizeOf_spec

tests/lean/run/grind_indexmap_trace.lean

@@ -243,25 +243,28 @@ example (m : IndexMap α β) (a a' : α) (b : β) :
 info: Try these:
   [apply] ⏎
     instantiate only [= mem_indices_of_mem, insert, = getElem_def]
-    instantiate only [= getElem?_neg, = getElem?_pos]
+    instantiate only [usr getElem?_pos, = getElem?_neg, = getElem?_pos]
+    instantiate only [=_ WF]
+    instantiate only [= getElem?_neg, = getElem?_pos, = WF]
+    instantiate only [= getElem?_neg, = getElem?_pos, = size_keys]
     cases #f590
-    · cases #ffdf
+    · instantiate only [size]
+      cases #ffdf
       · instantiate only
         instantiate only [= Array.getElem_set]
       · instantiate only
-        instantiate only [size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
-    · instantiate only [= mem_indices_of_mem, = getElem_def]
-      instantiate only [usr getElem_indices_lt]
-      instantiate only [size]
+        instantiate only [= HashMap.getElem?_insert, = Array.getElem_push]
+    · instantiate only [= mem_indices_of_mem, = getElem_def, size]
+      instantiate only [usr getElem_indices_lt, =_ WF]
+      instantiate only [= getElem?_pos]
       cases #ffdf
-      · instantiate only [usr getElem_indices_lt, =_ WF]
-        instantiate only [= mem_indices_of_mem, = getElem?_pos, = Array.size_set, = Array.getElem_set]
-        instantiate only [WF']
+      · instantiate only [WF']
+        instantiate only [= Array.getElem_set]
       · instantiate only
-        instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
-  [apply] finish only [= mem_indices_of_mem, insert, = getElem_def, = getElem?_neg, = getElem?_pos, = Array.getElem_set,
-    size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, usr getElem_indices_lt, =_ WF,
-    = Array.size_set, WF', #f590, #ffdf]
+        instantiate only [= HashMap.getElem?_insert, = Array.getElem_push]
+  [apply] finish only [= mem_indices_of_mem, insert, = getElem_def, usr getElem?_pos, = getElem?_neg, = getElem?_pos,
+    =_ WF, = WF, = size_keys, size, = Array.getElem_set, = HashMap.getElem?_insert, = Array.getElem_push,
+    usr getElem_indices_lt, WF', #f590, #ffdf]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
@@ -293,30 +296,33 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
 
 /--
 info: Try these:
-  [apply] grind only [= mem_indices_of_mem, insert, = getElem_def, = getElem?_neg, = getElem?_pos, = Array.getElem_set,
-    size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, usr getElem_indices_lt, =_ WF,
-    = Array.size_set, WF', #f590, #ffdf]
-  [apply] grind only [= mem_indices_of_mem, insert, = getElem_def, = getElem?_neg, = getElem?_pos, = Array.getElem_set,
-    size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, usr getElem_indices_lt, =_ WF,
-    = Array.size_set, WF']
+  [apply] grind only [= mem_indices_of_mem, insert, = getElem_def, usr getElem?_pos, = getElem?_neg, = getElem?_pos,
+    =_ WF, = WF, = size_keys, size, = Array.getElem_set, = HashMap.getElem?_insert, = Array.getElem_push,
+    usr getElem_indices_lt, WF', #f590, #ffdf]
+  [apply] grind only [= mem_indices_of_mem, insert, = getElem_def, usr getElem?_pos, = getElem?_neg, = getElem?_pos,
+    =_ WF, = WF, = size_keys, size, = Array.getElem_set, = HashMap.getElem?_insert, = Array.getElem_push,
+    usr getElem_indices_lt, WF']
   [apply] grind =>
     instantiate only [= mem_indices_of_mem, insert, = getElem_def]
-    instantiate only [= getElem?_neg, = getElem?_pos]
+    instantiate only [usr getElem?_pos, = getElem?_neg, = getElem?_pos]
+    instantiate only [=_ WF]
+    instantiate only [= getElem?_neg, = getElem?_pos, = WF]
+    instantiate only [= getElem?_neg, = getElem?_pos, = size_keys]
     cases #f590
-    · cases #ffdf
+    · instantiate only [size]
+      cases #ffdf
       · instantiate only
         instantiate only [= Array.getElem_set]
       · instantiate only
-        instantiate only [size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
-    · instantiate only [= mem_indices_of_mem, = getElem_def]
-      instantiate only [usr getElem_indices_lt]
-      instantiate only [size]
+        instantiate only [= HashMap.getElem?_insert, = Array.getElem_push]
+    · instantiate only [= mem_indices_of_mem, = getElem_def, size]
+      instantiate only [usr getElem_indices_lt, =_ WF]
+      instantiate only [= getElem?_pos]
       cases #ffdf
-      · instantiate only [usr getElem_indices_lt, =_ WF]
-        instantiate only [= mem_indices_of_mem, = getElem?_pos, = Array.size_set, = Array.getElem_set]
-        instantiate only [WF']
+      · instantiate only [WF']
+        instantiate only [= Array.getElem_set]
       · instantiate only
-        instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
+        instantiate only [= HashMap.getElem?_insert, = Array.getElem_push]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
@@ -356,13 +362,16 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
 info: Try these:
   [apply] ⏎
     instantiate only [findIdx, insert, = mem_indices_of_mem]
-    instantiate only [= getElem?_neg, = getElem?_pos]
+    instantiate only [usr getElem?_pos, = getElem?_neg, = getElem?_pos]
+    instantiate only [=_ WF]
+    instantiate only [= getElem?_neg]
+    instantiate only [= size_keys]
     cases #1bba
     · instantiate only [findIdx]
     · instantiate only
-      instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert]
-  [apply] finish only [findIdx, insert, = mem_indices_of_mem, = getElem?_neg, = getElem?_pos, = HashMap.mem_insert,
-    = HashMap.getElem_insert, #1bba]
+      instantiate only [= HashMap.getElem?_insert]
+  [apply] finish only [findIdx, insert, = mem_indices_of_mem, usr getElem?_pos, = getElem?_neg, = getElem?_pos, =_ WF,
+    = size_keys, = HashMap.getElem?_insert, #1bba]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a : α) (b : β) :
@@ -372,17 +381,20 @@ example (m : IndexMap α β) (a : α) (b : β) :
 /--
 info: Try these:
   [apply] grind
-  [apply] grind only [findIdx, insert, = mem_indices_of_mem, = getElem?_neg, = getElem?_pos, = HashMap.mem_insert,
-    = HashMap.getElem_insert, #1bba]
-  [apply] grind only [findIdx, insert, = mem_indices_of_mem, = getElem?_neg, = getElem?_pos, = HashMap.mem_insert,
-    = HashMap.getElem_insert]
+  [apply] grind only [findIdx, insert, = mem_indices_of_mem, usr getElem?_pos, = getElem?_neg, = getElem?_pos, =_ WF,
+    = size_keys, = HashMap.getElem?_insert, #1bba]
+  [apply] grind only [findIdx, insert, = mem_indices_of_mem, usr getElem?_pos, = getElem?_neg, = getElem?_pos, =_ WF,
+    = size_keys, = HashMap.getElem?_insert]
   [apply] grind =>
     instantiate only [findIdx, insert, = mem_indices_of_mem]
-    instantiate only [= getElem?_neg, = getElem?_pos]
+    instantiate only [usr getElem?_pos, = getElem?_neg, = getElem?_pos]
+    instantiate only [=_ WF]
+    instantiate only [= getElem?_neg]
+    instantiate only [= size_keys]
     cases #1bba
     · instantiate only [findIdx]
     · instantiate only
-      instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert]
+      instantiate only [= HashMap.getElem?_insert]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a : α) (b : β) :

tests/lean/run/grind_interactive.lean

@@ -53,11 +53,17 @@ example [CommRing α] (a b c : α)
 trace: [facts] Asserted facts
   [_] (bs.set i₂ v₂ ⋯).size = bs.size
   [_] (as.set i₁ v₁ ⋯).size = as.size
+  [_] ∀ (h : j + 1 ≤ as.size), as[j]? = some as[j]
+  [_] ∀ (h : j + 1 ≤ cs.size), cs[j]? = some cs[j]
   [_] (bs.set i₂ v₂ ⋯)[j] = if i₂ = j then v₂ else bs[j]
 ---
 trace: [props] True propositions
   [_] j < (bs.set i₂ v₂ ⋯).size
   [_] j < bs.size
+  [_] cs[j]? = some cs[j]
+  [_] ∀ (h : j + 1 ≤ cs.size), cs[j]? = some cs[j]
+  [_] as[j]? = some as[j]
+  [_] ∀ (h : j + 1 ≤ as.size), as[j]? = some as[j]
 ---
 trace: [eqc] Equivalence classes
   [eqc] {bs, as.set i₁ v₁ ⋯}
@@ -65,6 +71,7 @@ trace: [eqc] Equivalence classes
   [eqc] {as.size, bs.size, cs.size, (as.set i₁ v₁ ⋯).size, (bs.set i₂ v₂ ⋯).size}
   [eqc] {cs[j], bs[j], (bs.set i₂ v₂ ⋯)[j]}
     [eqc] {if i₂ = j then v₂ else bs[j]}
+  [eqc] {some as[j], as[j]?}
   [eqc] {as.size = 0, bs.size = 0, cs.size = 0}
   [eqc] others
     [eqc] {↑as.size, ↑bs.size, ↑cs.size, ↑(bs.set i₂ v₂ ⋯).size}
@@ -142,14 +149,22 @@ trace: [grind] Grind state
   [facts] Asserted facts
     [_] (bs.set i₂ v₂ ⋯).size = bs.size
     [_] (as.set i₁ v₁ ⋯).size = as.size
+    [_] ∀ (h : j + 1 ≤ as.size), as[j]? = some as[j]
+    [_] ∀ (h : j + 1 ≤ cs.size), cs[j]? = some cs[j]
     [_] (bs.set i₂ v₂ ⋯)[j] = if i₂ = j then v₂ else bs[j]
   [props] True propositions
     [_] j < (bs.set i₂ v₂ ⋯).size
     [_] j < bs.size
+    [_] cs[j]? = some cs[j]
+    [_] ∀ (h : j + 1 ≤ cs.size), cs[j]? = some cs[j]
+    [_] as[j]? = some as[j]
+    [_] ∀ (h : j + 1 ≤ as.size), as[j]? = some as[j]
   [eqc] Equivalence classes
     [eqc] {as.size, bs.size, cs.size, (as.set i₁ v₁ ⋯).size, (bs.set i₂ v₂ ⋯).size}
     [eqc] {cs[j], bs[j], (bs.set i₂ v₂ ⋯)[j]}
       [eqc] {if i₂ = j then v₂ else bs[j]}
+    [eqc] {some as[j], as[j]?}
+    [eqc] {some cs[j], cs[j]?}
     [eqc] {as.size = 0, bs.size = 0, cs.size = 0}
     [eqc] others
       [eqc] {↑as.size, ↑bs.size, ↑cs.size, ↑(bs.set i₂ v₂ ⋯).size}
@@ -435,6 +450,12 @@ example (as bs cs : Array α) (v₁ v₂ : α)
 
 /--
 trace: [grind.ematch.instance] Array.getElem_set: (as.set i₁ v₁ ⋯)[j] = if i₁ = j then v₁ else as[j]
+[grind.ematch.instance] Array.getElem?_set: (bs.set i₂ v₂ ⋯)[j]? = if i₂ = j then some v₂ else bs[j]?
+[grind.ematch.instance] getElem?_neg: ¬j < cs.size → cs[j]? = none
+[grind.ematch.instance] getElem?_neg: ¬j < as.size → as[j]? = none
+[grind.ematch.instance] getElem?_pos: ∀ (h : j < cs.size), cs[j]? = some cs[j]
+[grind.ematch.instance] getElem?_pos: ∀ (h : j < as.size), as[j]? = some as[j]
+[grind.ematch.instance] getElem?_pos: ∀ (h : j < bs.size), bs[j]? = some bs[j]
 -/
 #guard_msgs in
 example (as bs cs : Array α) (v₁ v₂ : α)

tests/lean/run/grind_lint_1.lean

@@ -59,9 +59,12 @@ info: Try this to display the actual theorem instances:
 #grind_lint inspect Array.range_succ Array.range'_succ
 
 -- These go slightly over 20, but seem reasonable.
+#grind_lint skip Array.back_singleton
 #grind_lint skip Array.count_singleton
 #grind_lint skip Array.foldl_empty
 #grind_lint skip Array.foldr_empty
+#grind_lint skip Array.getElem_zero_filter
+#grind_lint skip Array.getElem_zero_filterMap
 
 #guard_msgs in
 #grind_lint check (min := 20) in Array
@@ -104,12 +107,15 @@ info: instantiating `Array.findIdx_empty` triggers 20 additional `grind` theorem
 ---
 info: instantiating `Array.findIdx_singleton` triggers 16 additional `grind` theorem instantiations
 ---
+info: instantiating `Array.getElem_eraseIdx` triggers 17 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
+  #grind_lint inspect Array.getElem_eraseIdx
 -/
 #guard_msgs in
 #grind_lint check (min := 15) in Array

tests/lean/run/grind_lint_array.lean

@@ -11,5 +11,17 @@ import Lean.Elab.Tactic.Grind.LintExceptions
 #guard_msgs in
 #grind_lint inspect (min := 22) Array.foldr_empty
 
+-- `Array.back_singleton` is reasonable at 23.
+#guard_msgs in
+#grind_lint inspect (min := 25) Array.back_singleton
+
+-- `Array.getElem_zero_filter` is reasonable at 20.
+#guard_msgs in
+#grind_lint inspect (min := 22) Array.getElem_zero_filter
+
+-- `Array.getElem_zero_filterMap` is reasonable at 20.
+#guard_msgs in
+#grind_lint inspect (min := 22) Array.getElem_zero_filterMap
+
 #guard_msgs in
 #grind_lint check (min := 20) in Array

tests/lean/run/grind_lint_list.lean

@@ -23,6 +23,18 @@ import Lean.Elab.Tactic.Grind.LintExceptions
 #guard_msgs in
 #grind_lint inspect (min := 25) List.Sublist.middle
 
+-- `List.getLast_attach` is reasonable at 21.
+#guard_msgs in
+#grind_lint inspect (min := 25) List.getLast_attach
+
+-- `List.getLast_attachWith` is reasonable at 22.
+#guard_msgs in
+#grind_lint inspect (min := 25) List.getLast_attachWith
+
+-- `List.head_attachWith` is reasonable at 21.
+#guard_msgs in
+#grind_lint inspect (min := 25) List.head_attachWith
+
 /-! Check List namespace: -/
 
 #guard_msgs in

tests/lean/run/grind_lint_std_hashmap.lean

@@ -1,7 +1,15 @@
 import Std
 import Lean.Elab.Tactic.Grind.LintExceptions
 
-/-! Check Std hash/tree map/set namespaces: -/
+/-! Check Std hash map/set namespaces: -/
+
+-- `Std.ExtHashMap.getElem_filterMap'` is reasonable at 30.
+#guard_msgs in
+#grind_lint inspect (min := 35) Std.ExtHashMap.getElem_filterMap'
+
+-- `Std.HashMap.getElem_filterMap'` is reasonable at 28.
+#guard_msgs in
+#grind_lint inspect (min := 30) Std.HashMap.getElem_filterMap'
 
 #guard_msgs in
 #grind_lint check (min := 20) in Std.DHashMap Std.HashMap Std.HashSet Std.ExtDHashMap Std.ExtHashMap Std.ExtHashSet

tests/lean/run/grind_lint_std_treemap.lean

@@ -3,5 +3,13 @@ import Lean.Elab.Tactic.Grind.LintExceptions
 
 /-! Check Std tree map/set namespaces: -/
 
+-- `Std.ExtTreeMap.getElem_filterMap'` is reasonable at 30.
+#guard_msgs in
+#grind_lint inspect (min := 35) Std.ExtTreeMap.getElem_filterMap'
+
+-- `Std.TreeMap.getElem_filterMap'` is reasonable at 28.
+#guard_msgs in
+#grind_lint inspect (min := 30) Std.TreeMap.getElem_filterMap'
+
 #guard_msgs in
 #grind_lint check (min := 20) in Std.DTreeMap Std.TreeMap Std.TreeSet Std.ExtDTreeMap Std.ExtTreeMap Std.ExtTreeSet