feat: improve grind diagnostics (#10466)

This PR reduces noise in the 'Equivalence classes' section of the
`grind` diagnostics. It now uses a notion of *support expressions*.
Right now, it is hard-coded, but we will probably make it extensible in
the future. The current definition is

- `match`, `ite` and `dite`-applications. They have builtin support in
`grind`.
- Cast-like applications used by `grind`: `toQ`, `toInt`, `Nat.cast`,
`Int.cast`, and `cast`
- `grind` gadget applications (e.g., `Grind.nestedDecidable`)
- Projections of constructors (e.g., `{ x := 1, y := 2}.x`)
- Auxiliary arithmetic terms constructed by solvers such as `cutsat` and
`ring`.

If an equivalence class contains at most one non-support term, it goes
into the “others” bucket. Otherwise, we display the non-support elements
and place the support terms in a child node.

**BEFORE**:
<img width="1397" height="1558" alt="image"
src="https://github.com/user-attachments/assets/4fd4de31-7300-4158-908b-247024381243"
/>

**AFTER**:
<img width="840" height="340" alt="image"
src="https://github.com/user-attachments/assets/05020f34-4ade-49bf-8ccc-9eb0ba53c861"
/>

**Remark**: No information is lost; it is just grouped differently."

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

@@ -0,0 +1,30 @@
+/-
+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.Expr
+import Init.Grind.ToInt
+import Init.Grind.Ring.Envelope
+import Init.Grind.Module.Envelope
+namespace Lean.Meta.Grind
+
+/-- Returns `true` if `declName` is the name of a cast-like function used to implement `grind` solvers -/
+public def isCastLikeDeclName (declName : Name) : Bool :=
+  declName == ``Grind.Ring.OfSemiring.toQ ||
+  declName == ``Grind.IntModule.OfNatModule.toQ ||
+  declName == ``Grind.ToInt.toInt ||
+  declName == ``NatCast.natCast ||
+  declName == ``IntCast.intCast
+
+/-- Returns `true` if `f` is a cast-like operation. -/
+public def isCastLikeFn (f : Expr) : Bool := Id.run do
+  let .const declName _ := f | return false
+  return isCastLikeDeclName declName
+
+public def isCastLikeApp (e : Expr) : Bool :=
+  isCastLikeFn e.getAppFn
+
+end Lean.Meta.Grind

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

@@ -7,8 +7,7 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.Canon
-import Init.Grind.Ring.Envelope
-import Init.Grind.Module.Envelope
+import Lean.Meta.Tactic.Grind.CastLike
 public section
 namespace Lean.Meta.Grind
 
@@ -88,14 +87,6 @@ private def isFnInstance (f : Expr) : CoreM Bool := do
   let .const declName _ := f | return false
   isInstance declName
 
-/-- Return `true` if `f` is a cast-like operation. We don't perform mbtc in this kind of function. -/
-private def isCastLike (f : Expr) : Bool := Id.run do
-  let .const declName _ := f | return false
-  return declName == ``Grind.Ring.OfSemiring.toQ ||
-    declName == ``Grind.IntModule.OfNatModule.toQ ||
-    declName == ``NatCast.natCast ||
-    declName == ``IntCast.intCast
-
 /-- Model-based theory combination. -/
 def mbtc (ctx : MBTC.Context) : GoalM Bool := do
   unless (← getConfig).mbtc do return false
@@ -113,7 +104,7 @@ def mbtc (ctx : MBTC.Context) : GoalM Bool := do
       `grind` treats instances as support elements, and they are handled by the canonicalizer.
       cast-like internal operations and handled by their associated solver.
       -/
-      if !(← isFnInstance f) && !isCastLike f then
+      if !(← isFnInstance f) && !isCastLikeFn f then
         let mut i := 0
         for arg in e.getAppArgs do
           let some arg ← getRoot? arg | pure ()

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

@@ -13,7 +13,9 @@ public import Lean.Meta.Tactic.Grind.Arith.Offset.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.PP
 public import Lean.Meta.Tactic.Grind.Arith.Linear.PP
 public import Lean.Meta.Tactic.Grind.AC.PP
+import Lean.Meta.Tactic.Grind.CastLike
 import Lean.PrettyPrinter
+import Lean.Meta.CtorRecognizer
 public section
 
 namespace Lean.Meta.Grind
@@ -88,9 +90,72 @@ def ppExprArray (cls : Name) (header : String) (es : Array Expr) (clsElem : Name
   let es := es.map (toTraceElem · clsElem)
   .trace { cls } header es
 
+section EqcFilter
+/-!
+Functions for deciding whether an expression is a support application or not
+when displaying equivalence classes.
+This is hard-coded for now. We will probably make it extensible in the future.
+-/
+private def isGadget (declName : Name) : Bool :=
+  declName == ``Grind.nestedDecidable
+
+private def isBuiltin (declName : Name) : Bool :=
+  declName == ``ite || declName == ``dite || declName == ``cast
+
+/-- Result for helper function `isArithOfCastLike` -/
+private inductive Result where
+  | num | cast | no
+  deriving Inhabited
+
+@[macro_inline] private def Result.and : Result → Result → Result
+  | .no,   _ | _, .no   => .no
+  | .cast, _ | _, .cast => .cast
+  | .num, .num => .num
+
+/--
+Returns `true` if `e` is an expression constructed using numerals,
+`grind` cast-like operations, and arithmetic terms. Moreover, the
+expression contains at least one cast-like application.
+This kind of term is constructed by `grind` satellite solvers.
+-/
+private partial def isArithOfCastLike (e : Expr) : Bool :=
+  go e matches .cast
+where
+  go (e : Expr) : Result :=
+    match_expr e with
+    | HAdd.hAdd _ _ _ _ a b => go a |>.and (go b)
+    | HSub.hSub _ _ _ _ a b => go a |>.and (go b)
+    | HMul.hMul _ _ _ _ a b => go a |>.and (go b)
+    | HDiv.hDiv _ _ _ _ a b => go a |>.and (go b)
+    | HMod.hMod _ _ _ _ a b => go a |>.and (go b)
+    | HPow.hPow _ _ _ _ a _ => go a
+    | Neg.neg _ _ a         => go a
+    | OfNat.ofNat _ _ _     => .num
+    | _ => if isCastLikeApp e then .cast else .no
+
+/--
+Returns `true` if `e` is a support-like application.
+Recall that equivalence classes that contain only support applications are displayed in the "others" category.
+-/
+private def isSupportApp (e : Expr) : MetaM Bool := do
+  if isArithOfCastLike e then return true
+  let .const declName _ := e.getAppFn | return false
+  -- Check whether `e` is the projection of a constructor
+  if let some info ← getProjectionFnInfo? declName then
+    if e.getAppNumArgs == info.numParams + 1 then
+      if (← isConstructorApp e.appArg!) then
+        return true
+  return isCastLikeDeclName declName || isGadget declName || isBuiltin declName || isMatcherCore (← getEnv) declName
+
+end EqcFilter
+
+private def ppEqc (eqc : List Expr) (children : Array MessageData := #[]) : MessageData :=
+  .trace { cls := `eqc } (.group ("{" ++ (MessageData.joinSep (eqc.map toMessageData) ("," ++ Format.line)) ++  "}")) children
+
 private def ppEqcs : M Unit := do
    let mut trueEqc?  : Option MessageData := none
    let mut falseEqc? : Option MessageData := none
+   let mut regularEqcs : Array MessageData := #[]
    let mut otherEqcs : Array MessageData := #[]
    let goal ← read
    for eqc in goal.getEqcs (sort := true) do
@@ -105,11 +170,22 @@ private def ppEqcs : M Unit := do
      else if let e :: _ :: _ := eqc then
        -- We may want to add a flag to pretty print equivalence classes of nested proofs
        unless (← isProof e) do
-         otherEqcs := otherEqcs.push <| .trace { cls := `eqc } (.group ("{" ++ (MessageData.joinSep (eqc.map toMessageData) ("," ++ Format.line)) ++  "}")) #[]
+         let mainEqc ← eqc.filterM fun e => return !(← isSupportApp e)
+         if mainEqc.length <= 1 then
+           otherEqcs := otherEqcs.push <| ppEqc eqc
+         else
+           let supportEqc ← eqc.filterM fun e => isSupportApp e
+           if supportEqc.isEmpty then
+             regularEqcs := regularEqcs.push <| ppEqc mainEqc
+           else
+             regularEqcs := regularEqcs.push <| ppEqc mainEqc #[ppEqc supportEqc]
+
+   unless otherEqcs.isEmpty do
+     regularEqcs := regularEqcs.push <| .trace { cls := `eqc } "others" otherEqcs
    if let some trueEqc := trueEqc? then pushMsg trueEqc
    if let some falseEqc := falseEqc? then pushMsg falseEqc
-   unless otherEqcs.isEmpty do
-     pushMsg <| .trace { cls := `eqc } "Equivalence classes" otherEqcs
+   unless regularEqcs.isEmpty do
+     pushMsg <| .trace { cls := `eqc } "Equivalence classes" regularEqcs
 
 private def ppEMatchTheorem (thm : EMatchTheorem) : MetaM MessageData := do
   let m := m!"{thm.origin.pp}: {thm.patterns.map ppPattern}"

tests/lean/run/grind_t1.lean

@@ -376,7 +376,8 @@ h_1 : b = true
   [eqc] True propositions
     [prop] b = true
   [eqc] Equivalence classes
-    [eqc] {a, 10, if b = true then 10 else 20}
+    [eqc] {a, 10}
+      [eqc] {if b = true then 10 else 20}
     [eqc] {b, true}
   [cutsat] Assignment satisfying linear constraints
     [assign] a := 10