From 5a103b4c755215d34abc568ecd60649a87deed3b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Nov 2026 03:29:09 +0000 Subject: [PATCH] fix: relate casts from Nat and Int in grind rings MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR fixes `grind` failing on goals that mix a cast from `Nat` and a cast from `Int` into the same ring, such as `(m : Int) (k : Nat) (h : m = k) : (m : R) = (k : R)`. With the new normalizer (`backward.grind.normalizer false`) this also affected goals written as `(m : R) = ((k : Int) : R)`, because the normalizer rewrites `((k : Int) : R)` to `(k : R)`. A ring has two casts, `NatCast.natCast` and `IntCast.intCast`, and congruence only relates applications of the same function, so `↑m` and `↑k` stayed unrelated even when `m = ↑k`. The ring solver now asserts `((a : Int) : α) = ↑a` for each cast `↑a` of a non-numeral from `Nat`, but only once the ring contains a cast of a non-numeral from `Int`. The equation bypasses the normalizer, which would rewrite it to `↑a = ↑a`. Co-Authored-By: Claude Opus 5.5 --- .../Grind/Arith/CommRing/Internalize.lean | 51 +++++++++++ .../Tactic/Grind/Arith/CommRing/Types.lean | 6 ++ tests/elab/grind_ring_natCast_intCast.lean | 86 +++++++++++++++++++ 3 files changed, 143 insertions(+) create mode 100644 tests/elab/grind_ring_natCast_intCast.lean diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean index af9ac67ab3bb..2df83caad8a9 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean @@ -156,6 +156,56 @@ private def processPowIdentityVars : RingM Unit := do pushNewFact proof modifyCommRingState fun s => { s with powIdentityVarCount := vars.size } +/-- Asserts `((a : Int) : α) = ↑a` for `e := ↑a`. -/ +private def pushNatCastFact (ring : Sym.Arith.Ring) (intCastFn e : Expr) : GoalM Unit := do + let_expr NatCast.natCast _ _ a := e | return () + let natCastInt := mkApp3 (mkConst ``NatCast.natCast [0]) Int.mkType (mkConst ``instNatCastInt) a + let expected ← shareCommon (← canon (← mkEq (mkApp intCastFn natCastInt) e)) + let proof := mkApp3 (mkConst ``Grind.Ring.intCast_natCast [ring.u]) ring.type ring.ringInst a + pushNewFactCore expected (mkExpectedPropHint proof expected) (← getGeneration e) + +/-- +A ring has two casts, and congruence only relates applications of the same function: without +`((a : Int) : α) = ↑a`, the terms `↑m` for `m : Int` and `↑a` for `a : Nat` are unrelated even +when `m = ↑a`. The equation is asserted for each cast `↑a` of a non-numeral, but only once the +ring has a cast `↑m` of a non-numeral, since it relates nothing else. It bypasses the normalizer, +which rewrites `((a : Int) : α)` to `↑a`. +-/ +private def processCast [MonadLiftT GoalM m] [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] + [MonadRing m] [MonadRingState m] (e : Expr) : m Unit := do + match_expr e with + | NatCast.natCast _ inst a => + if Sym.isNatValue a then return () + if (← getRingState).natCastSet.contains { expr := e } then return () + unless isSameExpr (← getNatCastFn).appArg! inst do return () + modifyRingState fun s => { s with natCastSet := s.natCastSet.insert { expr := e } } + if (← getRingState).hasIntCast then + pushNatCastFact (← getRing) (← getIntCastFn) e + else + modifyRingState fun s => { s with natCasts := s.natCasts.push e } + | IntCast.intCast _ inst m => + if (← getRingState).hasIntCast then return () + if (Sym.getIntValue? m).run.isSome then return () + unless isSameExpr (← getIntCastFn).appArg! inst do return () + let natCasts := (← getRingState).natCasts + modifyRingState fun s => { s with hasIntCast := true, natCasts := {} } + let ring ← getRing + let intCastFn ← getIntCastFn + natCasts.forM fun e => pushNatCastFact ring intCastFn e + | _ => return () + +/-- Runs `processCast` if `e` is a cast into a ring other than `Int`. -/ +private def internalizeCast (e : Expr) : GoalM Unit := do + let α ← match_expr e with + | NatCast.natCast α _ _ => pure α + | IntCast.intCast α _ _ => pure α + | _ => return () + if α.isConstOf ``Int then return () + if let some ringId ← getCommRingId? α then + RingM.run ringId do processCast e + else if let some ringId ← getNonCommRingId? α then + NonCommRingM.run ringId do processCast e + /-- Returns `true` if `e` is a term `a⁻¹`. -/ private def internalizeInv (e : Expr) : GoalM Bool := do match_expr e with @@ -171,6 +221,7 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do -- `e` is an auxiliary term used to convert `CommRing` to `IntModule` return () if (← internalizeInv e) then return () + internalizeCast e let some type := getType? e | return () if isForbiddenParent parent? then return () if (← pure (isIneqParent parent?) <&&> Cutsat.isCutsatType type) then return () diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean index f0c081f0f08c..0916a7f5cb99 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean @@ -176,6 +176,12 @@ structure RingState where varMap : PHashMap ExprPtr Var := {} /-- Mapping from Lean expressions to their representations as `RingExpr` -/ denote : PHashMap ExprPtr RingExpr := {} + /-- Casts `↑a` from `Nat` that have been seen. -/ + natCastSet : PHashSet ExprPtr := {} + /-- Casts `↑a` from `Nat` for which `((a : Int) : α) = ↑a` has not been asserted yet. -/ + natCasts : PArray Expr := {} + /-- `true` once a cast `↑m` from `Int` of a non-numeral `m` has been seen. -/ + hasIntCast : Bool := false deriving Inhabited /-- Per-goal solver state of a commutative ring: the Gröbner basis machinery. -/ diff --git a/tests/elab/grind_ring_natCast_intCast.lean b/tests/elab/grind_ring_natCast_intCast.lean new file mode 100644 index 000000000000..acac66dc7241 --- /dev/null +++ b/tests/elab/grind_ring_natCast_intCast.lean @@ -0,0 +1,86 @@ +/-! +A ring has two casts from the integers: `NatCast.natCast` and `IntCast.intCast`. `grind` must +relate `(k : R)` for `k : Nat` and `(m : R)` for `m : Int` when `m = ↑k`, with both normalizers. +The `mbtc` examples come from `grind_mbtc_natCast_ring.lean`, where the `Sym.simp` normalizer +rewrites `((k : Int) : R)` to `(k : R)`. +-/ + +open Lean Grind +attribute [instance] Semiring.natCast Ring.intCast + +section +variable [CommRing R] + +example (m : Int) (k : Nat) (h : m = k) : (m : R) = (k : R) := by grind +example (m : Int) (k : Nat) (h : (k : Int) = m) : (k : R) = (m : R) := by grind +example (k : Nat) : ((k : Int) : R) = (k : R) := by grind +example (m : Int) (k : Nat) (h : m = k) : (m : R) = ((k : Int) : R) := by grind +example (m : Int) (k : Nat) (h₁ : m ≤ k) (h₂ : k ≤ m) : (m : R) = (k : R) := by grind +example (m : Int) (k : Nat) (h : m = k) (h' : (m : R) ≠ (k : R)) : False := by grind +example (x : R) (m : Int) (k : Nat) (h : m = k) : x * (m : R) = x * (k : R) := by grind +example (f : R → Nat) (m : Int) (k : Nat) (h : m = k) : f (m : R) = f (k : R) := by grind +example (m : Int) (a b : Nat) (h₁ : m = a) (h₂ : a = b) : (m : R) = (b : R) := by grind + +/-- trace: [grind.mbtc] m = ↑k -/ +#guard_msgs in +set_option trace.grind.mbtc true in +example (m : Int) (k : Nat) (h₁ : m ≤ k) (h₂ : k ≤ m + 1) (h₃ : 2 ∣ k - m) : + (m : R) = (k : R) := by + grind + +/-- trace: [grind.mbtc] m = ↑k -/ +#guard_msgs in +set_option trace.grind.mbtc true in +example (m : Int) (k : Nat) (h₁ : m ≤ k) (h₂ : k ≤ m + 1) (h₃ : 2 ∣ k - m) : + (m : R) = ((k : Int) : R) := by + grind + +end + +example [Ring R] (m : Int) (k : Nat) (h : m = k) : (m : R) = (k : R) := by grind +example [Ring R] (m : Int) (k : Nat) (h₁ : m ≤ k) (h₂ : k ≤ m + 1) (h₃ : 2 ∣ k - m) : + (m : R) = (k : R) := by + grind +example [Field R] (m : Int) (k : Nat) (h : m = k) : (m : R) = (k : R) := by grind +example (m : Int) (k : Nat) (h : m = k) : (m : Rat) = (k : Rat) := by grind +example (m : Int) (k : Nat) (h : m = k) : (m : Fin 5) = (k : Fin 5) := by grind + +/-! The same examples with the `Sym.simp` normalizer. -/ + +section +set_option backward.grind.normalizer false +variable [CommRing R] + +example (m : Int) (k : Nat) (h : m = k) : (m : R) = (k : R) := by grind +example (m : Int) (k : Nat) (h : (k : Int) = m) : (k : R) = (m : R) := by grind +example (k : Nat) : ((k : Int) : R) = (k : R) := by grind +example (m : Int) (k : Nat) (h : m = k) : (m : R) = ((k : Int) : R) := by grind +example (m : Int) (k : Nat) (h₁ : m ≤ k) (h₂ : k ≤ m) : (m : R) = (k : R) := by grind +example (m : Int) (k : Nat) (h : m = k) (h' : (m : R) ≠ (k : R)) : False := by grind +example (x : R) (m : Int) (k : Nat) (h : m = k) : x * (m : R) = x * (k : R) := by grind +example (f : R → Nat) (m : Int) (k : Nat) (h : m = k) : f (m : R) = f (k : R) := by grind +example (m : Int) (a b : Nat) (h₁ : m = a) (h₂ : a = b) : (m : R) = (b : R) := by grind + +/-- trace: [grind.mbtc] m = ↑k -/ +#guard_msgs in +set_option trace.grind.mbtc true in +example (m : Int) (k : Nat) (h₁ : m ≤ k) (h₂ : k ≤ m + 1) (h₃ : 2 ∣ k - m) : + (m : R) = (k : R) := by + grind + +/-- trace: [grind.mbtc] m = ↑k -/ +#guard_msgs in +set_option trace.grind.mbtc true in +example (m : Int) (k : Nat) (h₁ : m ≤ k) (h₂ : k ≤ m + 1) (h₃ : 2 ∣ k - m) : + (m : R) = ((k : Int) : R) := by + grind + +example [Ring S] (m : Int) (k : Nat) (h : m = k) : (m : S) = (k : S) := by grind +example [Ring S] (m : Int) (k : Nat) (h₁ : m ≤ k) (h₂ : k ≤ m + 1) (h₃ : 2 ∣ k - m) : + (m : S) = (k : S) := by + grind +example [Field F] (m : Int) (k : Nat) (h : m = k) : (m : F) = (k : F) := by grind +example (m : Int) (k : Nat) (h : m = k) : (m : Rat) = (k : Rat) := by grind +example (m : Int) (k : Nat) (h : m = k) : (m : Fin 5) = (k : Fin 5) := by grind + +end