fix: instance tactic generation at finish? (#10846)

This PR fixes a few issues on `instance only [...]` tactic generation at
`finish?`.

Author: leodemoura

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

@@ -264,7 +264,7 @@ def logAnchor (numDigits : Nat) (anchorPrefix : UInt64) (e : Expr) : TermElabM U
     -/
     Term.addTermInfo' stx e
     logAt (severity := .information) (isSilent := true) stx
-       m!"#{anchorToString numDigits anchorPrefix} := {e}"
+       m!"#{anchorPrefixToString numDigits anchorPrefix} := {e}"
 
 @[builtin_grind_tactic cases] def evalCases : GrindTactic := fun stx => do
   let `(grind| cases #$anchor:hexnum) := stx | throwUnsupportedSyntax

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

@@ -276,9 +276,9 @@ If `s?` is `none` just returns `true`.
 -/
 def checkSeqAt (s? : Option SavedState) (goal : Goal) (seq : List TGrind) : GrindM Bool := do
   let some s := s? | return true
-  let tac ← mkGrindParen seq
   Lean.withoutModifyingState do
     s.restore
+    let tac ← mkGrindParen seq
     -- **Note**: Ensure tracing is disabled.
     withTheReader Grind.Context (fun ctx => { ctx with config.trace := false }) do
       try

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

@@ -23,9 +23,12 @@ def hashName (n : Name) : UInt64 :=
   else if isPrivateName n then
     hash (privateToUserName n)
   else if n.isInternal then
-    match n with
-    | .str p _ | .num p _ => hashName p
-    | _ => 0
+    /-
+    **Note** We consider hashing the prefix, but it was not good enough.
+    For example, an internal name may depend on the name of theorem being defined.
+    Moreover, changing a `theorem` to an `example` would break anchors.
+    -/
+    0
   else
     hash n
 
@@ -45,8 +48,10 @@ public partial def getAnchor (e : Expr) : GrindM UInt64 := do
       "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
+      else pure <| hashName declName
+    | .fvar fvarId =>
+      let userName := (← fvarId.getDecl).userName
+      pure <| hashName userName
     | .mdata _ b => getAnchor b
     | .letE n v t b _ =>
       pure <| mix (hashName n) <| mix (← getAnchor t) <| mix (← getAnchor v) (← getAnchor b)

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

@@ -481,7 +481,12 @@ where
     let mut proof := proof
     let mut prop := prop
     if (← getConfig).trace then
-      let uniqueId ← mkFreshId
+      /-
+      **Note**: It is incorrect to use `mkFreshId` here because we use `withFreshNGen` at
+      `instantiateTheorem`. So, we generate an unique id by using the number of instances generated so far.
+      The code relies on the fact that `addTheoremInstance` bumps this counter.
+      -/
+      let uniqueId := Name.num `_grind_inst (← getNumTheoremInstances)
       proof := markTheoremInstanceProof proof uniqueId
       modify fun s => { s with instanceMap := s.instanceMap.insert uniqueId thm }
     if (← isMatchEqLikeDeclName thm.origin.key) then

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

@@ -86,7 +86,7 @@ def getAllTheorems (map : EMatch.InstanceMap) : Array EMatchTheorem :=
   map.toArray.map (·.2)
 
 public def instantiate' : Action := fun goal kna kp => do
-  let s ← saveStateIfTracing
+  let saved? ← saveStateIfTracing
   let ((progress, map), goal') ← GoalM.run goal ematch'
   if progress then
     match (← kp goal') with
@@ -95,7 +95,7 @@ public def instantiate' : Action := fun goal kna kp => do
         let proof ← instantiateMVars (mkMVar goal.mvarId)
         let usedThms := collect proof map
         let newSeq ← mkNewSeq goal usedThms seq (approx := false)
-        if (← checkSeqAt s goal newSeq) then
+        if (← checkSeqAt saved? goal newSeq) then
           return .closed newSeq
         else
           let allThms := getAllTheorems map

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

@@ -902,6 +902,10 @@ def addNewRawFact (proof : Expr) (prop : Expr) (generation : Nat) (splitSource :
         which is not definitionally equal with `reducible` transparency setting}"
   modify fun s => { s with newRawFacts := s.newRawFacts.enqueue { proof, prop, generation, splitSource } }
 
+/-- Returns the number of theorem instances generated so far. -/
+def getNumTheoremInstances : GoalM Nat := do
+  return (← get).ematch.numInstances
+
 /-- Adds a new theorem instance produced using E-matching. -/
 def addTheoremInstance (thm : EMatchTheorem) (proof : Expr) (prop : Expr) (generation : Nat) : GoalM Unit := do
   saveEMatchTheorem thm