From d07862db2a60295f9089cee2d7f6faa0f8aa297b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 19 Sep 2025 14:12:25 -0700 Subject: [PATCH] chore: skip cast-like operations in `grind mbtc` (#10465) This PR skips cast-like helper `grind` functions during `grind mbtc` --- src/Lean/Meta/Tactic/Grind/MBTC.lean | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind/MBTC.lean b/src/Lean/Meta/Tactic/Grind/MBTC.lean index dcdd42bb1e..b8fc249357 100644 --- a/src/Lean/Meta/Tactic/Grind/MBTC.lean +++ b/src/Lean/Meta/Tactic/Grind/MBTC.lean @@ -7,6 +7,8 @@ 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 public section namespace Lean.Meta.Grind @@ -86,6 +88,14 @@ 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 @@ -99,10 +109,11 @@ def mbtc (ctx : MBTC.Context) : GoalM Bool := do unless (← ctx.isInterpreted e) do let f := e.getAppFn /- - Remark: we ignore type class instances in model-based theory combination. + Remark: we ignore type class instances and cast-like applications in model-based theory combination. `grind` treats instances as support elements, and they are handled by the canonicalizer. + cast-like internal operations and handled by their associated solver. -/ - unless (← isFnInstance f) do + if !(← isFnInstance f) && !isCastLike f then let mut i := 0 for arg in e.getAppArgs do let some arg ← getRoot? arg | pure ()