From 0da54f517aafc52bedd0982c8bf1a5809fd004cf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 16 Mar 2025 14:23:49 -0700
Subject: [PATCH] fix: missing `Nat` div and mod norm rules in `grind` (#7512)

This PR adds missing normalization rules for `Nat` div and mod to the
`grind` tactic.
---
 src/Init/Grind/Norm.lean                | 18 ++++++++++--------
 tests/lean/run/grind_cutsat_nat_eq.lean |  8 ++++++++
 2 files changed, 18 insertions(+), 8 deletions(-)

diff --git a/src/Init/Grind/Norm.lean b/src/Init/Grind/Norm.lean
index 4fd8368491..155f0b6168 100644
--- a/src/Init/Grind/Norm.lean
+++ b/src/Init/Grind/Norm.lean
@@ -71,6 +71,12 @@ theorem beq_eq_decide_eq {_ : BEq α} [LawfulBEq α] [DecidableEq α] (a b : α)
 theorem bne_eq_decide_not_eq {_ : BEq α} [LawfulBEq α] [DecidableEq α] (a b : α) : (a != b) = (decide (¬ a = b)) := by
   by_cases a = b <;> simp [*]
 
+theorem natCast_div (a b : Nat) : (↑(a / b) : Int) = ↑a / ↑b := by
+  rfl
+
+theorem natCast_mod (a b : Nat) : (↑(a % b) : Int) = ↑a % ↑b := by
+  rfl
+
 init_grind_norm
   /- Pre theorems -/
   not_and not_or not_ite not_forall not_exists
@@ -114,19 +120,15 @@ init_grind_norm
   Bool.not_eq_true Bool.not_eq_false
   -- decide
   decide_eq_true_eq decide_not not_decide_eq_true
-  -- Nat LE
-  Nat.le_zero_eq
-  -- Nat/Int LT
-  Nat.lt_eq
-  -- Nat.succ
-  Nat.succ_eq_add_one
-  -- Nat op folding
+  -- Nat
+  Nat.le_zero_eq Nat.lt_eq Nat.succ_eq_add_one
   Nat.add_eq Nat.sub_eq Nat.mul_eq Nat.zero_eq Nat.le_eq
+  Nat.div_zero Nat.mod_zero
   -- Int
   Int.lt_eq
   Int.emod_neg Int.ediv_zero Int.emod_zero
   Int.natCast_add Int.natCast_mul Int.natCast_pow
-  Int.natCast_succ Int.natCast_zero
+  Int.natCast_succ Int.natCast_zero natCast_div natCast_mod
   -- GT GE
   ge_eq gt_eq
   -- Int op folding
diff --git a/tests/lean/run/grind_cutsat_nat_eq.lean b/tests/lean/run/grind_cutsat_nat_eq.lean
index ed5731f1ce..0bb2d7cdaf 100644
--- a/tests/lean/run/grind_cutsat_nat_eq.lean
+++ b/tests/lean/run/grind_cutsat_nat_eq.lean
@@ -47,3 +47,11 @@ example (x y : Nat) : x + y - x = y := by
 
 example (x y : Nat) : (x - y) - y = x - 2*y := by
   grind
+
+example (x : Nat) : x / 0 = 0 := by
+  grind
+
+example (x : Nat) : x % 0 = x := by
+  grind
+
+example (x : Nat) : x % 4 - x % 8 = 0 := by grind