From b9e888df4e48ca17f1019752f0d424da2fef7027 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 10 Dec 2025 02:56:47 -0800 Subject: [PATCH] fix: add `Nat.cast` normalizer missing case (#11580) 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 d4cfb667c8..69f65bdf03 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 a69d9776af..8eec03c522 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