fix: natCast in grind cutsat (#8776)

This PR ensures that user provided `natCast` application are properly
internalized in the grind cutsat module.

Author: leodemoura

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean

@@ -290,7 +290,7 @@ def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
 
 /-- Different kinds of terms internalized by this module. -/
 private inductive SupportedTermKind where
-  | add | mul | num | div | mod | sub | pow | natAbs | toNat
+  | add | mul | num | div | mod | sub | pow | natAbs | toNat | natCast
   deriving BEq
 
 private def getKindAndType? (e : Expr) : Option (SupportedTermKind × Expr) :=
@@ -307,6 +307,7 @@ private def getKindAndType? (e : Expr) : Option (SupportedTermKind × Expr) :=
     some (.num, α)
   | Int.natAbs _ => some (.natAbs, Nat.mkType)
   | Int.toNat _ => some (.toNat, Nat.mkType)
+  | NatCast.natCast α _ _ => some (.natCast, α)
   | _ => none
 
 private def isForbiddenParent (parent? : Option Expr) (k : SupportedTermKind) : Bool := Id.run do
@@ -315,7 +316,7 @@ private def isForbiddenParent (parent? : Option Expr) (k : SupportedTermKind) :
   -- TODO: document `NatCast.natCast` case.
   -- Remark: we added it to prevent natCast_sub from being expanded twice.
   if declName == ``NatCast.natCast then return true
-  if k matches .div | .mod | .sub | .pow | .natAbs | .toNat then return false
+  if k matches .div | .mod | .sub | .pow | .natAbs | .toNat | .natCast then return false
   if declName == ``HAdd.hAdd || declName == ``LE.le || declName == ``Dvd.dvd then return true
   match k with
   | .add => return false

tests/lean/grind/omega_regressions.lean

@@ -27,7 +27,9 @@ example (a b : Int) : a + b = Int.ofNat 2 → a - 2 = -b := by
   grind
 
 /--
-trace: [grind.cutsat.assert] -1*「↑a * ↑b」 ≤ 0
+trace: [grind.cutsat.assert] -1*↑a ≤ 0
+[grind.cutsat.assert] -1*↑b ≤ 0
+[grind.cutsat.assert] -1*「↑a * ↑b」 ≤ 0
 [grind.cutsat.assert] -1*↑c ≤ 0
 [grind.cutsat.assert] -1*↑c + 「↑a * ↑b」 + 1 ≤ 0
 [grind.cutsat.assert] -1*↑0 = 0

tests/lean/run/grind_cutsat_nat_le.lean

@@ -0,0 +1,2 @@
+example (n : Int) (n0 : ¬0 ≤ n) (a : Nat) : n ≠ (a : Int) := by
+  grind