From e897478d2c3d1e96fb3ef0986982a7bedc8122d0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 10 Dec 2025 11:40:02 +0100 Subject: [PATCH] fix: add `Nat.cast` normalizer missing case This PR adds a missing `Nat.cast` missing normalization rule for `grind`. Example: ```lean example (n : Nat) : Nat.cast n = n := by grind ``` --- src/Init/Grind/Norm.lean | 3 ++- tests/lean/run/grind_natCast.lean | 6 ++++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/Init/Grind/Norm.lean b/src/Init/Grind/Norm.lean index d4cfb667c879..69f65bdf036b 100644 --- a/src/Init/Grind/Norm.lean +++ b/src/Init/Grind/Norm.lean @@ -82,6 +82,7 @@ theorem natCast_mod (a b : Nat) : (NatCast.natCast (a % b) : Int) = (NatCast.nat theorem natCast_add (a b : Nat) : (NatCast.natCast (a + b : Nat) : Int) = (NatCast.natCast a : Int) + (NatCast.natCast b : Int) := rfl theorem natCast_mul (a b : Nat) : (NatCast.natCast (a * b : Nat) : Int) = (NatCast.natCast a : Int) * (NatCast.natCast b : Int) := rfl theorem natCast_pow (a b : Nat) : (NatCast.natCast (a ^ b : Nat) : Int) = (NatCast.natCast a : Int) ^ b := by simp +theorem natCast_id (a : Nat) : NatCast.natCast a = a := rfl theorem Nat.pow_one (a : Nat) : a ^ 1 = a := by simp @@ -184,7 +185,7 @@ init_grind_norm Int.ediv_zero Int.emod_zero Int.ediv_one Int.emod_one Int.negSucc_eq - natCast_div natCast_mod + natCast_div natCast_mod natCast_id natCast_add natCast_mul natCast_pow Int.one_pow Int.pow_zero Int.pow_one diff --git a/tests/lean/run/grind_natCast.lean b/tests/lean/run/grind_natCast.lean index a69d9776af4a..8eec03c52228 100644 --- a/tests/lean/run/grind_natCast.lean +++ b/tests/lean/run/grind_natCast.lean @@ -5,3 +5,9 @@ example (x : Nat) : NatCast.natCast x ≥ 0 := by grind example (x : Nat) : x ≥ (-1 : Int) := by grind example (x : Nat) : Int.ofNat x ≥ (-1 : Int) := by grind example (x : Nat) : NatCast.natCast x ≥ -1 := by grind + +example (n : Nat) : Nat.cast n = n := by + grind + +example (n m a : Nat) : n = m → Nat.cast n - a = m - a := by + grind