From ac376c880fb2120ee4ffe24592c457788abd03a9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 11 Dec 2025 09:09:28 +0100 Subject: [PATCH] Revert "fix: ground theorems as `grind` parameters (#11579)" This reverts commit aa4aff280b9d1f6c1d82f2b3661d6e49e9f5f389. --- src/Lean/Elab/Tactic/Grind/Main.lean | 21 +++++++++-------- src/Lean/Elab/Tactic/Grind/Param.lean | 26 ++------------------- src/Lean/Meta/Tactic/Grind/Main.lean | 2 -- tests/lean/run/grind_ground_param.lean | 17 -------------- tests/lean/run/try_library_suggestions.lean | 13 +++++------ 5 files changed, 19 insertions(+), 60 deletions(-) delete mode 100644 tests/lean/run/grind_ground_param.lean diff --git a/src/Lean/Elab/Tactic/Grind/Main.lean b/src/Lean/Elab/Tactic/Grind/Main.lean index daebf9ff27dc..6b2846433de9 100644 --- a/src/Lean/Elab/Tactic/Grind/Main.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Grind/Param.lean b/src/Lean/Elab/Tactic/Grind/Param.lean index e6afd46a7cd4..b9755fba303f 100644 --- a/src/Lean/Elab/Tactic/Grind/Param.lean +++ b/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. diff --git a/src/Lean/Meta/Tactic/Grind/Main.lean b/src/Lean/Meta/Tactic/Grind/Main.lean index 488ccf15843d..862d9835d555 100644 --- a/src/Lean/Meta/Tactic/Grind/Main.lean +++ b/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 diff --git a/tests/lean/run/grind_ground_param.lean b/tests/lean/run/grind_ground_param.lean deleted file mode 100644 index 1a11f198e5fc..000000000000 --- a/tests/lean/run/grind_ground_param.lean +++ /dev/null @@ -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] diff --git a/tests/lean/run/try_library_suggestions.lean b/tests/lean/run/try_library_suggestions.lean index 75799532ba36..84155231162e 100644 --- a/tests/lean/run/try_library_suggestions.lean +++ b/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