chore: revert fix: ground theorems as grind parameters" (#11603)

This PR reverts leanprover/lean4#11579

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

@@ -188,13 +188,7 @@ 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,
@@ -341,12 +335,19 @@ 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,21 +67,7 @@ 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
-      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 }
+      return { params with extra := params.extra.push thm }
   | .defn =>
     if (← isReducible declName) then
       throwError "`{.ofConstName declName}` is a reducible definition, `grind` automatically unfolds them"
@@ -125,10 +111,7 @@ 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
@@ -156,10 +139,7 @@ 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 }
@@ -225,9 +205,7 @@ 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,
-      extraFactsSyntax := params.extraFactsSyntax.push p.raw }
+    return { params with extraFacts := params.extraFacts.push proof }
 
 /--
 Elaborates `grind` parameters.

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

@@ -40,8 +40,6 @@ 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

@@ -1,17 +0,0 @@
-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,11 +27,10 @@ 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 this:
+info: Try these:
   [apply] grind only [special_7]
+  [apply] grind => instantiate only [special_7]
 -/
 #guard_msgs in
 example : SpecialProperty 7 := by
@@ -79,11 +78,11 @@ set_library_suggestions (fun _ _ => pure #[
   { name := `prop2_5, score := 0.7 }
 ])
 
--- Note: Both ground theorems are included since we can't track which
--- extraFacts were actually used. This is conservative but correct.
+-- Expected: try? should use the best applicable one
 /--
-info: Try this:
-  [apply] grind only [prop1_5, prop2_5]
+info: Try these:
+  [apply] grind only [prop1_5]
+  [apply] grind => instantiate only [prop1_5]
 -/
 #guard_msgs in
 example : Property1 5 := by