fix: kernel error in grind order module for Nat casts to non-Int types (#13453)

This PR fixes a kernel error in `grind` when propagating a `Nat`
equality to an order structure whose carrier type is not `Int` (e.g.
`Rat`). The auxiliary `Lean.Grind.Order.of_nat_eq` lemma was specialized
to `Int`, so the kernel rejected the application when the cast
destination differed.

We add a polymorphic `of_natCast_eq` lemma over `{α : Type u} [NatCast
α]` and cache the cast destination type in `TermMapEntry`.
`processNewEq` now uses the original `of_nat_eq` when the destination is
`Int` (the common case) and the new lemma otherwise. The symmetric
`nat_eq` propagation (deriving `Nat` equality from a derived cast
equality) is now guarded to fire only when the destination is `Int`,
since the `nat_eq` lemma is still specialized to `Int`.

Closes #13265.

src/Init/Grind/Order.lean

@@ -75,6 +75,9 @@ theorem nat_eq (a b : Nat) (x y : Int) : NatCast.natCast a = x → NatCast.natCa
 theorem of_nat_eq (a b : Nat) (x y : Int) : NatCast.natCast a = x → NatCast.natCast b = y → a = b → x = y := by
   intro _ _; subst x y; intro; simp [*]
 
+theorem of_natCast_eq {α : Type u} [NatCast α] (a b : Nat) (x y : α) : NatCast.natCast a = x → NatCast.natCast b = y → a = b → x = y := by
+  intro h₁ h₂ h; subst h; exact h₁.symm.trans h₂
+
 theorem le_of_not_le {α} [LE α] [Std.IsLinearPreorder α]
     {a b : α} : ¬ a ≤ b → b ≤ a := by
   intro h

src/Lean/Meta/Tactic/Grind/Order/Assert.lean

@@ -148,11 +148,14 @@ def propagatePending : OrderM Unit := do
         - `h₁ : ↑ue' = ue`
         - `h₂ : ↑ve' = ve`
         - `h : ue = ve`
-        **Note**: We currently only support `Nat`. Thus `↑a` is actually
-        `NatCast.natCast a`. If we decide to support arbitrary semirings
-        in this module, we must adjust this code.
+        **Note**: We currently only support `Nat` originals. Thus `↑a` is actually
+        `NatCast.natCast a`. The lemma `nat_eq` is specialized to `Int`, so we
+        only invoke it when the cast destination is `Int`. For other types (e.g.
+        `Rat`), `pushEq ue ve h` above is sufficient and `grind` core can derive
+        the `Nat` equality via `norm_cast`/cast injectivity if needed.
         -/
-        pushEq ue' ve' <| mkApp7 (mkConst ``Grind.Order.nat_eq) ue' ve' ue ve h₁ h₂ h
+        if (← inferType ue) == Int.mkType then
+          pushEq ue' ve' <| mkApp7 (mkConst ``Grind.Order.nat_eq) ue' ve' ue ve h₁ h₂ h
 where
   /--
   If `e` is an auxiliary term used to represent some term `a`, returns
@@ -343,7 +346,7 @@ def getStructIdOf? (e : Expr) : GoalM (Option Nat) := do
   return (← get').exprToStructId.find? { expr := e }
 
 def propagateIneq (e : Expr) : GoalM Unit := do
-  if let some (e', he) := (← get').termMap.find? { expr := e } then
+  if let some { e := e', h := he, .. } := (← get').termMap.find? { expr := e } then
     go e' (some he)
   else
     go e none
@@ -369,20 +372,27 @@ builtin_grind_propagator propagateLT ↓LT.lt := propagateIneq
 public def processNewEq (a b : Expr) : GoalM Unit := do
   unless isSameExpr a b do
     let h ← mkEqProof a b
-    if let some (a', h₁) ← getAuxTerm? a then
-      let some (b', h₂) ← getAuxTerm? b | return ()
+    if let some { e := a', h := h₁, α } ← getAuxTerm? a then
+      let some { e := b', h := h₂, .. } ← getAuxTerm? b | return ()
       /-
       We have
       - `h  : a = b`
       - `h₁ : ↑a = a'`
       - `h₂ : ↑b = b'`
+      where `a'` and `b'` are `NatCast.natCast α inst _` for some type `α`.
       -/
-      let h := mkApp7 (mkConst ``Grind.Order.of_nat_eq) a b a' b' h₁ h₂ h
-      go a' b' h
+      if α == Int.mkType then
+        let h := mkApp7 (mkConst ``Grind.Order.of_nat_eq) a b a' b' h₁ h₂ h
+        go a' b' h
+      else
+        let u ← getDecLevel α
+        let inst ← synthInstance (mkApp (mkConst ``NatCast [u]) α)
+        let h := mkApp9 (mkConst ``Grind.Order.of_natCast_eq [u]) α inst a b a' b' h₁ h₂ h
+        go a' b' h
     else
       go a b h
 where
-  getAuxTerm? (e : Expr) : GoalM (Option (Expr × Expr)) := do
+  getAuxTerm? (e : Expr) : GoalM (Option TermMapEntry) := do
     return (← get').termMap.find? { expr := e }
 
   go (a b h : Expr) : GoalM Unit := do

src/Lean/Meta/Tactic/Grind/Order/Internalize.lean

@@ -166,9 +166,9 @@ def setStructId (e : Expr) : OrderM Unit := do
     exprToStructId := s.exprToStructId.insert { expr := e } structId
   }
 
-def updateTermMap (e eNew h : Expr) : GoalM Unit := do
+def updateTermMap (e eNew h α : Expr) : GoalM Unit := do
   modify' fun s => { s with
-    termMap    := s.termMap.insert { expr := e } (eNew, h)
+    termMap    := s.termMap.insert { expr := e } { e := eNew, h, α }
     termMapInv := s.termMapInv.insert { expr := eNew } (e, h)
   }
 
@@ -198,9 +198,9 @@ where
   getOriginal? (e : Expr) : GoalM (Option Expr) := do
     if let some (e', _) := (← get').termMapInv.find? { expr := e } then
       return some e'
-    let_expr NatCast.natCast _ _ a := e | return none
+    let_expr NatCast.natCast α _ a := e | return none
     if (← alreadyInternalized a) then
-      updateTermMap a e (← mkEqRefl e)
+      updateTermMap a e (← mkEqRefl e) α
       return some a
     else
       return none
@@ -290,7 +290,7 @@ def internalizeTerm (e : Expr) : OrderM Unit := do
 
 open Arith.Cutsat in
 def adaptNat (e : Expr) : GoalM Expr := do
-  if let some (eNew, _) := (← get').termMap.find? { expr := e } then
+  if let some { e := eNew, .. } := (← get').termMap.find? { expr := e } then
     return eNew
   else match_expr e with
     | LE.le _ _ lhs rhs => adaptCnstr lhs rhs (isLT := false)
@@ -307,12 +307,12 @@ where
     let h := mkApp6
         (mkConst (if isLT then ``Nat.ToInt.lt_eq else ``Nat.ToInt.le_eq))
         lhs rhs lhs' rhs' h₁ h₂
-    updateTermMap e eNew h
+    updateTermMap e eNew h (← getIntExpr)
     return eNew
 
   adaptTerm : GoalM Expr := do
     let (eNew, h) ← natToInt e
-    updateTermMap e eNew h
+    updateTermMap e eNew h (← getIntExpr)
     return eNew
 
 def adapt (α : Expr) (e : Expr) : GoalM (Expr × Expr) := do

src/Lean/Meta/Tactic/Grind/Order/Types.lean

@@ -128,6 +128,13 @@ structure Struct where
   propagate          : List ToPropagate := []
   deriving Inhabited
 
+/-- Entry/Value for the map `termMap` in `State` -/
+structure TermMapEntry where
+  e : Expr
+  h : Expr
+  α : Expr
+deriving Inhabited
+
 /-- State for all order types detected by `grind`. -/
 structure State where
   /-- Order structures detected. -/
@@ -143,7 +150,7 @@ structure State where
   Example: given `x y : Nat`, `x ≤ y + 1` is mapped to `Int.ofNat x ≤ Int.ofNat y + 1`, and proof
   of equivalence.
   -/
-  termMap    : PHashMap ExprPtr (Expr × Expr) := {}
+  termMap    : PHashMap ExprPtr TermMapEntry := {}
   /-- `termMap` inverse -/
   termMapInv : PHashMap ExprPtr (Expr × Expr) := {}
   deriving Inhabited

tests/elab/grind_order_eq.lean

@@ -30,3 +30,6 @@ example
 example
     : a = b + 1 → a ≤ b + 2 := by
   grind -lia -linarith -ring (splits := 0) only
+
+-- Issue #13265: kernel error from `of_nat_eq` when the cast is to a non-`Int` type.
+example (j k : Nat) (h : j = k) : (j + 1 : Rat) = (k + 1 : Rat) := by grind