feat: finish params

Author: leodemoura

src/Init/Grind/Interactive.lean

@@ -127,10 +127,12 @@ syntax (name := casesTrace) "cases?" grindFilter : grind
 syntax (name := done) "done" : grind
 
 /-- `finish` tries to close the current goal using `grind`'s default strategy -/
-syntax (name := finish) "finish" ppSpace configItem* : grind
+syntax (name := finish) "finish" ppSpace configItem*
+    (&" only")? (" [" withoutPosition(grindParam,*) "]")? : grind
 
 /-- `finish?` tries to close the current goal using `grind`'s default strategy and suggests a tactic script. -/
-syntax (name := finishTrace) "finish?" ppSpace configItem* : grind
+syntax (name := finishTrace) "finish?" ppSpace configItem*
+    (&" only")? (" [" withoutPosition(grindParam,*) "]")? : grind
 
 /--
 The `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.

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

@@ -27,6 +27,7 @@ import Lean.Elab.Tactic.Grind.Filter
 import Lean.Elab.Tactic.Grind.Anchor
 import Lean.Elab.Tactic.Grind.ShowState
 import Lean.Elab.Tactic.Grind.Config
+import Lean.Elab.Tactic.Grind.Param
 import Lean.Elab.SetOption
 namespace Lean.Elab.Tactic.Grind
 
@@ -84,8 +85,10 @@ def evalGrindSeq : GrindTactic := fun stx =>
 open Meta Grind
 
 @[builtin_grind_tactic finish] def evalFinish : GrindTactic := fun stx => withMainContext do
-  let `(grind| finish $[$configItems]*) := stx | throwUnsupportedSyntax
+  let `(grind| finish $[$configItems]* $[only%$only]? $[[$params?,*]]?) := stx | throwUnsupportedSyntax
   withConfigItems configItems do
+  let params := params?.getD {}
+  withParams (← read).params params only.isSome do
     let goal ← getMainGoal
     if let some goal ← liftGrindM <| solve goal then
       let params := (← read).params

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

@@ -5,7 +5,10 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
+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.Elab.Tactic.Grind.Basic
 import Lean.Elab.Tactic.Grind.Anchor
 namespace Lean.Elab.Tactic
@@ -81,6 +84,7 @@ def processParam (params : Grind.Params)
     (id : TSyntax `ident)
     (minIndexable : Bool)
     (only : Bool)
+    (incremental : Bool)
     : MetaM Grind.Params := do
   let mut params := params
   let declName ← try
@@ -106,11 +110,13 @@ def processParam (params : Grind.Params)
   | .ematch kind =>
     params ← withRef p <| addEMatchTheorem params id declName kind minIndexable
   | .cases eager =>
+    if incremental then throwError "`cases` parameter are not supported here"
     ensureNoMinIndexable minIndexable
     withRef p <| Grind.validateCasesAttr declName eager
     params := { params with casesTypes := params.casesTypes.insert declName eager }
   | .intro =>
     if let some info ← Grind.isCasesAttrPredicateCandidate? declName false then
+      if incremental then throwError "`cases` parameter are not supported here"
       for ctor in info.ctors do
         params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable
     else
