fix: bugs in grind (#6748)

This PR fixes a few bugs in the `grind` tactic: missing issues, bad
error messages, incorrect threshold in the canonicalizer, and bug in the
ground pattern internalizer.

src/Lean/Elab/Tactic/Grind.lean

@@ -105,9 +105,9 @@ def grind
     (ps   :  TSyntaxArray ``Parser.Tactic.grindParam)
     (mainDeclName : Name) (fallback : Grind.Fallback) : MetaM Unit := do
   let params ← mkGrindParams config only ps
-  let goals ← Grind.main mvarId params mainDeclName fallback
-  unless goals.isEmpty do
-    throwError "`grind` failed\n{← Grind.goalsToMessageData goals config}"
+  let result ← Grind.main mvarId params mainDeclName fallback
+  if result.hasFailures then
+    throwError "`grind` failed\n{← result.toMessageData}"
 
 private def elabFallback (fallback? : Option Term) : TermElabM (Grind.GoalM Unit) := do
   let some fallback := fallback? | return (pure ())

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

@@ -50,17 +50,16 @@ Furthermore, `grind` will not be able to infer that  `HEq (a + a) (b + b)` even
 /--
 Helper function for `canonElemCore`. It tries `isDefEq a b` with default transparency, but using
 at most `canonHeartbeats` heartbeats. It reports an issue if the threshold is reached.
-Remark: `parent` is use only to report an issue
+Remark: `parent` is use only to report an issue.
 -/
 private def isDefEqBounded (a b : Expr) (parent : Expr) : GoalM Bool := do
   withCurrHeartbeats do
-  let config ← getConfig
+  let curr := (← getConfig).canonHeartbeats
   tryCatchRuntimeEx
-    (withTheReader Core.Context (fun ctx => { ctx with maxHeartbeats := config.canonHeartbeats }) do
+    (withTheReader Core.Context (fun ctx => { ctx with maxHeartbeats := curr*1000 }) do
       withDefault <| isDefEq a b)
     fun ex => do
       if ex.isRuntime then
-        let curr := (← getConfig).canonHeartbeats
         reportIssue m!"failed to show that{indentExpr a}\nis definitionally equal to{indentExpr b}\nwhile canonicalizing{indentExpr parent}\nusing `{curr}*1000` heartbeats, `(canonHeartbeats := {curr})`"
         return false
       else

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

@@ -109,7 +109,7 @@ private def pushCastHEqs (e : Expr) : GoalM Unit := do
   | _ => return ()
 
 private def preprocessGroundPattern (e : Expr) : GoalM Expr := do
-  shareCommon (← canon (← normalizeLevels (← unfoldReducible e)))
+  shareCommon (← canon (← normalizeLevels (← eraseIrrelevantMData (← unfoldReducible e))))
 
 private def mkENode' (e : Expr) (generation : Nat) : GoalM Unit :=
   mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
@@ -189,8 +189,12 @@ partial def internalize (e : Expr) (generation : Nat) (parent? : Option Expr :=
       propagateUp e
   | .lit .. | .const .. =>
     mkENode e generation
-  | .mvar ..
-  | .mdata ..
+  | .mvar .. =>
+    reportIssue m!"unexpected metavariable during internalization{indentExpr e}\n`grind` is not supposed to be used in goals containing metavariables."
+    mkENode' e generation
+  | .mdata .. =>
+    reportIssue m!"unexpected metadata found during internalization{indentExpr e}\n`grind` uses a pre-processing step that eliminates metadata"
+    mkENode' e generation
   | .proj .. =>
     reportIssue m!"unexpected kernel projection term during internalization{indentExpr e}\n`grind` uses a pre-processing step that folds them as projection applications, the pre-processor should have failed to fold this term"
     mkENode' e generation

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

@@ -88,18 +88,32 @@ private def initCore (mvarId : MVarId) (params : Params) : GrindM (List Goal) :=
   goals.forM (·.checkInvariants (expensive := true))
   return goals.filter fun goal => !goal.inconsistent
 
-def main (mvarId : MVarId) (params : Params) (mainDeclName : Name) (fallback : Fallback) : MetaM (List Goal) := do
-  let go : GrindM (List Goal) := do
+structure Result where
+  failures : List Goal
+  skipped  : List Goal
+  issues   : List MessageData
+  config   : Grind.Config
+
+def Result.hasFailures (r : Result) : Bool :=
+  !r.failures.isEmpty
+
+def Result.toMessageData (result : Result) : MetaM MessageData := do
+  let mut msgs ← result.failures.mapM (goalToMessageData · result.config)
+  let mut issues := result.issues
+  unless result.skipped.isEmpty do
+    let m := m!"#{result.skipped.length} other goal(s) were not fully processed due to previous failures, threshold: `(failures := {result.config.failures})`"
+    issues := .trace { cls := `issue } m #[] :: issues
+  unless issues.isEmpty do
+    msgs := msgs ++ [.trace { cls := `grind } "Issues" issues.reverse.toArray]
+  return MessageData.joinSep msgs m!"\n"
+
+def main (mvarId : MVarId) (params : Params) (mainDeclName : Name) (fallback : Fallback) : MetaM Result := do
+  let go : GrindM Result := do
     let goals ← initCore mvarId params
-    let goals ← solve goals
-    let goals ← goals.filterMapM fun goal => do
-      if goal.inconsistent then return none
-      let goal ← GoalM.run' goal fallback
-      if goal.inconsistent then return none
-      if (← goal.mvarId.isAssigned) then return none
-      return some goal
+    let (failures, skipped) ← solve goals fallback
     trace[grind.debug.final] "{← ppGoals goals}"
-    return goals
+    let issues := (← get).issues
+    return { failures, skipped, issues, config := params.config }
   go.run mainDeclName params fallback
 
 end Lean.Meta.Grind

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

@@ -127,11 +127,6 @@ private def ppOffset : M Unit := do
     ms := ms.push <| .trace { cls := `assign } m!"{e} := {val}" #[]
   pushMsg <| .trace { cls := `offset } "Assignment satisfying offset contraints" ms
 
-private def ppIssues : M Unit := do
-  let issues := (← read).issues
-  unless issues.isEmpty do
-    pushMsg <| .trace { cls := `issues } "Issues" issues.reverse.toArray
-
 private def ppThresholds (c : Grind.Config) : M Unit := do
   let goal ← read
   let maxGen := goal.enodes.foldl (init := 0) fun g _ n => Nat.max g n.generation
@@ -159,9 +154,5 @@ where
     ppActiveTheorems
     ppOffset
     ppThresholds config
-    ppIssues
-
-def goalsToMessageData (goals : List Goal) (config : Grind.Config) : MetaM MessageData :=
-  return MessageData.joinSep (← goals.mapM (goalToMessageData · config)) m!"\n"
 
 end Lean.Meta.Grind

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

@@ -40,7 +40,7 @@ def pushFailure (goal : Goal) : M Unit := do
     x goal
   catch ex =>
     if ex.isMaxHeartbeat || ex.isMaxRecDepth then
-      let goal ← goal.reportIssue ex.toMessageData
+      reportIssue ex.toMessageData
       pushFailure goal
       return true
     else
@@ -62,7 +62,7 @@ def trySplit : Goal → M Bool := applyTac splitNext
 def maxNumFailuresReached : M Bool := do
   return (← get).failures.length ≥ (← getConfig).failures
 
-partial def main : M Unit := do
+partial def main (fallback : Fallback) : M Unit := do
   repeat do
     if (← get).stop then
       return ()
@@ -76,17 +76,18 @@ partial def main : M Unit := do
       continue
     if (← trySplit goal) then
       continue
+    let goal ← GoalM.run' goal fallback
+    if goal.inconsistent || (← goal.mvarId.isAssigned) then
+      continue
     pushFailure goal
 
 end Solve
 
 /--
 Try to solve/close the given goals, and returns the ones that could not be solved.
 -/
-def solve (goals : List Goal) : GrindM (List Goal) := do
-  let (_, s) ← Solve.main.run { todo := goals }
-  let todo ← s.todo.mapM fun goal => do
-    goal.reportIssue m!"this goal was not fully processed due to previous failures, threshold: `(failures := {(← getConfig).failures})`"
-  return s.failures.reverse ++ todo
+def solve (goals : List Goal) (fallback : Fallback) : GrindM (List Goal × List Goal) := do
+  let (_, s) ← Solve.main fallback |>.run { todo := goals }
+  return (s.failures.reverse, s.todo)
 
 end Lean.Meta.Grind

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

@@ -86,6 +86,11 @@ structure State where
   and implement the macro `trace_goal`.
   -/
   lastTag    : Name := .anonymous
+  /--
+  Issues found during the proof search. These issues are reported to
+  users when `grind` fails.
+  -/
+  issues     : List MessageData := []
 
 private opaque MethodsRefPointed : NonemptyType.{0}
 private def MethodsRef : Type := MethodsRefPointed.type
@@ -133,9 +138,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 { scState, nextThmIdx, congrThms, trueExpr, falseExpr, natZExpr, simpStats, lastTag } =>
+  modifyGet fun { scState, nextThmIdx, congrThms, trueExpr, falseExpr, natZExpr, simpStats, lastTag, issues } =>
     let (e, scState) := ShareCommon.State.shareCommon scState e
-    (e, { scState, nextThmIdx, congrThms, trueExpr, falseExpr, natZExpr, simpStats, lastTag })
+    (e, { scState, nextThmIdx, congrThms, trueExpr, falseExpr, natZExpr, simpStats, lastTag, issues })
 
 /-- Returns `true` if `e` is the internalized `True` expression.  -/
 def isTrueExpr (e : Expr) : GrindM Bool :=
@@ -160,6 +165,15 @@ def mkHCongrWithArity (f : Expr) (numArgs : Nat) : GrindM CongrTheorem := do
   modify fun s => { s with congrThms := s.congrThms.insert key result }
   return result
 
+def reportIssue (msg : MessageData) : GrindM Unit := do
+  let msg ← addMessageContext msg
+  modify fun s => { s with issues := .trace { cls := `issue } msg #[] :: s.issues }
+  /-
+  We also add a trace message because we may want to know when
+  an issue happened relative to other trace messages.
+  -/
+  trace[grind.issues] msg
+
 /--
 Stores information for a node in the egraph.
 Each internalized expression `e` has an `ENode` associated with it.
@@ -394,11 +408,6 @@ structure Goal where
   nextThmIdx : Nat := 0
   /-- Asserted facts -/
   facts      : PArray Expr := {}
-  /--
-  Issues found during the proof search in this goal. This issues are reported to
-  users when `grind` fails.
-  -/
-  issues     : List MessageData := []
   /-- Cached extensionality theorems for types. -/
   extThms    : PHashMap ENodeKey (Array Ext.ExtTheorem) := {}
   deriving Inhabited
@@ -421,20 +430,6 @@ def updateLastTag : GoalM Unit := do
       trace[grind] "working on goal `{currTag}`"
       modifyThe Grind.State fun s => { s with lastTag := currTag }
 
-def Goal.reportIssue (goal : Goal) (msg : MessageData) : MetaM Goal := do
-  let msg ← addMessageContext msg
-  let goal := { goal with issues := .trace { cls := `issue } msg #[] :: goal.issues }
-  /-
-  We also add a trace message because we may want to know when
-  an issue happened relative to other trace messages.
-  -/
-  trace[grind.issues] msg
-  return goal
-
-def reportIssue (msg : MessageData) : GoalM Unit := do
-  let goal ← (← get).reportIssue msg
-  set goal
-
 /--
 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.

tests/lean/run/grind_cat2.lean

@@ -261,97 +261,12 @@ In this example, we restrict the number of heartbeats used by the canonicalizer.
 The idea is to test the issue tracker.
 -/
 
-/--
-error: `grind` failed
-case grind
-C✝¹ : Type u₁
-inst✝⁸ : Category C✝¹
-D✝ : Type u₂
-inst✝⁷ : Category D✝
-E✝ : Type u₃
-inst✝⁶ : Category E✝
-F✝ G✝ H : C✝¹ ⥤ D✝
-C✝ : Type u
-inst✝⁵ : Category C✝
-X✝ Y✝ Z✝ : C✝
-C : Type u₁
-inst✝⁴ : Category C
-D : Type u₂
-inst✝³ : Category D
-E : Type u₃
-inst✝² : Category E
-F : C → D
-inst✝¹ : Functorial F
-G : D → E
-inst✝ : Functorial G
-__src✝ : C ⥤ E := of F ⋙ of G
-X Y Z : C
-f : X ⟶ Y
-g : Y ⟶ Z
-x✝ : ¬map G (map F (f ≫ g)) = map G (map F f) ≫ map G (map F g)
-⊢ False
-[grind] Diagnostics
-  [facts] Asserted facts
-    [prop] __src✝ = of F ⋙ of G
-    [prop] ¬map G (map F (f ≫ g)) = map G (map F f) ≫ map G (map F g)
-    [prop] map F (f ≫ g) = map F f ≫ map F g
-    [prop] map G (map F f ≫ map F g) = map G (map F f) ≫ map G (map F g)
-  [eqc] False propositions
-    [prop] map G (map F (f ≫ g)) = map G (map F f) ≫ map G (map F g)
-  [eqc] Equivalence classes
-    [eqc] {map G (map F f ≫ map F g), map G (map F (f ≫ g)), map G (map F f) ≫ map G (map F g)}
-    [eqc] {map F (f ≫ g), map F f ≫ map F g}
-    [eqc] {__src✝, of F ⋙ of G}
-  [ematch] E-matching
-    [thm] Functorial.map_comp:
-        ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C → D} [inst_2 : Functorial F]
-          {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z}, map F (f ≫ g) = map F f ≫ map F g
-        patterns: [@map #10 #9 #8 #7 #6 #5 #4 #2 (@Category.comp ? ? #4 #3 #2 #1 #0)]
-    [thm] assoc:
-        ∀ {obj : Type u} [self : Category obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z),
-          (f ≫ g) ≫ h = f ≫ g ≫ h
-        patterns: [@Category.comp #8 #7 #6 #5 #3 #2 (@Category.comp ? ? #5 #4 #3 #1 #0)]
-    [thm] assoc:
-        ∀ {obj : Type u} [self : Category obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z),
-          (f ≫ g) ≫ h = f ≫ g ≫ h
-        patterns: [@Category.comp #8 #7 #6 #4 #3 (@Category.comp ? ? #6 #5 #4 #2 #1) #0]
-  [issues] Issues
-    [issue] failed to show that
-          F Y
-        is definitionally equal to
-          F Z
-        while canonicalizing
-          map G (map F f)
-        using `100*1000` heartbeats, `(canonHeartbeats := 100)`
-    [issue] failed to show that
-          G (F X)
-        is definitionally equal to
-          (G ∘ F) X
-        while canonicalizing
-          map G (map F f) ≫ map G (map F g)
-        using `100*1000` heartbeats, `(canonHeartbeats := 100)`
-    [issue] failed to show that
-          G (F Y)
-        is definitionally equal to
-          (G ∘ F) Y
-        while canonicalizing
-          map G (map F f) ≫ map G (map F g)
-        using `100*1000` heartbeats, `(canonHeartbeats := 100)`
-    [issue] failed to show that
-          G (F Z)
-        is definitionally equal to
-          (G ∘ F) Z
-        while canonicalizing
-          map G (map F f) ≫ map G (map F g)
-        using `100*1000` heartbeats, `(canonHeartbeats := 100)`
--/
-#guard_msgs (error) in
 def functorial_comp' (F : C → D) [Functorial.{v₁, v₂} F] (G : D → E) [Functorial.{v₂, v₃} G] :
     Functorial.{v₁, v₃} (G ∘ F) :=
   { Functor.of F ⋙ Functor.of G with
     map' := fun f => map G (map F f)
     map_id' := sorry
-    map_comp' := by grind (canonHeartbeats := 100)
+    map_comp' := by grind (canonHeartbeats := 1)
   }
 
 end Ex2

tests/lean/run/grind_pre.lean

@@ -173,37 +173,8 @@ h : ¬r
     [prop] p
     [prop] q
     [prop] r
-case grind.2
-α : Type
-a : α
-p q r : Prop
-h₁ : HEq p a
-h₂ : HEq q a
-h₃ : p = r
-left : ¬p ∨ r
-h : p
-⊢ False
-[grind] Diagnostics
-  [facts] Asserted facts
-    [prop] HEq p a
-    [prop] HEq q a
-    [prop] p = r
-    [prop] ¬p ∨ r
-    [prop] ¬r ∨ p
-    [prop] p
-  [eqc] True propositions
-    [prop] p = r
-    [prop] ¬p ∨ r
-    [prop] ¬r ∨ p
-    [prop] a
-    [prop] p
-    [prop] q
-    [prop] r
-  [eqc] False propositions
-    [prop] ¬p
-    [prop] ¬r
-  [issues] Issues
-    [issue] this goal was not fully processed due to previous failures, threshold: `(failures := 1)`
+[grind] Issues
+  [issue] #1 other goal(s) were not fully processed due to previous failures, threshold: `(failures := 1)`
 -/
 #guard_msgs (error) in
 example (a : α) (p q r : Prop) : (h₁ : HEq p a) → (h₂ : HEq q a) → (h₃ : p = r) → False := by
@@ -252,8 +223,8 @@ x✝ : ¬f a = g b
   [eqc] Equivalence classes
     [eqc] {a, b}
     [eqc] {f, g}
-  [issues] Issues
-    [issue] found congruence between g b and f a but functions have different types
+[grind] Issues
+  [issue] found congruence between g b and f a but functions have different types
 -/
 #guard_msgs (error) in
 example (f : Nat → Bool) (g : Int → Bool) (a : Nat) (b : Int) : HEq f g → HEq a b → f a = g b := by