From d9eed723efec75c987172c5e3eec0438156c697d Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Tue, 22 Apr 2025 10:42:29 +0200 Subject: [PATCH 1/3] Code --- src/Init/Data/BitVec/Bitblast.lean | 6 +-- src/Init/Data/BitVec/Lemmas.lean | 12 ++--- src/Init/Data/Int/Cooper.lean | 6 +-- src/Init/Data/Int/DivMod/Basic.lean | 5 +- src/Init/Data/Int/DivMod/Bootstrap.lean | 11 ++-- src/Init/Data/Int/DivMod/Lemmas.lean | 8 +-- src/Init/Data/Int/Lemmas.lean | 65 +++++++++++++----------- src/Init/Data/Int/OfNat.lean | 2 +- src/Init/Data/Int/Order.lean | 16 +++--- src/Init/Omega/Int.lean | 6 +-- src/Lean/Elab/Tactic/Omega/Frontend.lean | 6 +-- 11 files changed, 74 insertions(+), 69 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 6db9718bfbcd..a2ed6e681b66 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1358,7 +1358,7 @@ theorem negOverflow_eq {w : Nat} (x : BitVec w) : rcases w with _|w · simp [toInt_of_zero_length, Int.min_eq_right] · suffices - 2 ^ w = (intMin (w + 1)).toInt by simp [beq_eq_decide_eq, ← toInt_inj, this] - simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod, Int.neg_inj] + simp only [toInt_intMin, Nat.add_one_sub_one, Int.natCast_emod, Int.neg_inj] rw_mod_cast [Nat.mod_eq_of_lt (by simp [Nat.pow_lt_pow_succ])] /-- @@ -1574,7 +1574,7 @@ theorem sdiv_ne_intMin_of_ne_intMin {x y : BitVec w} (h : x ≠ intMin w) : theorem toInt_eq_neg_toNat_neg_of_msb_true {x : BitVec w} (h : x.msb = true) : x.toInt = -((-x).toNat) := by - simp only [toInt_eq_msb_cond, h, ↓reduceIte, toNat_neg, Int.ofNat_emod] + simp only [toInt_eq_msb_cond, h, ↓reduceIte, toNat_neg, Int.natCast_emod] norm_cast rw [Nat.mod_eq_of_lt] · omega @@ -1669,7 +1669,7 @@ theorem toInt_sdiv_of_ne_or_ne (a b : BitVec w) (h : a ≠ intMin w ∨ b ≠ -1 (a.sdiv b).toInt = -((-a).toNat / b.toNat) := by simp only [sdiv_eq, ha, hb, udiv_eq] rw [toInt_eq_neg_toNat_neg_of_nonpos] - · rw [neg_neg, toNat_udiv, toNat_neg, Int.ofNat_emod, Int.neg_inj] + · rw [neg_neg, toNat_udiv, toNat_neg, Int.natCast_emod, Int.neg_inj] norm_cast · rw [neg_eq_zero_iff] by_cases h' : -a / b = 0#w diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 25d68ea1ca27..3db766f82fc1 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -620,10 +620,10 @@ theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := simp only [toInt_eq_toNat_cond] split next g => - rw [Int.bmod_pos] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel] + rw [Int.bmod_pos] <;> simp only [←Int.natCast_emod, toNat_mod_cancel] omega next g => - rw [Int.bmod_neg] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel] + rw [Int.bmod_neg] <;> simp only [←Int.natCast_emod, toNat_mod_cancel] omega theorem toInt_neg_of_msb_true {x : BitVec w} (h : x.msb = true) : x.toInt < 0 := by @@ -639,7 +639,7 @@ theorem toInt_nonneg_of_msb_false {x : BitVec w} (h : x.msb = false) : 0 ≤ x.t @[simp] theorem toInt_one_of_lt {w : Nat} (h : 1 < w) : (1#w).toInt = 1 := by rw [toInt_eq_msb_cond] simp only [msb_one, show w ≠ 1 by omega, decide_false, Bool.false_eq_true, ↓reduceIte, - toNat_ofNat, Int.ofNat_emod] + toNat_ofNat, Int.natCast_emod] norm_cast apply Nat.mod_eq_of_lt apply Nat.one_lt_two_pow (by omega) @@ -2548,7 +2548,7 @@ where simp [getElem_signExtend, Nat.le_sub_one_of_lt hv] omega have H : 2^w ≤ 2^v := Nat.pow_le_pow_right (by omega) (by omega) - simp only [this, toNat_setWidth, Int.natCast_add, Int.ofNat_emod, Int.natCast_mul] + simp only [this, toNat_setWidth, Int.natCast_add, Int.natCast_emod, Int.natCast_mul] by_cases h : x.msb <;> norm_cast <;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H), -Int.natCast_pow] @@ -3871,7 +3871,7 @@ theorem le_zero_iff {x : BitVec w} : x ≤ 0#w ↔ x = 0#w := by theorem lt_one_iff {x : BitVec w} (h : 0 < w) : x < 1#w ↔ x = 0#w := by constructor · intro h₂ - rw [lt_def, toNat_ofNat, ← Int.ofNat_lt, Int.ofNat_emod, Int.ofNat_one, Int.natCast_pow, + rw [lt_def, toNat_ofNat, ← Int.ofNat_lt, Int.natCast_emod, Int.ofNat_one, Int.natCast_pow, Int.ofNat_two, @Int.emod_eq_of_lt 1 (2^w) (by omega) (by omega)] at h₂ simp [toNat_eq, show x.toNat = 0 by omega] · simp_all @@ -5056,7 +5056,7 @@ theorem toInt_intMin_le (x : BitVec w) : cases w case zero => simp [toInt_intMin, @of_length_zero x] case succ w => - simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod] + simp only [toInt_intMin, Nat.add_one_sub_one, Int.natCast_emod] have : 0 < 2 ^ w := Nat.two_pow_pos w rw [Int.emod_eq_of_lt (by omega) (by omega)] rw [BitVec.toInt_eq_toNat_bmod] diff --git a/src/Init/Data/Int/Cooper.lean b/src/Init/Data/Int/Cooper.lean index 4afc3286f6bc..e7700fbe236c 100644 --- a/src/Init/Data/Int/Cooper.lean +++ b/src/Init/Data/Int/Cooper.lean @@ -94,7 +94,7 @@ def resolve_left' (a c d p x : Int) (h₁ : p ≤ a * x) : Nat := (add_of_le h @[simp] theorem resolve_left_eq (a c d p x : Int) (h₁ : p ≤ a * x) : resolve_left a c d p x = resolve_left' a c d p x h₁ := by - simp only [resolve_left, resolve_left', add_of_le, ofNat_emod, ofNat_toNat] + simp only [resolve_left, resolve_left', add_of_le, natCast_emod, ofNat_toNat] rw [Int.max_eq_left] omega @@ -129,14 +129,14 @@ theorem resolve_left_dvd₁ (a c d p x : Int) (h₁ : p ≤ a * x) : a ∣ resolve_left a c d p x + p := by simp only [h₁, resolve_left_eq, resolve_left'] obtain ⟨k', w⟩ := add_of_le h₁ - exact Int.ofNat_emod _ _ ▸ dvd_emod_add_of_dvd_add (x := k') ⟨x, by rw [w, Int.add_comm]⟩ (dvd_lcm_left ..) + exact Int.natCast_emod _ _ ▸ dvd_emod_add_of_dvd_add (x := k') ⟨x, by rw [w, Int.add_comm]⟩ (dvd_lcm_left ..) theorem resolve_left_dvd₂ (a c d p x : Int) (h₁ : p ≤ a * x) (h₃ : d ∣ c * x + s) : a * d ∣ c * resolve_left a c d p x + c * p + a * s := by simp only [h₁, resolve_left_eq, resolve_left'] obtain ⟨k', w⟩ := add_of_le h₁ - simp only [Int.add_assoc, ofNat_emod] + simp only [Int.add_assoc, natCast_emod] apply dvd_mul_emod_add_of_dvd_mul_add · obtain ⟨z, r⟩ := h₃ refine ⟨z, ?_⟩ diff --git a/src/Init/Data/Int/DivMod/Basic.lean b/src/Init/Data/Int/DivMod/Basic.lean index e7e1de68d884..401bf736b9ca 100644 --- a/src/Init/Data/Int/DivMod/Basic.lean +++ b/src/Init/Data/Int/DivMod/Basic.lean @@ -112,7 +112,10 @@ because mathematical reasoning tends to be easier. instance : Mod Int where mod := Int.emod -@[norm_cast] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl +@[simp, norm_cast] theorem natCast_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl + +@[deprecated natCast_ediv (since := "2025-04-17")] +theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := natCast_ediv m n theorem ofNat_ediv_ofNat {a b : Nat} : (↑a / ↑b : Int) = (a / b : Nat) := rfl @[norm_cast] diff --git a/src/Init/Data/Int/DivMod/Bootstrap.lean b/src/Init/Data/Int/DivMod/Bootstrap.lean index 6cade6b73a79..b08723b0992b 100644 --- a/src/Init/Data/Int/DivMod/Bootstrap.lean +++ b/src/Init/Data/Int/DivMod/Bootstrap.lean @@ -34,7 +34,7 @@ protected theorem dvd_trans : ∀ {a b c : Int}, a ∣ b → b ∣ c → a ∣ c | _, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => Exists.intro (d * e) (by rw [Int.mul_assoc]) @[norm_cast] theorem ofNat_dvd {m n : Nat} : (↑m : Int) ∣ ↑n ↔ m ∣ n := by - refine ⟨fun ⟨a, ae⟩ => ?_, fun ⟨k, e⟩ => ⟨k, by rw [e, Int.ofNat_mul]⟩⟩ + refine ⟨fun ⟨a, ae⟩ => ?_, fun ⟨k, e⟩ => ⟨k, by rw [e, Int.natCast_mul]⟩⟩ match Int.le_total a 0 with | .inl h => have := ae.symm ▸ Int.mul_nonpos_of_nonneg_of_nonpos (ofNat_zero_le _) h @@ -89,7 +89,10 @@ theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) ∣ z ↔ n ∣ z.natA /-! ### ofNat mod -/ -@[simp, norm_cast] theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := rfl +@[simp, norm_cast] theorem natCast_emod (m n : Nat) : (↑(m % n) : Int) = m % n := rfl + +@[deprecated natCast_emod (since := "2025-04-17")] +theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := natCast_emod m n /-! ### mod definitions -/ @@ -103,7 +106,7 @@ theorem emod_add_ediv : ∀ a b : Int, a % b + b * (a / b) = a | -[m+1], -[n+1] => aux m n.succ where aux (m n : Nat) : n - (m % n + 1) - (n * (m / n) + n) = -[m+1] := by - rw [← ofNat_emod, ← ofNat_ediv, ← Int.sub_sub, negSucc_eq, Int.sub_sub n, + rw [← natCast_emod, ← natCast_ediv, ← Int.sub_sub, negSucc_eq, Int.sub_sub n, ← Int.neg_neg (_-_), Int.neg_sub, Int.sub_sub_self, Int.add_right_comm] exact congrArg (fun x => -(ofNat x + 1)) (Nat.mod_add_div ..) @@ -184,7 +187,7 @@ theorem ediv_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : 0 ≤ a / b ↔ 0 ≤ a rw [Int.div_def] match b, h with | Int.ofNat (b+1), _ => - rcases a with ⟨a⟩ <;> simp [Int.ediv] + rcases a with ⟨a⟩ <;> simp [Int.ediv, -natCast_ediv] @[deprecated ediv_nonneg_iff_of_pos (since := "2025-02-28")] abbrev div_nonneg_iff_of_pos := @ediv_nonneg_iff_of_pos diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean index 2a8e26c6223c..7e047836439c 100644 --- a/src/Init/Data/Int/DivMod/Lemmas.lean +++ b/src/Init/Data/Int/DivMod/Lemmas.lean @@ -604,8 +604,6 @@ theorem sign_ediv (a b : Int) : sign (a / b) = if 0 ≤ a ∧ a < b.natAbs then | negSucc a => norm_cast -@[simp, norm_cast] theorem natCast_ediv (m n : Nat) : ((m / n : Nat) : Int) = m / n := rfl - /-! ### emod -/ theorem mod_def' (m n : Int) : m % n = emod m n := rfl @@ -714,8 +712,6 @@ theorem one_emod {b : Int} : 1 % b = if b.natAbs = 1 then 0 else 1 := by @[simp] theorem neg_emod_two (i : Int) : -i % 2 = i % 2 := by omega -@[simp, norm_cast] theorem natCast_emod (m n : Nat) : (↑(m % n) : Int) = ↑m % ↑n := rfl - /-! ### properties of `/` and `%` -/ theorem mul_ediv_cancel_of_dvd {a b : Int} (H : b ∣ a) : b * (a / b) = a := @@ -1325,7 +1321,7 @@ theorem lt_tmod_of_pos (a : Int) {b : Int} (H : 0 < b) : -b < tmod a b := match a, b, eq_succ_of_zero_lt H with | ofNat _, _, ⟨n, rfl⟩ => by rw [ofNat_eq_coe, ← Int.natCast_succ, ← ofNat_tmod]; omega | -[a+1], _, ⟨n, rfl⟩ => by - rw [negSucc_eq, neg_tmod, ← Int.natCast_succ, ← Int.natCast_succ, ← ofNat_tmod] + rw [negSucc_eq, neg_tmod, ← Int.natCast_add_one, ← Int.natCast_add_one, ← ofNat_tmod] have : (a + 1) % (n + 1) < n + 1 := Nat.mod_lt _ (Nat.zero_lt_succ n) omega @@ -2017,7 +2013,7 @@ theorem neg_fdiv {a b : Int} : (-a).fdiv b = -(a.fdiv b) - if b = 0 ∨ b ∣ a rw [neg_negSucc, ← negSucc_eq] | -[a+1], -[b+1] => unfold fdiv - simp only [ofNat_eq_coe, ofNat_ediv, Nat.succ_eq_add_one, Int.natCast_add, cast_ofNat_Int] + simp only [ofNat_eq_coe, natCast_ediv, Nat.succ_eq_add_one, Int.natCast_add, cast_ofNat_Int] rw [neg_negSucc, neg_negSucc] simp diff --git a/src/Init/Data/Int/Lemmas.lean b/src/Init/Data/Int/Lemmas.lean index e3b75a596284..84ae8d108341 100644 --- a/src/Init/Data/Int/Lemmas.lean +++ b/src/Init/Data/Int/Lemmas.lean @@ -25,9 +25,17 @@ theorem subNatNat_of_sub_eq_succ {m n k : Nat} (h : n - m = succ k) : subNatNat @[simp] protected theorem neg_zero : -(0:Int) = 0 := rfl -@[norm_cast] theorem ofNat_add (n m : Nat) : (↑(n + m) : Int) = n + m := rfl -@[norm_cast] theorem ofNat_mul (n m : Nat) : (↑(n * m) : Int) = n * m := rfl -@[norm_cast] theorem ofNat_succ (n : Nat) : (succ n : Int) = n + 1 := rfl +@[simp, norm_cast] theorem natCast_add (n m : Nat) : (↑(n + m) : Int) = n + m := rfl +@[simp, norm_cast] theorem natCast_mul (n m : Nat) : (↑(n * m) : Int) = n * m := rfl +@[norm_cast] theorem natCast_succ (n : Nat) : (succ n : Int) = n + 1 := rfl +@[norm_cast] theorem natCast_add_one (n : Nat) : ((n + 1 : Nat) : Int) = n + 1 := rfl + +@[deprecated natCast_add (since := "2025-04-17")] +theorem ofNat_add (n m : Nat) : (↑(n + m) : Int) = n + m := rfl +@[deprecated natCast_mul (since := "2025-04-17")] +theorem ofNat_mul (n m : Nat) : (↑(n * m) : Int) = n * m := rfl +@[deprecated natCast_succ (since := "2025-04-17")] +theorem ofNat_succ (n : Nat) : (succ n : Int) = n + 1 := rfl theorem neg_ofNat_zero : -((0 : Nat) : Int) = 0 := rfl theorem neg_ofNat_succ (n : Nat) : -(succ n : Int) = -[n+1] := rfl @@ -157,7 +165,7 @@ theorem subNatNat_add (m n k : Nat) : subNatNat (m + n) k = m + subNatNat n k := conv => lhs; rw [← Nat.sub_add_cancel (Nat.le_of_lt h')] apply subNatNat_add_add | inr h' => simp [subNatNat_of_le h', - subNatNat_of_le (Nat.le_trans h' (le_add_left ..)), Nat.add_sub_assoc h'] + subNatNat_of_le (Nat.le_trans h' (le_add_left ..)), Nat.add_sub_assoc h', -natCast_add] theorem subNatNat_add_negSucc (m n k : Nat) : subNatNat m n + -[k+1] = subNatNat m (n + succ k) := by @@ -184,7 +192,7 @@ theorem subNatNat_self : ∀ n, subNatNat n n = 0 /- addition -/ protected theorem add_comm : ∀ a b : Int, a + b = b + a - | ofNat n, ofNat m => by simp [Nat.add_comm] + | ofNat n, ofNat m => by simp [Nat.add_comm, -natCast_add] | ofNat _, -[_+1] => rfl | -[_+1], ofNat _ => rfl | -[_+1], -[_+1] => by simp [Nat.add_comm] @@ -218,8 +226,8 @@ protected theorem add_assoc : ∀ a b c : Int, a + b + c = a + (b + c) simp [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc] where aux1 (m n : Nat) : ∀ c : Int, m + n + c = m + (n + c) - | (k:Nat) => by simp [Nat.add_assoc] - | -[k+1] => by simp [subNatNat_add] + | (k:Nat) => by simp [Nat.add_assoc, -natCast_add] + | -[k+1] => by simp [subNatNat_add, -natCast_add] aux2 (m n k : Nat) : -[m+1] + -[n+1] + k = -[m+1] + (-[n+1] + k) := by simp rw [Int.add_comm, subNatNat_add_negSucc] @@ -236,8 +244,8 @@ protected theorem add_right_comm (a b c : Int) : a + b + c = a + c + b := by protected theorem add_left_neg : ∀ a : Int, -a + a = 0 | 0 => rfl - | succ m => by simp [neg_ofNat_succ] - | -[m+1] => by simp [neg_negSucc] + | succ m => by simp [neg_ofNat_succ, -natCast_add] + | -[m+1] => by simp [neg_negSucc, -natCast_add] protected theorem add_right_neg (a : Int) : a + -a = 0 := by rw [Int.add_comm, Int.add_left_neg] @@ -283,7 +291,7 @@ theorem wlog_sign {P : Int → Prop} (inv : ∀ i, P i ↔ P (-i)) (w : ∀ n : cases i with | ofNat n => exact w n | negSucc n => - rw [negSucc_eq, ← inv, ← ofNat_succ] + rw [negSucc_eq, ← inv, ← natCast_succ] apply w /- ## subtraction -/ @@ -342,10 +350,10 @@ theorem negSucc_coe' (n : Nat) : -[n+1] = -↑n - 1 := by protected theorem subNatNat_eq_coe {m n : Nat} : subNatNat m n = ↑m - ↑n := by apply subNatNat_elim m n fun m n i => i = m - n · intros i n - rw [Int.ofNat_add, Int.sub_eq_add_neg, Int.add_assoc, Int.add_left_comm, + rw [Int.natCast_add, Int.sub_eq_add_neg, Int.add_assoc, Int.add_left_comm, Int.add_right_neg, Int.add_zero] · intros i n - simp only [negSucc_eq, ofNat_add, ofNat_one, Int.sub_eq_add_neg, Int.neg_add, ← Int.add_assoc] + simp only [negSucc_eq, natCast_add, ofNat_one, Int.sub_eq_add_neg, Int.neg_add, ← Int.add_assoc] rw [Int.add_neg_eq_sub (a := n), ← ofNat_sub, Nat.sub_self, ofNat_zero, Int.zero_add] apply Nat.le_refl @@ -410,7 +418,7 @@ theorem negSucc_mul_ofNat (m n : Nat) : -[m+1] * n = -↑(succ m * n) := rfl theorem negSucc_mul_negSucc (m n : Nat) : -[m+1] * -[n+1] = succ m * succ n := rfl protected theorem mul_comm (a b : Int) : a * b = b * a := by - cases a <;> cases b <;> simp [Nat.mul_comm] + cases a <;> cases b <;> simp [Nat.mul_comm, -natCast_mul] instance : Std.Commutative (α := Int) (· * ·) := ⟨Int.mul_comm⟩ theorem ofNat_mul_negOfNat (m n : Nat) : (m : Nat) * negOfNat n = negOfNat (m * n) := by @@ -427,7 +435,8 @@ theorem negOfNat_mul_negSucc (m n : Nat) : negOfNat n * -[m+1] = ofNat (n * succ protected theorem mul_assoc (a b c : Int) : a * b * c = a * (b * c) := by cases a <;> cases b <;> cases c <;> - simp [Nat.mul_assoc, ofNat_mul_negOfNat, negOfNat_mul_ofNat, negSucc_mul_negOfNat, negOfNat_mul_negSucc] + simp [Nat.mul_assoc, ofNat_mul_negOfNat, negOfNat_mul_ofNat, negSucc_mul_negOfNat, + negOfNat_mul_negSucc, -natCast_mul] instance : Std.Associative (α := Int) (· * ·) := ⟨Int.mul_assoc⟩ @@ -450,12 +459,14 @@ theorem ofNat_mul_subNatNat (m n k : Nat) : | succ m => cases n.lt_or_ge k with | inl h => have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m) - simp [subNatNat_of_lt h, subNatNat_of_lt h'] + simp only [subNatNat_of_lt h, pred_eq_sub_one, ofNat_mul_negSucc', succ_eq_add_one, + subNatNat_of_lt h'] rw [sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h), ← neg_ofNat_succ, Nat.mul_sub_left_distrib, ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]; rfl | inr h => have h' : succ m * k ≤ succ m * n := Nat.mul_le_mul_left _ h - simp [subNatNat_of_le h, subNatNat_of_le h', Nat.mul_sub_left_distrib] + simp [subNatNat_of_le h, subNatNat_of_le h', Nat.mul_sub_left_distrib, + -natCast_mul, -natCast_add] theorem negOfNat_add (m n : Nat) : negOfNat m + negOfNat n = negOfNat (m + n) := by cases m <;> cases n <;> simp [Nat.succ_add] <;> rfl @@ -476,17 +487,17 @@ theorem negSucc_mul_subNatNat (m n k : Nat) : attribute [local simp] ofNat_mul_subNatNat negOfNat_add negSucc_mul_subNatNat in protected theorem mul_add : ∀ a b c : Int, a * (b + c) = a * b + a * c - | (m:Nat), (n:Nat), (k:Nat) => by simp [Nat.left_distrib] + | (m:Nat), (n:Nat), (k:Nat) => by simp [Nat.left_distrib, -natCast_add, -natCast_mul] | (m:Nat), (n:Nat), -[k+1] => by - simp [negOfNat_eq_subNatNat_zero]; rw [← subNatNat_add]; rfl + simp [negOfNat_eq_subNatNat_zero, -natCast_mul]; rw [← subNatNat_add]; rfl | (m:Nat), -[n+1], (k:Nat) => by - simp [negOfNat_eq_subNatNat_zero]; rw [Int.add_comm, ← subNatNat_add]; rfl + simp [negOfNat_eq_subNatNat_zero, -natCast_mul]; rw [Int.add_comm, ← subNatNat_add]; rfl | (m:Nat), -[n+1], -[k+1] => by simp [← Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc] - | -[m+1], (n:Nat), (k:Nat) => by simp [Nat.mul_comm]; rw [← Nat.right_distrib, Nat.mul_comm] + | -[m+1], (n:Nat), (k:Nat) => by simp [Nat.mul_comm, -natCast_mul, -natCast_add]; rw [← Nat.right_distrib, Nat.mul_comm] | -[m+1], (n:Nat), -[k+1] => by - simp [negOfNat_eq_subNatNat_zero]; rw [Int.add_comm, ← subNatNat_add]; rfl - | -[m+1], -[n+1], (k:Nat) => by simp [negOfNat_eq_subNatNat_zero]; rw [← subNatNat_add]; rfl - | -[m+1], -[n+1], -[k+1] => by simp [← Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc] + simp [negOfNat_eq_subNatNat_zero, -natCast_add, -natCast_mul]; rw [Int.add_comm, ← subNatNat_add]; rfl + | -[m+1], -[n+1], (k:Nat) => by simp [negOfNat_eq_subNatNat_zero, -natCast_add, -natCast_mul]; rw [← subNatNat_add]; rfl + | -[m+1], -[n+1], -[k+1] => by simp [← Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc, -natCast_mul] protected theorem add_mul (a b c : Int) : (a + b) * c = a * c + b * c := by simp [Int.mul_comm, Int.mul_add] @@ -583,12 +594,4 @@ protected theorem natCast_zero : ((0 : Nat) : Int) = (0 : Int) := rfl protected theorem natCast_one : ((1 : Nat) : Int) = (1 : Int) := rfl -@[simp, norm_cast] protected theorem natCast_add (a b : Nat) : ((a + b : Nat) : Int) = (a : Int) + (b : Int) := by - rfl - -protected theorem natCast_succ (n : Nat) : ((n + 1 : Nat) : Int) = (n : Int) + 1 := rfl - -@[simp] protected theorem natCast_mul (a b : Nat) : ((a * b : Nat) : Int) = (a : Int) * (b : Int) := by - simp - end Int diff --git a/src/Init/Data/Int/OfNat.lean b/src/Init/Data/Int/OfNat.lean index fee57a5f0b4a..4626f3c82bfc 100644 --- a/src/Init/Data/Int/OfNat.lean +++ b/src/Init/Data/Int/OfNat.lean @@ -48,7 +48,7 @@ def Expr.denoteAsInt (ctx : Context) : Expr → Int | .mod a b => Int.emod (denoteAsInt ctx a) (denoteAsInt ctx b) theorem Expr.denoteAsInt_eq (ctx : Context) (e : Expr) : e.denoteAsInt ctx = e.denote ctx := by - induction e <;> simp [denote, denoteAsInt, Int.ofNat_ediv, *] <;> rfl + induction e <;> simp [denote, denoteAsInt, Int.natCast_ediv, *] <;> rfl theorem Expr.eq_denoteAsInt (ctx : Context) (e : Expr) : e.denote ctx = e.denoteAsInt ctx := by apply Eq.symm; apply denoteAsInt_eq diff --git a/src/Init/Data/Int/Order.lean b/src/Init/Data/Int/Order.lean index baae77bfa65d..64c1410cc026 100644 --- a/src/Init/Data/Int/Order.lean +++ b/src/Init/Data/Int/Order.lean @@ -51,7 +51,7 @@ protected theorem le_total (a b : Int) : a ≤ b ∨ b ≤ a := @[simp, norm_cast] theorem ofNat_le {m n : Nat} : (↑m : Int) ≤ ↑n ↔ m ≤ n := ⟨fun h => let ⟨k, hk⟩ := le.dest h - Nat.le.intro <| Int.ofNat.inj <| (Int.ofNat_add m k).trans hk, + Nat.le.intro <| Int.ofNat.inj <| (Int.natCast_add m k).trans hk, fun h => let ⟨k, (hk : m + k = n)⟩ := Nat.le.dest h le.intro k (by rw [← hk]; rfl)⟩ @@ -75,7 +75,7 @@ theorem lt.dest {a b : Int} (h : a < b) : ∃ n : Nat, a + Nat.succ n = b := let ⟨n, h⟩ := le.dest h; ⟨n, by rwa [Int.add_comm, Int.add_left_comm] at h⟩ @[simp, norm_cast] theorem ofNat_lt {n m : Nat} : (↑n : Int) < ↑m ↔ n < m := by - rw [lt_iff_add_one_le, ← ofNat_succ, ofNat_le]; rfl + rw [lt_iff_add_one_le, ← natCast_succ, ofNat_le]; rfl @[simp, norm_cast] theorem ofNat_pos {n : Nat} : 0 < (↑n : Int) ↔ 0 < n := ofNat_lt @@ -93,11 +93,11 @@ protected theorem ge_of_eq {a b : Int} (hab : a = b) : b ≤ a := Int.le_of_eq h protected theorem le_trans {a b c : Int} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c := let ⟨n, hn⟩ := le.dest h₁; let ⟨m, hm⟩ := le.dest h₂ - le.intro (n + m) <| by rw [← hm, ← hn, Int.add_assoc, ofNat_add] + le.intro (n + m) <| by rw [← hm, ← hn, Int.add_assoc, natCast_add] protected theorem le_antisymm {a b : Int} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b := by let ⟨n, hn⟩ := le.dest h₁; let ⟨m, hm⟩ := le.dest h₂ - have := hn; rw [← hm, Int.add_assoc, ← ofNat_add] at this + have := hn; rw [← hm, Int.add_assoc, ← natCast_add] at this have := Int.ofNat.inj <| Int.add_left_cancel <| this.trans (Int.add_zero _).symm rw [← hn, Nat.eq_zero_of_add_eq_zero_left this, ofNat_zero, Int.add_zero a] @@ -475,7 +475,7 @@ instance : Std.IdempotentOp (α := Int) max := ⟨Int.max_self⟩ protected theorem mul_nonneg {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b := by let ⟨n, hn⟩ := eq_ofNat_of_zero_le ha let ⟨m, hm⟩ := eq_ofNat_of_zero_le hb - rw [hn, hm, ← ofNat_mul]; apply ofNat_nonneg + rw [hn, hm, ← natCast_mul]; apply ofNat_nonneg protected theorem mul_pos {a b : Int} (ha : 0 < a) (hb : 0 < b) : 0 < a * b := by let ⟨n, hn⟩ := eq_succ_of_zero_lt ha @@ -673,7 +673,7 @@ theorem toNat_add_nat {a : Int} (ha : 0 ≤ a) (n : Nat) : (a + n).toNat = a.toN @[simp] theorem pred_toNat : ∀ i : Int, (i - 1).toNat = i.toNat - 1 | 0 => rfl - | (_+1:Nat) => by simp [ofNat_add] + | (_+1:Nat) => by simp [natCast_add] | -[_+1] => rfl theorem toNat_sub_toNat_neg : ∀ n : Int, ↑n.toNat - ↑(-n).toNat = n @@ -1306,7 +1306,7 @@ theorem natAbs_mul_natAbs_eq {a b : Int} {c : Nat} (h : a * b = (c : Int)) : a.natAbs * b.natAbs = c := by rw [← natAbs_mul, h, natAbs.eq_def] @[simp] theorem natAbs_mul_self' (a : Int) : (natAbs a * natAbs a : Int) = a * a := by - rw [← Int.ofNat_mul, natAbs_mul_self] + rw [← Int.natCast_mul, natAbs_mul_self] theorem natAbs_eq_iff {a : Int} {n : Nat} : a.natAbs = n ↔ a = n ∨ a = -↑n := by rw [← Int.natAbs_eq_natAbs_iff, Int.natAbs_natCast] @@ -1314,7 +1314,7 @@ theorem natAbs_eq_iff {a : Int} {n : Nat} : a.natAbs = n ↔ a = n ∨ a = -↑n theorem natAbs_add_le (a b : Int) : natAbs (a + b) ≤ natAbs a + natAbs b := by suffices ∀ a b : Nat, natAbs (subNatNat a b.succ) ≤ (a + b).succ by match a, b with - | (a:Nat), (b:Nat) => rw [← ofNat_add, natAbs_natCast]; apply Nat.le_refl + | (a:Nat), (b:Nat) => rw [← natCast_add, natAbs_natCast]; apply Nat.le_refl | (a:Nat), -[b+1] => rw [natAbs_natCast, natAbs_negSucc]; apply this | -[a+1], (b:Nat) => rw [natAbs_negSucc, natAbs_natCast, Nat.succ_add, Nat.add_comm a b]; apply this diff --git a/src/Init/Omega/Int.lean b/src/Init/Omega/Int.lean index 97d5fd151b01..423de2e87f5b 100644 --- a/src/Init/Omega/Int.lean +++ b/src/Init/Omega/Int.lean @@ -25,7 +25,7 @@ namespace Int theorem ofNat_pow (a b : Nat) : ((a ^ b : Nat) : Int) = (a : Int) ^ b := by induction b with | zero => rfl - | succ b ih => rw [Nat.pow_succ, Int.ofNat_mul, ih]; rfl + | succ b ih => rw [Nat.pow_succ, Int.natCast_mul, ih]; rfl theorem pos_pow_of_pos (a : Int) (b : Nat) (h : 0 < a) : 0 < a ^ b := by rw [Int.eq_natAbs_of_nonneg (Int.le_of_lt h), ← Int.ofNat_zero, ← Int.ofNat_pow, Int.ofNat_lt] @@ -50,7 +50,7 @@ theorem ofNat_shiftLeft_eq {x y : Nat} : (x <<< y : Int) = (x : Int) * (2 ^ y : simp [Nat.shiftLeft_eq] theorem ofNat_shiftRight_eq_div_pow {x y : Nat} : (x >>> y : Int) = (x : Int) / (2 ^ y : Nat) := by - simp only [Nat.shiftRight_eq_div_pow, Int.ofNat_ediv] + simp only [Nat.shiftRight_eq_div_pow, Int.natCast_ediv] theorem emod_ofNat_nonneg {x : Nat} {y : Int} : 0 ≤ (x : Int) % y := Int.ofNat_zero_le _ @@ -86,7 +86,7 @@ theorem lt_of_gt {x y : Int} (h : x > y) : y < x := gt_iff_lt.mp h theorem le_of_ge {x y : Int} (h : x ≥ y) : y ≤ x := ge_iff_le.mp h theorem ofNat_mul_nonneg {a b : Nat} : 0 ≤ (a : Int) * b := by - rw [← Int.ofNat_mul] + rw [← Int.natCast_mul] exact Int.ofNat_zero_le (a * b) theorem ofNat_sub_eq_zero {b a : Nat} (h : ¬ b ≤ a) : ((a - b : Nat) : Int) = 0 := diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean index 618245b9d904..1b8c83e0c1f8 100644 --- a/src/Lean/Elab/Tactic/Omega/Frontend.lean +++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean @@ -255,14 +255,14 @@ where mkAtomLinearCombo e | _ => match n.getAppFnArgs with | (``Nat.succ, #[n]) => rewrite e (.app (.const ``Int.ofNat_succ []) n) - | (``HAdd.hAdd, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_add []) a b) + | (``HAdd.hAdd, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.natCast_add []) a b) | (``HMul.hMul, #[_, _, _, _, a, b]) => let (lc, prf, r) ← rewrite e (mkApp2 (.const ``Int.ofNat_mul []) a b) -- Add the fact that the multiplication is non-negative. pure (lc, prf, r.insert (mkApp2 (.const ``Int.ofNat_mul_nonneg []) a b)) - | (``HDiv.hDiv, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_ediv []) a b) + | (``HDiv.hDiv, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.natCast_ediv []) a b) | (``OfNat.ofNat, #[_, n, _]) => rewrite e (.app (.const ``Int.natCast_ofNat []) n) - | (``HMod.hMod, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_emod []) a b) + | (``HMod.hMod, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.natCast_emod []) a b) | (``HSub.hSub, #[_, _, _, _, mkApp6 (.const ``HSub.hSub _) _ _ _ _ a b, c]) => rewrite e (mkApp3 (.const ``Int.ofNat_sub_sub []) a b c) | (``HPow.hPow, #[_, _, _, _, a, b]) => From d1d363dcd5c4ed91c28a0fcd0fa2bf8fceff2630 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Tue, 22 Apr 2025 14:54:29 +0200 Subject: [PATCH 2/3] Fix --- src/Init/Grind/CommRing/Basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Init/Grind/CommRing/Basic.lean b/src/Init/Grind/CommRing/Basic.lean index f332b4ca782b..e1f05d8908fa 100644 --- a/src/Init/Grind/CommRing/Basic.lean +++ b/src/Init/Grind/CommRing/Basic.lean @@ -151,9 +151,9 @@ theorem intCast_one : ((1 : Int) : α) = 1 := intCast_ofNat 1 theorem intCast_neg_one : ((-1 : Int) : α) = -1 := by rw [intCast_neg, intCast_ofNat] theorem intCast_natCast (n : Nat) : ((n : Int) : α) = (n : α) := intCast_ofNat n theorem intCast_natCast_add_one (n : Nat) : ((n + 1 : Int) : α) = (n : α) + 1 := by - rw [← Int.natCast_succ, intCast_natCast, natCast_add, ofNat_eq_natCast] + rw [← Int.natCast_add_one, intCast_natCast, natCast_add, ofNat_eq_natCast] theorem intCast_negSucc (n : Nat) : ((-(n + 1) : Int) : α) = -((n : α) + 1) := by - rw [intCast_neg, ← Int.natCast_succ, intCast_natCast, ofNat_eq_natCast, natCast_add] + rw [intCast_neg, ← Int.natCast_add_one, intCast_natCast, ofNat_eq_natCast, natCast_add] theorem intCast_nat_add {x y : Nat} : ((x + y : Int) : α) = ((x : α) + (y : α)) := by rw [Int.ofNat_add_ofNat, intCast_natCast, natCast_add] theorem intCast_nat_sub {x y : Nat} (h : x ≥ y) : (((x - y : Nat) : Int) : α) = ((x : α) - (y : α)) := by @@ -280,7 +280,7 @@ theorem intCast_ext_iff {x y : Int} : (x : α) = (y : α) ↔ x % p = y % p := b theorem ofNat_ext_iff {x y : Nat} : OfNat.ofNat (α := α) x = OfNat.ofNat (α := α) y ↔ x % p = y % p := by have := intCast_ext_iff (α := α) p (x := x) (y := y) - simp only [intCast_natCast, ← Int.ofNat_emod] at this + simp only [intCast_natCast, ← Int.natCast_emod] at this simp only [ofNat_eq_natCast] norm_cast at this @@ -296,7 +296,7 @@ theorem intCast_emod (x : Int) : ((x % p : Int) : α) = (x : α) := by theorem natCast_emod (x : Nat) : ((x % p : Nat) : α) = (x : α) := by simp only [← intCast_natCast] - rw [Int.ofNat_emod, intCast_emod] + rw [Int.natCast_emod, intCast_emod] theorem ofNat_emod (x : Nat) : OfNat.ofNat (α := α) (x % p) = OfNat.ofNat x := natCast_emod _ _ From f5964402242cfb21856b5c48dacfd42d356ee4fe Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Fri, 25 Apr 2025 15:26:48 +0200 Subject: [PATCH 3/3] More --- src/Init/Data/Int/DivMod/Lemmas.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean index 7e047836439c..56114117b931 100644 --- a/src/Init/Data/Int/DivMod/Lemmas.lean +++ b/src/Init/Data/Int/DivMod/Lemmas.lean @@ -2899,7 +2899,7 @@ theorem ediv_lt_self_of_pos_of_ne_one {x y : Int} (hx : 0 < x) (hy : y ≠ 1) : by_cases hy' : 1 < y · obtain ⟨xn, rfl⟩ := Int.eq_ofNat_of_zero_le (a := x) (by omega) obtain ⟨yn, rfl⟩ := Int.eq_ofNat_of_zero_le (a := y) (by omega) - rw [← Int.ofNat_ediv] + rw [← Int.natCast_ediv] norm_cast apply Nat.div_lt_self (by omega) (by omega) · have := @Int.ediv_nonpos_of_nonneg_of_nonpos x y (by omega) (by omega) @@ -2909,7 +2909,7 @@ theorem ediv_nonneg_of_nonneg_of_nonneg {x y : Int} (hx : 0 ≤ x) (hy : 0 ≤ y 0 ≤ x / y := by obtain ⟨xn, rfl⟩ := Int.eq_ofNat_of_zero_le (a := x) (by omega) obtain ⟨yn, rfl⟩ := Int.eq_ofNat_of_zero_le (a := y) (by omega) - rw [← Int.ofNat_ediv] + rw [← Int.natCast_ediv] exact Int.ofNat_zero_le (xn / yn) /-- When both x and y are negative we need stricter bounds on x and y