fix: include term parameters in grind? suggestions (#11594)

This PR fixes `grind?` to include term parameters (like `[show P by
tac]`) in its suggestions. Previously, these were being dropped because
term arguments are stored in `extraFacts` and not tracked via E-matching
like named lemmas.

For example, `grind? [show False by exact h]` now correctly suggests
`grind only [show False by exact h]` instead of just `grind only`.

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.5 <[email protected]>

Author: kim-em

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

@@ -334,22 +334,39 @@ def evalGrindTraceCore (stx : Syntax) (trace := true) (verbose := true) (useSorr
   let config ← elabGrindConfig configStx
   let config := { config with clean := false, trace, verbose, useSorry }
   let only := only.isSome
-  let params := if let some params := params? then params.getElems else #[]
+  let paramStxs := if let some params := params? then params.getElems else #[]
+  -- Extract term parameters (non-ident params) to include in the suggestion.
+  -- These are not tracked via E-matching, so we conservatively include them all.
+  -- Ident params resolve to global declarations and are tracked via E-matching.
+  -- Non-ident terms (like `show P by tac`) need to be preserved explicitly.
+  let termParamStxs : Array Grind.TParam := paramStxs.filter fun p =>
+    match p with
+    | `(Parser.Tactic.grindParam| $[$_:grindMod]? $_:ident) => false
+    | `(Parser.Tactic.grindParam| ! $[$_:grindMod]? $_:ident) => false
+    | `(Parser.Tactic.grindParam| - $_:ident) => false
+    | `(Parser.Tactic.grindParam| #$_:hexnum) => false
+    | _ => true
   let mvarId ← getMainGoal
-  let params ← mkGrindParams config only params mvarId
+  let params ← mkGrindParams config only paramStxs mvarId
   Grind.withProtectedMCtx config.abstractProof mvarId fun mvarId' => do
     let (tacs, _) ← Grind.GrindTacticM.runAtGoal mvarId' params do
       let finish ← Grind.Action.mkFinish
       let goal :: _ ← Grind.getGoals
-        | let tac ← `(tactic| grind only)
-          return #[tac]
+        | -- Goal was closed during initialization
+          let configStx' := filterSuggestionsFromGrindConfig configStx
+          if termParamStxs.isEmpty then
+            let tac ← `(tactic| grind $configStx':optConfig only)
+            return #[tac]
+          else
+            let tac ← `(tactic| grind $configStx':optConfig only [$termParamStxs,*])
+            return #[tac]
       Grind.liftGrindM do
         -- **Note**: If we get failures when using the first suggestion, we should test is using `saved`
         -- let saved ← saveState
         match (← finish.run goal) with
         | .closed seq =>
           let configStx' := filterSuggestionsFromGrindConfig configStx
-          let tacs ← Grind.mkGrindOnlyTactics configStx' seq
+          let tacs ← Grind.mkGrindOnlyTactics configStx' seq termParamStxs
           let seq := Grind.Action.mkGrindSeq seq
           let tac ← `(tactic| grind $configStx':optConfig => $seq:grindSeq)
           let tacs := tacs.push tac

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

@@ -11,7 +11,7 @@ namespace Lean.Meta.Grind
 Given an auto-generated `grind` tactic script, collect params for
 single shot `finish` or top-level `grind` tactic.
 -/
-abbrev TParam := TSyntax ``Parser.Tactic.grindParam
+public abbrev TParam := TSyntax ``Parser.Tactic.grindParam
 abbrev TAnchor := TSyntax ``Parser.Tactic.anchor
 
 namespace Collector
@@ -93,16 +93,20 @@ Given a `grind` tactic sequence, extracts parameters and builds a `grind only` t
 It returns at most two. The first tactic uses anchors to restrict the search if applicable.
 The second does not restrict the search using anchors. The second option is included only if there
 are anchors.
+
+The `extraParams` are additional parameters (e.g., term arguments from the original `grind?` call)
+that should always be included in the suggestion.
 -/
-public def mkGrindOnlyTactics (cfg : TSyntax `Lean.Parser.Tactic.optConfig) (seq : List TGrind) : CoreM (Array (TSyntax `tactic)) := do
+public def mkGrindOnlyTactics (cfg : TSyntax `Lean.Parser.Tactic.optConfig) (seq : List TGrind)
+    (extraParams : Array TParam := #[]) : CoreM (Array (TSyntax `tactic)) := do
   let (hasSorry, params, anchors) ← collectParamsCore seq
   if hasSorry then return #[]
-  let allParams := params ++ anchors
+  let allParams := params ++ anchors ++ extraParams
   let s₁ ← mkTac allParams
   if anchors.isEmpty then
     return #[s₁]
   else
-    let s₂ ← mkTac params
+    let s₂ ← mkTac (params ++ extraParams)
     return #[s₁, s₂]
 where
   mkTac (params : Array TParam) : CoreM (TSyntax `tactic) :=

tests/lean/run/grind_trace_term_params.lean

@@ -0,0 +1,15 @@
+/-!
+# Test that `grind?` includes term parameters in its suggestion
+
+When a user provides term arguments to `grind?`, they should be included
+in the suggestion even if they are not tracked via E-matching.
+-/
+
+-- Test: Term argument should be included in suggestion
+-- The term `show False by exact h` is passed as argument and should appear in output
+/--
+info: Try this:
+  [apply] grind only [show False by exact h]
+-/
+#guard_msgs in
+example (h : False) : False := by grind? [show False by exact h]