From 76b3234c8108871fc44f39a8777517045aeeaf2b Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Wed, 23 Nov 2022 03:12:55 +0000 Subject: [PATCH] feat: port Data.Int.Cast.Basic (#670) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit mathlib3 SHA: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3 Porting notes: 1. Some lemmas were transferred from `Data.Int.Cast.Defs` in order to match mathlib3 (I accidentally put them in the wrong place when I had ported that file because those lemmas were already present in mathlib4.) 2. The lemmas just mentioned have retained their `simp` attribute for the reason Gabriel mentioned on that PR (#641), even though that attribute isn't present on the mathlib3 version. 3. The `bit0` and `bit1` lemmas have been marked as deprecated. 4. There were many dubious translation errors, I believe primarily because of the difference in the way coercions are handled, so I have `#align`ed all of these with `ₓ`. I believe this is the correct thing to do, but confirmation would be nice. --- Mathlib/Algebra/Ring/Basic.lean | 4 +- Mathlib/Data/Int/Cast/Basic.lean | 144 +++++++++++++++++++++++++------ Mathlib/Data/Int/Cast/Defs.lean | 17 ---- 3 files changed, 119 insertions(+), 46 deletions(-) diff --git a/Mathlib/Algebra/Ring/Basic.lean b/Mathlib/Algebra/Ring/Basic.lean index 339eab5d83a43..4b4b1418febaa 100644 --- a/Mathlib/Algebra/Ring/Basic.lean +++ b/Mathlib/Algebra/Ring/Basic.lean @@ -1,6 +1,6 @@ import Mathlib.Algebra.Group.Commute import Mathlib.Algebra.GroupWithZero.Defs -import Mathlib.Data.Int.Cast.Defs +import Mathlib.Data.Int.Cast.Basic import Mathlib.Tactic.Spread import Mathlib.Algebra.Ring.Defs @@ -115,7 +115,7 @@ instance : CommRing ℤ where @[simp, norm_cast] lemma cast_Nat_cast [AddGroupWithOne R] : (Int.cast (Nat.cast n) : R) = Nat.cast n := - Int.cast_ofNat + Int.cast_ofNat _ @[simp, norm_cast] lemma cast_eq_cast_iff_Nat (m n : ℕ) : (m : ℤ) = (n : ℤ) ↔ m = n := ofNat_inj diff --git a/Mathlib/Data/Int/Cast/Basic.lean b/Mathlib/Data/Int/Cast/Basic.lean index f496f825308ed..8d451cdec02ed 100644 --- a/Mathlib/Data/Int/Cast/Basic.lean +++ b/Mathlib/Data/Int/Cast/Basic.lean @@ -7,59 +7,149 @@ import Mathlib.Data.Int.Cast.Defs import Mathlib.Algebra.Group.Basic /-! -# Cast of integers +# Cast of integers (additional theorems) -This file defines the *canonical* homomorphism from the integers into an -additive group with a one (typically a `ring`). In additive groups with a one -element, there exists a unique such homomorphism and we store it in the -`int_cast : ℤ → R` field. +This file proves additional properties about the *canonical* homomorphism from +the integers into an additive group with a one (`int.cast`). -Preferentially, the homomorphism is written as a coercion. +There is also `Data.Int.Cast.Lemmas`, +which includes lemmas stated in terms of algebraic homomorphisms, +and results involving the order structure of `ℤ`. -## Main declarations - -* `int.cast`: Canonical homomorphism `ℤ → R`. -* `add_group_with_one`: Type class for `int.cast`. +By contrast, this file's only import beyond `Data.Int.Cast.Defs` is `Algebra.Group.Basic`. -/ + +universe u + namespace Nat -variable [AddGroupWithOne R] + +variable {R : Type u} [AddGroupWithOne R] @[simp, norm_cast] theorem cast_sub {m n} (h : m ≤ n) : ((n - m : ℕ) : R) = n - m := eq_sub_of_add_eq <| by rw [← cast_add, Nat.sub_add_cancel h] +#align nat.cast_sub Nat.cast_subₓ +-- `HasLiftT` appeared in the type signature + +@[simp, norm_cast] +theorem cast_pred : ∀ {n}, 0 < n → ((n - 1 : ℕ) : R) = n - 1 + | 0, h => by cases h + | n + 1, _ => by rw [cast_succ, add_sub_cancel]; rfl +#align nat.cast_pred Nat.cast_pred end Nat +open Nat + namespace Int -variable [AddGroupWithOne R] + +variable {R : Type u} [AddGroupWithOne R] + +@[simp, norm_cast] +theorem cast_negSucc (n : ℕ) : (-[n+1] : R) = -(n + 1 : ℕ) := + AddGroupWithOne.intCast_negSucc n +#align int.cast_neg_succ_of_nat Int.cast_negSuccₓ +-- expected `n` to be implicit, and `HasLiftT` + +@[simp, norm_cast] +theorem cast_zero : ((0 : ℤ) : R) = 0 := + (AddGroupWithOne.intCast_ofNat 0).trans Nat.cast_zero +#align int.cast_zero Int.cast_zeroₓ +-- type had `HasLiftT` + +@[simp high, nolint simpNF] -- this lemma competes with `Int.ofNat_eq_cast` to come later +theorem cast_ofNat (n : ℕ) : ((n : ℤ) : R) = n := + AddGroupWithOne.intCast_ofNat _ +#align int.cast_coe_nat Int.cast_ofNatₓ +-- expected `n` to be implicit, and `HasLiftT` + +@[simp, norm_cast] +theorem cast_one : ((1 : ℤ) : R) = 1 := by + erw [cast_ofNat, Nat.cast_one] +#align int.cast_one Int.cast_oneₓ +-- type had `HasLiftT` @[simp, norm_cast] -theorem cast_neg [AddGroupWithOne R] : ∀ n:ℤ, ((-n : ℤ) : R) = -↑n +theorem cast_neg : ∀ n, ((-n : ℤ) : R) = -n | (0 : ℕ) => by erw [cast_zero, neg_zero] | (n + 1 : ℕ) => by erw [cast_ofNat, cast_negSucc] - | -[n +1] => by erw [cast_ofNat, cast_negSucc, neg_neg] + | -[n+1] => by erw [cast_ofNat, cast_negSucc, neg_neg] +#align int.cast_neg Int.cast_negₓ +-- type had `HasLiftT` -@[simp] -theorem cast_subNatNat [AddGroupWithOne R] (m n) : ((subNatNat m n : ℤ) : R) = m - n := by - unfold Int.subNatNat +@[simp, norm_cast] +theorem cast_subNatNat (m n) : ((Int.subNatNat m n : ℤ) : R) = m - n := by + unfold subNatNat cases e : n - m - · simp only [subNatNat, cast_ofNat] + · rw [cast_ofNat] simp [e, Nat.le_of_sub_eq_zero e] · rw [cast_negSucc, Nat.add_one, ← e, Nat.cast_sub <| _root_.le_of_lt <| Nat.lt_of_sub_eq_succ e, neg_sub] -#align int.cast_sub_nat_nat Int.cast_subNatNat +#align int.cast_sub_nat_nat Int.cast_subNatNatₓ +-- type had `HasLiftT` + +#align int.neg_of_nat_eq Int.negOfNat_eq + +@[simp] +theorem cast_negOfNat (n : ℕ) : ((negOfNat n : ℤ) : R) = -n := by simp [Int.cast_neg, negOfNat_eq] +#align int.cast_neg_of_nat Int.cast_negOfNat @[simp, norm_cast] -theorem cast_add [AddGroupWithOne R] : ∀ m n, ((m + n : ℤ) : R) = m + n - | (m : ℕ), (n : ℕ) => by simp [← ofNat_add] +theorem cast_add : ∀ m n, ((m + n : ℤ) : R) = m + n + | (m : ℕ), (n : ℕ) => by simp [← Int.ofNat_add, Nat.cast_add] | (m : ℕ), -[n+1] => by erw [cast_subNatNat, cast_ofNat, cast_negSucc, sub_eq_add_neg] | -[m+1], (n : ℕ) => by - erw [cast_subNatNat, cast_ofNat, cast_negSucc, sub_eq_iff_eq_add, - add_assoc, eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm] - | -[m+1], -[n+1] => show (-[m + n + 1 +1] : R) = _ by - rw [cast_negSucc, cast_negSucc, cast_negSucc, ← neg_add_rev, ← Nat.cast_add, - Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm] + erw [cast_subNatNat, cast_ofNat, cast_negSucc, sub_eq_iff_eq_add, add_assoc, + eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm] + | -[m+1], -[n+1] => + show (-[m + n + 1+1] : R) = _ by + rw [cast_negSucc, cast_negSucc, cast_negSucc, ← neg_add_rev, ← Nat.cast_add, + Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm] +#align int.cast_add Int.cast_addₓ +-- type had `HasLiftT` @[simp, norm_cast] -theorem cast_sub (m n) : ((m - n : ℤ) : R) = m - n := by simp [Int.sub_eq_add_neg, sub_eq_add_neg] +theorem cast_sub (m n) : ((m - n : ℤ) : R) = m - n := by + simp [Int.sub_eq_add_neg, sub_eq_add_neg, Int.cast_neg, Int.cast_add] +#align int.cast_sub Int.cast_subₓ +-- type had `HasLiftT` + +section deprecated +set_option linter.deprecated false + +@[norm_cast, deprecated] +theorem ofNat_bit0 (n : ℕ) : (↑(bit0 n) : ℤ) = bit0 ↑n := + rfl +#align int.coe_nat_bit0 Int.ofNat_bit0 + +@[norm_cast, deprecated] +theorem ofNat_bit1 (n : ℕ) : (↑(bit1 n) : ℤ) = bit1 ↑n := + rfl +#align int.coe_nat_bit1 Int.ofNat_bit1 + +@[norm_cast, deprecated] +theorem cast_bit0 (n : ℤ) : ((bit0 n : ℤ) : R) = bit0 (n : R) := + Int.cast_add _ _ +#align int.cast_bit0 Int.cast_bit0 + +@[norm_cast, deprecated] +theorem cast_bit1 (n : ℤ) : ((bit1 n : ℤ) : R) = bit1 (n : R) := + by rw [bit1, Int.cast_add, Int.cast_one, cast_bit0]; rfl +#align int.cast_bit1 Int.cast_bit1 + +end deprecated + +theorem cast_two : ((2 : ℤ) : R) = 2 := + show (((2 : ℕ) : ℤ) : R) = ((2 : ℕ) : R) by rw [cast_ofNat, Nat.cast_ofNat] +#align int.cast_two Int.cast_two + +theorem cast_three : ((3 : ℤ) : R) = 3 := + show (((3 : ℕ) : ℤ) : R) = ((3 : ℕ) : R) by rw [cast_ofNat, Nat.cast_ofNat] +#align int.cast_three Int.cast_three + +theorem cast_four : ((4 : ℤ) : R) = 4 := + show (((4 : ℕ) : ℤ) : R) = ((4 : ℕ) : R) by rw [cast_ofNat, Nat.cast_ofNat] +#align int.cast_four Int.cast_four + +end Int diff --git a/Mathlib/Data/Int/Cast/Defs.lean b/Mathlib/Data/Int/Cast/Defs.lean index d5f045c1d7d6b..a00b589db8173 100644 --- a/Mathlib/Data/Int/Cast/Defs.lean +++ b/Mathlib/Data/Int/Cast/Defs.lean @@ -65,23 +65,6 @@ namespace Int instance [IntCast R] : CoeTail ℤ R where coe := cast -@[simp high, nolint simpNF] -- this lemma competes with `Int.ofNat_eq_cast` to come later -theorem cast_ofNat [AddGroupWithOne R] : (cast (ofNat n) : R) = Nat.cast n := - AddGroupWithOne.intCast_ofNat _ -#align int.cast_coe_nat Int.cast_ofNat - -@[simp, norm_cast] -theorem cast_negSucc [AddGroupWithOne R] : (cast (negSucc n) : R) = (-(Nat.cast (n + 1)) : R) := - AddGroupWithOne.intCast_negSucc _ -#align int.cast_neg_succ_of_nat Int.cast_negSucc - -@[simp, norm_cast] theorem cast_zero [AddGroupWithOne R] : ((0 : ℤ) : R) = 0 := by - erw [cast_ofNat, Nat.cast_zero] -#align int.cast_zero Int.cast_zero -@[simp, norm_cast] theorem cast_one [AddGroupWithOne R] : ((1 : ℤ) : R) = 1 := by - erw [cast_ofNat, Nat.cast_one] -#align int.cast_one Int.cast_one - end Int /-- An `AddCommGroupWithOne` is an `AddGroupWithOne` satisfying `a + b = b + a`. -/