From c6abc3c0368e10c49e9762fda1819ad0e95c9bb0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 19 Sep 2025 16:44:30 -0700 Subject: [PATCH] feat: improve `grind` diagnostics (#10466) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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**: image **AFTER**: image **Remark**: No information is lost; it is just grouped differently." --- src/Lean/Meta/Tactic/Grind/CastLike.lean | 30 +++++++++ src/Lean/Meta/Tactic/Grind/MBTC.lean | 13 +--- src/Lean/Meta/Tactic/Grind/PP.lean | 82 +++++++++++++++++++++++- tests/lean/run/grind_t1.lean | 3 +- 4 files changed, 113 insertions(+), 15 deletions(-) create mode 100644 src/Lean/Meta/Tactic/Grind/CastLike.lean diff --git a/src/Lean/Meta/Tactic/Grind/CastLike.lean b/src/Lean/Meta/Tactic/Grind/CastLike.lean new file mode 100644 index 0000000000..963461361a --- /dev/null +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/MBTC.lean b/src/Lean/Meta/Tactic/Grind/MBTC.lean index b8fc249357..3145a5c914 100644 --- a/src/Lean/Meta/Tactic/Grind/MBTC.lean +++ b/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 () diff --git a/src/Lean/Meta/Tactic/Grind/PP.lean b/src/Lean/Meta/Tactic/Grind/PP.lean index 76fc1dbbf2..c785550f5c 100644 --- a/src/Lean/Meta/Tactic/Grind/PP.lean +++ b/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}" diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean index 06d05fd672..312a708734 100644 --- a/tests/lean/run/grind_t1.lean +++ b/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