From 206eb73cd9de4b58abbb2eae20a41fd9b7af187b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 18 Oct 2025 20:52:32 -0700
Subject: [PATCH] feat: `finish?` tactic for `grind` interactive mode (#10837)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR implements the `finish?` tactic for the `grind` interactive
mode. When it successfully closes the goal, it produces a code action
that allows the user to close the goal using explicit grind tactic
steps, i.e., without any search. It also makes explicit which solvers
have been used.

This is just the first version, we will add many "bells and whistles"
later. For example, `instantiate` steps will clearly show which theorems
have been instantiated.

Example:

```lean
/--
info: Try this:
  [apply] ⏎
    cases #b0f4
    next => cases #50fc
    next => cases #50fc <;> lia
-/
#guard_msgs in
example (p : Nat → Prop) (x y z w : Int) :
    (x = 1 ∨ x = 2) →
    (w = 1 ∨ w = 4) →
    (y = 1 ∨ (∃ x : Nat, y = 3 - x ∧ p x)) →
    (z = 1 ∨ z = 0) → x + y ≤ 6 := by
  grind => finish?
```

The anchors in the generated script are based on stable hash codes.
Moreover, users can hover over them to see the exact term used in the
case split. `grind?` will also be implemented using the new framework.
---
 src/Init/Grind/Interactive.lean              |  3 +
 src/Lean/Elab/Tactic/Grind.lean              |  1 +
 src/Lean/Elab/Tactic/Grind/Trace.lean        | 42 +++++++++++++
 src/Lean/Meta/Tactic/Grind.lean              |  3 +-
 src/Lean/Meta/Tactic/Grind/EMatchAction.lean | 25 ++++++++
 tests/lean/run/grind_finish_trace.lean       | 62 ++++++++++++++++++++
 6 files changed, 134 insertions(+), 2 deletions(-)
 create mode 100644 src/Lean/Elab/Tactic/Grind/Trace.lean
 create mode 100644 src/Lean/Meta/Tactic/Grind/EMatchAction.lean
 create mode 100644 tests/lean/run/grind_finish_trace.lean

diff --git a/src/Init/Grind/Interactive.lean b/src/Init/Grind/Interactive.lean
index 3c9571dafa..ea442bb0c9 100644
--- a/src/Init/Grind/Interactive.lean
+++ b/src/Init/Grind/Interactive.lean
@@ -100,6 +100,9 @@ syntax (name := done) "done" : grind
 /-- `finish` tries to close the current goal using `grind`'s default strategy -/
 syntax (name := finish) "finish" : grind
 
+/-- `finish?` tries to close the current goal using `grind`'s default strategy and suggests a tactic script. -/
+syntax (name := finishTrace) "finish?" : grind
+
 syntax (name := «have») "have" letDecl : grind
 
 /-- Executes the given tactic block to close the current goal. -/
diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean
index d0e403e847..973cd14519 100644
--- a/src/Lean/Elab/Tactic/Grind.lean
+++ b/src/Lean/Elab/Tactic/Grind.lean
@@ -10,3 +10,4 @@ public import Lean.Elab.Tactic.Grind.Basic
 public import Lean.Elab.Tactic.Grind.BuiltinTactic
 public import Lean.Elab.Tactic.Grind.ShowState
 public import Lean.Elab.Tactic.Grind.Have
+public import Lean.Elab.Tactic.Grind.Trace
diff --git a/src/Lean/Elab/Tactic/Grind/Trace.lean b/src/Lean/Elab/Tactic/Grind/Trace.lean
new file mode 100644
index 0000000000..022cb2ce02
--- /dev/null
+++ b/src/Lean/Elab/Tactic/Grind/Trace.lean
@@ -0,0 +1,42 @@
+/-
+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.Elab.Tactic.Grind.Basic
+import Init.Grind.Interactive
+import Lean.Meta.Tactic.TryThis
+import Lean.Meta.Tactic.Grind.Action
+import Lean.Meta.Tactic.Grind.EMatchAction
+import Lean.Meta.Tactic.Grind.Split
+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
+  let solvers ← Solvers.mkAction
+  return Action.checkTactic >> (Action.done <|> solvers <|> Action.instantiate <|> Action.splitNext).loop maxIterations
+
+def maxIterations := 1000 -- **TODO**: Add option
+
+@[builtin_grind_tactic finishTrace] def evalFinishTrace : GrindTactic := fun stx => do
+  let a ← mkFinish maxIterations
+  let goal ← getMainGoal
+  withTracing do
+  match (← liftGrindM <| a.run goal) with
+  | .closed seq =>
+    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
diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean
index d1dbda90cd..e4ebaa386d 100644
--- a/src/Lean/Meta/Tactic/Grind.lean
+++ b/src/Lean/Meta/Tactic/Grind.lean
@@ -43,9 +43,8 @@ public import Lean.Meta.Tactic.Grind.PropagateInj
 public import Lean.Meta.Tactic.Grind.Order
 public import Lean.Meta.Tactic.Grind.Anchor
 public import Lean.Meta.Tactic.Grind.Action
-
+public import Lean.Meta.Tactic.Grind.EMatchAction
 public section
-
 namespace Lean
 
 /-! Trace options for `grind` users -/
diff --git a/src/Lean/Meta/Tactic/Grind/EMatchAction.lean b/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
new file mode 100644
index 0000000000..64be0ae696
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
@@ -0,0 +1,25 @@
+/-
+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.Action
+public import Lean.Meta.Tactic.Grind.Intro
+import Lean.Meta.Tactic.Grind.EMatch
+public section
+namespace Lean.Meta.Grind.Action
+
+def instantiate' : Action := fun goal kna kp => do
+  let (progress, goal') ← GoalM.run goal ematch
+  -- **TODO**: filter relevant instances
+  if progress then
+    concatTactic (← kp goal') `(grind| instantiate)
+  else
+    kna goal
+
+def instantiate : Action :=
+  instantiate' >> assertAll
+
+end Lean.Meta.Grind.Action
diff --git a/tests/lean/run/grind_finish_trace.lean b/tests/lean/run/grind_finish_trace.lean
new file mode 100644
index 0000000000..cbfed722cc
--- /dev/null
+++ b/tests/lean/run/grind_finish_trace.lean
@@ -0,0 +1,62 @@
+open Lean Grind
+
+/--
+info: Try this:
+  [apply] cases #c4b6 <;> ring <;> cases #4c68 <;> ring
+-/
+#guard_msgs in
+example {α : Type} [CommRing α] (a b c d e : α) :
+    (a * a = b * c ∨ a^2 = c * b) →
+    (a^2 = c * b ∨ e^2 = d * c) →
+    (b^2 = d*c ∨ b^2 = c*d) →
+    a*b*(b*a) = c^2*b*d := by
+ grind => finish?
+
+
+/--
+info: Try this:
+  [apply] ⏎
+    cases #b0f4
+    next => cases #50fc
+    next => cases #50fc <;> lia
+-/
+#guard_msgs in
+example (p : Nat → Prop) (x y z w : Int) :
+    (x = 1 ∨ x = 2) →
+    (w = 1 ∨ w = 4) →
+    (y = 1 ∨ (∃ x : Nat, y = 3 - x ∧ p x)) →
+    (z = 1 ∨ z = 0) → x + y ≤ 6 := by
+  grind => finish?
+
+/--
+info: Try this:
+  [apply] ⏎
+    ac
+    cases #5c4b <;> cases #896f <;> ac
+-/
+#guard_msgs in
+example {α : Type} (op : α → α → α) [Std.Associative op] [Std.Commutative op] (a b c d e : α) :
+    (op a a = op b c ∨ op a a = op c b) →
+    (op a a = op c b ∨ op e e = op d c) →
+    (op b b = op d c ∨ op b b = op c d) →
+    op (op a b) (op b a) = op (op c c) (op b d) := by
+  grind => finish?
+
+/--
+info: Try this:
+  [apply] ⏎
+    instantiate
+    instantiate
+-/
+#guard_msgs in
+example (as bs cs : Array α) (v₁ v₂ : α)
+        (i₁ i₂ j : Nat)
+        (h₁ : i₁ < as.size)
+        (h₂ : bs = as.set i₁ v₁)
+        (h₃ : i₂ < bs.size)
+        (h₃ : cs = bs.set i₂ v₂)
+        (h₄ : i₁ ≠ j ∧ i₂ ≠ j)
+        (h₅ : j < cs.size)
+        (h₆ : j < as.size)
+        : cs[j] = as[j] := by
+  grind => finish?