fix: relate casts from Nat and Int in grind rings

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 ()

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. -/

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