@@ -143,14 +149,18 @@ def processAnchor (params : Grind.Params) (val : TSyntax `hexnum) : CoreM Grind.
 
 /--
 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) : MetaM Grind.Params := do
+    (only : Bool) (lax : Bool := false) (incremental := false) : MetaM Grind.Params := do
   let mut params := params
   for p in ps do
     try
       match p with
       | `(Parser.Tactic.grindParam| - $id:ident) =>
+        if incremental then
+          throwErrorAt p "invalid `-` occurrence, it can only used at the `grind` tactic entry point"
         let declName ← realizeGlobalConstNoOverloadWithInfo id
         if let some declName ← Grind.isCasesAttrCandidate? declName false then
           Grind.ensureNotBuiltinCases declName
@@ -160,9 +170,9 @@ public def elabGrindParams (params : Grind.Params) (ps : TSyntaxArray ``Parser.T
         else
           params := { params with ematch := (← params.ematch.eraseDecl declName) }
       | `(Parser.Tactic.grindParam| $[$mod?:grindMod]? $id:ident) =>
-        params ← processParam params p mod? id (minIndexable := false) (only := only)
+        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)
+        params ← processParam params p mod? id (minIndexable := true) (only := only) (incremental := incremental)
       | `(Parser.Tactic.grindParam| #$anchor:hexnum) =>
         unless only do
           throwErrorAt anchor "invalid anchor, `only` modifier expected"
@@ -172,4 +182,63 @@ public def elabGrindParams (params : Grind.Params) (ps : TSyntaxArray ``Parser.T
       if !lax then throw ex
   return params
 
+namespace Grind
+open Meta Grind
+
+/--
+Returns `true` if we should keep the theorem when `only` is used.
+We keep
+1- Local theorems. We use anchors to restrict their instantiation.
+2- `match`-equations. They are always active.
+-/
+def shouldKeep (thm : EMatchTheorem) : GrindM Bool := do
+  if let .decl declName := thm.origin then
+    isMatchEqLikeDeclName declName
+  else
+    checkAnchorRefsEMatchTheoremProof thm.proof
+
+/--
+Removes all theorems that are not `match`-equations nor local theorems.
+-/
+def filterThms (thms : PArray EMatchTheorem) : GrindM (PArray EMatchTheorem) := do
+  let mut result := {}
+  for thm in thms do
+    if (← shouldKeep thm) then
+      result := result.push thm
+  return result
+
+/--
+Helper method for processing parameters in tactics such as `finish` and `finish?`
+-/
+public def withParams (params : Grind.Params) (ps : TSyntaxArray ``Parser.Tactic.grindParam) (only : Bool)
+    (k : GrindTacticM α) : GrindTacticM α := do
+  if !only && ps.isEmpty then
+    k
+  else
+    let mut params := params
+    if only then
+      params := { params with anchorRefs? := none }
+    params ← elabGrindParams params ps (only := only) (incremental := true)
+    let anchorRefs? := params.anchorRefs?
+    withReader (fun c => { c with params, ctx.anchorRefs? := anchorRefs? }) do
+    if only then
+      -- Cleanup main goal before adding new facts
+      let goal ← getMainGoal
+      let goal ← liftGrindM do
+        pure { goal with
+        -- **TODO**: cleanup injective theorems
+        ematch.thmMap  := {}
+        ematch.thms    := (← filterThms goal.ematch.thms)
+        ematch.newThms := (← filterThms goal.ematch.newThms)
+      }
+      replaceMainGoal [goal]
+    liftGoalM do
+      for thm in params.extra do
+        activateTheorem thm 0
+      for thm in params.extraInj do
+        activateInjectiveTheorem thm 0
+      -- **TODO**: `cases` parameters
+    k
+
+end Grind
 end Lean.Elab.Tactic

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

@@ -7,6 +7,7 @@ module
 prelude
 public import Lean.Elab.Tactic.Grind.Basic
 import Lean.Elab.Tactic.Grind.Config
+import Lean.Elab.Tactic.Grind.Param
 import Init.Grind.Interactive
 import Lean.Meta.Tactic.TryThis
 import Lean.Meta.Tactic.Grind.Action
@@ -27,8 +28,10 @@ def mkFinish (maxIterations : Nat) : IO Action := do
 def maxIterations := 1000 -- **TODO**: Add option
 
 @[builtin_grind_tactic finishTrace] def evalFinishTrace : GrindTactic := fun stx => do
-  let `(grind| finish? $[$configItems]*) := stx | throwUnsupportedSyntax
+  let `(grind| finish? $[$configItems]* $[only%$only]? $[[$params?,*]]?) := stx | throwUnsupportedSyntax
   withConfigItems configItems do
+  let params := params?.getD {}
+  withParams (← read).params params only.isSome do
     let a ← mkFinish maxIterations
     let goal ← getMainGoal
     withTracing do

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

@@ -76,10 +76,11 @@ private def isNewPat (patternsFoundSoFar : Array (List Expr)) (thm' : EMatchTheo
   patternsFoundSoFar.all fun ps => thm'.patterns != ps
 
 /--
-Returns `true`, if there are no anchor references restricting the search,
-or there is an anchor references `ref` s.t. `ref` matches `proof`.
+Given a proof of an `EMatchTheorem`, returns `true`, if there are no
+anchor references restricting the search, or there is an anchor
+references `ref` s.t. `ref` matches `proof`.
 -/
-private def checkAnchorRefs (proof : Expr) : GrindM Bool := do
+def checkAnchorRefsEMatchTheoremProof (proof : Expr) : GrindM Bool := do
   let some anchorRefs ← getAnchorRefs | return true
   let anchor ← getAnchor (← inferType proof)
   return anchorRefs.any (·.matches anchor)
@@ -94,7 +95,7 @@ private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
   let proof := mkOfEqTrueCore e proof
   -- **Note**: Do we really need to restrict the instantiation of local theorems?
   -- **Note**: Should we distinguish anchors restricting case-splits and local theorems?
-  unless (← checkAnchorRefs proof) do return ()
+  unless (← checkAnchorRefsEMatchTheoremProof proof) do return ()
   let size := (← get).ematch.newThms.size
   let gen ← getGeneration e
   let mut patternsFoundSoFar := #[]

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

@@ -268,7 +268,7 @@ private def mkEMatchTheoremWithKind'? (origin : Origin) (levelParams : Array Nam
   catch _ =>
     return none
 
-private def activateInjectiveTheorem (injThm : InjectiveTheorem) (generation : Nat) : GoalM Unit := do
+def activateInjectiveTheorem (injThm : InjectiveTheorem) (generation : Nat) : GoalM Unit := do
   let type ← inferType injThm.proof
   if type.isForall then
     let symPrios ← getSymbolPriorities

tests/lean/run/grind_finish_trace.lean

@@ -220,6 +220,19 @@ example (f g : Int → Int) (x y z w : Int)
   set_option trace.grind.split true in
   grind only [#23ad, #beb4] -- Only these two splits were performed.
 
+/--
+trace: [grind.split] x = 0, generation: 0
+[grind.split] x = 1, generation: 0
+-/
+#guard_msgs in
+example (f g : Int → Int) (x y z w : Int)
+    : 0 ≤ x → x ≤ 1 → 0 ≤ w →
+      g 0 = z → g 1 = z → g 2 = z →
+      f 0 = y → f 1 = y →
+      g w ≠ z → f x = y := by
+  set_option trace.grind.split true in
+  grind => finish only [#23ad, #beb4] -- Only these two splits were performed.
+
 /--
 trace: [grind.ematch.instance] h: f (f a) = f a
 [grind.ematch.instance] h: f (f (f a)) = f (f a)
@@ -251,3 +264,18 @@ example (f g : Int → Int)
     : f (f (f a)) = f a := by
   set_option trace.grind.ematch.instance true in
   grind only [#99cb]
+
+/--
+trace: [grind.ematch.instance] h✝³: f (f a) = f a
+[grind.ematch.instance] h✝³: f (f (f a)) = f (f a)
+[grind.ematch.instance] h✝³: f (f (f (f a))) = f (f (f a))
+-/
+#guard_msgs in
+example (f g : Int → Int)
+    (_ : ∀ x, f (f x) = f x)
+    (_ : ∀ x, g (g x) = g x)
+    (a b : Int)
+    (_ : g (g b) = b)
+    : f (f (f a)) = f a := by
+  set_option trace.grind.ematch.instance true in
+  grind => finish only [#99cb]

tests/lean/run/grind_set_config.lean

@@ -34,3 +34,13 @@ example : foo 10 ≥ 5 := by
   grind [fooAx1] =>
     have := fooAx2
     finish? (gen := 10) (ematch := 10)
+
+attribute [grind] fooAx2
+
+example : foo 30 ≥ 5 := by
+  have := fooAx2
+  grind => finish (gen := 50) (ematch := 50) [fooAx1]
+
+example : foo 30 ≥ 5 := by
+  have := fooAx2
+  grind => finish? (gen := 50) (ematch := 50) [fooAx1]