From 47228b94fdc9a2c008ec83987f78221053ee258c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 19 Nov 2025 13:01:01 -0800 Subject: [PATCH] feat: arbitrary `grind` parameters (#11268) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR implements support for arbitrary `grind` parameters. The feature is similar to the one available in `simp`, where a proof term is treated as a local universe-polymorphic lemma. This feature relies on `grind -revert` (see #11248). For example, users can now write: ```lean def snd (p : α × β) : β := p.2 theorem snd_eq (a : α) (b : β) : snd (a, b) = b := rfl /-- trace: [grind.ematch.instance] snd_eq (a + 1): snd (a + 1, Type) = Type [grind.ematch.instance] snd_eq (a + 1): snd (a + 1, true) = true -/ #guard_msgs (trace) in set_option trace.grind.ematch.instance true in example (a : Nat) : (snd (a + 1, true), snd (a + 1, Type), snd (2, 2)) = (true, Type, snd (2, 2)) := by grind [snd_eq (a + 1)] ``` Note that in the example above, `snd_eq` is instantiated only twice, but with different universe parameters. As described in #11248, the new feature cannot be used with `grind +revert`. --- src/Init/Grind/Interactive.lean | 8 ++-- src/Lean/Elab/Tactic/Grind/Main.lean | 4 +- src/Lean/Elab/Tactic/Grind/Param.lean | 54 +++++++++++++++++++++- tests/lean/run/grind_arbitrary_params.lean | 19 ++++++++ 4 files changed, 78 insertions(+), 7 deletions(-) create mode 100644 tests/lean/run/grind_arbitrary_params.lean diff --git a/src/Init/Grind/Interactive.lean b/src/Init/Grind/Interactive.lean index ba32dee067..1dd7021d34 100644 --- a/src/Init/Grind/Interactive.lean +++ b/src/Init/Grind/Interactive.lean @@ -11,19 +11,19 @@ namespace Lean.Parser.Tactic syntax anchor := "#" noWs hexnum -syntax grindLemma := ppGroup((Attr.grindMod ppSpace)? ident) +syntax grindLemma := ppGroup((Attr.grindMod ppSpace)? term) /-- The `!` modifier instructs `grind` to consider only minimal indexable subexpressions when selecting patterns. -/ -syntax grindLemmaMin := ppGroup("!" (Attr.grindMod ppSpace)? ident) +syntax grindLemmaMin := ppGroup("!" (Attr.grindMod ppSpace)? term) syntax grindErase := "-" ident /-- The `!` modifier instructs `grind` to consider only minimal indexable subexpressions when selecting patterns. -/ -syntax grindParam := grindErase <|> grindLemma <|> grindLemmaMin <|> anchor +syntax grindParam := grindErase <|> grindLemmaMin <|> grindLemma <|> anchor namespace Grind declare_syntax_cat grind_filter (behavior := both) @@ -72,7 +72,7 @@ syntax (name := linarith) "linarith" : grind /-- The `sorry` tactic is a temporary placeholder for an incomplete tactic proof. -/ syntax (name := «sorry») "sorry" : grind -syntax thm := anchor <|> grindLemma <|> grindLemmaMin +syntax thm := anchor <|> grindLemmaMin <|> grindLemma /-- Instantiates theorems using E-matching. diff --git a/src/Lean/Elab/Tactic/Grind/Main.lean b/src/Lean/Elab/Tactic/Grind/Main.lean index c4602c669e..815d04b7c0 100644 --- a/src/Lean/Elab/Tactic/Grind/Main.lean +++ b/src/Lean/Elab/Tactic/Grind/Main.lean @@ -146,13 +146,13 @@ def elabGrindParamsAndSuggestions (params : Grind.Params) (ps : TSyntaxArray ``Parser.Tactic.grindParam) (suggestions : Array Suggestion := #[]) - (only : Bool) (lax : Bool := false) : MetaM Grind.Params := do + (only : Bool) (lax : Bool := false) : TermElabM Grind.Params := do let params ← elabGrindParams params ps (lax := lax) (only := only) elabGrindSuggestions params suggestions def mkGrindParams (config : Grind.Config) (only : Bool) (ps : TSyntaxArray ``Parser.Tactic.grindParam) (mvarId : MVarId) : - MetaM Grind.Params := do + TermElabM Grind.Params := do let params ← Grind.mkParams config let ematch ← if only then pure default else Grind.getEMatchTheorems let inj ← if only then pure default else Grind.getInjectiveTheorems diff --git a/src/Lean/Elab/Tactic/Grind/Param.lean b/src/Lean/Elab/Tactic/Grind/Param.lean index 000b1e6426..913711b91d 100644 --- a/src/Lean/Elab/Tactic/Grind/Param.lean +++ b/src/Lean/Elab/Tactic/Grind/Param.lean @@ -11,6 +11,7 @@ import Lean.Meta.Tactic.Grind.Internalize import Lean.Meta.Tactic.Grind.ForallProp import Lean.Elab.Tactic.Grind.Basic import Lean.Elab.Tactic.Grind.Anchor +import Lean.Elab.SyntheticMVars namespace Lean.Elab.Tactic open Meta @@ -147,13 +148,60 @@ def processAnchor (params : Grind.Params) (val : TSyntax `hexnum) : CoreM Grind. let anchorRef ← Grind.elabAnchorRef val return { params with anchorRefs? := some <| anchorRefs.push anchorRef } +def checkNoRevert (params : Grind.Params) : CoreM Unit := do + if params.config.revert then + throwError "invalid `grind` parameter, only global declarations are allowed when `+revert` is used" + +def processTermParam (params : Grind.Params) + (p : TSyntax `Lean.Parser.Tactic.grindParam) + (mod? : Option (TSyntax `Lean.Parser.Attr.grindMod)) + (term : Term) + (minIndexable : Bool) + : TermElabM Grind.Params := withRef p do + checkNoRevert params + let kind ← if let some mod := mod? then Grind.getAttrKindCore mod else pure .infer + let kind ← match kind with + | .ematch .user | .cases _ | .intro | .inj | .ext | .symbol _ => + throwError "invalid `grind` parameter, only global declarations are allowed with this kind of modifier" + | .ematch kind => pure kind + | .infer => pure <| .default false + let thm? ← Term.withoutModifyingElabMetaStateWithInfo <| withRef p do + let e ← Term.elabTerm term .none + Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true) + let e ← instantiateMVars e + if e.hasSyntheticSorry then + return .none + let e := e.eta + if e.hasMVar then + let r ← abstractMVars e + return some (r.paramNames, r.expr) + else + return some (#[], e) + let some (levelParams, proof) := thm? | return params + unless (← isProof proof) do + throwError "invalid `grind` parameter, proof term expected" + let mkThm (kind : Grind.EMatchTheoremKind) (idx : Nat) : MetaM Grind.EMatchTheorem := do + let id := ((`extra).appendIndexAfter idx) + let some thm ← Grind.mkEMatchTheoremWithKind? (.stx id p) levelParams proof kind params.symPrios (minIndexable := minIndexable) + | throwError "invalid `grind` parameter, failed to infer patterns" + return thm + let idx := params.extra.size + match kind with + | .eqBoth gen => + ensureNoMinIndexable minIndexable + return { params with extra := params.extra.push (← mkThm (.eqLhs gen) idx) |>.push (← mkThm (.eqRhs gen) idx) } + | _ => + if kind matches .eqLhs _ | .eqRhs _ then + ensureNoMinIndexable minIndexable + return { params with extra := params.extra.push (← mkThm kind idx) } + /-- Elaborates `grind` parameters. `incremental = true` for tactics such as `finish`, in this case, we disable some kinds of parameters such as `- ident`. -/ public def elabGrindParams (params : Grind.Params) (ps : TSyntaxArray ``Parser.Tactic.grindParam) - (only : Bool) (lax : Bool := false) (incremental := false) : MetaM Grind.Params := do + (only : Bool) (lax : Bool := false) (incremental := false) : TermElabM Grind.Params := do let mut params := params for p in ps do try @@ -173,6 +221,10 @@ public def elabGrindParams (params : Grind.Params) (ps : TSyntaxArray ``Parser.T params ← processParam params p mod? id (minIndexable := false) (only := only) (incremental := incremental) | `(Parser.Tactic.grindParam| ! $[$mod?:grindMod]? $id:ident) => params ← processParam params p mod? id (minIndexable := true) (only := only) (incremental := incremental) + | `(Parser.Tactic.grindParam| $[$mod?:grindMod]? $e:term) => + params ← processTermParam params p mod? e (minIndexable := false) + | `(Parser.Tactic.grindParam| ! $[$mod?:grindMod]? $e:term) => + params ← processTermParam params p mod? e (minIndexable := true) | `(Parser.Tactic.grindParam| #$anchor:hexnum) => unless only do throwErrorAt anchor "invalid anchor, `only` modifier expected" diff --git a/tests/lean/run/grind_arbitrary_params.lean b/tests/lean/run/grind_arbitrary_params.lean new file mode 100644 index 0000000000..b4cd9bc155 --- /dev/null +++ b/tests/lean/run/grind_arbitrary_params.lean @@ -0,0 +1,19 @@ +def snd (p : α × β) : β := + p.2 + +theorem snd_eq (a : α) (b : β) : snd (a, b) = b := + rfl + +/-- error: invalid `grind` parameter, only global declarations are allowed when `+revert` is used -/ +#guard_msgs in +example (a : Nat) : (snd (a + 1, true), snd (a + 1, Type), snd (2, 2)) = (true, Type, snd (2, 2)) := by + grind +revert [snd_eq (a + 1)] + +/-- +trace: [grind.ematch.instance] snd_eq (a + 1): snd (a + 1, Type) = Type +[grind.ematch.instance] snd_eq (a + 1): snd (a + 1, true) = true +-/ +#guard_msgs (trace) in +set_option trace.grind.ematch.instance true in +example (a : Nat) : (snd (a + 1, true), snd (a + 1, Type), snd (2, 2)) = (true, Type, snd (2, 2)) := by + grind only [snd_eq (a + 1)]