fix: grind? suggestions for goals with inaccessible hypothesis names (#14022)

This PR fixes `grind?` for goals containing hypotheses with inaccessible
names. Distinct terms that differ only in inaccessible variables have
identical anchors, so anchor references in generated tactic scripts
could resolve to the wrong term during replay, producing empty `grind
only` suggestions and scripts that could not close the goal. The `cases`
tactic now supports anchor ordinal references (e.g., `cases #a56e/2`
selects the second candidate matching the anchor), and `grind?` uses
them to disambiguate colliding anchors.

The fix consists of the following changes:

* Add anchor ordinal references to the `cases` tactic and use them in
generated scripts and `cases?` suggestions. The ordinal is resolved
against the case-split candidates that are ready to be split, skipping
resolved ones.

* Compute the anchor reference for a case-split from the candidate list
as it was before `selectNextSplit?` prunes it. The pruned list does not
contain the selected candidate, so ordinals computed from it did not
match the list inspected by the `cases` tactic during replay. This also
fixes a latent issue where the number of anchor digits did not account
for the candidate being split.

* Stop expanding the number of anchor digits when two terms have
identical 64-bit anchors. Expanding cannot disambiguate them, and it
produced confusing 16-digit references such as `#e48b8a1c9d724d48` that
were still ambiguous.

* Report an issue (in verbose mode) when a local theorem anchor collides
with a different local theorem. The collision is harmless for
`instantiate`: all matching theorems are instantiated during replay.

* Preserve parameters that mark types for case-splitting in the
suggestions. A parameter such as `[EqvGen]` both adds the constructors
as E-matching theorems and marks the type for case-splitting. The latter
has no script representation, so dropping the parameter made `cases`
steps on facts of these types fail when the suggestion was applied. The
script suggestion now carries these parameters: `grind [EqvGen] => ...`.

For the example in #13877, `grind?` now produces the same replayable
suggestions for both the inaccessible-name and the named version of the
goal:

```lean
grind [EqvGen] =>
  instantiate only [= reflTransGen_iff_eq, EqvGen.rel]
  instantiate only [#9242]
  cases #14e8
  · cases #d806 <;> cases #f38a <;> cases #e48b <;> instantiate only [#9242]
  · instantiate only [= reflTransGen_iff_eq]
    cases #d806
    · cases #f38a <;> cases #5525 <;> instantiate only [#3442]
    · cases #f38a
      · cases #ae98/2
        · instantiate only [#3442]
        · cases #e48b <;> instantiate only [#9242]
      · cases #ae98/2
        · instantiate only [#3442]
        · cases #e48b <;> instantiate only [#9242]
```

Closes #13877.

Author: leodemoura

src/Init/Grind/Interactive.lean

@@ -113,12 +113,20 @@ syntax (name := showGoals) "show_goals" : grind
 declare_syntax_cat grind_ref (behavior := both)
 
 syntax:max anchor : grind_ref
+/--
+Anchor with an ordinal disambiguator. Distinct case-split candidates may have the same anchor.
+For example, two candidates that differ only in inaccessible variables have identical anchors.
+`#a56e/2` refers to the second candidate (in the case-split candidate list) matching the anchor `#a56e`.
+-/
+syntax:max anchor noWs "/" noWs num : grind_ref
 syntax term : grind_ref
 
 /--
 Performs a case-split on a logical connective, `match`-expression, `if-then-else`-expression,
 or inductive predicate. The argument is an anchor referencing one of the case-split candidates
 in the `grind` state. You can use `cases?` to select a specific candidate using a code action.
+If multiple candidates match the anchor (e.g., they differ only in inaccessible variables),
+an ordinal reference such as `#a56e/2` selects the second matching candidate.
 -/
 syntax (name := cases) "cases " grind_ref : grind
 

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

@@ -287,29 +287,63 @@ def split? (c : SplitInfo) : Action := fun goal kna kp => do
     Action.splitCore c numCases isRec (stopAtFirstFailure := false) (compress := false) >> Action.intros genNew >> Action.assertAll
   a goal kna kp
 
-@[builtin_grind_tactic cases] def evalCases : GrindTactic := fun stx => do
-  let `(grind| cases #$anchor:hexnum) := stx | throwUnsupportedSyntax
+@[builtin_grind_tactic cases] def evalCases : GrindTactic := fun stx => withMainContext do
+  let (anchor, ordinal) ← match stx with
+    | `(grind| cases #$anchor:hexnum) => pure ((anchor : TSyntax `hexnum), 1)
+    | `(grind| cases #$anchor:hexnum/$i:num) =>
+      if i.getNat == 0 then
+        throwErrorAt i "invalid anchor ordinal, it must be ≥ 1"
+      pure (anchor, i.getNat)
+    | _ => throwUnsupportedSyntax
   let anchorRef ← elabAnchorRef anchor
+  let c? ← liftGoalM do
+    let mut remaining := ordinal
+    let mut firstMatch? := none
+    for c in (← get).split.candidates do
+      let a ← c.getAnchor
+      if anchorRef.matches a then
+        if firstMatch?.isNone then
+          firstMatch? := some c
+        if (← checkSplitStatus c) matches .ready .. then
+          remaining := remaining - 1
+          if remaining == 0 then
+            return some c
+    if ordinal == 1 then
+      /-
+      **Note**: Fall back to a candidate that is not ready so that `split?` can
+      produce a more informative error message.
+      -/
+      return firstMatch?
+    else
+      return none
+  let some c := c? | throwError "`cases` tactic failed, invalid anchor"
   let goal ← getMainGoal
-  let candidates := goal.split.candidates
-  let c ← liftGrindM <| goal.withContext do
-    for c in candidates do
-      let anchor ← c.getAnchor
-      if anchorRef.matches anchor then
-        return c
-    throwError "`cases` tactic failed, invalid anchor"
   goal.withContext <| withRef anchor <| logAnchor c
   liftAction <| split? c
 
 def mkCasesSuggestions (candidates : Array SplitCandidateWithAnchor) (numDigits : Nat) : MetaM (Array Tactic.TryThis.Suggestion) := do
-  candidates.mapM fun { anchor, e, .. } => do
+  let shift := (64 - 4*numDigits).toUInt64
+  let mut counts : Std.HashMap UInt64 Nat := {}
+  let mut suggestions := #[]
+  for { anchor, e, .. } in candidates do
     let anchorStx ← mkAnchorSyntax numDigits anchor
-    let tac ← `(grind| cases $anchorStx:anchor)
+    /-
+    **Note**: Distinct candidates may have identical anchors (e.g., they differ only in
+    inaccessible variables). We use ordinal references (e.g., `#a56e/2`) to disambiguate them.
+    -/
+    let anchorPrefix := anchor >>> shift
+    let ordinal := counts.getD anchorPrefix 0
+    counts := counts.insert anchorPrefix (ordinal + 1)
+    let tac ← if ordinal == 0 then
+      `(grind| cases $anchorStx:anchor)
+    else
+      `(grind| cases $anchorStx:anchor/$(quote (ordinal + 1)):num)
     let msg ← addMessageContext m!"{tac} for{indentExpr e}"
-    return {
+    suggestions := suggestions.push {
       suggestion   := .tsyntax tac
       messageData? := some msg
     }
+  return suggestions
 
 @[builtin_grind_tactic casesTrace] def evalCasesTrace : GrindTactic := fun stx => withMainContext do
   let `(grind| cases? $[$filter?]?) := stx | throwUnsupportedSyntax

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

@@ -374,20 +374,29 @@ def evalGrindTraceCore (stx : Syntax) (trace := true) (verbose := true) (useSorr
   -- is a local variable) must be preserved because they produce anchors that need
   -- the original term to be loaded during replay.
   -- Non-ident terms (like `show P by tac`) need to be preserved explicitly.
-  let termParamStxs : Array Grind.TParam ← paramStxs.filterM fun p => do
-    match p with
-    | `(Parser.Tactic.grindParam| $[$_:grindMod]? $id:ident) =>
-      -- Check if this ident resolves to local variable dot notation
-      -- If so, keep it because it's not a simple global declaration
-      if let some (_, _ :: _) := (← resolveLocalName id.getId) then
-        return true
-      else
-        return false
-    | `(Parser.Tactic.grindParam| ! $[$_:grindMod]? $id:ident) =>
-      if let some (_, _ :: _) := (← resolveLocalName id.getId) then
-        return true
+  -- Params that mark types for case-splitting (e.g., `[EqvGen]` where `EqvGen` is an
+  -- inductive predicate, or `[cases T]`) must also be preserved: the marking is not
+  -- representable in the generated script, and without it `cases` steps on facts of
+  -- these types fail during replay.
+  -- **TODO**: This syntactic filtering is a stopgap: it duplicates parameter-elaboration
+  -- logic and silently depends on which side effects are representable in scripts.
+  -- A more robust solution is to make the script self-contained, e.g., a script step that
+  -- marks a type for case-splitting, and tracking which parameters were actually used.
+  let keepIdentParam (mod? : Option (TSyntax ``Parser.Attr.grindMod)) (id : Ident) : TacticM Bool := do
+    if let some (_, _ :: _) := (← resolveLocalName id.getId) then
+      return true
+    else if let some mod := mod? then
+      return (← Grind.getAttrKindCore mod) matches .cases _
+    else
+      let declName? ← try pure (some (← realizeGlobalConstNoOverload id)) catch _ => pure none
+      if let some declName := declName? then
+        Grind.isCasesAttrCandidate declName false
       else
         return false
+  let termParamStxs : Array Grind.TParam ← paramStxs.filterM fun p => do
+    match p with
+    | `(Parser.Tactic.grindParam| $[$mod?:grindMod]? $id:ident) => keepIdentParam mod? id
+    | `(Parser.Tactic.grindParam| ! $[$mod?:grindMod]? $id:ident) => keepIdentParam mod? id
     | `(Parser.Tactic.grindParam| - $_:ident) => return false
     | `(Parser.Tactic.grindParam| #$_:hexnum) => return false
     | _ => return true
@@ -413,7 +422,15 @@ def evalGrindTraceCore (stx : Syntax) (trace := true) (verbose := true) (useSorr
           let configStx' := filterSuggestionsAndLocalsFromGrindConfig configStx
           let tacs ← Grind.mkGrindOnlyTactics configStx' seq termParamStxs
           let seq := Grind.Action.mkGrindSeq seq
-          let tac ← `(tactic| grind $configStx':optConfig => $seq:grindSeq)
+          /-
+          **Note**: The script must carry the preserved parameters (e.g., types marked for
+          case-splitting). The tactic was verified with these parameters active, and `cases`
+          steps may fail without them.
+          -/
+          let tac ← if termParamStxs.isEmpty then
+            `(tactic| grind $configStx':optConfig => $seq:grindSeq)
+          else
+            `(tactic| grind $configStx':optConfig [$termParamStxs,*] => $seq:grindSeq)
           let tacs := tacs.push tac
           return tacs
         | .stuck gs =>

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

@@ -97,22 +97,28 @@ public class HasAnchor (α : Type u) where
   getAnchor : α → UInt64
 
 /--
-Returns the number of digits needed to distinguish the anchors in `es`
+Returns the number of digits needed to distinguish the anchors in `es`.
+
+Elements with identical (full) anchors cannot be distinguished by adding more digits.
+Thus, they are ignored by this function. Callers must handle these collisions separately
+(e.g., the `cases` tactic uses ordinal references such as `#a56e/2`).
 -/
 public def getNumDigitsForAnchors [HasAnchor α] (es : Array α) : Nat :=
   go 4
 where
   go (numDigits : Nat) : Nat := Id.run do
     if 4*numDigits  < 64 then
       let shift := 64 - 4*numDigits
-      let mut found : Std.HashSet UInt64 := {}
+      let mut found : Std.HashMap UInt64 UInt64 := {}
       for e in es do
         let a := HasAnchor.getAnchor e
         let a' := a >>> shift.toUInt64
-        if found.contains a' then
-          return (← go (numDigits+1))
+        if let some b := found[a']? then
+          -- **Note**: if the full anchors are equal, expanding the number of digits does not help.
+          if b != a then
+            return (← go (numDigits+1))
         else
-          found  := found.insert a'
+          found  := found.insert a' a
       return numDigits
     else
       return numDigits

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

@@ -59,6 +59,7 @@ partial def collect (tac : TGrind) : Collect Unit := do
       | _ => return ()
   | `(grind| $tac₁:grind <;> $tac₂:grind) => collect tac₁; collect tac₂
   | `(grind| cases $a:anchor) => pushAnchor a
+  | `(grind| cases $a:anchor/$_:num) => pushAnchor a
   | `(grind| use [$params,*]) =>
     collectInstantiateParams params
   | `(grind| instantiate $[only]? $[approx]? $[[$params?,*]]?) =>

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

@@ -79,7 +79,8 @@ where
 Creates an `instantiate` tactic that takes the `usedThms` as parameters.
 -/
 def mkInstantiateTactic (goal : Goal) (usedThms : Array EMatchTheorem) (approx : Bool) : GrindM TGrind := goal.withContext do
-  let numDigits ← getNumDigitsForLocalTheoremAnchors goal
+  let entries ← getLocalTheoremAnchors goal
+  let numDigits := getNumDigitsForAnchors entries
   let mut params : Array (TSyntax ``Parser.Tactic.Grind.thm) := #[]
   let mut foundFns : NameSet := {}
   let mut foundLocals : Std.HashSet Grind.Origin := {}
@@ -97,7 +98,15 @@ def mkInstantiateTactic (goal : Goal) (usedThms : Array EMatchTheorem) (approx :
           params := params.push param
       | _ => unless foundLocals.contains thm.origin do
         foundLocals := foundLocals.insert thm.origin
-        let anchor ← getAnchor (← inferType thm.proof)
+        let type ← inferType thm.proof
+        let anchor ← getAnchor type
+        /-
+        **Note**: Distinct local theorems may have the same anchor (e.g., they differ only in
+        inaccessible variables). This is not an error: when replaying the generated tactic,
+        all matching theorems are instantiated. We just report an issue flagging the collision.
+        -/
+        if entries.any fun entry => entry.anchor == anchor && entry.e != type then
+          reportIssue! "anchor `#{anchorToString numDigits anchor}` is ambiguous, distinct local theorems have the same anchor{indentExpr type}\nall of them are instantiated by the generated `instantiate` tactic"
         let param ← `(Parser.Tactic.Grind.thm| $(← mkAnchorSyntax numDigits anchor):anchor)
         params := params.push param
   match params.isEmpty, approx with

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

@@ -281,9 +281,13 @@ structure SplitCandidateAnchors where
 /--
 Returns case-split candidates. Case-splits that are tagged as `.resolved` or `.notReady` are skipped.
 Applies additional `filter` if provided.
+If `candidates?` is provided, it is used instead of the candidates stored in the goal.
 -/
-def getSplitCandidateAnchors (filter : Expr → GoalM Bool := fun _ => return true) : GoalM SplitCandidateAnchors := do
-  let candidates := (← get).split.candidates
+def getSplitCandidateAnchors (filter : Expr → GoalM Bool := fun _ => return true)
+    (candidates? : Option (List SplitInfo) := none) : GoalM SplitCandidateAnchors := do
+  let candidates ← match candidates? with
+    | some candidates => pure candidates
+    | none => pure (← get).split.candidates
   let candidates ← candidates.toArray.filterMapM fun c => do
     let e := c.getExpr
     let anchor ← c.getAnchor
@@ -302,6 +306,47 @@ def getSplitCandidateAnchors (filter : Expr → GoalM Bool := fun _ => return tr
   let numDigits := getNumDigitsForAnchors candidates
   return { candidates, numDigits }
 
+/--
+Anchor reference for a case-split candidate in generated tactic scripts.
+`ordinal` is the 0-based position of the candidate among the (ready) candidates whose
+anchors share the same displayed prefix. Distinct candidates may have identical anchors
+(e.g., candidates that differ only in inaccessible variables), and the ordinal is used
+to disambiguate them.
+-/
+structure SplitAnchorRefInfo where
+  numDigits : Nat
+  anchor    : UInt64
+  ordinal   : Nat
+
+/--
+Computes the anchor reference information for the case-split candidate `c`.
+The candidate list must be the one stored in the goal before the case-split is selected and
+performed (i.e., before `selectNextSplit?` prunes the list and before `c` is marked as resolved),
+so that it matches the list inspected by the `cases` tactic when replaying the generated script.
+-/
+def mkSplitAnchorRefInfo (c : SplitInfo) (candidates? : Option (List SplitInfo) := none) : GoalM SplitAnchorRefInfo := do
+  let { candidates, numDigits } ← getSplitCandidateAnchors (candidates? := candidates?)
+  let anchor ← c.getAnchor
+  let shift := (64 - 4*numDigits).toUInt64
+  let mut ordinal := 0
+  for cand in candidates do
+    if cand.anchor >>> shift == anchor >>> shift then
+      if cand.c == c then
+        return { numDigits, anchor, ordinal }
+      ordinal := ordinal + 1
+  -- `c` should be in the candidate list; fall back to the first match.
+  return { numDigits, anchor, ordinal := 0 }
+
+/--
+Creates the anchor reference syntax for the result of `mkSplitAnchorRefInfo`.
+-/
+def SplitAnchorRefInfo.toSyntax (info : SplitAnchorRefInfo) : CoreM (TSyntax `grind) := do
+  let anchorStx ← mkAnchorSyntax info.numDigits info.anchor
+  if info.ordinal == 0 then
+    `(grind| cases $anchorStx:anchor)
+  else
+    `(grind| cases $anchorStx:anchor/$(quote (info.ordinal + 1)):num)
+
 namespace Action
 
 /--
@@ -404,11 +449,23 @@ Remark: `numCases` and `isRec` are computed using `checkSplitStatus`.
 -/
 def splitCore (c : SplitInfo) (numCases : Nat) (isRec : Bool)
     (stopAtFirstFailure : Bool)
-    (compress : Bool) : Action := fun goal _ kp => do
+    (compress : Bool)
+    (candidates? : Option (List SplitInfo) := none) : Action := fun goal _ kp => do
   let traceEnabled := (← getConfig).trace
   let mvarId ← goal.mkAuxMVar
   let cExpr := c.getExpr
-  let ((mvarIds, numDigits), goal) ← GoalM.run goal do
+  let ((mvarIds, anchorInfo?), goal) ← GoalM.run goal do
+    /-
+    **Note**: The anchor reference must be computed before the case-split is performed,
+    so that the candidate list matches the one inspected by the `cases` tactic when
+    replaying the generated script. Callers that prune the candidate list during
+    case-split selection (e.g., `splitNext` via `selectNextSplit?`) must provide the
+    original list using `candidates?`.
+    -/
+    let anchorInfo? ← if traceEnabled then
+      pure (some (← mkSplitAnchorRefInfo c candidates?))
+    else
+      pure none
     let gen ← getGeneration cExpr
     let genNew := if numCases > 1 || isRec then gen+1 else gen
     saveSplitDiagInfo cExpr genNew numCases c.source
@@ -420,11 +477,7 @@ def splitCore (c : SplitInfo) (numCases : Nat) (isRec : Bool)
       casesMatch mvarId cExpr
     else
       casesWithTrace mvarId (← mkCasesMajor cExpr)
-    let numDigits ← if traceEnabled then
-      pure (← getSplitCandidateAnchors).numDigits
-    else
-      pure 0
-    return (mvarIds, numDigits)
+    return (mvarIds, anchorInfo?)
   let numSubgoals := mvarIds.length
   /-
   **Split counter heuristic**: We do not increment `numSplits` for the first case (`i = 0`)
@@ -470,9 +523,8 @@ def splitCore (c : SplitInfo) (numCases : Nat) (isRec : Bool)
   else
     goal.mvarId.assign (← instantiateMVars (mkMVar mvarId))
   if stuckNew.isEmpty then
-    if traceEnabled then
-      let anchor ← goal.withContext <| getAnchor cExpr
-      let cases ← `(grind| cases $(← mkAnchorSyntax numDigits anchor):anchor)
+    if let some anchorInfo := anchorInfo? then
+      let cases ← anchorInfo.toSyntax
       return .closed (← mkCasesResultSeq cases seqNew compress)
     else
       return .closed []
@@ -497,13 +549,19 @@ next => lia
 Then with `compress = true` it generates `cases #50fc <;> lia`
 -/
 def splitNext (stopAtFirstFailure := true) (compress := true) : Action := fun goal kna kp => do
+  /-
+  **Note**: `selectNextSplit?` prunes the candidate list (e.g., it removes the selected
+  candidate and resolved ones). We save the original list because it is needed for
+  computing anchor reference information for the generated tactic script.
+  -/
+  let candidates := goal.split.candidates
   let (r, goal) ← GoalM.run goal selectNextSplit?
   let .some c numCases isRec _ := r
     | kna goal
   let cExpr := c.getExpr
   let gen := goal.getGeneration cExpr
   let genNew := if numCases > 1 || isRec then gen+1 else gen
-  let x : Action := splitCore c numCases isRec stopAtFirstFailure compress >> intros genNew >> assertAll
+  let x : Action := splitCore c numCases isRec stopAtFirstFailure compress (candidates? := some candidates) >> intros genNew >> assertAll
   x goal kna kp
 
 end Action