From fc1e7a2ae9b96af027767aa0b7ed7f3b1166da5a Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 10 Dec 2025 02:42:52 +0000 Subject: [PATCH] feat: add Nat.cast_id and grind attribute to Int.cast_id MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds `Nat.cast_id` to `Init/Data/Nat/Lemmas.lean` with `simp`, `norm_cast`, and `grind =` attributes. Also adds `grind =` to the existing `Int.cast_id`. 🤖 Prepared with Claude Code Co-Authored-By: Claude --- src/Init/Data/Int/LemmasAux.lean | 2 +- src/Init/Data/Nat/Lemmas.lean | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/Init/Data/Int/LemmasAux.lean b/src/Init/Data/Int/LemmasAux.lean index 73f7359e61ad..a2285f1167c3 100644 --- a/src/Init/Data/Int/LemmasAux.lean +++ b/src/Init/Data/Int/LemmasAux.lean @@ -62,7 +62,7 @@ theorem natCast_succ_pos (n : Nat) : 0 < (n.succ : Int) := natCast_pos.2 n.succ_ @[simp high] theorem natCast_nonpos_iff {n : Nat} : (n : Int) ≤ 0 ↔ n = 0 := by omega -@[simp, norm_cast] theorem cast_id {n : Int} : Int.cast n = n := rfl +@[simp, norm_cast, grind =] theorem cast_id {n : Int} : Int.cast n = n := rfl @[simp] theorem ble'_eq_true (a b : Int) : (Int.ble' a b = true) = (a ≤ b) := by cases a <;> cases b <;> simp [Int.ble'] <;> omega diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index 76ca3d778226..3bfe7f193a6b 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -12,6 +12,7 @@ public import Init.Data.Nat.Log2 import all Init.Data.Nat.Log2 public import Init.Data.Nat.Power2 public import Init.Data.Nat.Mod +public import Init.Data.Cast import Init.TacticsExtra import Init.BinderPredicates @@ -1800,3 +1801,7 @@ instance decidableExistsFin (P : Fin n → Prop) [DecidablePred P] : Decidable ( decidable_of_iff (∃ k, k < n ∧ ((h: k < n) → P ⟨k, h⟩)) ⟨fun ⟨k, a⟩ => Exists.intro ⟨k, a.left⟩ (a.right a.left), fun ⟨i, e⟩ => Exists.intro i.val ⟨i.isLt, fun _ => e⟩⟩ + +/-! ### cast -/ + +@[simp, norm_cast, grind =] theorem cast_id (n : Nat) : Nat.cast n = n := rfl