feat: Nat.cast dsimproc

This PR removes the `grind` normalization rule `Int.natCast_succ`
because it may produce stack overflows in examples containing big constants.
See new test for an example.

src/Init/Grind/Norm.lean

@@ -130,7 +130,7 @@ init_grind_norm
   Int.ediv_zero Int.emod_zero
   Int.ediv_one Int.emod_one
   Int.natCast_add Int.natCast_mul Int.natCast_pow
-  Int.natCast_succ Int.natCast_zero natCast_div natCast_mod
+  Int.natCast_zero natCast_div natCast_mod
   -- GT GE
   ge_eq gt_eq
   -- Int op folding

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean

@@ -118,10 +118,17 @@ builtin_simproc [simp, seval] reduceDvd ((_ : Int) ∣ _) := fun e => do
   else
     return .done { expr := mkConst ``False, proof? := mkApp3 (mkConst ``Int.dvd_eq_false_of_mod_ne_zero) a b reflBoolTrue}
 
-builtin_dsimproc [simp, seval] reduceNatCast ((NatCast.natCast _ : Int))  := fun e => do
-  let_expr NatCast.natCast _ inst a ← e | return .continue
+private def reduceNatCastCore (inst : Expr) (a : Expr) : SimpM DStep := do
   let some a ← getNatValue? a | return .continue
   let_expr instNatCastInt ← inst | return .continue
   return .done <| toExpr (Int.ofNat a)
 
+builtin_dsimproc [simp, seval] reduceNatCast ((NatCast.natCast _ : Int))  := fun e => do
+  let_expr NatCast.natCast _ inst a ← e | return .continue
+  reduceNatCastCore inst a
+
+builtin_dsimproc [simp, seval] reduceNatCast' ((Nat.cast _ : Int))  := fun e => do
+  let_expr Nat.cast _ inst a ← e | return .continue
+  reduceNatCastCore inst a
+
 end Int

tests/lean/run/grind_cutsat_nat_dvd.lean

@@ -27,3 +27,6 @@ example (x y : Nat) :
     → x - y ≤ 2 → x ≥ 6
     → False := by
   grind
+
+example (i : Nat) : i < 330 → 7 ∣ (660 + i) * (1319 - i) → 1319 - i < 1979 := by
+  grind