feat: support grind parameters in finish and finish? (#11012)

This PR ensures the `grind` tactics `finish` and `finish?` can take
parameters.

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/Main.lean

@@ -89,12 +89,12 @@ def elabGrindPremises
     | .ematch kind =>
       try
         params ← addEMatchTheorem params (mkIdent p.name) p.name kind false (warn := false)
-      catch _ => pure () -- Don't worry if premise suggestion gave bad suggetions.
+      catch _ => pure () -- Don't worry if premise suggestion gave bad suggestions.
     | _ =>
       -- 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.
+      -- Let's only do this if there is a prospect of a premise selector supporting this.
       throwError "unexpected modifier {p.flag}"
   return params
 
@@ -113,7 +113,11 @@ def mkGrindParams
   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
+  /-
+  **Note**: We used to skip the global cases attribute when `only = true`, but
+  this is not very effective. We now use anchors to restrict the set of case-splits.
+  -/
+  let casesTypes ← Grind.getCasesTypes
   let params := { params with ematch, casesTypes, inj }
   let premises ← if config.premises then
     let suggestions ← PremiseSelection.select mvarId
@@ -213,16 +217,6 @@ def mkGrindOnly
       else
         let param ← Grind.globalDeclToGrindParamSyntax declName kind minIndexable
         params := params.push param
-  for declName in trace.eagerCases.toList do
-    unless Grind.isBuiltinEagerCases declName do
-      let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
-      let param ← `(Parser.Tactic.grindParam| cases eager $decl)
-      params := params.push param
-  for declName in trace.cases.toList do
-    unless trace.eagerCases.contains declName || Grind.isBuiltinEagerCases declName do
-      let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
-      let param ← `(Parser.Tactic.grindParam| cases $decl)
-      params := params.push param
   let result ← `(tactic| grind $config:optConfig only)
   return setGrindParams result 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,18 +110,20 @@ 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
       throwError "invalid use of `intro` modifier, `{.ofConstName declName}` is not an inductive predicate"
   | .inj =>
     let thm ← Grind.mkInjectiveTheorem declName
-    params := { params with inj := params.inj.insert thm }
+    params := { params with extraInj := params.extraInj.push thm }
   | .ext =>
     throwError "`[grind ext]` cannot be set using parameters"
   | .infer =>
@@ -141,13 +147,20 @@ def processAnchor (params : Grind.Params) (val : TSyntax `hexnum) : CoreM Grind.
   let anchorRef ← Grind.elabAnchorRef val
   return { params with anchorRefs? := some <| anchorRefs.push anchorRef }
 
+/--
+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
@@ -157,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"
@@ -169,4 +182,66 @@ 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
+        ematch := {}
+        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

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

@@ -35,6 +35,7 @@ structure Params where
   symPrios    : SymbolPriorities := {}
   casesTypes  : CasesTypes := {}
   extra       : PArray EMatchTheorem := {}
+  extraInj    : PArray InjectiveTheorem := {}
   norm        : Simp.Context
   normProcs   : Array Simprocs
   anchorRefs? : Option (Array AnchorRef) := none

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

@@ -166,6 +166,9 @@ E-match theorems and case-splits performed by `grind`.
 Note that it may contain elements that are not needed by the final proof.
 For example, `grind` instantiated the theorem, but theorem instance was not actually used
 in the proof.
+
+**Note**: Consider removing this, we are using a new approach for implementing
+`grind?`
 -/
 structure Trace where
   thms       : PHashSet EMatchTheoremTrace := {}

tests/lean/run/grind_ematch_gen_pattern.lean

@@ -10,7 +10,7 @@ example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = som
 
 /--
 info: Try this:
-  [apply] grind only [= gen Option.pbind_some', f, cases Or]
+  [apply] grind only [= gen Option.pbind_some', f]
 -/
 #guard_msgs (info) in
 example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by

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_indexmap_trace.lean

@@ -292,12 +292,18 @@ example (m : IndexMap α β) (a : α) (b : β) :
 example (m : IndexMap α β) (a : α) (b : β) :
     (m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
   grind =>
-    instantiate only [insert, = mem_indices_of_mem, findIdx]
-    instantiate only [= getElem?_pos, = getElem?_neg]
+    instantiate only [findIdx, insert, = mem_indices_of_mem]
+    instantiate only [= getElem?_neg, = getElem?_pos]
     cases #1bba
-    next => instantiate only [findIdx]
-    next =>
-      instantiate only
-      instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert]
+    · instantiate only [findIdx]
+    · finish only [= HashMap.mem_insert, = HashMap.getElem_insert]
+
+example (m : IndexMap α β) (a : α) (b : β) :
+    (m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
+  grind =>
+    instantiate only [findIdx, insert, = mem_indices_of_mem]
+    instantiate only [= getElem?_neg, = getElem?_pos]
+    cases #1bba <;>
+      finish only [findIdx, = HashMap.mem_insert, = HashMap.getElem_insert]
 
 end IndexMap

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]