feat: grind +premises (#10920)

This PR adds support for `grind +premises`, calling the currently
configured premise selection algorithm and including the results as
parameters to `grind`. (Recall that there is not currently a default
premise selector provided by Lean4: you need a downstream premise
selector to make use of this.)

src/Init/Grind/Tactics.lean

@@ -19,6 +19,9 @@ structure Config where
   /-- If `lax` is `true`, `grind` will silently ignore any parameters referring to non-existent theorems
   or for which no patterns can be generated. -/
   lax : Bool := false
+  /-- If `premises` is `true`, `grind` will invoke the currently configured premise selecor on the current goal,
+  and add attempt to use the resulting suggestions as premises to the `grind` tactic. -/
+  premises : Bool := false
   /-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
   splits : Nat := 9
   /-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/

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

@@ -9,11 +9,13 @@ public import Lean.Meta.Tactic.Grind.Main
 public import Lean.Meta.Tactic.TryThis
 public import Lean.Elab.Command
 public import Lean.Elab.Tactic.Config
+public import Lean.PremiseSelection.Basic
 import Lean.Meta.Tactic.Grind.SimpUtil
 import Lean.Meta.Tactic.Grind.EMatchTheoremParam
 import Lean.Elab.Tactic.Grind.Basic
 import Lean.Elab.MutualDef
 meta import Lean.Meta.Tactic.Grind.Parser
+
 public section
 namespace Lean.Elab.Tactic
 open Meta
@@ -82,7 +84,16 @@ private def warnRedundantEMatchArg (s : Grind.EMatchTheorems) (declName : Name)
       pure m!"{ks}"
   logWarning m!"this parameter is redundant, environment already contains `{declName}` annotated with `{kinds}`"
 
-def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.grindParam) (only : Bool) (lax : Bool := false) :
+private def parseModifier (s : String) : CoreM Grind.AttrKind := do
+  let stx := Parser.runParserCategory (← getEnv) `Lean.Parser.Attr.grindMod s
+  match stx with
+  | .ok stx => Grind.getAttrKindCore stx
+  | _ => throwError "unexpected modifier {s}"
+
+open PremiseSelection in
+def elabGrindParams
+    (params : Grind.Params) (ps : TSyntaxArray ``Parser.Tactic.grindParam) (only : Bool)
+    (premises : Array Suggestion := #[]) (lax : Bool := false) :
     MetaM Grind.Params := do
   let mut params := params
   for p in ps do
@@ -104,6 +115,19 @@ def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.
       | _ => throwError "unexpected `grind` parameter{indentD p}"
     catch ex =>
       if !lax then throw ex
+  for p in premises do
+    let attr ← match p.flag with
+    | some flag => parseModifier flag
+    | none => pure <| .ematch (.default false)
+    match attr with
+    | .ematch kind =>
+      params ← addEMatchTheorem params (mkIdent p.name) p.name kind false
+    | _ =>
+      -- We could actually support arbitrary grind modifiers,
+      -- and call `processParam` rather than `addEMatchTheorem`,
+      -- but this would require a larger refactor.
+      -- Let's only do this if there is a prospect of a premise selector supprting this.
+      throwError "unexpected modifier {p.flag}"
   return params
 where
   ensureNoMinIndexable (minIndexable : Bool) : MetaM Unit := do
@@ -206,13 +230,20 @@ where
     | _ =>
       throwError "invalid `grind` parameter, `{.ofConstName declName}` is not a theorem, definition, or inductive type"
 
-def mkGrindParams (config : Grind.Config) (only : Bool) (ps :  TSyntaxArray ``Parser.Tactic.grindParam) : MetaM Grind.Params := do
+def mkGrindParams
+    (config : Grind.Config) (only : Bool) (ps : TSyntaxArray ``Parser.Tactic.grindParam) (mvarId : MVarId) :
+    MetaM 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
   let casesTypes ← if only then pure default else Grind.getCasesTypes
   let params := { params with ematch, casesTypes, inj }
-  let params ← elabGrindParams params ps only (lax := config.lax)
+  let premises ← if config.premises then
+    let suggestions ← PremiseSelection.select mvarId
+    pure suggestions
+  else
+    pure #[]
+  let params ← elabGrindParams params ps only premises (lax := config.lax)
   trace[grind.debug.inj] "{params.inj.getOrigins.map (·.pp)}"
   return params
 
@@ -226,7 +257,7 @@ def grind
     mvarId.admit
     return {}
   mvarId.withContext do
-    let params ← mkGrindParams config only ps
+    let params ← mkGrindParams config only ps mvarId
     let type ← mvarId.getType
     let mvar' ← mkFreshExprSyntheticOpaqueMVar type
     let finalize (result : Grind.Result) : TacticM Grind.Trace := do

src/Lean/PremiseSelection/Basic.lean

@@ -195,7 +195,9 @@ builtin_initialize premiseSelectorExt : EnvExtension (Option Selector) ←
 def select (m : MVarId) (c : Config := {}) : MetaM (Array Suggestion) := do
   let some selector := premiseSelectorExt.getState (← getEnv) |
     throwError "No premise selector registered. \
-      (Note the Lean does not provide a default premise selector, these must be installed by a downstream library.)"
+      (Note that Lean does not provide a default premise selector, \
+      these must be provided by a downstream library, \
+      and configured using `set_premise_selector`.)"
   selector m c
 
 /-!
@@ -216,6 +218,8 @@ open Lean Elab Command in
 @[builtin_command_elab setPremiseSelectorCmd, inherit_doc setPremiseSelectorCmd]
 def elabSetPremiseSelector : CommandElab
   | `(command| set_premise_selector $selector) => do
