feat: improve grind anchors computation

This PR improves anchor stability (aka stable hash codes) used to
reference terms in a `grind` goal.

src/Lean/Meta/Tactic/Grind/Anchor.lean

@@ -20,6 +20,12 @@ Hashes names for computing anchors (aka stable hash codes)
 def hashName (n : Name) : UInt64 :=
   if n.hasMacroScopes || n.isInaccessibleUserName || n.isImplementationDetail then
     0
+  else if isPrivateName n then
+    hash (privateToUserName n)
+  else if n.isInternal then
+    match n with
+    | .str p _ | .num p _ => hashName p
+    | _ => 0
   else
     hash n
 
@@ -33,7 +39,13 @@ public partial def getAnchor (e : Expr) : GrindM UInt64 := do
   if let some a := (← get).anchors.find? { expr := e } then
     return a
   let a ← match e with
-    | .const declName _ => pure <| hash declName
+    | .const declName _ =>
+      /-
+      **Note**: we skip matcher declaration names because they may introduce some
+      "instability". Recall that `match` auxiliary declarations are reused.
+      -/
+      if (← isMatcher declName) then pure 0
+      else pure <| hash declName
     | .fvar fvarId => pure <| hashName (← fvarId.getDecl).userName
     | .mdata _ b => getAnchor b
     | .letE n v t b _ =>

tests/lean/run/grind_interactive.lean

@@ -189,11 +189,11 @@ def h (as : List Nat) :=
 
 /--
 trace: [splits] Case split candidates
-  [split] #7577 := match bs with
+  [split] #4615 := match bs with
       | [] => 1
       | [head] => 2
       | head :: head_1 :: tail => 3
-  [split] #448c := match as with
+  [split] #ec88 := match as with
       | [] => 1
       | [head] => 2
       | head :: head_1 :: tail => 3