fix: ground theorems as grind parameters (#11579)

This PR ensures that ground theorems are properly handled as `grind`
parameters. Additionally, `grind [(thm)]` and `grind [thm]` should be
handled the same way.

---------

Co-authored-by: Kim Morrison <[email protected]>

Author: leodemoura

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

@@ -188,7 +188,13 @@ def elabGrindSuggestions
     match attr with
     | .ematch kind =>
       try
+        let oldSize := params.extraFacts.size
         params ← addEMatchTheorem params (mkIdent p.name) p.name kind false (warn := false)
+        -- If the theorem went to extraFacts (ground theorem), synthesize syntax for it.
+        -- Ground theorems bypass E-matching, so we need to track them separately for suggestions.
+        if params.extraFacts.size > oldSize then
+          let stx ← `(Parser.Tactic.grindParam| $(mkIdent p.name):ident)
+          params := { params with extraFactsSyntax := params.extraFactsSyntax.push stx.raw }
       catch _ => pure () -- Don't worry if library suggestions gave bad theorems.
     | _ =>
       -- We could actually support arbitrary grind modifiers,
@@ -335,19 +341,12 @@ def evalGrindTraceCore (stx : Syntax) (trace := true) (verbose := true) (useSorr
   let config := { config with clean := false, trace, verbose, useSorry }
   let only := only.isSome
   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 paramStxs mvarId
+  -- Extract syntax of params that went to `extraFacts` (ground theorems and term arguments).
+  -- These need to be included in `grind only` suggestions since they're not tracked via E-matching.
+  let termParamStxs : Array Grind.TParam := params.extraFactsSyntax.filterMap fun s =>
+    if s.isOfKind ``Parser.Tactic.grindParam then some ⟨s⟩ else none
   Grind.withProtectedMCtx config.abstractProof mvarId fun mvarId' => do
     let (tacs, _) ← Grind.GrindTacticM.runAtGoal mvarId' params do
       let finish ← Grind.Action.mkFinish

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

@@ -67,7 +67,21 @@ public def addEMatchTheorem (params : Grind.Params) (id : Ident) (declName : Nam
         Grind.mkEMatchTheoremForDecl declName kind params.symPrios (minIndexable := minIndexable)
       if warn && params.ematch.containsWithSamePatterns thm.origin thm.patterns thm.cnstrs then
         warnRedundantEMatchArg params.ematch declName
-      return { params with extra := params.extra.push thm }
+      if thm.numParams == 0 && kind matches .default _ then
+        /-
+        **Note**: ignores pattern and adds ground fact directly
+        Motivation:
+        ```
+        opaque π : Rat
+        axiom pi_pos : 0 < π
+        example : π = 0 → False := by
+          grind [pi_pos]
+
+        ```
+        -/
+        return { params with extraFacts := params.extraFacts.push thm.proof }
+      else
+        return { params with extra := params.extra.push thm }
   | .defn =>
     if (← isReducible declName) then
       throwError "`{.ofConstName declName}` is a reducible definition, `grind` automatically unfolds them"
@@ -111,7 +125,10 @@ def processParam (params : Grind.Params)
     for thm in thms do
       params := { params with extra := params.extra.push thm }
   | .ematch kind =>
+    let oldSize := params.extraFacts.size
     params ← withRef p <| addEMatchTheorem params id declName kind minIndexable
+    if params.extraFacts.size > oldSize then
+      params := { params with extraFactsSyntax := params.extraFactsSyntax.push p.raw }
   | .cases eager =>
     if incremental then throwError "`cases` parameter are not supported here"
     ensureNoMinIndexable minIndexable
@@ -139,7 +156,10 @@ def processParam (params : Grind.Params)
           -- **Note**: We should not warn if `declName` is an inductive
           params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable (warn := False)
     else
+      let oldSize := params.extraFacts.size
       params ← withRef p <| addEMatchTheorem params id declName (.default false) minIndexable (suggest := true)
+      if params.extraFacts.size > oldSize then
+        params := { params with extraFactsSyntax := params.extraFactsSyntax.push p.raw }
   | .symbol prio =>
     ensureNoMinIndexable minIndexable
     params := { params with symPrios := params.symPrios.insert declName prio }
@@ -205,7 +225,9 @@ def processTermParam (params : Grind.Params)
       throwError "invalid `grind` parameter, modifier is redundant since the parameter type is not a `forall`{indentExpr type}"
     unless levelParams.isEmpty do
       throwError "invalid `grind` parameter, parameter type is not a `forall` and is universe polymorphic{indentExpr type}"
-    return { params with extraFacts := params.extraFacts.push proof }
+    return { params with
+      extraFacts := params.extraFacts.push proof,
+      extraFactsSyntax := params.extraFactsSyntax.push p.raw }
 
 /--
 Elaborates `grind` parameters.

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

@@ -40,6 +40,8 @@ structure Params where
   extra       : PArray EMatchTheorem := {}
   extraInj    : PArray InjectiveTheorem := {}
   extraFacts  : PArray Expr := {}
+  /-- Syntax of params that went to `extraFacts`, for `grind?` suggestions. -/
+  extraFactsSyntax : Array Syntax := {}
   funCCs      : NameSet := {}
   norm        : Simp.Context
   normProcs   : Array Simprocs

tests/lean/run/grind_ground_param.lean

@@ -0,0 +1,17 @@
+opaque π : Rat
+axiom pi_pos : 0 < π
+
+example : π = 0 → False := by
+  grind [pi_pos]
+
+example : 0 < 2 * π := by
+  grind [pi_pos]
+
+-- Test that grind? includes ground theorems in suggestions
+/--
+info: Try this:
+  [apply] grind only [pi_pos]
+-/
+#guard_msgs in
+example : π = 0 → False := by
+  grind? [pi_pos]

tests/lean/run/try_library_suggestions.lean

@@ -27,10 +27,11 @@ axiom special_7 : SpecialProperty 7
 set_library_suggestions (fun _ _ => pure #[{ name := `special_7, score := 1.0 }])
 
 -- Expected: try? should find grind only [special_7]
+-- Note: Ground theorems (0 parameters) are added as facts during initialization,
+-- not via E-matching, so there's no instantiate script.
 /--
-info: Try these:
+info: Try this:
   [apply] grind only [special_7]
-  [apply] grind => instantiate only [special_7]
 -/
 #guard_msgs in
 example : SpecialProperty 7 := by
@@ -78,11 +79,11 @@ set_library_suggestions (fun _ _ => pure #[
   { name := `prop2_5, score := 0.7 }
 ])
 
--- Expected: try? should use the best applicable one
+-- Note: Both ground theorems are included since we can't track which
+-- extraFacts were actually used. This is conservative but correct.
 /--
-info: Try these:
-  [apply] grind only [prop1_5]
-  [apply] grind => instantiate only [prop1_5]
+info: Try this:
+  [apply] grind only [prop1_5, prop2_5]
 -/
 #guard_msgs in
 example : Property1 5 := by