feat: arbitrary grind parameters (#11268)

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

@@ -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.

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

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"

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)]