fix: anchor values in grind? (#11077)

This PR fixes the anchor values produced by `grind?`

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

@@ -126,8 +126,16 @@ def mkGrindParams
     LibrarySuggestions.select mvarId
   else
     pure #[]
-  let params ← elabGrindParamsAndSuggestions params ps suggestions (only := only) (lax := config.lax)
+  let mut params ← elabGrindParamsAndSuggestions params ps suggestions (only := only) (lax := config.lax)
   trace[grind.debug.inj] "{params.inj.getOrigins.map (·.pp)}"
+  if params.anchorRefs?.isSome then
+    /-
+    **Note**: anchors are automatically computed in interactive mode where
+    hygiene is turned on. So, we must disable hypotheses id cleanup since
+    different ids will affect the anchor values.
+    **TODO**: a more robust solution since users may use `grind +clean => finish?`
+    -/
+    params := { params with config.clean := false }
   return params
 
 -- **TODO**: Remove `Grind.Trace`
@@ -260,7 +268,7 @@ private def elabGrindConfig' (config : TSyntax ``Lean.Parser.Tactic.optConfig) (
   let `(tactic| grind? $configStx:optConfig $[only%$only]?  $[ [$params?:grindParam,*] ]?) := stx
     | throwUnsupportedSyntax
   let config ← elabGrindConfig configStx
-  let config := { config with trace := true }
+  let config := { config with trace := true, clean := false }
   let only := only.isSome
   let params := if let some params := params? then params.getElems else #[]
   let mvarId ← getMainGoal

tests/lean/run/grind_finish_trace.lean

@@ -265,9 +265,9 @@ example (f g : Int → Int)
   grind
 
 /--
-trace: [grind.ematch.instance] h: f (f a) = f a
-[grind.ematch.instance] h: f (f (f a)) = f (f a)
-[grind.ematch.instance] h: f (f (f (f a))) = f (f (f a))
+trace: [grind.ematch.instance] h✝³: f (f a) = f a
+[grind.ematch.instance] h✝³: f (f (f a)) = f (f a)
+[grind.ematch.instance] h✝³: f (f (f (f a))) = f (f (f a))
 -/
 #guard_msgs in
 example (f g : Int → Int)

tests/lean/run/grind_indexmap_trace.lean

@@ -198,6 +198,21 @@ example (m : IndexMap α β) (a a' : α) (b : β) :
     a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := by
   grind => finish?
 
+example (m : IndexMap α β) (a a' : α) (b : β) :
+    a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := by
+  grind =>
+    instantiate only [= mem_indices_of_mem, insert]
+    instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
+    cases #4ed2
+    · cases #ffdf
+      · instantiate only
+      · instantiate only
+        set_option trace.grind.ematch.instance true in
+        instantiate only [= HashMap.contains_insert]
+    · cases #95a0
+      · cases #2688 <;> finish [= HashMap.contains_insert]
+      · cases #ffdf <;> finish
+
 example (m : IndexMap α β) (a a' : α) (b : β) :
     a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := by
   grind =>
@@ -277,6 +292,67 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
       · instantiate only
         instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
 
+/--
+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 =>
+    instantiate only [= mem_indices_of_mem, insert, = getElem_def]
+    instantiate only [= getElem?_neg, = getElem?_pos]
+    cases #f590
+    · 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]
+      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
+        instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
+-/
+#guard_msgs in
+example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
+    (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
+  grind?
+
+example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
+    (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
+  grind =>
+    instantiate only [= mem_indices_of_mem, insert, = getElem_def]
+    instantiate only [= getElem?_neg, = getElem?_pos]
+    cases #f590
+    · 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]
+      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
+        instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
+
+example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
+    (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
+  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]
+
 /--
 info: Try these:
   [apply] ⏎

tests/lean/run/grind_trace.lean

@@ -42,20 +42,20 @@ attribute [grind ext] List.ext_getElem?
 info: Try these:
   [apply] grind only [= List.getElem?_replicate, = List.getElem?_map, = List.getElem?_eq_none,
     = List.getElem?_eq_getElem, = List.length_replicate, = List.getElem?_eq_some_iff, = Option.map_some,
-    = Option.map_none, #b53f, #3f91, #ea98]
+    = Option.map_none, #12fe, #986e, #0323]
   [apply] grind only [= List.getElem?_replicate, = List.getElem?_map, = List.getElem?_eq_none,
     = List.getElem?_eq_getElem, = List.length_replicate, = List.getElem?_eq_some_iff, = Option.map_some,
     = Option.map_none]
   [apply] grind =>
-    cases #b53f
+    cases #12fe
     instantiate only [= List.getElem?_replicate, = List.getElem?_map, = List.getElem?_eq_none,
       = List.getElem?_eq_getElem]
     instantiate only [= List.getElem?_replicate, = List.getElem?_eq_none, = List.getElem?_eq_getElem,
       = List.length_replicate]
     instantiate only [= List.length_replicate]
-    cases #3f91
+    cases #986e
     · instantiate only [= List.getElem?_eq_some_iff]
-      cases #ea98
+      cases #0323
       · instantiate only [= Option.map_some]
       · instantiate only [= Option.map_none]
     · instantiate only [= Option.map_some]