+    if `Lean.PremiseSelection.Basic ∉ (← getEnv).header.moduleNames then
+      logWarning "Add `import Lean.PremiseSelection.Basic` before using the `set_premise_selector` command."
     let selector ← liftTermElabM do
       try
         let selectorTerm ← Term.elabTermEnsuringType selector (some (Expr.const ``Selector []))

tests/lean/run/grind_lax.lean

@@ -0,0 +1,66 @@
+/-- error: Unknown constant `foo` -/
+#guard_msgs in
+example : False := by
+  grind [foo]
+
+/--
+error: `grind` failed
+case grind
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+-/
+#guard_msgs in
+example : False := by
+  grind +lax [foo]
+
+/-- error: Unknown constant `foo` -/
+#guard_msgs in
+example : False := by
+  grind [-foo]
+
+/--
+error: `grind` failed
+case grind
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+-/
+#guard_msgs in
+example : False := by
+  grind +lax [-foo]
+
+theorem foo : True := .intro
+
+/--
+error: invalid E-matching equality theorem, conclusion must be an equality
+  True
+-/
+#guard_msgs in
+example : False := by
+  grind [= foo]
+
+/--
+error: `grind` failed
+case grind
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+-/
+#guard_msgs in
+example : False := by
+  grind +lax [= foo]
+
+theorem bar : Nat = Int := sorry
+
+/--
+error: invalid E-matching equality theorem, conclusion must be an equality
+  True
+-/
+#guard_msgs in
+example : Int = Nat := by
+  grind [= foo, = bar]
+
+#guard_msgs in
+example : Int = Nat := by
+  grind +lax [= foo, = bar]

tests/lean/run/grind_premises.lean

@@ -0,0 +1,40 @@
+import Lean.PremiseSelection.Basic
+
+/--
+error: No premise selector registered. (Note that Lean does not provide a default premise selector, these must be provided by a downstream library, and configured using `set_premise_selector`.)
+-/
+#guard_msgs in
+example : True := by
+  grind +premises
+
+set_premise_selector (fun _ _ => pure #[])
+
+#guard_msgs in
+example : True := by
+  grind +premises
+
+def P (_ : Nat) := True
+theorem p : P 7 := trivial
+
+/--
+error: `grind` failed
+case grind
+h : ¬P 37
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+    [prop] ¬P 37
+  [eqc] False propositions
+    [prop] P 37
+-/
+#guard_msgs in
+example : P 37 := by
+  grind
+
+example : P 7 := by
+  grind [p]
+
+set_premise_selector (fun _ _ => pure #[{ name := `p, score := 1.0 }])
+
+example : P 7 := by
+  grind +premises

tests/lean/run/premise_selection.lean

@@ -15,7 +15,7 @@ error: Failed to elaborate Nat as a `MVarId → Config → MetaM (Array Suggesti
 set_premise_selector Nat
 
 /--
-error: No premise selector registered. (Note the Lean does not provide a default premise selector, these must be installed by a downstream library.)
+error: No premise selector registered. (Note that Lean does not provide a default premise selector, these must be provided by a downstream library, and configured using `set_premise_selector`.)
 -/
 #guard_msgs in
 example : True := by

tests/lean/run/premise_selection_import.lean

@@ -0,0 +1,5 @@
+/--
+warning: Add `import Lean.PremiseSelection.Basic` before using the `set_premise_selector` command.
+-/
+#guard_msgs (warning, drop error) in
+set_premise_selector (fun _ _ => pure #[])