From 3a42ee0c3060e2a8365927d205ead5990366053d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 26 Oct 2025 21:47:02 -0700
Subject: [PATCH] feat: `grind` tactic mode improvements (#10978)

This PR implements the following `grind` improvements:
1. `set_option` can now be used to set `grind` configuration options in
the interactive mode.
2. Fixes a bug in the repeated theorem instantiation detection.
3. Adds the macro `use [...]` as a shorthand for `instantiate only
[...]`.
---
 src/Init/Grind/Interactive.lean               |  4 ++
 src/Lean/Elab/Tactic/ConfigSetter.lean        | 65 +++++++++++++++++++
 src/Lean/Elab/Tactic/Grind.lean               |  1 +
 src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean | 26 +++++++-
 src/Lean/Elab/Tactic/Grind/Config.lean        | 16 +++++
 src/Lean/Elab/Tactic/Grind/Filter.lean        | 35 +---------
 src/Lean/Meta/Tactic/Grind.lean               |  2 +-
 src/Lean/Meta/Tactic/Grind/Filter.lean        | 41 ++++++++++++
 src/Lean/Meta/Tactic/Grind/Types.lean         | 15 ++++-
 tests/lean/run/grind_preinstance_set_bug.lean | 12 ++++
 tests/lean/run/grind_set_config.lean          | 15 +++++
 11 files changed, 194 insertions(+), 38 deletions(-)
 create mode 100644 src/Lean/Elab/Tactic/ConfigSetter.lean
 create mode 100644 src/Lean/Elab/Tactic/Grind/Config.lean
 create mode 100644 src/Lean/Meta/Tactic/Grind/Filter.lean
 create mode 100644 tests/lean/run/grind_preinstance_set_bug.lean
 create mode 100644 tests/lean/run/grind_set_config.lean

diff --git a/src/Init/Grind/Interactive.lean b/src/Init/Grind/Interactive.lean
index ec91d16125..a8e23143e5 100644
--- a/src/Init/Grind/Interactive.lean
+++ b/src/Init/Grind/Interactive.lean
@@ -83,6 +83,10 @@ that may have redundant arguments.
 -/
 syntax (name := instantiate) "instantiate" (&" only")? (&" approx")? (" [" withoutPosition(thm,*,?) "]")? : grind
 
+/-- Shorthand for `instantiate only` -/
+syntax (name := use) "use" " [" withoutPosition(thm,*,?) "]" : grind
+macro_rules | `(grind| use%$u [$ts:thm,*]) => `(grind| instantiate%$u only [$ts,*])
+
 -- **Note**: Should we rename the following tactics to `trace_`?
 /-- Shows asserted facts. -/
 syntax (name := showAsserted) "show_asserted" ppSpace grindFilter : grind
diff --git a/src/Lean/Elab/Tactic/ConfigSetter.lean b/src/Lean/Elab/Tactic/ConfigSetter.lean
new file mode 100644
index 0000000000..dc0bbdbf86
--- /dev/null
+++ b/src/Lean/Elab/Tactic/ConfigSetter.lean
@@ -0,0 +1,65 @@
+/-
+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.Command
+meta import Lean.Elab.Command
+public import Lean.Data.KVMap
+public section
+namespace Lean.Elab
+open Command Meta
+
+/--
+Generates a function `setterName` for updating the `Bool` and `Nat` fields
+of the structure `struct`.
+This is a very simple implementation. There is no support for subobjects.
+-/
+meta def mkConfigSetter (doc? : Option (TSyntax ``Parser.Command.docComment))
+    (setterName struct : Ident) : CommandElabM Unit := do
+  let structName ← resolveGlobalConstNoOverload struct
+  let .inductInfo val ← getConstInfo structName
+    | throwErrorAt struct "`{structName}` is not s structure"
+  unless val.levelParams.isEmpty do
+    throwErrorAt struct "`{structName}` is universe polymorphic"
+  unless val.numIndices == 0 && val.numParams == 0 do
+    throwErrorAt struct "`{structName}` must not be parametric"
+  let env ← getEnv
+  let some structInfo := getStructureInfo? env structName
+    | throwErrorAt struct "`{structName}` is not a structure"
+  let code : Term ← liftTermElabM do
+    let mut code : Term ← `(throwError "invalid configuration option `{fieldName}`")
+    for fieldInfo in structInfo.fieldInfo do
+      if fieldInfo.subobject?.isSome then continue -- ignore subobject's
+      let projInfo ← getConstInfo fieldInfo.projFn
+      let fieldType ← forallTelescope projInfo.type fun _ body => pure body
+      -- **Note**: We only support `Nat` and `Bool` fields
+      let fieldIdent : Ident := mkCIdent fieldInfo.fieldName
+      if fieldType.isConstOf ``Nat then
+        code ← `(if fieldName == $(quote fieldInfo.fieldName) then
+                   return { s with $fieldIdent:ident := (← getNatField) }
+                 else $code)
+      else if fieldType.isConstOf ``Bool then
+        code ← `(if fieldName == $(quote fieldInfo.fieldName) then
+                   return { s with $fieldIdent:ident := (← getBoolField) }
+                 else $code)
+    return code
+  let cmd ← `(command|
+     $[$doc?:docComment]?
+     def $setterName (s : $struct) (fieldName : Name) (val : DataValue) : CoreM $struct :=
+       let getBoolField : CoreM Bool := do
+          let .ofBool b := val | throwError "`{fieldName}` is a Boolean"
+          return b
+       let getNatField : CoreM Nat := do
+         let .ofNat n := val | throwError "`{fieldName}` is a natural number"
+         return n
+       $code
+  )
+  elabCommand cmd
+
+elab (name := elabConfigGetter) doc?:(docComment)? "declare_config_getter" setterName:ident type:ident : command => do
+  mkConfigSetter doc? setterName type
+
+end Lean.Elab
diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean
index 973cd14519..97d5c084d5 100644
--- a/src/Lean/Elab/Tactic/Grind.lean
+++ b/src/Lean/Elab/Tactic/Grind.lean
@@ -11,3 +11,4 @@ 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
+public import Lean.Elab.Tactic.Grind.Config
diff --git a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
index 41bc6613a6..8dd3a41818 100644
--- a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
@@ -25,6 +25,7 @@ import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.RenameInaccessibles
 import Lean.Elab.Tactic.Grind.Filter
 import Lean.Elab.Tactic.Grind.ShowState
+import Lean.Elab.Tactic.Grind.Config
 import Lean.Elab.SetOption
 namespace Lean.Elab.Tactic.Grind
 
@@ -425,9 +426,30 @@ where
   liftGrindM <| resetAnchors
   replaceMainGoal [{ goal with mvarId }]
 
+def isGrindConfigField? (stx : Syntax) : CoreM (Option Name) := do
+  unless stx.isIdent do return none
+  let id := stx.getId
+  let env ← getEnv
+  let info := getStructureInfo env ``Grind.Config
+  unless info.fieldNames.contains id do return none
+  return some id
+
 @[builtin_grind_tactic setOption] def elabSetOption : GrindTactic := fun stx => do
-  let options ← Elab.elabSetOption stx[1] stx[3]
-  withOptions (fun _ => options) do evalGrindTactic stx[5]
+  if let some fieldName ← isGrindConfigField? stx[1] then
+    let val := stx[3]
+    let val ← match val.isNatLit? with
+      | some num => pure <| DataValue.ofNat num
+      | none     => match val with
+        | Syntax.atom _ "true"  => pure <| DataValue.ofBool true
+        | Syntax.atom _ "false" => pure <| DataValue.ofBool false
+        | _ => throwErrorAt val "`grind` configuration option must be a Boolean or a numeral"
+    let config := (← read).ctx.config
+    let config ← setConfigField config fieldName val
+    withReader (fun c => { c with ctx.config := config }) do
+      evalGrindTactic stx[5]
+  else
+    let options ← Elab.elabSetOption stx[1] stx[3]
+    withOptions (fun _ => options) do evalGrindTactic stx[5]
 
 @[builtin_grind_tactic mbtc] def elabMBTC : GrindTactic := fun _ => do
   liftGoalM do
diff --git a/src/Lean/Elab/Tactic/Grind/Config.lean b/src/Lean/Elab/Tactic/Grind/Config.lean
new file mode 100644
index 0000000000..6e6519e218
--- /dev/null
+++ b/src/Lean/Elab/Tactic/Grind/Config.lean
@@ -0,0 +1,16 @@
+/-
+Copyright (c) 2024 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.CoreM
+meta import Lean.Elab.Tactic.ConfigSetter
+public section
+namespace Lean.Elab.Tactic.Grind
+
+/-- Sets a field of the `grind` configuration object. -/
+declare_config_getter setConfigField Grind.Config
+
+end Lean.Elab.Tactic.Grind
diff --git a/src/Lean/Elab/Tactic/Grind/Filter.lean b/src/Lean/Elab/Tactic/Grind/Filter.lean
index 77bdcd6cbf..d9b0889650 100644
--- a/src/Lean/Elab/Tactic/Grind/Filter.lean
+++ b/src/Lean/Elab/Tactic/Grind/Filter.lean
@@ -6,18 +6,10 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Elab.Tactic.Grind.Basic
+public import Lean.Meta.Tactic.Grind.Filter
 import Init.Grind.Interactive
 namespace Lean.Elab.Tactic.Grind
-open Meta
-
-public inductive Filter where
-  | true
-  | const (declName : Name)
-  | fvar (fvarId : FVarId)
-  | gen (pred : Nat → Bool)
-  | or (a b : Filter)
-  | and (a b : Filter)
-  | not (a : Filter)
+open Meta Grind
 
 public partial def elabFilter (filter? : Option (TSyntax `grind_filter)) : GrindTacticM Filter := do
   let some filter := filter? | return .true
@@ -44,27 +36,4 @@ where
     | `(grind_filter| gen != $n:num) => let n := n.getNat; return .gen fun x => x != n
     | _ => throwUnsupportedSyntax
 
-open Meta.Grind
-
--- **Note**: facts may not have been internalized if they are equalities.
-def getGen (e : Expr) : GoalM Nat := do
-  if (← alreadyInternalized e) then
-    getGeneration e
-  else match_expr e with
-   | Eq _ lhs rhs => return max (← getGeneration lhs) (← getGeneration rhs)
-   | _ => return 0
-
-public def Filter.eval (filter : Filter) (e : Expr) : GoalM Bool := do
-  go filter
-where
-  go (filter : Filter) : GoalM Bool := do
-  match filter with
-  | .true => return .true
-  | .and a b => go a <&&> go b
-  | .or a b => go a <||> go b
-  | .not a => return !(← go a)
-  | .const declName => return Option.isSome <| e.find? fun e => e.isConstOf declName
-  | .fvar fvarId => return Option.isSome <| e.find? fun e => e.isFVar && e.fvarId! == fvarId
-  | .gen pred => let gen ← getGen e; return pred gen
-
 end Lean.Elab.Tactic.Grind
diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean
index efc7f65952..96b618ba27 100644
--- a/src/Lean/Meta/Tactic/Grind.lean
+++ b/src/Lean/Meta/Tactic/Grind.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Attr
 public import Lean.Meta.Tactic.Grind.RevertAll
@@ -45,6 +44,7 @@ public import Lean.Meta.Tactic.Grind.Anchor
 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 section
 namespace Lean
 
diff --git a/src/Lean/Meta/Tactic/Grind/Filter.lean b/src/Lean/Meta/Tactic/Grind/Filter.lean
new file mode 100644
index 0000000000..64a38a8027
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Grind/Filter.lean
@@ -0,0 +1,41 @@
+/-
+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
+
+public inductive Filter where
+  | true
+  | const (declName : Name)
+  | fvar (fvarId : FVarId)
+  | gen (pred : Nat → Bool)
+  | or (a b : Filter)
+  | and (a b : Filter)
+  | not (a : Filter)
+
+-- **Note**: facts may not have been internalized if they are equalities.
+def getGen (e : Expr) : GoalM Nat := do
+  if (← alreadyInternalized e) then
+    getGeneration e
+  else match_expr e with
+   | Eq _ lhs rhs => return max (← getGeneration lhs) (← getGeneration rhs)
+   | _ => return 0
+
+public def Filter.eval (filter : Filter) (e : Expr) : GoalM Bool := do
+  go filter
+where
+  go (filter : Filter) : GoalM Bool := do
+    match filter with
+    | .true => return .true
+    | .and a b => go a <&&> go b
+    | .or a b => go a <||> go b
+    | .not a => return !(← go a)
+    | .const declName => return Option.isSome <| e.find? fun e => e.isConstOf declName
+    | .fvar fvarId => return Option.isSome <| e.find? fun e => e.isFVar && e.fvarId! == fvarId
+    | .gen pred => let gen ← getGen e; return pred gen
+
+end Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index a72fb0ba3b..33cc66f2cb 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -640,6 +640,17 @@ We want to avoid instantiating the same theorem with the same assignment more th
 Therefore, we store the (pre-)instance information in set.
 Recall that the proofs of activated theorems have been hash-consed.
 The assignment contains internalized expressions, which have also been hash-consed.
+
+**Note**: We used to use pointer equality to implement `PreInstanceSet`. However,
+this low-level trick was incorrect in interactive mode because we add new
+`EMatchTheorem` objects using `instantiate [...]`. For example, suppose we write
+```
+instantiate [thm_1]; instantiate [thm_1]
+```
+The `EMatchTheorem` object `thm_1` is created twice. Using pointer equality will
+miss instances created using the two different objects. Recall we do not use
+hash-consing on proof objects. If we hash-cons the proof objects, it would be ok
+to use pointer equality.
 -/
 structure PreInstance where
   proof      : Expr
@@ -647,14 +658,14 @@ structure PreInstance where
 
 instance : Hashable PreInstance where
   hash i := Id.run do
-    let mut r := hashPtrExpr i.proof
+    let mut r := hash i.proof -- **Note**: See note at `PreInstance`.
     for v in i.assignment do
       r := mixHash r (hashPtrExpr v)
     return r
 
 instance : BEq PreInstance where
   beq i₁ i₂ := Id.run do
-    unless isSameExpr i₁.proof i₂.proof do return false
+    unless i₁.proof == i₂.proof do return false -- **Note**: See note at `PreInstance`.
     unless i₁.assignment.size == i₂.assignment.size do return false
     for v₁ in i₁.assignment, v₂ in i₂.assignment do
       unless isSameExpr v₁ v₂ do return false
diff --git a/tests/lean/run/grind_preinstance_set_bug.lean b/tests/lean/run/grind_preinstance_set_bug.lean
new file mode 100644
index 0000000000..17ce0fb96b
--- /dev/null
+++ b/tests/lean/run/grind_preinstance_set_bug.lean
@@ -0,0 +1,12 @@
+opaque f : Nat → Nat
+opaque g : Nat → Nat
+theorem fax : f (x + 1) = g (f x) := sorry
+
+/--
+error: `instantiate` tactic failed to instantiate new facts, use `show_patterns` to see active theorems and their patterns.
+-/
+#guard_msgs in
+example : f (x + 5) = a := by
+  grind =>
+    use [fax]; use [fax]; use [fax]; use [fax]; use [fax];
+    use [fax] -- Should fail - no new facts
diff --git a/tests/lean/run/grind_set_config.lean b/tests/lean/run/grind_set_config.lean
new file mode 100644
index 0000000000..8df3acc450
--- /dev/null
+++ b/tests/lean/run/grind_set_config.lean
@@ -0,0 +1,15 @@
+set_option warn.sorry false
+opaque f : Nat → Nat
+opaque g : Nat → Nat
+theorem fax : f (x + 1) = g (f x) := sorry
+
+example : f (x + 100) = a := by
+  grind =>
+    set_option gen 15 in
+    -- The following instantiations should not fail since we set
+    -- `gen` to 15
+    use [fax]; use [fax]; use [fax]; use [fax]; use [fax]
+    use [fax]; use [fax]; use [fax]; use [fax]; use [fax]
+    use [fax]; use [fax]; use [fax]; use [fax]; use [fax]
+    fail_if_success use [fax] -- should fail
+    sorry