feat: finish? produces finish only suggestion (#11034)

This PR adds a new suggestion to `finish?`. It now generates the `grind`
tactic script as before, and a `finish only` tactic. Example:
```lean
/--
info: Try these:
  [apply] ⏎
    instantiate only [findIdx, insert, = mem_indices_of_mem]
    instantiate only [= getElem?_neg, = getElem?_pos]
    cases #1bba
    · instantiate only [findIdx]
    · instantiate only
      instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert]
  [apply] finish only [findIdx, insert, = mem_indices_of_mem, = getElem?_neg, = getElem?_pos, = HashMap.mem_insert,
    = HashMap.getElem_insert, #1bba]
-/
example (m : IndexMap α β) (a : α) (b : β) :
    (m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
  grind => finish?
```

Author: leodemoura

src/Init/Grind/Interactive.lean

@@ -127,12 +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*
-    (&" only")? (" [" withoutPosition(grindParam,*) "]")? : grind
+syntax (name := finish) "finish" (ppSpace configItem)*
+    (ppSpace &"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*
-    (&" only")? (" [" withoutPosition(grindParam,*) "]")? : grind
+syntax (name := finishTrace) "finish?" (ppSpace configItem)*
+    (ppSpace &"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/Trace.lean

@@ -13,14 +13,15 @@ import Lean.Meta.Tactic.TryThis
 import Lean.Meta.Tactic.Grind.Action
 import Lean.Meta.Tactic.Grind.EMatchAction
 import Lean.Meta.Tactic.Grind.Split
+import Lean.Meta.Tactic.Grind.CollectParams
 namespace Lean.Elab.Tactic.Grind
 open Meta
 open Meta.Grind
 
 def withTracing (x : GrindTacticM α) : GrindTacticM α := do
   withReader (fun ctx => { ctx with ctx.config.trace := true }) x
 
-def mkFinish (maxIterations : Nat) : IO Action := do
+def mkFinishAction (maxIterations : Nat) : IO Action := do
   let solvers ← Solvers.mkAction
   let step : Action := Action.done <|> solvers <|> Action.instantiate <|> Action.splitNext <|> Action.mbtc
   return Action.checkTactic (warnOnly := true) >> step.loop maxIterations
@@ -32,18 +33,30 @@ def maxIterations := 1000 -- **TODO**: Add option
   withConfigItems configItems do
   let params := params?.getD {}
   withParams (← read).params params only.isSome do
-    let a ← mkFinish maxIterations
+    let a ← mkFinishAction maxIterations
     let goal ← getMainGoal
+    let params := (← read).params
     withTracing do
-    match (← liftGrindM <| a.run goal) with
-    | .closed seq =>
+    let solved ← liftGrindM do
+      let saved ← saveState
+      match (← a.run goal) with
+      | .closed seq =>
+        let finishTac ← mkFinishTactic seq
+        let seq := Action.mkGrindSeq seq
+        if (← Action.checkSeqAt saved goal [finishTac]) then
+          Tactic.TryThis.addSuggestions stx #[
+            { suggestion := .tsyntax seq },
+            { suggestion := .tsyntax finishTac }
+          ]
+        else
+          Tactic.TryThis.addSuggestion stx { suggestion := .tsyntax seq }
+        return true
+      | .stuck gs =>
+        let goal :: _ := gs | throwError "`finish?` failed, but resulting goal is not available"
+        let result ← mkResult params (some goal)
+        throwError "`finish?` failed\n{← result.toMessageData}"
+        return false
+    if solved then
       replaceMainGoal []
-      let seq := Action.mkGrindSeq seq
-      Tactic.TryThis.addSuggestion stx { suggestion := .tsyntax seq }
-    | .stuck gs =>
-      let goal :: _ := gs | throwError "`finish?` failed, but resulting goal is not available"
-      let params := (← read).params
-      let result ← liftGrindM do mkResult params (some goal)
-      throwError "`finish?` failed\n{← result.toMessageData}"
 
 end Lean.Elab.Tactic.Grind

src/Lean/Meta/Tactic/Grind.lean

@@ -45,6 +45,7 @@ public import Lean.Meta.Tactic.Grind.Action
 public import Lean.Meta.Tactic.Grind.EMatchTheoremParam
 public import Lean.Meta.Tactic.Grind.EMatchAction
 public import Lean.Meta.Tactic.Grind.Filter
+public import Lean.Meta.Tactic.Grind.CollectParams
 public section
 namespace Lean
 

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

@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Types
+namespace Lean.Meta.Grind
+/-!
+Given an auto-generated `grind` tactic script, collect params for
+single shot `finish` or top-level `grind` tactic.
+-/
+abbrev TParam := TSyntax ``Parser.Tactic.grindParam
+abbrev TAnchor := TSyntax ``Parser.Tactic.anchor
+
+namespace Collector
+
+structure State where
+  params : Array TParam := #[]
+  anchors : Array TAnchor := #[]
+
+abbrev Collect := StateRefT State CoreM
+
+def pushParam (p : TParam) : Collect Unit := do
+  if (← get).params.contains p then
+    return ()
+  modify fun s => { s with params := s.params.push p }
+
+def pushAnchor (a : TAnchor) : Collect Unit := do
+  if (← get).anchors.contains a then
+    return ()
+  modify fun s => { s with anchors := s.anchors.push a }
+
+def collectInstantiateParams (params : Syntax.TSepArray `Lean.Parser.Tactic.Grind.thm ",") : Collect Unit := do
+  for p in params.getElems do
+    match p with
+    | `(Lean.Parser.Tactic.Grind.thm| $lemma:grindLemma) =>
+      let p ← `(Parser.Tactic.grindParam| $lemma:grindLemma)
+      pushParam p
+    | `(Lean.Parser.Tactic.Grind.thm| $lemma:grindLemmaMin) =>
+      let p ← `(Parser.Tactic.grindParam| $lemma:grindLemmaMin)
+      pushParam p
+    | `(Lean.Parser.Tactic.Grind.thm| $a:anchor) =>
+      pushAnchor a
+    | _ => pure ()
+
+partial def collect (tac : TGrind) : Collect Unit := do
+  match tac with
+  | `(grind| next => $$seq;*)
+  | `(grind| · $$seq;*) =>
+    for step in seq.getElems do
+      match step with
+      | `(Parser.Tactic.Grind.grindStep| $tac:grind $[| $_:grind_filter]?) => collect tac
+      | _ => return ()
+  | `(grind| $tac₁:grind <;> $tac₂:grind) => collect tac₁; collect tac₂
+  | `(grind| cases $a:anchor) => pushAnchor a
+  | `(grind| use [$params,*]) =>
+    collectInstantiateParams params
+  | `(grind| instantiate $[only]? $[approx]? $[[$params?,*]]?) =>
+    let some params := params? | return ()
+    collectInstantiateParams params
+  | _ => return ()
+
+def main (seq : List TGrind) : Collect Unit :=
+  seq.forM collect
+
+end Collector
+
+def collectParams (seq : List TGrind) : CoreM (Array TParam) := do
+  let (_, s) ← Collector.main seq |>.run {}
+  let anchors ← s.anchors.mapM fun anchor =>
+    `(Parser.Tactic.grindParam| $anchor:anchor)
+  return s.params ++ anchors
+
+/--
+Given a `grind` tactic sequence, extracts parameters and builds an terminal `finish only` tactic.
+-/
+public def mkFinishTactic (seq : List TGrind) : CoreM TGrind := do
+  let params ← collectParams seq
+  `(grind| finish only [$params,*])
+
+end Lean.Meta.Grind

tests/lean/run/grind_10885.lean

@@ -1,10 +1,11 @@
 example {a b : Nat} (ha : 1 ≤ a) : (a - 1 + 1) * b = a * b := by grind
 
 /--
-info: Try this:
+info: Try these:
   [apply] ⏎
     mbtc
     cases #9501
+  [apply] finish only [#9501]
 -/
 #guard_msgs in
 example {a b : Nat} (ha : 1 ≤ a) : (a - 1 + 1) * b = a * b := by

tests/lean/run/grind_finish_trace.lean

@@ -1,8 +1,9 @@
 open Lean Grind
 
 /--
-info: Try this:
+info: Try these:
   [apply] cases #c4b6 <;> cases #4c68 <;> ring
+  [apply] finish only [#c4b6, #4c68]
 -/
 #guard_msgs in
 example {α : Type} [CommRing α] (a b c d e : α) :
@@ -14,11 +15,12 @@ example {α : Type} [CommRing α] (a b c d e : α) :
 
 
 /--
-info: Try this:
+info: Try these:
   [apply] ⏎
     cases #b0f4
     · cases #50fc
     · cases #50fc <;> lia
+  [apply] finish only [#b0f4, #50fc]
 -/
 #guard_msgs in
 example (p : Nat → Prop) (x y z w : Int) :
@@ -29,8 +31,9 @@ example (p : Nat → Prop) (x y z w : Int) :
   grind => finish?
 
 /--
-info: Try this:
+info: Try these:
   [apply] cases #5c4b <;> cases #896f <;> ac
+  [apply] finish only [#5c4b, #896f]
 -/
 #guard_msgs in
 example {α : Type} (op : α → α → α) [Std.Associative op] [Std.Commutative op] (a b c d e : α) :
@@ -41,10 +44,11 @@ example {α : Type} (op : α → α → α) [Std.Associative op] [Std.Commutativ
   grind => finish?
 
 /--
-info: Try this:
+info: Try these:
   [apply] ⏎
     instantiate only [= Array.getElem_set]
     instantiate only [= Array.getElem_set]
+  [apply] finish only [= Array.getElem_set]
 -/
 #guard_msgs in
 example (as bs cs : Array α) (v₁ v₂ : α)
@@ -93,10 +97,11 @@ example (as : Array α) (lo hi i j : Nat) (h₁ : lo ≤ i) (_ : i < j) (_ : j 
   grind => finish?
 
 /--
-info: Try this:
+info: Try these:
   [apply] ⏎
     instantiate only [= getMsbD_setWidth']
     cases #aa9d
+  [apply] finish only [= getMsbD_setWidth', #aa9d]
 -/
 #guard_msgs in
 open BitVec in
@@ -112,43 +117,52 @@ example (ge : m ≥ n) (x : BitVec n) (i : Nat) :
     cases #aa9d
 
 /--
-info: Try this:
+info: Try these:
   [apply] cases #9942 <;>
       instantiate only [= BitVec.getElem_and] <;> instantiate only [= BitVec.getElem_or] <;> cases #cfbc
+  [apply] finish only [= BitVec.getElem_and, = BitVec.getElem_or, #9942, #cfbc]
 -/
 #guard_msgs in
 example (x y : BitVec 64) : (x ||| y) &&& x = x := by
   grind => finish?
 
+set_option trace.Meta.debug true in
+example (x y : BitVec 64) : (x ||| y) &&& x = x := by
+  grind => finish?
+
+
 macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| grind)
 
 /--
-info: Try this:
+info: Try these:
   [apply] ⏎
     instantiate only [= Array.getElem_set]
     ring
+  [apply] finish only [= Array.getElem_set]
 -/
 #guard_msgs in
 example (a : Array (BitVec 64)) (i : Nat) (v : BitVec 64)
     : (_ : i < a.size) → (_ : i + 1 < a.size) → (a.set i v)[i+1] + a[i+1] = 2*a[i+1] := by
   grind => finish?
 
 /--
-info: Try this:
+info: Try these:
   [apply] ⏎
     mbtc
     cases #a6c8
+  [apply] finish only [#a6c8]
 -/
 #guard_msgs in
 example (f : Nat → Nat) (x : Nat)
     : x ≠ 0 → x ≤ 1 → f x = 2 → f 1 = 2 := by
   grind => finish?
 
 /--
-info: Try this:
+info: Try these:
   [apply] ⏎
     mbtc
     cases #beb4
+  [apply] finish only [#beb4]
 -/
 #guard_msgs in
 example (f : Int → Int → Int) (x y : Int)

tests/lean/run/grind_indexmap_trace.lean

@@ -131,8 +131,9 @@ If the key is not present, the map is unchanged.
 attribute [local grind] getIdx findIdx insert
 
 /--
-info: Try this:
+info: Try these:
   [apply] instantiate only [getIdx, findIdx, = getElem_def]
+  [apply] finish only [getIdx, findIdx, = getElem_def]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a : α) (h : a ∈ m) :
@@ -144,7 +145,7 @@ example (m : IndexMap α β) (a : α) (h : a ∈ m) :
   grind => instantiate only [getIdx, findIdx, = getElem_def]
 
 /--
-info: Try this:
+info: Try these:
   [apply] ⏎
     instantiate only [= mem_indices_of_mem, insert]
     instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
@@ -162,14 +163,16 @@ info: Try this:
         · instantiate only
         · instantiate only
           instantiate only [= HashMap.contains_insert]
+  [apply] finish only [= mem_indices_of_mem, insert, =_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos,
+    = HashMap.contains_insert, #4ed2, #ffdf, #95a0, #2688]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a a' : α) (b : β) :
     a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := by
   grind => finish?
 
 /--
-info: Try this:
+info: Try these:
   [apply] ⏎
     instantiate only [= mem_indices_of_mem, insert]
     instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
@@ -187,6 +190,8 @@ info: Try this:
         · instantiate only
         · instantiate only
           instantiate only [= HashMap.contains_insert]
+  [apply] finish only [= mem_indices_of_mem, insert, =_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos,
+    = HashMap.contains_insert, #4ed2, #ffdf, #95a0, #2688]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a a' : α) (b : β) :
@@ -221,7 +226,7 @@ example (m : IndexMap α β) (a a' : α) (b : β) :
           instantiate only [= HashMap.contains_insert]
 
 /--
-info: Try this:
+info: Try these:
   [apply] ⏎
     instantiate only [= mem_indices_of_mem, insert, = getElem_def]
     instantiate only [= getElem?_neg, = getElem?_pos]
@@ -240,6 +245,9 @@ info: Try this:
         instantiate only [WF']
       · instantiate only
         instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
+  [apply] finish only [= mem_indices_of_mem, insert, = getElem_def, = getElem?_neg, = getElem?_pos, = Array.getElem_set,
+    size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, usr getElem_indices_lt, =_ WF, WF',
+    #f590, #ffdf]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
@@ -275,20 +283,26 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
         instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
 
 /--
-info: Try this:
+info: Try these:
   [apply] ⏎
     instantiate only [findIdx, insert, = mem_indices_of_mem]
     instantiate only [= getElem?_neg, = getElem?_pos]
     cases #1bba
     · instantiate only [findIdx]
     · instantiate only
       instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert]
+  [apply] finish only [findIdx, insert, = mem_indices_of_mem, = getElem?_neg, = getElem?_pos, = HashMap.mem_insert,
+    = HashMap.getElem_insert, #1bba]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a : α) (b : β) :
     (m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
   grind => finish?
 
+example (m : IndexMap α β) (a : α) (b : β) :
+    (m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
+  grind => finish?
+
 example (m : IndexMap α β) (a : α) (b : β) :
     (m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
   grind =>