From e1bccd6e40ae78370f01659715d3c948716e3b7e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 9 Jan 2023 16:42:07 +0000 Subject: [PATCH] chore(data/int/order/basic): Fix lemma name (#17967) `int.coe_nat_abs` wasn't referring to the correct lemma. Change the name, add the lemma it should correspond to and tag both with `simp` and `norm_cast`. Co-authored-by: Eric Wieser --- archive/imo/imo2013_q5.lean | 2 +- src/algebra/euclidean_domain/instances.lean | 2 +- src/algebra/group_power/lemmas.lean | 7 +++--- src/analysis/normed/field/basic.lean | 2 +- src/data/int/basic.lean | 4 +-- src/data/int/dvd/basic.lean | 4 +-- src/data/int/order/basic.lean | 9 +++++-- src/data/rat/floor.lean | 3 +-- src/data/sign.lean | 2 +- src/dynamics/ergodic/add_circle.lean | 2 +- src/number_theory/zsqrtd/gaussian_int.lean | 6 ++--- src/ring_theory/int/basic.lean | 28 ++++++++++----------- src/testing/slim_check/sampleable.lean | 2 +- 13 files changed, 37 insertions(+), 36 deletions(-) diff --git a/archive/imo/imo2013_q5.lean b/archive/imo/imo2013_q5.lean index 261f9526df2d7..53cb83b0df515 100644 --- a/archive/imo/imo2013_q5.lean +++ b/archive/imo/imo2013_q5.lean @@ -103,7 +103,7 @@ begin ... = ((q.num.nat_abs : ℤ) : ℝ) : congr_arg coe (int.nat_abs_of_nonneg num_pos.le).symm ... ≤ f q.num.nat_abs : H4 q.num.nat_abs (int.nat_abs_pos_of_ne_zero num_pos.ne') - ... = f q.num : by { rw ←int.nat_abs_of_nonneg num_pos.le, norm_cast } + ... = f q.num : by rw [nat.cast_nat_abs, abs_of_nonneg num_pos.le] ... = f (q * q.denom) : by rw ←rat.mul_denom_eq_num ... ≤ f q * f q.denom : H1 q q.denom hq (nat.cast_pos.mpr q.pos), have h_f_denom_pos := diff --git a/src/algebra/euclidean_domain/instances.lean b/src/algebra/euclidean_domain/instances.lean index 59e62167a406d..994324f38030d 100644 --- a/src/algebra/euclidean_domain/instances.lean +++ b/src/algebra/euclidean_domain/instances.lean @@ -33,7 +33,7 @@ instance int.euclidean_domain : euclidean_domain ℤ := r := λ a b, a.nat_abs < b.nat_abs, r_well_founded := measure_wf (λ a, int.nat_abs a), remainder_lt := λ a b b0, int.coe_nat_lt.1 $ - by { rw [int.nat_abs_of_nonneg (int.mod_nonneg _ b0), ← int.abs_eq_nat_abs], + by { rw [int.nat_abs_of_nonneg (int.mod_nonneg _ b0), int.coe_nat_abs], exact int.mod_lt _ b0 }, mul_left_not_lt := λ a b b0, not_lt_of_ge $ by {rw [← mul_one a.nat_abs, int.nat_abs_mul], diff --git a/src/algebra/group_power/lemmas.lean b/src/algebra/group_power/lemmas.lean index 7b6b520351d17..28338034995b0 100644 --- a/src/algebra/group_power/lemmas.lean +++ b/src/algebra/group_power/lemmas.lean @@ -300,9 +300,9 @@ lemma abs_zsmul (n : ℤ) (a : α) : |n • a| = |n| • |a| := begin obtain n0 | n0 := le_total 0 n, { lift n to ℕ using n0, - simp only [abs_nsmul, coe_nat_abs, coe_nat_zsmul] }, + simp only [abs_nsmul, abs_coe_nat, coe_nat_zsmul] }, { lift (- n) to ℕ using neg_nonneg.2 n0 with m h, - rw [← abs_neg (n • a), ← neg_zsmul, ← abs_neg n, ← h, coe_nat_zsmul, coe_nat_abs, + rw [← abs_neg (n • a), ← neg_zsmul, ← abs_neg n, ← h, coe_nat_zsmul, abs_coe_nat, coe_nat_zsmul], exact abs_nsmul m _ }, end @@ -524,8 +524,7 @@ end linear_ordered_ring namespace int -@[simp] lemma nat_abs_sq (x : ℤ) : (x.nat_abs ^ 2 : ℤ) = x ^ 2 := -by rw [sq, int.nat_abs_mul_self', sq] +lemma nat_abs_sq (x : ℤ) : (x.nat_abs ^ 2 : ℤ) = x ^ 2 := by rw [sq, int.nat_abs_mul_self', sq] alias nat_abs_sq ← nat_abs_pow_two diff --git a/src/analysis/normed/field/basic.lean b/src/analysis/normed/field/basic.lean index 8e327edcd3906..d7dd051897b82 100644 --- a/src/analysis/normed/field/basic.lean +++ b/src/analysis/normed/field/basic.lean @@ -699,7 +699,7 @@ lemma int.norm_eq_abs (n : ℤ) : ‖n‖ = |n| := rfl lemma nnreal.coe_nat_abs (n : ℤ) : (n.nat_abs : ℝ≥0) = ‖n‖₊ := nnreal.eq $ calc ((n.nat_abs : ℝ≥0) : ℝ) = (n.nat_abs : ℤ) : by simp only [int.cast_coe_nat, nnreal.coe_nat_cast] - ... = |n| : by simp only [← int.abs_eq_nat_abs, int.cast_abs] + ... = |n| : by simp only [int.coe_nat_abs, int.cast_abs] ... = ‖n‖ : rfl lemma int.abs_le_floor_nnreal_iff (z : ℤ) (c : ℝ≥0) : |z| ≤ ⌊c⌋₊ ↔ ‖z‖₊ ≤ c := diff --git a/src/data/int/basic.lean b/src/data/int/basic.lean index 52b27c99b41d9..433b7cb209ace 100644 --- a/src/data/int/basic.lean +++ b/src/data/int/basic.lean @@ -181,7 +181,7 @@ end variables {a b : ℤ} {n : ℕ} -attribute [simp] nat_abs nat_abs_of_nat nat_abs_zero nat_abs_one +attribute [simp] nat_abs_of_nat nat_abs_zero nat_abs_one theorem nat_abs_add_le (a b : ℤ) : nat_abs (a + b) ≤ nat_abs a + nat_abs b := begin @@ -212,7 +212,7 @@ lemma nat_abs_mul_nat_abs_eq {a b : ℤ} {c : ℕ} (h : a * b = (c : ℤ)) : a.nat_abs * b.nat_abs = c := by rw [← nat_abs_mul, h, nat_abs_of_nat] -@[simp] lemma nat_abs_mul_self' (a : ℤ) : (nat_abs a * nat_abs a : ℤ) = a * a := +lemma nat_abs_mul_self' (a : ℤ) : (nat_abs a * nat_abs a : ℤ) = a * a := by rw [← int.coe_nat_mul, nat_abs_mul_self] theorem neg_succ_of_nat_eq' (m : ℕ) : -[1+ m] = -m - 1 := diff --git a/src/data/int/dvd/basic.lean b/src/data/int/dvd/basic.lean index 034d16b7c309a..70b50fe2e31a9 100644 --- a/src/data/int/dvd/basic.lean +++ b/src/data/int/dvd/basic.lean @@ -27,10 +27,10 @@ namespace int λ ⟨k, e⟩, dvd.intro k $ by rw [e, int.coe_nat_mul]⟩ theorem coe_nat_dvd_left {n : ℕ} {z : ℤ} : (↑n : ℤ) ∣ z ↔ n ∣ z.nat_abs := -by rcases nat_abs_eq z with eq | eq; rw eq; simp [coe_nat_dvd] +by rcases nat_abs_eq z with eq | eq; rw eq; simp [←coe_nat_dvd] theorem coe_nat_dvd_right {n : ℕ} {z : ℤ} : z ∣ (↑n : ℤ) ↔ z.nat_abs ∣ n := -by rcases nat_abs_eq z with eq | eq; rw eq; simp [coe_nat_dvd] +by rcases nat_abs_eq z with eq | eq; rw eq; simp [←coe_nat_dvd] theorem le_of_dvd {a b : ℤ} (bpos : 0 < b) (H : a ∣ b) : a ≤ b := match a, b, eq_succ_of_zero_lt bpos, H with diff --git a/src/data/int/order/basic.lean b/src/data/int/order/basic.lean index de24db37ca9d1..94841ad2c1297 100644 --- a/src/data/int/order/basic.lean +++ b/src/data/int/order/basic.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad -/ import data.int.basic +import data.int.cast.basic import algebra.ring.divisibility import algebra.order.group.abs import algebra.order.ring.char_zero @@ -54,6 +55,11 @@ theorem abs_eq_nat_abs : ∀ a : ℤ, |a| = nat_abs a | (n : ℕ) := abs_of_nonneg $ coe_zero_le _ | -[1+ n] := abs_of_nonpos $ le_of_lt $ neg_succ_lt_zero _ +@[simp, norm_cast] lemma coe_nat_abs (n : ℤ) : (n.nat_abs : ℤ) = |n| := n.abs_eq_nat_abs.symm + +lemma _root_.nat.cast_nat_abs {α : Type*} [add_group_with_one α] (n : ℤ) : (n.nat_abs : α) = ↑|n| := +by rw [←int.coe_nat_abs, int.cast_coe_nat] + theorem nat_abs_abs (a : ℤ) : nat_abs (|a|) = nat_abs a := by rw [abs_eq_nat_abs]; refl @@ -68,8 +74,7 @@ lemma coe_nat_ne_zero_iff_pos {n : ℕ} : (n : ℤ) ≠ 0 ↔ 0 < n := ⟨λ h, nat.pos_of_ne_zero (coe_nat_ne_zero.1 h), λ h, (ne_of_lt (coe_nat_lt.2 h)).symm⟩ -theorem coe_nat_abs (n : ℕ) : |(n : ℤ)| = n := -abs_of_nonneg (coe_nat_nonneg n) +@[norm_cast] lemma abs_coe_nat (n : ℕ) : |(n : ℤ)| = n := abs_of_nonneg (coe_nat_nonneg n) /-! ### succ and pred -/ diff --git a/src/data/rat/floor.lean b/src/data/rat/floor.lean index b5096eae42c92..5428c18f5740e 100644 --- a/src/data/rat/floor.lean +++ b/src/data/rat/floor.lean @@ -126,9 +126,8 @@ begin have : ((q.denom - q.num * ⌊q_inv⌋ : ℚ) / q.num).num = q.denom - q.num * ⌊q_inv⌋, by { suffices : ((q.denom : ℤ) - q.num * ⌊q_inv⌋).nat_abs.coprime q.num.nat_abs, by exact_mod_cast (rat.num_div_eq_of_coprime q_num_pos this), - have : (q.num.nat_abs : ℚ) = (q.num : ℚ), by exact_mod_cast q_num_abs_eq_q_num, have tmp := nat.coprime_sub_mul_floor_rat_div_of_coprime q.cop.symm, - simpa only [this, q_num_abs_eq_q_num] using tmp }, + simpa only [nat.cast_nat_abs, abs_of_nonneg q_num_pos.le] using tmp }, rwa this }, -- to show the claim, start with the following inequality have q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * q⁻¹.denom < q⁻¹.denom, by diff --git a/src/data/sign.lean b/src/data/sign.lean index 99bde85fc7a58..0e2013bcf4553 100644 --- a/src/data/sign.lean +++ b/src/data/sign.lean @@ -379,7 +379,7 @@ begin λ a, a.1, λ a, a.1.prop, _, _⟩, { simp [@sum_attach _ _ _ _ (λ a, (f a).nat_abs)] }, { intros x hx, - simp [sum_sigma, hx, ← int.sign_eq_sign, int.sign_mul_nat_abs, mul_comm ((f _).nat_abs : ℤ), + simp [sum_sigma, hx, ← int.sign_eq_sign, int.sign_mul_abs, mul_comm (|f _|), @sum_attach _ _ _ _ (λ a, ∑ j in range (f a).nat_abs, if a = x then (f a).sign else 0)] } end diff --git a/src/dynamics/ergodic/add_circle.lean b/src/dynamics/ergodic/add_circle.lean index 5a22777975888..a1c40c7ea404e 100644 --- a/src/dynamics/ergodic/add_circle.lean +++ b/src/dynamics/ergodic/add_circle.lean @@ -102,7 +102,7 @@ lemma ergodic_zsmul {n : ℤ} (hn : 1 < |n|) : ergodic (λ (y : add_circle T), n have hu₀ : ∀ j, add_order_of (u j) = n.nat_abs^j, { exact λ j, add_order_of_div_of_gcd_eq_one (pow_pos (pos_of_gt hn) j) (gcd_one_left _), }, have hnu : ∀ j, n^j • (u j) = 0 := λ j, by rw [← add_order_of_dvd_iff_zsmul_eq_zero, hu₀, - int.coe_nat_pow, ← int.abs_eq_nat_abs, ← abs_pow, abs_dvd], + int.coe_nat_pow, int.coe_nat_abs, ← abs_pow, abs_dvd], have hu₁ : ∀ j, ((u j) +ᵥ s : set _) =ᵐ[volume] s := λ j, by rw vadd_eq_self_of_preimage_zsmul_eq_self hs' (hnu j), have hu₂ : tendsto (λ j, add_order_of $ u j) at_top at_top, diff --git a/src/number_theory/zsqrtd/gaussian_int.lean b/src/number_theory/zsqrtd/gaussian_int.lean index 02bd567c03491..8aa9a9f782990 100644 --- a/src/number_theory/zsqrtd/gaussian_int.lean +++ b/src/number_theory/zsqrtd/gaussian_int.lean @@ -96,12 +96,12 @@ by rw [← @int.cast_inj ℝ _ _ _]; simp lemma norm_pos {x : ℤ[i]} : 0 < norm x ↔ x ≠ 0 := by rw [lt_iff_le_and_ne, ne.def, eq_comm, norm_eq_zero]; simp [norm_nonneg] -lemma coe_nat_abs_norm (x : ℤ[i]) : (x.norm.nat_abs : ℤ) = x.norm := +lemma abs_coe_nat_norm (x : ℤ[i]) : (x.norm.nat_abs : ℤ) = x.norm := int.nat_abs_of_nonneg (norm_nonneg _) @[simp] lemma nat_cast_nat_abs_norm {α : Type*} [ring α] (x : ℤ[i]) : (x.norm.nat_abs : α) = x.norm := -by rw [← int.cast_coe_nat, coe_nat_abs_norm] +by rw [← int.cast_coe_nat, abs_coe_nat_norm] lemma nat_abs_norm_eq (x : ℤ[i]) : x.norm.nat_abs = x.re.nat_abs * x.re.nat_abs + x.im.nat_abs * x.im.nat_abs := @@ -169,7 +169,7 @@ lemma norm_le_norm_mul_left (x : ℤ[i]) {y : ℤ[i]} (hy : y ≠ 0) : (norm x).nat_abs ≤ (norm (x * y)).nat_abs := by rw [zsqrtd.norm_mul, int.nat_abs_mul]; exact le_mul_of_one_le_right (nat.zero_le _) - (int.coe_nat_le.1 (by rw [coe_nat_abs_norm]; exact int.add_one_le_of_lt (norm_pos.2 hy))) + (int.coe_nat_le.1 (by rw [abs_coe_nat_norm]; exact int.add_one_le_of_lt (norm_pos.2 hy))) instance : nontrivial ℤ[i] := ⟨⟨0, 1, dec_trivial⟩⟩ diff --git a/src/ring_theory/int/basic.lean b/src/ring_theory/int/basic.lean index 5b1ce2c369f36..cd86ca03afeb9 100644 --- a/src/ring_theory/int/basic.lean +++ b/src/ring_theory/int/basic.lean @@ -91,24 +91,22 @@ instance : normalization_monoid ℤ := lemma normalize_of_nonneg {z : ℤ} (h : 0 ≤ z) : normalize z = z := show z * ↑(ite _ _ _) = z, by rw [if_pos h, units.coe_one, mul_one] -lemma normalize_of_neg {z : ℤ} (h : z < 0) : normalize z = -z := -show z * ↑(ite _ _ _) = -z, -by rw [if_neg (not_le_of_gt h), units.coe_neg, units.coe_one, mul_neg_one] +lemma normalize_of_nonpos {z : ℤ} (h : z ≤ 0) : normalize z = -z := +begin + obtain rfl | h := h.eq_or_lt, + { simp }, + { change z * ↑(ite _ _ _) = -z, + rw [if_neg (not_le_of_gt h), units.coe_neg, units.coe_one, mul_neg_one] } +end lemma normalize_coe_nat (n : ℕ) : normalize (n : ℤ) = n := normalize_of_nonneg (coe_nat_le_coe_nat_of_le $ nat.zero_le n) -theorem coe_nat_abs_eq_normalize (z : ℤ) : (z.nat_abs : ℤ) = normalize z := -begin - by_cases 0 ≤ z, - { simp [nat_abs_of_nonneg h, normalize_of_nonneg h] }, - { simp [of_nat_nat_abs_of_nonpos (le_of_not_ge h), normalize_of_neg (lt_of_not_ge h)] } -end +lemma abs_eq_normalize (z : ℤ) : |z| = normalize z := +by cases le_total 0 z; simp [normalize_of_nonneg, normalize_of_nonpos, *] lemma nonneg_of_normalize_eq_self {z : ℤ} (hz : normalize z = z) : 0 ≤ z := -calc 0 ≤ (z.nat_abs : ℤ) : coe_zero_le _ -... = normalize z : coe_nat_abs_eq_normalize _ -... = z : hz +abs_eq_self.1 $ by rw [abs_eq_normalize, hz] lemma nonneg_iff_normalize_eq_self (z : ℤ) : normalize z = z ↔ 0 ≤ z := ⟨nonneg_of_normalize_eq_self, normalize_of_nonneg⟩ @@ -127,7 +125,7 @@ instance : gcd_monoid ℤ := gcd_dvd_right := assume a b, int.gcd_dvd_right _ _, dvd_gcd := assume a b c, dvd_gcd, gcd_mul_lcm := λ a b, by - { rw [← int.coe_nat_mul, gcd_mul_lcm, coe_nat_abs_eq_normalize], + { rw [← int.coe_nat_mul, gcd_mul_lcm, coe_nat_abs, abs_eq_normalize], exact normalize_associated (a * b) }, lcm_zero_left := assume a, coe_nat_eq_zero.2 $ nat.lcm_zero_left _, lcm_zero_right := assume a, coe_nat_eq_zero.2 $ nat.lcm_zero_right _} @@ -225,10 +223,10 @@ begin { refine (assume a, quotient.induction_on' a $ assume a, associates.mk_eq_mk_iff_associated.2 $ associated.symm $ ⟨norm_unit a, _⟩), show normalize a = int.nat_abs (normalize a), - rw [int.coe_nat_abs_eq_normalize, normalize_idem] }, + rw [int.coe_nat_abs, int.abs_eq_normalize, normalize_idem] }, { intro n, dsimp, - rw [←normalize_apply, ← int.coe_nat_abs_eq_normalize, int.nat_abs_of_nat, int.nat_abs_of_nat] } + rw [←normalize_apply, ←int.abs_eq_normalize, int.nat_abs_abs, int.nat_abs_of_nat] } end lemma int.prime.dvd_mul {m n : ℤ} {p : ℕ} diff --git a/src/testing/slim_check/sampleable.lean b/src/testing/slim_check/sampleable.lean index 3da36e6b25d90..c14c317264fde 100644 --- a/src/testing/slim_check/sampleable.lean +++ b/src/testing/slim_check/sampleable.lean @@ -371,7 +371,7 @@ begin rcases i with ⟨x,⟨y,hy⟩⟩; unfold_wf; dsimp [rat.mk_pnat], mono*, - { rw [← int.coe_nat_le, ← int.abs_eq_nat_abs, ← int.abs_eq_nat_abs], + { rw [← int.coe_nat_le, int.coe_nat_abs, int.coe_nat_abs], apply int.abs_div_le_abs }, { change _ - 1 ≤ y-1, apply tsub_le_tsub_right,