From 6dfaf1863c184268e02d6a2b4dd8e5b58b530ca4 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Thu, 22 Oct 2015 16:36:45 -0400 Subject: [PATCH] refactor(library/data/int/{basic,order}): protect theorem names --- library/algebra/group_power.lean | 4 +- library/data/int/basic.lean | 65 ++++++++------- library/data/int/div.lean | 14 ++-- library/data/int/order.lean | 96 +++++++++++----------- library/data/rat/basic.lean | 24 +++--- library/theories/number_theory/bezout.lean | 8 +- 6 files changed, 105 insertions(+), 106 deletions(-) diff --git a/library/algebra/group_power.lean b/library/algebra/group_power.lean index ab6a6bf22..d89d688ba 100644 --- a/library/algebra/group_power.lean +++ b/library/algebra/group_power.lean @@ -153,7 +153,7 @@ or.elim (nat.lt_or_ge m (nat.succ n)) theorem gpow_add (a : A) : ∀i j : int, gpow a (i + j) = gpow a i * gpow a j | (of_nat m) (of_nat n) := !pow_add | (of_nat m) -[1+n] := !gpow_add_aux -| -[1+m] (of_nat n) := by rewrite [int.add.comm, gpow_add_aux, ↑gpow, -*inv_pow, pow_inv_comm] +| -[1+m] (of_nat n) := by rewrite [add.comm, gpow_add_aux, ↑gpow, -*inv_pow, pow_inv_comm] | -[1+m] -[1+n] := calc gpow a (-[1+m] + -[1+n]) = (a^(#nat nat.succ m + nat.succ n))⁻¹ : rfl @@ -161,7 +161,7 @@ theorem gpow_add (a : A) : ∀i j : int, gpow a (i + j) = gpow a i * gpow a j ... = gpow a (-[1+m]) * gpow a (-[1+n]) : rfl theorem gpow_comm (a : A) (i j : ℤ) : gpow a i * gpow a j = gpow a j * gpow a i := -by rewrite [-*gpow_add, int.add.comm] +by rewrite [-*gpow_add, add.comm] end group section ordered_ring diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 8b02cbd63..babf96b2e 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -341,11 +341,11 @@ calc (pr1 p + pr1 q + pr1 r, pr2 p + pr2 q + pr2 r) = (pr1 p + (pr1 q + pr1 r), pr2 p + pr2 q + pr2 r) : by rewrite add.assoc ... = (pr1 p + (pr1 q + pr1 r), pr2 p + (pr2 q + pr2 r)) : by rewrite add.assoc -theorem add.comm (a b : ℤ) : a + b = b + a := +protected theorem add_comm (a b : ℤ) : a + b = b + a := eq_of_repr_equiv_repr (equiv.trans !repr_add (equiv.symm (!padd_comm ▸ !repr_add))) -theorem add.assoc (a b c : ℤ) : a + b + c = a + (b + c) := +protected theorem add_assoc (a b c : ℤ) : a + b + c = a + (b + c) := eq_of_repr_equiv_repr (calc repr (a + b + c) ≡ padd (repr (a + b)) (repr c) : repr_add @@ -354,9 +354,9 @@ eq_of_repr_equiv_repr (calc ... ≡ padd (repr a) (repr (b + c)) : padd_congr !equiv.refl !repr_add ... ≡ repr (a + (b + c)) : repr_add) -theorem add_zero : Π (a : ℤ), a + 0 = a := int.rec (λm, rfl) (λm, rfl) +protected theorem add_zero : Π (a : ℤ), a + 0 = a := int.rec (λm, rfl) (λm, rfl) -theorem zero_add (a : ℤ) : 0 + a = a := !add.comm ▸ !add_zero +protected theorem zero_add (a : ℤ) : 0 + a = a := !int.add_comm ▸ !int.add_zero /- negation -/ @@ -393,7 +393,7 @@ calc pr1 p + pr1 q + pr2 q + pr2 p ... = pr1 p + (pr2 p + pr2 q + pr1 q) : algebra.add.comm ... = pr2 p + pr2 q + pr1 q + pr1 p : algebra.add.comm -theorem add.left_inv (a : ℤ) : -a + a = 0 := +protected theorem add_left_inv (a : ℤ) : -a + a = 0 := have H : repr (-a + a) ≡ repr 0, from calc repr (-a + a) ≡ padd (repr (neg a)) (repr a) : repr_add @@ -485,7 +485,7 @@ begin { rewrite algebra.add.comm, congruence, repeat rewrite mul.comm } end -theorem mul.comm (a b : ℤ) : a * b = b * a := +protected theorem mul_comm (a b : ℤ) : a * b = b * a := eq_of_repr_equiv_repr ((calc repr (a * b) = pmul (repr a) (repr b) : repr_mul @@ -503,7 +503,7 @@ end theorem pmul_assoc (p q r: ℕ × ℕ) : pmul (pmul p q) r = pmul p (pmul q r) := pmul_assoc_prep -theorem mul.assoc (a b c : ℤ) : (a * b) * c = a * (b * c) := +protected theorem mul_assoc (a b c : ℤ) : (a * b) * c = a * (b * c) := eq_of_repr_equiv_repr ((calc repr (a * b * c) = pmul (repr (a * b)) (repr c) : repr_mul @@ -512,13 +512,12 @@ eq_of_repr_equiv_repr ... = pmul (repr a) (repr (b * c)) : repr_mul ... = repr (a * (b * c)) : repr_mul) ▸ !equiv.refl) -theorem mul_one : Π (a : ℤ), a * 1 = a -| (of_nat m) := !zero_add -- zero_add happens to be def. = to this thm +protected theorem mul_one : Π (a : ℤ), a * 1 = a +| (of_nat m) := !int.zero_add -- zero_add happens to be def. = to this thm | -[1+ m] := !nat.zero_add ▸ rfl - -theorem one_mul (a : ℤ) : 1 * a = a := -mul.comm a 1 ▸ mul_one a +protected theorem one_mul (a : ℤ) : 1 * a = a := +int.mul_comm a 1 ▸ int.mul_one a private theorem mul_distrib_prep {a1 a2 b1 b2 c1 c2 : ℕ} : ((a1+b1)*c1+(a2+b2)*c2, (a1+b1)*c2+(a2+b2)*c1) = @@ -529,7 +528,7 @@ begin {rewrite add.comm4} end -theorem mul.right_distrib (a b c : ℤ) : (a + b) * c = a * c + b * c := +protected theorem mul_right_distrib (a b c : ℤ) : (a + b) * c = a * c + b * c := eq_of_repr_equiv_repr (calc repr ((a + b) * c) = pmul (repr (a + b)) (repr c) : repr_mul @@ -539,40 +538,40 @@ eq_of_repr_equiv_repr ... = padd (repr (a * c)) (repr (b * c)) : repr_mul ... ≡ repr (a * c + b * c) : repr_add) -theorem mul.left_distrib (a b c : ℤ) : a * (b + c) = a * b + a * c := +protected theorem mul_left_distrib (a b c : ℤ) : a * (b + c) = a * b + a * c := calc - a * (b + c) = (b + c) * a : mul.comm - ... = b * a + c * a : mul.right_distrib - ... = a * b + c * a : mul.comm - ... = a * b + a * c : mul.comm + a * (b + c) = (b + c) * a : int.mul_comm + ... = b * a + c * a : int.mul_right_distrib + ... = a * b + c * a : int.mul_comm + ... = a * b + a * c : int.mul_comm -theorem zero_ne_one : (0 : int) ≠ 1 := +protected theorem zero_ne_one : (0 : int) ≠ 1 := assume H : 0 = 1, !succ_ne_zero (of_nat.inj H)⁻¹ -theorem eq_zero_or_eq_zero_of_mul_eq_zero {a b : ℤ} (H : a * b = 0) : a = 0 ∨ b = 0 := +protected theorem eq_zero_or_eq_zero_of_mul_eq_zero {a b : ℤ} (H : a * b = 0) : a = 0 ∨ b = 0 := or.imp eq_zero_of_nat_abs_eq_zero eq_zero_of_nat_abs_eq_zero (eq_zero_or_eq_zero_of_mul_eq_zero (by rewrite [-nat_abs_mul, H])) protected definition integral_domain [reducible] [trans_instance] : algebra.integral_domain int := ⦃algebra.integral_domain, add := int.add, - add_assoc := add.assoc, + add_assoc := int.add_assoc, zero := 0, - zero_add := zero_add, - add_zero := add_zero, + zero_add := int.zero_add, + add_zero := int.add_zero, neg := int.neg, - add_left_inv := add.left_inv, - add_comm := add.comm, + add_left_inv := int.add_left_inv, + add_comm := int.add_comm, mul := int.mul, - mul_assoc := mul.assoc, + mul_assoc := int.mul_assoc, one := 1, - one_mul := one_mul, - mul_one := mul_one, - left_distrib := mul.left_distrib, - right_distrib := mul.right_distrib, - mul_comm := mul.comm, - zero_ne_one := zero_ne_one, - eq_zero_or_eq_zero_of_mul_eq_zero := @eq_zero_or_eq_zero_of_mul_eq_zero⦄ + one_mul := int.one_mul, + mul_one := int.mul_one, + left_distrib := int.mul_left_distrib, + right_distrib := int.mul_right_distrib, + mul_comm := int.mul_comm, + zero_ne_one := int.zero_ne_one, + eq_zero_or_eq_zero_of_mul_eq_zero := @int.eq_zero_or_eq_zero_of_mul_eq_zero⦄ definition int_has_sub [reducible] [instance] [priority int.prio] : has_sub int := has_sub.mk has_sub.sub diff --git a/library/data/int/div.lean b/library/data/int/div.lean index 53c73225a..f510739b0 100644 --- a/library/data/int/div.lean +++ b/library/data/int/div.lean @@ -167,7 +167,7 @@ or.elim (nat.lt_or_ge m (n * k)) ... = of_nat (n - m div k - 1) : nat.mul_sub_div_of_lt (!nat.mul_comm ▸ m_lt_nk) ... = -[1+m] div k + n : - by rewrite [nat.sub_sub, of_nat_sub H4, add.comm, sub_eq_add_neg, + by rewrite [nat.sub_sub, of_nat_sub H4, int.add_comm, sub_eq_add_neg, !neg_succ_of_nat_div (of_nat_lt_of_nat_of_lt H2), of_nat_add, of_nat_div], Hm⁻¹ ▸ this) @@ -259,7 +259,7 @@ calc -[1+m] mod b = -(m + 1) - -[1+m] div b * b : rfl ... = -(m + 1) - -(m div b + 1) * b : neg_succ_of_nat_div _ bpos ... = -m + -1 + (b + m div b * b) : - by rewrite [neg_add, -neg_mul_eq_neg_mul, sub_neg_eq_add, mul.right_distrib, + by rewrite [neg_add, -neg_mul_eq_neg_mul, sub_neg_eq_add, right_distrib, one_mul, (add.comm b)] ... = b + -1 + (-m + m div b * b) : by rewrite [-*add.assoc, add.comm (-m), add.right_comm (-1), (add.comm b)] @@ -341,7 +341,7 @@ have H2 : a mod (abs b) < abs b, from theorem add_mul_mod_self {a b c : ℤ} : (a + b * c) mod c = a mod c := decidable.by_cases (assume cz : c = 0, by rewrite [cz, mul_zero, add_zero]) - (assume cnz, by rewrite [(modulo.def), !add_mul_div_self cnz, mul.right_distrib, + (assume cnz, by rewrite [(modulo.def), !add_mul_div_self cnz, right_distrib, sub_add_eq_sub_sub_swap, add_sub_cancel]) theorem add_mul_mod_self_left (a b c : ℤ) : (a + b * c) mod b = a mod b := @@ -405,7 +405,7 @@ calc a * b div (a * c) = a * (b div c * c + b mod c) div (a * c) : eq_div_mul_add_mod ... = (a * (b mod c) + a * c * (b div c)) div (a * c) : - by rewrite [!add.comm, mul.left_distrib, mul.comm _ c, -!mul.assoc] + by rewrite [!add.comm, int.mul_left_distrib, mul.comm _ c, -!mul.assoc] ... = a * (b mod c) div (a * c) + b div c : !add_mul_div_self_left H3 ... = 0 + b div c : {!div_eq_zero_of_lt H5 H4} ... = b div c : zero_add @@ -438,7 +438,7 @@ theorem lt_div_add_one_mul_self (a : ℤ) {b : ℤ} (H : b > 0) : a < (a div b + have H : a - a div b * b < b, from !mod_lt_of_pos H, calc a < a div b * b + b : iff.mpr !lt_add_iff_sub_lt_left H - ... = (a div b + 1) * b : by rewrite [mul.right_distrib, one_mul] + ... = (a div b + 1) * b : by rewrite [right_distrib, one_mul] theorem div_le_of_nonneg_of_nonneg {a b : ℤ} (Ha : a ≥ 0) (Hb : b ≥ 0) : a div b ≤ a := obtain (m : ℕ) (Hm : a = m), from exists_eq_of_nat Ha, @@ -647,7 +647,7 @@ have H3 : a * c < (b div c + 1) * c, from a * c ≤ b : H2 ... = b div c * c + b mod c : eq_div_mul_add_mod ... < b div c * c + c : add_lt_add_left (!mod_lt_of_pos H1) - ... = (b div c + 1) * c : by rewrite [mul.right_distrib, one_mul], + ... = (b div c + 1) * c : by rewrite [right_distrib, one_mul], le_of_lt_add_one (lt_of_mul_lt_mul_right H3 (le_of_lt H1)) theorem le_div_iff_mul_le {a b c : ℤ} (H : c > 0) : a ≤ b div c ↔ a * c ≤ b := @@ -668,7 +668,7 @@ lt_of_mul_lt_mul_right theorem lt_mul_of_div_lt {a b c : ℤ} (H1 : c > 0) (H2 : a div c < b) : a < b * c := assert H3 : (a div c + 1) * c ≤ b * c, from !mul_le_mul_of_nonneg_right (add_one_le_of_lt H2) (le_of_lt H1), -have H4 : a div c * c + c ≤ b * c, by rewrite [mul.right_distrib at H3, one_mul at H3]; apply H3, +have H4 : a div c * c + c ≤ b * c, by rewrite [right_distrib at H3, one_mul at H3]; apply H3, calc a = a div c * c + a mod c : eq_div_mul_add_mod ... < a div c * c + c : add_lt_add_left (!mod_lt_of_pos H1) diff --git a/library/data/int/order.lean b/library/data/int/order.lean index baef16fe6..0d662d05e 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -44,7 +44,7 @@ theorem le.elim {a b : ℤ} (H : a ≤ b) : ∃n : ℕ, a + n = b := obtain (n : ℕ) (H1 : b - a = n), from nonneg.elim H, exists.intro n (!add.comm ▸ iff.mpr !add_eq_iff_eq_add_neg (H1⁻¹)) -theorem le.total (a b : ℤ) : a ≤ b ∨ b ≤ a := +protected theorem le_total (a b : ℤ) : a ≤ b ∨ b ≤ a := or.imp_right (assume H : nonneg (-(b - a)), have -(b - a) = a - b, from !neg_sub, @@ -67,7 +67,7 @@ theorem lt_add_succ (a : ℤ) (n : ℕ) : a < a + succ n := le.intro (show a + 1 + n = a + succ n, from calc a + 1 + n = a + (1 + n) : add.assoc - ... = a + (n + 1) : by rewrite (add.comm 1 n) + ... = a + (n + 1) : by rewrite (int.add_comm 1 n) ... = a + succ n : rfl) theorem lt.intro {a b : ℤ} {n : ℕ} (H : a + succ n = b) : a < b := @@ -77,7 +77,7 @@ theorem lt.elim {a b : ℤ} (H : a < b) : ∃n : ℕ, a + succ n = b := obtain (n : ℕ) (Hn : a + 1 + n = b), from le.elim H, have a + succ n = b, from calc - a + succ n = a + 1 + n : by rewrite [add.assoc, add.comm 1 n] + a + succ n = a + 1 + n : by rewrite [add.assoc, int.add_comm 1 n] ... = b : Hn, exists.intro n this @@ -96,10 +96,10 @@ iff.mpr !of_nat_lt_of_nat_iff H /- show that the integers form an ordered additive group -/ -theorem le.refl (a : ℤ) : a ≤ a := +protected theorem le_refl (a : ℤ) : a ≤ a := le.intro (add_zero a) -theorem le.trans {a b c : ℤ} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c := +protected theorem le_trans {a b c : ℤ} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c := obtain (n : ℕ) (Hn : a + n = b), from le.elim H1, obtain (m : ℕ) (Hm : b + m = c), from le.elim H2, have a + of_nat (n + m) = c, from @@ -110,7 +110,7 @@ have a + of_nat (n + m) = c, from ... = c : Hm, le.intro this -theorem le.antisymm : ∀ {a b : ℤ}, a ≤ b → b ≤ a → a = b := +protected theorem le_antisymm : ∀ {a b : ℤ}, a ≤ b → b ≤ a → a = b := take a b : ℤ, assume (H₁ : a ≤ b) (H₂ : b ≤ a), obtain (n : ℕ) (Hn : a + n = b), from le.elim H₁, obtain (m : ℕ) (Hm : b + m = a), from le.elim H₂, @@ -130,23 +130,23 @@ show a = b, from ... = a + n : by rewrite this ... = b : Hn -theorem lt.irrefl (a : ℤ) : ¬ a < a := +protected theorem lt_irrefl (a : ℤ) : ¬ a < a := (suppose a < a, obtain (n : ℕ) (Hn : a + succ n = a), from lt.elim this, have a + succ n = a + 0, from Hn ⬝ !add_zero⁻¹, !succ_ne_zero (of_nat.inj (add.left_cancel this))) -theorem ne_of_lt {a b : ℤ} (H : a < b) : a ≠ b := -(suppose a = b, absurd (this ▸ H) (lt.irrefl b)) +protected theorem ne_of_lt {a b : ℤ} (H : a < b) : a ≠ b := +(suppose a = b, absurd (this ▸ H) (int.lt_irrefl b)) theorem le_of_lt {a b : ℤ} (H : a < b) : a ≤ b := obtain (n : ℕ) (Hn : a + succ n = b), from lt.elim H, le.intro Hn -theorem lt_iff_le_and_ne (a b : ℤ) : a < b ↔ (a ≤ b ∧ a ≠ b) := +protected theorem lt_iff_le_and_ne (a b : ℤ) : a < b ↔ (a ≤ b ∧ a ≠ b) := iff.intro - (assume H, and.intro (le_of_lt H) (ne_of_lt H)) + (assume H, and.intro (le_of_lt H) (int.ne_of_lt H)) (assume H, have a ≤ b, from and.elim_left H, have a ≠ b, from and.elim_right H, @@ -155,7 +155,7 @@ iff.intro obtain (k : ℕ) (Hk : n = nat.succ k), from nat.exists_eq_succ_of_ne_zero this, lt.intro (Hk ▸ Hn)) -theorem le_iff_lt_or_eq (a b : ℤ) : a ≤ b ↔ (a < b ∨ a = b) := +protected theorem le_iff_lt_or_eq (a b : ℤ) : a ≤ b ↔ (a < b ∨ a = b) := iff.intro (assume H, by_cases @@ -168,12 +168,12 @@ iff.intro (assume H, or.elim H (assume H1, le_of_lt H1) - (assume H1, H1 ▸ !le.refl)) + (assume H1, H1 ▸ !int.le_refl)) theorem lt_succ (a : ℤ) : a < a + 1 := -le.refl (a + 1) +int.le_refl (a + 1) -theorem add_le_add_left {a b : ℤ} (H : a ≤ b) (c : ℤ) : c + a ≤ c + b := +protected theorem add_le_add_left {a b : ℤ} (H : a ≤ b) (c : ℤ) : c + a ≤ c + b := obtain (n : ℕ) (Hn : a + n = b), from le.elim H, have H2 : c + a + n = c + b, from calc @@ -181,13 +181,13 @@ have H2 : c + a + n = c + b, from ... = c + b : {Hn}, le.intro H2 -theorem add_lt_add_left {a b : ℤ} (H : a < b) (c : ℤ) : c + a < c + b := +protected theorem add_lt_add_left {a b : ℤ} (H : a < b) (c : ℤ) : c + a < c + b := let H' := le_of_lt H in -(iff.mpr (lt_iff_le_and_ne _ _)) (and.intro (add_le_add_left H' _) +(iff.mpr (int.lt_iff_le_and_ne _ _)) (and.intro (int.add_le_add_left H' _) (take Heq, let Heq' := add_left_cancel Heq in - !lt.irrefl (Heq' ▸ H))) + !int.lt_irrefl (Heq' ▸ H))) -theorem mul_nonneg {a b : ℤ} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a * b := +protected theorem mul_nonneg {a b : ℤ} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a * b := obtain (n : ℕ) (Hn : 0 + n = a), from le.elim Ha, obtain (m : ℕ) (Hm : 0 + m = b), from le.elim Hb, le.intro @@ -199,7 +199,7 @@ le.intro ... = n * m : by rewrite zero_add ... = 0 + n * m : by rewrite zero_add)) -theorem mul_pos {a b : ℤ} (Ha : 0 < a) (Hb : 0 < b) : 0 < a * b := +protected theorem mul_pos {a b : ℤ} (Ha : 0 < a) (Hb : 0 < b) : 0 < a * b := obtain (n : ℕ) (Hn : 0 + nat.succ n = a), from lt.elim Ha, obtain (m : ℕ) (Hm : 0 + nat.succ m = b), from lt.elim Hb, lt.intro @@ -214,45 +214,45 @@ lt.intro ... = of_nat (nat.succ (nat.succ n * m + n)) : by rewrite nat.add_succ ... = 0 + nat.succ (nat.succ n * m + n) : by rewrite zero_add)) -theorem zero_lt_one : (0 : ℤ) < 1 := trivial +protected theorem zero_lt_one : (0 : ℤ) < 1 := trivial -theorem not_le_of_gt {a b : ℤ} (H : a < b) : ¬ b ≤ a := +protected theorem not_le_of_gt {a b : ℤ} (H : a < b) : ¬ b ≤ a := assume Hba, - let Heq := le.antisymm (le_of_lt H) Hba in - !lt.irrefl (Heq ▸ H) + let Heq := int.le_antisymm (le_of_lt H) Hba in + !int.lt_irrefl (Heq ▸ H) -theorem lt_of_lt_of_le {a b c : ℤ} (Hab : a < b) (Hbc : b ≤ c) : a < c := +protected theorem lt_of_lt_of_le {a b c : ℤ} (Hab : a < b) (Hbc : b ≤ c) : a < c := let Hab' := le_of_lt Hab in - let Hac := le.trans Hab' Hbc in - (iff.mpr !lt_iff_le_and_ne) (and.intro Hac - (assume Heq, not_le_of_gt (Heq ▸ Hab) Hbc)) + let Hac := int.le_trans Hab' Hbc in + (iff.mpr !int.lt_iff_le_and_ne) (and.intro Hac + (assume Heq, int.not_le_of_gt (Heq ▸ Hab) Hbc)) -theorem lt_of_le_of_lt {a b c : ℤ} (Hab : a ≤ b) (Hbc : b < c) : a < c := +protected theorem lt_of_le_of_lt {a b c : ℤ} (Hab : a ≤ b) (Hbc : b < c) : a < c := let Hbc' := le_of_lt Hbc in - let Hac := le.trans Hab Hbc' in - (iff.mpr !lt_iff_le_and_ne) (and.intro Hac - (assume Heq, not_le_of_gt (Heq⁻¹ ▸ Hbc) Hab)) + let Hac := int.le_trans Hab Hbc' in + (iff.mpr !int.lt_iff_le_and_ne) (and.intro Hac + (assume Heq, int.not_le_of_gt (Heq⁻¹ ▸ Hbc) Hab)) protected definition linear_ordered_comm_ring [reducible] [trans_instance] : algebra.linear_ordered_comm_ring int := ⦃algebra.linear_ordered_comm_ring, int.integral_domain, le := int.le, - le_refl := le.refl, - le_trans := @le.trans, - le_antisymm := @le.antisymm, + le_refl := int.le_refl, + le_trans := @int.le_trans, + le_antisymm := @int.le_antisymm, lt := int.lt, - le_of_lt := @le_of_lt, - lt_irrefl := lt.irrefl, - lt_of_lt_of_le := @lt_of_lt_of_le, - lt_of_le_of_lt := @lt_of_le_of_lt, - add_le_add_left := @add_le_add_left, - mul_nonneg := @mul_nonneg, - mul_pos := @mul_pos, - le_iff_lt_or_eq := le_iff_lt_or_eq, - le_total := le.total, - zero_ne_one := zero_ne_one, - zero_lt_one := zero_lt_one, - add_lt_add_left := @add_lt_add_left⦄ + le_of_lt := @int.le_of_lt, + lt_irrefl := int.lt_irrefl, + lt_of_lt_of_le := @int.lt_of_lt_of_le, + lt_of_le_of_lt := @int.lt_of_le_of_lt, + add_le_add_left := @int.add_le_add_left, + mul_nonneg := @int.mul_nonneg, + mul_pos := @int.mul_pos, + le_iff_lt_or_eq := int.le_iff_lt_or_eq, + le_total := int.le_total, + zero_ne_one := int.zero_ne_one, + zero_lt_one := int.zero_lt_one, + add_lt_add_left := @int.add_lt_add_left⦄ protected definition decidable_linear_ordered_comm_ring [reducible] [instance] : algebra.decidable_linear_ordered_comm_ring int := @@ -387,7 +387,7 @@ theorem exists_least_of_bdd {P : ℤ → Prop} [HP : decidable_pred P] let Hzb' := lt_of_not_ge Hzb, let Hpos := iff.mpr !sub_pos_iff_lt Hzb', have Hzbk : z = b + of_nat (nat_abs (z - b)), - by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), int.add.comm, algebra.sub_add_cancel], + by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), int.add_comm, algebra.sub_add_cancel], have Hk : nat_abs (z - b) < least (λ n, P (b + of_nat n)) (nat.succ (nat_abs (elt - b))), begin let Hz' := iff.mp !lt_add_iff_sub_lt_left Hz, rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'], diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean index 8416abe7e..985f09633 100644 --- a/library/data/rat/basic.lean +++ b/library/data/rat/basic.lean @@ -158,12 +158,12 @@ theorem add_equiv_add {a1 b1 a2 b2 : prerat} (eqv1 : a1 ≡ a2) (eqv2 : b1 ≡ b calc (num a1 * denom b1 + num b1 * denom a1) * (denom a2 * denom b2) = num a1 * denom a2 * denom b1 * denom b2 + num b1 * denom b2 * denom a1 * denom a2 : - by rewrite [mul.right_distrib, *mul.assoc, mul.left_comm (denom b1), + by rewrite [right_distrib, *mul.assoc, mul.left_comm (denom b1), mul.comm (denom b2), *mul.assoc] ... = num a2 * denom a1 * denom b1 * denom b2 + num b2 * denom b1 * denom a1 * denom a2 : by rewrite [↑equiv at *, eqv1, eqv2] ... = (num a2 * denom b2 + num b2 * denom a2) * (denom a1 * denom b1) : - by rewrite [mul.right_distrib, *mul.assoc, *mul.left_comm (denom b2), + by rewrite [right_distrib, *mul.assoc, *mul.left_comm (denom b2), *mul.comm (denom b1), *mul.assoc, mul.left_comm (denom a2)] theorem mul_equiv_mul {a1 b1 a2 b2 : prerat} (eqv1 : a1 ≡ a2) (eqv2 : b1 ≡ b2) : @@ -215,8 +215,8 @@ theorem add.comm (a b : prerat) : add a b ≡ add b a := by rewrite [↑add, ↑equiv, ▸*, add.comm, mul.comm (denom a)] theorem add.assoc (a b c : prerat) : add (add a b) c ≡ add a (add b c) := -by rewrite [↑add, ↑equiv, ▸*, *(mul.comm (num c)), *(λy, mul.comm y (denom a)), *mul.left_distrib, - *mul.right_distrib, *mul.assoc, *add.assoc] +by rewrite [↑add, ↑equiv, ▸*, *(mul.comm (num c)), *(λy, mul.comm y (denom a)), *left_distrib, + *right_distrib, *mul.assoc, *add.assoc] theorem add_zero (a : prerat) : add a zero ≡ a := by rewrite [↑add, ↑equiv, ↑zero, ↑of_int, ▸*, *mul_one, zero_mul, add_zero] @@ -238,12 +238,12 @@ have H : smul (denom a) (mul a (add b c)) (denom_pos a) = add (mul a b) (mul a c), from begin rewrite[↑smul, ↑mul, ↑add], congruence, - rewrite[*mul.left_distrib, *mul.right_distrib, -*int.mul.assoc], + rewrite[*left_distrib, *right_distrib, -+(int.mul_assoc)], have T : ∀ {x y z w : ℤ}, x*y*z*w=y*z*x*w, from - λx y z w, (!int.mul.assoc ⬝ !int.mul.comm) ▸ rfl, + λx y z w, (!int.mul_assoc ⬝ !int.mul_comm) ▸ rfl, exact !congr_arg2 T T, rewrite [mul.left_comm (denom a) (denom b) (denom c)], - rewrite int.mul.assoc + rewrite int.mul_assoc end, equiv.symm (H ▸ smul_equiv (denom_pos a)) @@ -258,7 +258,7 @@ theorem mul_inv_cancel : ∀{a : prerat}, ¬ a ≡ zero → mul a (inv a) ≡ on mul a (inv a) ≡ mul a ia : mul_equiv_mul !equiv.refl (inv_of_neg an_neg adp) ... ≡ one : begin esimp [equiv, num, denom, one, mul, of_int], - rewrite [*int.mul_one, *int.one_mul, int.mul.comm, + rewrite [*int.mul_one, *int.one_mul, algebra.mul.comm, neg_mul_comm] end) (assume an_zero : an = 0, absurd (equiv_zero_of_num_eq_zero an_zero) H) @@ -268,7 +268,7 @@ theorem mul_inv_cancel : ∀{a : prerat}, ¬ a ≡ zero → mul a (inv a) ≡ on mul a (inv a) ≡ mul a ia : mul_equiv_mul !equiv.refl (inv_of_pos an_pos adp) ... ≡ one : begin esimp [equiv, num, denom, one, mul, of_int], - rewrite [*int.mul_one, *int.one_mul, int.mul.comm] + rewrite [*int.mul_one, *int.one_mul, algebra.mul.comm] end) theorem zero_not_equiv_one : ¬ zero ≡ one := @@ -306,8 +306,8 @@ theorem reduce_equiv : ∀ a : prerat, reduce a ≡ a (assume anz : an = 0, begin rewrite [↑reduce, if_pos anz, ↑equiv, anz], krewrite zero_mul end) (assume annz : an ≠ 0, - by rewrite [↑reduce, if_neg annz, ↑equiv, int.mul.comm, -!mul_div_assoc !gcd_dvd_left, - -!mul_div_assoc !gcd_dvd_right, int.mul.comm]) + by rewrite [↑reduce, if_neg annz, ↑equiv, algebra.mul.comm, -!mul_div_assoc !gcd_dvd_left, + -!mul_div_assoc !gcd_dvd_right, algebra.mul.comm]) theorem reduce_eq_reduce : ∀{a b : prerat}, a ≡ b → reduce a = reduce b | (mk an ad adpos) (mk bn bd bdpos) := @@ -331,7 +331,7 @@ theorem reduce_eq_reduce : ∀{a b : prerat}, a ≡ b → reduce a = reduce b {apply div_gcd_eq_div_gcd H adpos bdpos}, {esimp, rewrite [gcd.comm, gcd.comm bn], apply div_gcd_eq_div_gcd_of_nonneg, - rewrite [int.mul.comm, -H, int.mul.comm], + rewrite [algebra.mul.comm, -H, algebra.mul.comm], apply annz, apply bnnz, apply le_of_lt adpos, diff --git a/library/theories/number_theory/bezout.lean b/library/theories/number_theory/bezout.lean index 7d7f44a33..95c6257ea 100644 --- a/library/theories/number_theory/bezout.lean +++ b/library/theories/number_theory/bezout.lean @@ -66,7 +66,7 @@ gcd.induction x y rewrite [-of_nat_mod], rewrite [int.modulo.def], rewrite [+algebra.mul_sub_right_distrib], - rewrite [+algebra.mul_sub_left_distrib, *mul.left_distrib], + rewrite [+algebra.mul_sub_left_distrib, *left_distrib], rewrite [*sub_eq_add_neg, {pr₂ (egcd n (m mod n)) * of_nat m + - _}algebra.add.comm, -algebra.add.assoc], rewrite [algebra.mul.assoc] end) @@ -79,7 +79,7 @@ obtain a' b' (H : a' * nat_abs x + b' * nat_abs y = gcd x y), from !Bezout_aux, begin existsi (a' * sign x), existsi (b' * sign y), - rewrite [*int.mul.assoc, -*abs_eq_sign_mul, -*of_nat_nat_abs], + rewrite [*mul.assoc, -*abs_eq_sign_mul, -*of_nat_nat_abs], apply H end end Bezout @@ -99,7 +99,7 @@ decidable.by_cases have cpx : coprime p x, from coprime_of_prime_of_not_dvd pp this, obtain (a b : ℤ) (Hab : a * p + b * x = gcd p x), from Bezout_aux p x, assert a * p * y + b * x * y = y, - by rewrite [-int.mul.right_distrib, Hab, ↑coprime at cpx, cpx, int.one_mul], + by rewrite [-right_distrib, Hab, ↑coprime at cpx, cpx, int.one_mul], have p ∣ y, begin apply dvd_of_of_nat_dvd_of_nat, @@ -108,7 +108,7 @@ decidable.by_cases {apply dvd_mul_of_dvd_left, apply dvd_mul_of_dvd_right, apply dvd.refl}, - {rewrite int.mul.assoc, + {rewrite mul.assoc, apply dvd_mul_of_dvd_right, apply of_nat_dvd_of_nat_of_dvd H} end,