feat: trace messages for working and closing goals in the grind tactic (#6567)

This PR adds support for erasing the `[grind]` attribute used to mark
theorems for heuristic instantiation in the `grind` tactic.

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

@@ -36,14 +36,17 @@ def cases (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := mvarId.withConte
     let mut recursor := mkApp (mkAppN recursor indicesExpr) (mkFVar fvarId)
     let mut recursorType ← inferType recursor
     let mut mvarIdsNew := #[]
+    let mut idx := 1
     for _ in [:recursorInfo.numMinors] do
       let .forallE _ targetNew recursorTypeNew _ ← whnf recursorType
         | throwTacticEx `grind.cases mvarId "unexpected recursor type"
       recursorType := recursorTypeNew
-      let mvar ← mkFreshExprSyntheticOpaqueMVar targetNew tag
+      let tagNew := if recursorInfo.numMinors > 1 then Name.num tag idx else tag
+      let mvar ← mkFreshExprSyntheticOpaqueMVar targetNew tagNew
       recursor := mkApp recursor mvar
       let mvarIdNew ← mvar.mvarId!.tryClearMany (indices.push fvarId)
       mvarIdsNew := mvarIdsNew.push mvarIdNew
+      idx := idx + 1
     mvarId.assign recursor
     return mvarIdsNew.toList
   if recursorInfo.numIndices > 0 then

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

@@ -43,7 +43,7 @@ private def removeParents (root : Expr) : GoalM ParentSet := do
   for parent in parents do
     -- Recall that we may have `Expr.forallE` in `parents` because of `ForallProp.lean`
     if (← pure parent.isApp <&&> isCongrRoot parent) then
-      trace[grind.debug.parent] "remove: {parent}"
+      trace_goal[grind.debug.parent] "remove: {parent}"
       modify fun s => { s with congrTable := s.congrTable.erase { e := parent } }
   return parents
 
@@ -54,7 +54,7 @@ This is an auxiliary function performed while merging equivalence classes.
 private def reinsertParents (parents : ParentSet) : GoalM Unit := do
   for parent in parents do
     if (← pure parent.isApp <&&> isCongrRoot parent) then
-      trace[grind.debug.parent] "reinsert: {parent}"
+      trace_goal[grind.debug.parent] "reinsert: {parent}"
       addCongrTable parent
 
 /-- Closes the goal when `True` and `False` are in the same equivalence class. -/
@@ -91,9 +91,9 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
   let rhsNode ← getENode rhs
   if isSameExpr lhsNode.root rhsNode.root then
     -- `lhs` and `rhs` are already in the same equivalence class.
-    trace[grind.debug] "{← ppENodeRef lhs} and {← ppENodeRef rhs} are already in the same equivalence class"
+    trace_goal[grind.debug] "{← ppENodeRef lhs} and {← ppENodeRef rhs} are already in the same equivalence class"
     return ()
-  trace[grind.eqc] "{← if isHEq then mkHEq lhs rhs else mkEq lhs rhs}"
+  trace_goal[grind.eqc] "{← if isHEq then mkHEq lhs rhs else mkEq lhs rhs}"
   let lhsRoot ← getENode lhsNode.root
   let rhsRoot ← getENode rhsNode.root
   let mut valueInconsistency := false
@@ -118,11 +118,11 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
   unless (← isInconsistent) do
     if valueInconsistency then
       closeGoalWithValuesEq lhsRoot.self rhsRoot.self
-  trace[grind.debug] "after addEqStep, {← ppState}"
+  trace_goal[grind.debug] "after addEqStep, {← ppState}"
   checkInvariants
 where
   go (lhs rhs : Expr) (lhsNode rhsNode lhsRoot rhsRoot : ENode) (flipped : Bool) : GoalM Unit := do
-    trace[grind.debug] "adding {← ppENodeRef lhs} ↦ {← ppENodeRef rhs}"
+    trace_goal[grind.debug] "adding {← ppENodeRef lhs} ↦ {← ppENodeRef rhs}"
     /-
     We have the following `target?/proof?`
     `lhs -> ... -> lhsNode.root`
@@ -139,7 +139,7 @@ where
     }
     let parents ← removeParents lhsRoot.self
     updateRoots lhs rhsNode.root
-    trace[grind.debug] "{← ppENodeRef lhs} new root {← ppENodeRef rhsNode.root}, {← ppENodeRef (← getRoot lhs)}"
+    trace_goal[grind.debug] "{← ppENodeRef lhs} new root {← ppENodeRef rhsNode.root}, {← ppENodeRef (← getRoot lhs)}"
     reinsertParents parents
     setENode lhsNode.root { (← getENode lhsRoot.self) with -- We must retrieve `lhsRoot` since it was updated.
       next := rhsRoot.next
@@ -208,7 +208,7 @@ def addNewEq (lhs rhs proof : Expr) (generation : Nat) : GoalM Unit := do
 
 /-- Adds a new `fact` justified by the given proof and using the given generation. -/
 def add (fact : Expr) (proof : Expr) (generation := 0) : GoalM Unit := do
-  trace[grind.assert] "{fact}"
+  trace_goal[grind.assert] "{fact}"
   if (← isInconsistent) then return ()
   resetNewEqs
   let_expr Not p := fact

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

@@ -20,7 +20,7 @@ private partial def propagateInjEqs (eqs : Expr) (proof : Expr) : GoalM Unit :=
   | HEq _ lhs _ rhs =>
     pushHEq (← shareCommon lhs) (← shareCommon rhs) proof
   | _ =>
-   trace[grind.issues] "unexpected injectivity theorem result type{indentExpr eqs}"
+   trace_goal[grind.issues] "unexpected injectivity theorem result type{indentExpr eqs}"
    return ()
 
 /--

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

@@ -221,7 +221,7 @@ private def addNewInstance (origin : Origin) (proof : Expr) (generation : Nat) :
     -- `initApp` is a match-application that we don't need to split at anymore.
     markCaseSplitAsResolved (← read).initApp
     prop ← annotateMatchEqnType prop
-  trace[grind.ematch.instance] "{← origin.pp}: {prop}"
+  trace_goal[grind.ematch.instance] "{← origin.pp}: {prop}"
   addTheoremInstance proof prop (generation+1)
 
 /--
@@ -232,13 +232,13 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
   let thm := (← read).thm
   unless (← markTheoremInstance thm.proof c.assignment) do
     return ()
-  trace[grind.ematch.instance.assignment] "{← thm.origin.pp}: {assignmentToMessageData c.assignment}"
+  trace_goal[grind.ematch.instance.assignment] "{← thm.origin.pp}: {assignmentToMessageData c.assignment}"
   let proof ← thm.getProofWithFreshMVarLevels
   let numParams := thm.numParams
   assert! c.assignment.size == numParams
   let (mvars, bis, _) ← forallMetaBoundedTelescope (← inferType proof) numParams
   if mvars.size != thm.numParams then
-    trace[grind.issues] "unexpected number of parameters at {← thm.origin.pp}"
+    trace_goal[grind.issues] "unexpected number of parameters at {← thm.origin.pp}"
     return ()
   -- Apply assignment
   for h : i in [:mvars.size] do
@@ -246,14 +246,14 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
     unless isSameExpr v unassigned do
       let mvarId := mvars[i].mvarId!
       unless (← isDefEq (← mvarId.getType) (← inferType v) <&&> mvarId.checkedAssign v) do
-        trace[grind.issues] "type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}"
+        trace_goal[grind.issues] "type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}"
         return ()
   -- Synthesize instances
   for mvar in mvars, bi in bis do
     if bi.isInstImplicit && !(← mvar.mvarId!.isAssigned) then
       let type ← inferType mvar
       unless (← synthesizeInstance mvar type) do
-        trace[grind.issues] "failed to synthesize instance when instantiating {← thm.origin.pp}{indentExpr type}"
+        trace_goal[grind.issues] "failed to synthesize instance when instantiating {← thm.origin.pp}{indentExpr type}"
         return ()
   let proof := mkAppN proof mvars
   if (← mvars.allM (·.mvarId!.isAssigned)) then
@@ -261,7 +261,7 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
   else
     let mvars ← mvars.filterM fun mvar => return !(← mvar.mvarId!.isAssigned)
     if let some mvarBad ← mvars.findM? fun mvar => return !(← isProof mvar) then
-      trace[grind.issues] "failed to instantiate {← thm.origin.pp}, failed to instantiate non propositional argument with type{indentExpr (← inferType mvarBad)}"
+      trace_goal[grind.issues] "failed to instantiate {← thm.origin.pp}, failed to instantiate non propositional argument with type{indentExpr (← inferType mvarBad)}"
     let proof ← mkLambdaFVars (binderInfoForMVars := .default) mvars (← instantiateMVars proof)
     addNewInstance thm.origin proof c.gen
 where

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

@@ -17,19 +17,19 @@ If so, internalize the term `proj_i (ctor ... a_i ...)` and add the equality `pr
 -/
 def propagateForallPropUp (e : Expr) : GoalM Unit := do
   let .forallE n p q bi := e | return ()
-  trace[grind.debug.forallPropagator] "{e}"
+  trace_goal[grind.debug.forallPropagator] "{e}"
   if !q.hasLooseBVars then
     propagateImpliesUp p q
   else
     unless (← isEqTrue p) do return
-    trace[grind.debug.forallPropagator] "isEqTrue, {e}"
+    trace_goal[grind.debug.forallPropagator] "isEqTrue, {e}"
     let h₁ ← mkEqTrueProof p
     let qh₁ := q.instantiate1 (mkApp2 (mkConst ``of_eq_true) p h₁)
     let r ← simp qh₁
     let q := mkLambda n bi p q
     let q' := r.expr
     internalize q' (← getGeneration e)
-    trace[grind.debug.forallPropagator] "q': {q'} for{indentExpr e}"
+    trace_goal[grind.debug.forallPropagator] "q': {q'} for{indentExpr e}"
     let h₂ ← r.getProof
     let h := mkApp5 (mkConst ``Lean.Grind.forall_propagator) p q q' h₁ h₂
     pushEq e q' h

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

@@ -22,9 +22,9 @@ def addCongrTable (e : Expr) : GoalM Unit := do
     let g := e'.getAppFn
     unless isSameExpr f g do
       unless (← hasSameType f g) do
-        trace[grind.issues] "found congruence between{indentExpr e}\nand{indentExpr e'}\nbut functions have different types"
+        trace_goal[grind.issues] "found congruence between{indentExpr e}\nand{indentExpr e'}\nbut functions have different types"
         return ()
-    trace[grind.debug.congr] "{e} = {e'}"
+    trace_goal[grind.debug.congr] "{e} = {e'}"
     pushEqHEq e e' congrPlaceholderProof
     let node ← getENode e
     setENode e { node with congr := e' }
@@ -46,7 +46,7 @@ private def updateAppMap (e : Expr) : GoalM Unit := do
 
 /-- Inserts `e` into the list of case-split candidates. -/
 private def addSplitCandidate (e : Expr) : GoalM Unit := do
-  trace[grind.split.candidate] "{e}"
+  trace_goal[grind.split.candidate] "{e}"
   modify fun s => { s with splitCandidates := e :: s.splitCandidates }
 
 -- TODO: add attribute to make this extensible
@@ -89,7 +89,7 @@ private partial def activateTheorem (thm : EMatchTheorem) (generation : Nat) : G
   -- We don't want to use structural equality when comparing keys.
   let proof ← shareCommon thm.proof
   let thm := { thm with proof, patterns := (← thm.patterns.mapM (internalizePattern · generation)) }
-  trace[grind.ematch] "activated `{thm.origin.key}`, {thm.patterns.map ppPattern}"
+  trace_goal[grind.ematch] "activated `{thm.origin.key}`, {thm.patterns.map ppPattern}"
   modify fun s => { s with newThms := s.newThms.push thm }
 
 /--
@@ -117,12 +117,12 @@ private partial def activateTheoremPatterns (fName : Name) (generation : Nat) :
         match symbols with
         | [] => activateTheorem thm generation
         | _ =>
-          trace[grind.ematch] "reinsert `{thm.origin.key}`"
+          trace_goal[grind.ematch] "reinsert `{thm.origin.key}`"
           modify fun s => { s with thmMap := s.thmMap.insert thm }
 
 partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
   if (← alreadyInternalized e) then return ()
-  trace[grind.internalize] "{e}"
+  trace_goal[grind.internalize] "{e}"
   match e with
   | .bvar .. => unreachable!
   | .sort .. => return ()
@@ -142,7 +142,7 @@ partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
   | .mvar ..
   | .mdata ..
   | .proj .. =>
-    trace[grind.issues] "unexpected term during internalization{indentExpr e}"
+    trace_goal[grind.issues] "unexpected term during internalization{indentExpr e}"
     mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
   | .app .. =>
     if (← isLitValue e) then

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

@@ -85,9 +85,9 @@ private def checkProofs : GoalM Unit := do
       for b in eqc do
         unless isSameExpr a b do
           let p ← mkEqHEqProof a b
-          trace[grind.debug.proofs] "{a} = {b}"
+          trace_goal[grind.debug.proofs] "{a} = {b}"
           check p
-          trace[grind.debug.proofs] "checked: {← inferType p}"
+          trace_goal[grind.debug.proofs] "checked: {← inferType p}"
 
 /--
 Checks basic invariants if `grind.debug` is enabled.

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

@@ -60,6 +60,7 @@ private def initCore (mvarId : MVarId) : GrindM (List Goal) := do
   let mvarId ← mvarId.revertAll
   let mvarId ← mvarId.unfoldReducible
   let mvarId ← mvarId.betaReduce
+  appendTagSuffix mvarId `grind
   let goals ← intros (← mkGoal mvarId) (generation := 0)
   goals.forM (·.checkInvariants (expensive := true))
   return goals.filter fun goal => !goal.inconsistent

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

@@ -30,7 +30,7 @@ def propagateProjEq (parent : Expr) : GoalM Unit := do
     let parentNew ← shareCommon (mkApp parent.appFn! ctor)
     internalize parentNew (← getGeneration parent)
     pure parentNew
-  trace[grind.debug.proj] "{parentNew}"
+  trace_goal[grind.debug.proj] "{parentNew}"
   let idx := info.numParams + info.i
   unless idx < ctor.getAppNumArgs do return ()
   let v := ctor.getArg! idx

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

@@ -110,7 +110,7 @@ def splitNext : GrindTactic := fun goal => do
     let some c ← selectNextSplit?
       | return none
     let gen ← getGeneration c
-    trace[grind.split] "{c}, generation: {gen}"
+    trace_goal[grind.split] "{c}, generation: {gen}"
     -- TODO: `match`
     let major ← mkCasesMajor c
     let mvarIds ← cases (← get).mvarId major

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

@@ -83,6 +83,11 @@ structure State where
   simpStats  : Simp.Stats := {}
   trueExpr   : Expr
   falseExpr  : Expr
+  /--
+  Used to generate trace messages of the for `[grind] working on <tag>`,
+  and implement the macro `trace_goal`.
+  -/
+  lastTag    : Name := .anonymous
 
 private opaque MethodsRefPointed : NonemptyType.{0}
 private def MethodsRef : Type := MethodsRefPointed.type
@@ -126,9 +131,9 @@ Applies hash-consing to `e`. Recall that all expressions in a `grind` goal have
 been hash-consed. We perform this step before we internalize expressions.
 -/
 def shareCommon (e : Expr) : GrindM Expr := do
-  modifyGet fun { canon, scState, nextThmIdx, congrThms, trueExpr, falseExpr, simpStats } =>
+  modifyGet fun { canon, scState, nextThmIdx, congrThms, trueExpr, falseExpr, simpStats, lastTag } =>
     let (e, scState) := ShareCommon.State.shareCommon scState e
-    (e, { canon, scState, nextThmIdx, congrThms, trueExpr, falseExpr, simpStats })
+    (e, { canon, scState, nextThmIdx, congrThms, trueExpr, falseExpr, simpStats, lastTag })
 
 /--
 Canonicalizes nested types, type formers, and instances in `e`.
@@ -401,6 +406,25 @@ abbrev GoalM := StateRefT Goal GrindM
 @[inline] def GoalM.run' (goal : Goal) (x : GoalM Unit) : GrindM Goal :=
   goal.mvarId.withContext do StateRefT'.run' (x *> get) goal
 
+def updateLastTag : GoalM Unit := do
+  if (← isTracingEnabledFor `grind) then
+    let currTag ← (← get).mvarId.getTag
+    if currTag != (← getThe Grind.State).lastTag then
+      trace[grind] "working on goal `{currTag}`"
+      modifyThe Grind.State fun s => { s with lastTag := currTag }
+
+/--
+Macro similar to `trace[...]`, but it includes the trace message `trace[grind] "working on <current goal>"`
+if the tag has changed since the last trace message.
+-/
+macro "trace_goal[" id:ident "]" s:(interpolatedStr(term) <|> term) : doElem => do
+  let msg ← if s.raw.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
+  `(doElem| do
+    let cls := $(quote id.getId.eraseMacroScopes)
+    if (← Lean.isTracingEnabledFor cls) then
+      updateLastTag
+      Lean.addTrace cls $msg)
+
 /--
 A helper function used to mark a theorem instance found by the E-matching module.
 It returns `true` if it is a new instance and `false` otherwise.
@@ -652,7 +676,9 @@ def mkEqFalseProof (a : Expr) : GoalM Expr := do
 
 /-- Marks current goal as inconsistent without assigning `mvarId`. -/
 def markAsInconsistent : GoalM Unit := do
-  modify fun s => { s with inconsistent := true }
+  unless (← get).inconsistent do
+    trace[grind] "closed `{← (← get).mvarId.getTag}`"
+    modify fun s => { s with inconsistent := true }
 
 /--
 Closes the current goal using the given proof of `False` and
@@ -751,7 +777,7 @@ Remark: we currently use this feature to disable `match`-case-splits
 -/
 def markCaseSplitAsResolved (e : Expr) : GoalM Unit := do
   unless (← isResolvedCaseSplit e) do
-    trace[grind.split.resolved] "{e}"
+    trace_goal[grind.split.resolved] "{e}"
     modify fun s => { s with resolvedSplits := s.resolvedSplits.insert { expr := e } }
 
 end Lean.Meta.Grind

src/Lean/Util/Trace.lean

@@ -293,13 +293,16 @@ def registerTraceClass (traceClassName : Name) (inherited := false) (ref : Name
   if inherited then
     inheritedTraceOptions.modify (·.insert optionName)
 
-macro "trace[" id:ident "]" s:(interpolatedStr(term) <|> term) : doElem => do
-  let msg ← if s.raw.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
+def expandTraceMacro (id : Syntax) (s : Syntax) : MacroM (TSyntax `doElem) := do
+  let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
   `(doElem| do
     let cls := $(quote id.getId.eraseMacroScopes)
     if (← Lean.isTracingEnabledFor cls) then
       Lean.addTrace cls $msg)
 
+macro "trace[" id:ident "]" s:(interpolatedStr(term) <|> term) : doElem => do
+  expandTraceMacro id s.raw
+
 def bombEmoji := "💥️"
 def checkEmoji := "✅️"
 def crossEmoji := "❌️"

tests/lean/run/grind_erase_attr.lean

@@ -25,6 +25,7 @@ attribute [-grind] fthm
 
 /--
 error: `grind` failed
+case grind
 a : Nat
 x✝ : ¬f (f (f a)) = f a
 ⊢ False
@@ -60,6 +61,7 @@ attribute [-grind] g
 
 /--
 error: `grind` failed
+case grind
 a b : Nat
 a✝¹ : g a = b
 a✝ : a = 0

tests/lean/run/grind_pre.lean

@@ -5,6 +5,7 @@ set_option grind.debug.proofs true
 
 /--
 error: `grind` failed
+case grind.1.2
 a b c : Bool
 p q : Prop
 left✝ : a = true
@@ -23,6 +24,7 @@ theorem ex (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by
 open Lean.Grind.Eager in
 /--
 error: `grind` failed
+case grind.2.1
 a b c : Bool
 p q : Prop
 left✝ : a = true
@@ -40,6 +42,7 @@ def g (i : Nat) (j : Nat) (_ : i > j := by omega) := i + j
 
 /--
 error: `grind` failed
+case grind
 i j : Nat
 h : j + 1 < i + 1
 h✝ : j + 1 ≤ i
@@ -56,6 +59,7 @@ structure Point where
 
 /--
 error: `grind` failed
+case grind
 a₁ : Point
 a₂ : Nat
 a₃ : Int
@@ -82,6 +86,7 @@ example (p : Prop) (a b c : Nat) : p → a = 0 → a = b → h a = h c → a = c
 set_option trace.grind.debug.proof true
 /--
 error: `grind` failed
+case grind
 α : Type
 a : α
 p q r : Prop

tests/lean/run/grind_split.lean

@@ -5,10 +5,29 @@ example (p q : Prop) : p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p ∨ ¬q → F
 
 opaque R : Nat → Prop
 
+/--
+info: [grind] working on goal `grind`
+[grind.eqc] (if p then a else b) = c
+[grind.eqc] R a = True
+[grind.eqc] R b = True
+[grind.eqc] R c = False
+[grind.split] if p then a else b, generation: 0
+[grind] working on goal `grind.1`
+[grind.eqc] p = True
+[grind.eqc] (if p then a else b) = a
+[grind.eqc] R a = R c
+[grind] closed `grind.1`
+[grind] working on goal `grind.2`
+[grind.eqc] p = False
+[grind.eqc] (if p then a else b) = b
+[grind.eqc] R b = R c
+[grind] closed `grind.2`
+-/
+#guard_msgs (info) in
+set_option trace.grind true in
 example (p : Prop) [Decidable p] (a b c : Nat) : (if p then a else b) = c → R a → R b → R c := by
   grind
 
-
 namespace grind_test_induct_pred
 
 inductive Expr where
@@ -29,6 +48,7 @@ inductive HasType : Expr → Ty → Prop
   | bool : HasType (.bool v) .bool
   | and  : HasType a .bool → HasType b .bool → HasType (.and a b) .bool
 
+set_option trace.grind true
 theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t₂ := by
   grind