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
[...]`.

Author: leodemoura

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

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

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

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

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

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

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
 

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

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

@@ -640,21 +640,32 @@ 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
   assignment : Array Expr
 
 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

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