feat: grind proof parameters whose type is not a forall (#11326)

This PR ensures that users can provide `grind` proof parameters whose
types are not `forall`-quantified. Examples:

```lean
opaque f : Nat → Nat
axiom le_f (a : Nat) : a ≤ f a

example (a : Nat) : a ≤ f a := by
  grind [le_f a]

example (a b : α) (h : ∀ x y : α, x = y) : a = b := by
  grind [h a b]
```

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

@@ -9,6 +9,7 @@ public import Lean.Elab.Tactic.Grind.Basic
 public import Lean.Meta.Tactic.Grind.Main
 import Lean.Meta.Tactic.Grind.Internalize
 import Lean.Meta.Tactic.Grind.ForallProp
+import Lean.Meta.Tactic.Grind.Main
 import Lean.Elab.Tactic.Grind.Basic
 import Lean.Elab.Tactic.Grind.Anchor
 import Lean.Elab.SyntheticMVars
@@ -180,22 +181,30 @@ def processTermParam (params : Grind.Params)
     else
       return some (#[], e)
   let some (levelParams, proof) := thm? | return params
-  unless (← isProof proof) do
+  let type ← inferType proof
+  unless (← isProp type) 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
+  if type.isForall then
+    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 kind idx) }
+      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) }
+  else
+    unless mod?.isNone do
+      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 }
 
 /--
 Elaborates `grind` parameters.
@@ -290,10 +299,7 @@ public def withParams (params : Grind.Params) (ps : TSyntaxArray ``Parser.Tactic
       }
       replaceMainGoal [goal]
     liftGoalM do
-      for thm in params.extra do
-        activateTheorem thm 0
-      for thm in params.extraInj do
-        activateInjectiveTheorem thm 0
+      Grind.assertExtra params
       -- **TODO**: `cases` parameters
     k
 

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

@@ -39,6 +39,7 @@ structure Params where
   casesTypes  : CasesTypes := {}
   extra       : PArray EMatchTheorem := {}
   extraInj    : PArray InjectiveTheorem := {}
+  extraFacts  : PArray Expr := {}
   funCCs      : NameSet := {}
   norm        : Simp.Context
   normProcs   : Array Simprocs
@@ -108,6 +109,18 @@ private def mkCleanState (mvarId : MVarId) (params : Params) : MetaM Clean.State
     used := used.insert localDecl.userName
   return { used }
 
+/--
+Asserts extra facts provided as `grind` parameters.
+-/
+def assertExtra (params : Params) : GoalM Unit := do
+  for proof in params.extraFacts do
+    let prop ← inferType proof
+    addNewRawFact proof prop 0 .input
+  for thm in params.extra do
+    activateTheorem thm 0
+  for thm in params.extraInj do
+    activateInjectiveTheorem thm 0
+
 private def mkGoal (mvarId : MVarId) (params : Params) : GrindM Goal := do
   let mvarId ← if params.config.clean then mvarId.exposeNames else pure mvarId
   let trueExpr ← getTrueExpr
@@ -127,8 +140,7 @@ private def mkGoal (mvarId : MVarId) (params : Params) : GrindM Goal := do
     mkENodeCore bfalseExpr (interpreted := false) (ctor := true) (generation := 0) (funCC := false)
     mkENodeCore natZeroExpr (interpreted := true) (ctor := false) (generation := 0) (funCC := false)
     mkENodeCore ordEqExpr (interpreted := false) (ctor := true) (generation := 0) (funCC := false)
-    for thm in params.extra do
-      activateTheorem thm 0
+    assertExtra params
 
 structure Result where
   failure?   : Option Goal

tests/lean/run/grind_nonforall_params.lean

@@ -0,0 +1,21 @@
+/-
+Tests `grind` proof parameters whose type is not a `forall`.
+-/
+
+opaque f : Nat → Nat
+axiom le_f (a : Nat) : a ≤ f a
+
+example (a : Nat) : a ≤ f a := by
+  grind [le_f a]
+
+example (a b : α) (h : ∀ x y : α, x = y) : a = b := by
+  fail_if_success grind
+  grind [h a b]
+
+/--
+error: invalid `grind` parameter, modifier is redundant since the parameter type is not a `forall`
+  a ≤ f a
+-/
+#guard_msgs in
+example (a : Nat) : a ≤ f a := by
+  grind [← le_f a]