diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean index 5cdd804915..43edd19e22 100644 --- a/src/Init/Grind/Tactics.lean +++ b/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. -/ diff --git a/src/Lean/Elab/Tactic/Grind/Main.lean b/src/Lean/Elab/Tactic/Grind/Main.lean index 04857c1041..d6e009f27e 100644 --- a/src/Lean/Elab/Tactic/Grind/Main.lean +++ b/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 diff --git a/src/Lean/PremiseSelection/Basic.lean b/src/Lean/PremiseSelection/Basic.lean index 51f348ec4b..1ec615f646 100644 --- a/src/Lean/PremiseSelection/Basic.lean +++ b/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 [])) diff --git a/tests/lean/run/grind_lax.lean b/tests/lean/run/grind_lax.lean new file mode 100644 index 0000000000..bbe320138c --- /dev/null +++ b/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] diff --git a/tests/lean/run/grind_premises.lean b/tests/lean/run/grind_premises.lean new file mode 100644 index 0000000000..2c7c72e44b --- /dev/null +++ b/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 diff --git a/tests/lean/run/premise_selection.lean b/tests/lean/run/premise_selection.lean index 258d31a9cc..c1e7c4afd5 100644 --- a/tests/lean/run/premise_selection.lean +++ b/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 diff --git a/tests/lean/run/premise_selection_import.lean b/tests/lean/run/premise_selection_import.lean new file mode 100644 index 0000000000..424df7fe8f --- /dev/null +++ b/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 #[])