From 07b33ec75e1af045999dcb447d1aab3cbdc097be Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 9 Oct 2015 14:50:17 -0700 Subject: [PATCH] fix(library/data/int,library/data/rat): int and rat --- library/algebra/ring_power.lean | 9 ++++ library/data/int/basic.lean | 4 +- library/data/int/order.lean | 2 +- library/data/int/power.lean | 2 +- library/data/nat/basic.lean | 3 +- library/data/nat/order.lean | 2 +- library/data/rat/basic.lean | 6 +-- library/data/rat/order.lean | 6 +-- .../number_theory/irrational_roots.lean | 45 +++++++++---------- 9 files changed, 43 insertions(+), 36 deletions(-) diff --git a/library/algebra/ring_power.lean b/library/algebra/ring_power.lean index 126ca789a3..b8d3c26c1a 100644 --- a/library/algebra/ring_power.lean +++ b/library/algebra/ring_power.lean @@ -18,6 +18,9 @@ section semiring variable [s : semiring A] include s +definition semiring_has_pow_nat [reducible] [instance] : has_pow_nat A := +monoid_has_pow_nat + theorem zero_pow {m : ℕ} (mpos : m > 0) : 0^m = (0 : A) := have h₁ : ∀ m : nat, (0 : A)^(succ m) = (0 : A), begin @@ -34,6 +37,9 @@ section integral_domain variable [s : integral_domain A] include s +definition integral_domain_has_pow_nat [reducible] [instance] : has_pow_nat A := +monoid_has_pow_nat + theorem eq_zero_of_pow_eq_zero {a : A} {m : ℕ} (H : a^m = 0) : a = 0 := or.elim (eq_zero_or_pos m) (suppose m = 0, @@ -128,6 +134,9 @@ section decidable_linear_ordered_comm_ring variable [s : decidable_linear_ordered_comm_ring A] include s +definition decidable_linear_ordered_comm_ring_has_pow_nat [reducible] [instance] : has_pow_nat A := +monoid_has_pow_nat + theorem abs_pow (a : A) (n : ℕ) : abs (a^n) = abs a^n := begin induction n with n ih, diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 40bd598313..95e3c05261 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -107,7 +107,7 @@ private definition has_decidable_eq₂ : Π (a b : ℤ), decidable (a = b) | -[1+ m] -[1+ n] := if H : m = n then inl (congr_arg neg_succ_of_nat H) else inr (not.mto neg_succ_of_nat.inj H) -definition has_decidable_eq [instance] : decidable_eq ℤ := has_decidable_eq₂ +definition has_decidable_eq [instance] [priority int.prio] : decidable_eq ℤ := has_decidable_eq₂ theorem of_nat_add (n m : nat) : of_nat (n + m) = of_nat n + of_nat m := rfl @@ -501,7 +501,7 @@ theorem eq_zero_or_eq_zero_of_mul_eq_zero {a b : ℤ} (H : a * b = 0) : a = 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] [instance] : algebra.integral_domain int := +protected definition integral_domain [reducible] [trans_instance] : algebra.integral_domain int := ⦃algebra.integral_domain, add := int.add, add_assoc := add.assoc, diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 63f2623aee..9a745d7517 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -233,7 +233,7 @@ theorem lt_of_le_of_lt {a b c : ℤ} (Hab : a ≤ b) (Hbc : b < c) : a < c := (iff.mpr !lt_iff_le_and_ne) (and.intro Hac (assume Heq, not_le_of_gt (Heq⁻¹ ▸ Hbc) Hab)) -protected definition linear_ordered_comm_ring [reducible] [instance] : +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, diff --git a/library/data/int/power.lean b/library/data/int/power.lean index 60418e2cf7..3b19e7c898 100644 --- a/library/data/int/power.lean +++ b/library/data/int/power.lean @@ -10,7 +10,7 @@ import data.int.basic data.int.order data.int.div algebra.group_power data.nat.p namespace int open - [notations] algebra -definition int_has_pow_nat : has_pow_nat int := +definition int_has_pow_nat [reducible] [instance] [priority int.prio] : has_pow_nat int := has_pow_nat.mk has_pow_nat.pow_nat /- diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index 4cb8567867..d65258a293 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -290,9 +290,10 @@ nat.cases_on n !succ_ne_zero)) open - [notations] algebra -protected definition comm_semiring [reducible] [instance] : algebra.comm_semiring nat := +protected definition comm_semiring [reducible] [trans_instance] : algebra.comm_semiring nat := ⦃algebra.comm_semiring, add := nat.add, + add_assoc := add.assoc, zero := nat.zero, zero_add := zero_add, diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 40d9895ede..2c95f86b04 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -136,7 +136,7 @@ else (eq_max_left h) ▸ !le.refl open - [notations] algebra -protected definition decidable_linear_ordered_semiring [reducible] [instance] : +protected definition decidable_linear_ordered_semiring [reducible] [trans_instance] : algebra.decidable_linear_ordered_semiring nat := ⦃ algebra.decidable_linear_ordered_semiring, nat.comm_semiring, add_left_cancel := @add.cancel_left, diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean index 12bd48df9a..4cb65382ae 100644 --- a/library/data/rat/basic.lean +++ b/library/data/rat/basic.lean @@ -535,7 +535,7 @@ decidable.by_cases end)) -protected definition discrete_field [reducible] [instance] : algebra.discrete_field rat := +protected definition discrete_field [reducible] [trans_instance] : algebra.discrete_field rat := ⦃algebra.discrete_field, add := rat.add, add_assoc := add.assoc, @@ -560,10 +560,10 @@ protected definition discrete_field [reducible] [instance] : algebra.discrete_fi has_decidable_eq := has_decidable_eq⦄ definition rat_has_division [instance] [reducible] [priority rat.prio] : has_division rat := -has_division.mk algebra.division +has_division.mk has_division.division definition rat_has_pow_nat [instance] [reducible] [priority rat.prio] : has_pow_nat rat := -has_pow_nat.mk pow_nat +has_pow_nat.mk has_pow_nat.pow_nat theorem eq_num_div_denom (a : ℚ) : a = num a / denom a := have H : of_int (denom a) ≠ 0, from assume H', ne_of_gt (denom_pos a) (of_int.inj H'), diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean index 10c464d902..01625ad45f 100644 --- a/library/data/rat/order.lean +++ b/library/data/rat/order.lean @@ -302,7 +302,7 @@ let H' := le_of_lt H in (take Heq, let Heq' := add_left_cancel Heq in !lt_irrefl (Heq' ▸ H))) -protected definition discrete_linear_ordered_field [reducible] [instance] : +protected definition discrete_linear_ordered_field [reducible] [trans_instance] : algebra.discrete_linear_ordered_field rat := ⦃algebra.discrete_linear_ordered_field, rat.discrete_field, @@ -386,7 +386,7 @@ section rewrite [-mul_denom], apply mul_neg_of_neg_of_pos H, change of_int (denom q) > of_int 0, - rewrite [of_int_lt_of_int_iff], + xrewrite [of_int_lt_of_int_iff], exact !denom_pos end, show num q < 0, from lt_of_of_int_lt_of_int this @@ -397,7 +397,7 @@ section rewrite [-mul_denom], apply mul_nonpos_of_nonpos_of_nonneg H, change of_int (denom q) ≥ of_int 0, - rewrite [of_int_le_of_int_iff], + xrewrite [of_int_le_of_int_iff], exact int.le_of_lt !denom_pos end, show num q ≤ 0, from le_of_of_int_le_of_int this diff --git a/library/theories/number_theory/irrational_roots.lean b/library/theories/number_theory/irrational_roots.lean index 0c2fbef1ab..1f910df74f 100644 --- a/library/theories/number_theory/irrational_roots.lean +++ b/library/theories/number_theory/irrational_roots.lean @@ -38,26 +38,25 @@ section open nat decidable theorem root_irrational {a b c n : ℕ} (npos : n > 0) (apos : a > 0) (co : coprime a b) - (H : a^n = c * b^n) : - b = 1 := + (H : a^n = c * b^n) : b = 1 := have bpos : b > 0, from pos_of_ne_zero (suppose b = 0, have a^n = 0, by krewrite [H, this, zero_pow npos], assert a = 0, from eq_zero_of_pow_eq_zero this, - show false, from ne_of_lt `0 < a` this⁻¹), + show false, from ne_of_lt `0 < a` this⁻¹), have H₁ : ∀ p, prime p → ¬ p ∣ b, from take p, suppose prime p, suppose p ∣ b, - assert p ∣ b^n, from dvd_pow_of_dvd_of_pos `p ∣ b` `n > 0`, - have p ∣ a^n, by rewrite H; apply dvd_mul_of_dvd_right this, - have p ∣ a, from dvd_of_prime_of_dvd_pow `prime p` this, + assert p ∣ b^n, from dvd_pow_of_dvd_of_pos `p ∣ b` `n > 0`, + have p ∣ a^n, by rewrite H; apply dvd_mul_of_dvd_right this, + have p ∣ a, from dvd_of_prime_of_dvd_pow `prime p` this, have ¬ coprime a b, from not_coprime_of_dvd_of_dvd (gt_one_of_prime `prime p`) `p ∣ a` `p ∣ b`, - show false, from this `coprime a b`, - have blt2 : b < 2, from by_contradiction + show false, from this `coprime a b`, + have blt2 : b < 2, from by_contradiction (suppose ¬ b < 2, - have b ≥ 2, from le_of_not_gt this, + have b ≥ 2, from le_of_not_gt this, obtain p [primep pdvdb], from exists_prime_and_dvd this, - show false, from H₁ p primep pdvdb), - show b = 1, from (le.antisymm (le_of_lt_succ blt2) (succ_le_of_lt bpos)) + show false, from H₁ p primep pdvdb), + show b = 1, from (le.antisymm (le_of_lt_succ blt2) (succ_le_of_lt bpos)) end /- @@ -71,10 +70,10 @@ section theorem denom_eq_one_of_pow_eq {q : ℚ} {n : ℕ} {c : ℤ} (npos : n > 0) (H : q^n = c) : denom q = 1 := let a := num q, b := denom q in - have b ≠ 0, from ne_of_gt (denom_pos q), - have bnz : b ≠ (0 : ℚ), from assume H, `b ≠ 0` (of_int.inj H), - have bnnz : ((b : rat)^n ≠ 0), from assume bneqz, bnz (eq_zero_of_pow_eq_zero bneqz), - have a^n /[rat] b^n = c, using bnz, begin krewrite [*of_int_pow, -div_pow, -eq_num_div_denom, -H] end, + have b ≠ 0, from ne_of_gt (denom_pos q), + have bnz : b ≠ (0 : ℚ), from assume H, `b ≠ 0` (of_int.inj H), + have bnnz : ((b : rat)^n ≠ 0), from assume bneqz, bnz (algebra.eq_zero_of_pow_eq_zero bneqz), + have a^n /[rat] b^n = c, using bnz, begin rewrite [*of_int_pow, -algebra.div_pow, -eq_num_div_denom, -H] end, have (a^n : rat) = c *[rat] b^n, from eq.symm (!mul_eq_of_eq_div bnnz this⁻¹), have a^n = c * b^n, -- int version using this, by rewrite [-of_int_pow at this, -of_int_mul at this]; exact of_int.inj this, @@ -82,7 +81,7 @@ section using this, by rewrite [-abs_pow, this, abs_mul, abs_pow], have H₁ : (nat_abs a)^n = nat_abs c * (nat_abs b)^n, using this, - by apply int.of_nat.inj; rewrite [int.of_nat_mul, +int.of_nat_pow, +of_nat_nat_abs]; assumption, + begin apply int.of_nat.inj, rewrite [int.of_nat_mul, +int.of_nat_pow, +of_nat_nat_abs], exact this end, have H₂ : nat.coprime (nat_abs a) (nat_abs b), from of_nat.inj !coprime_num_denom, have nat_abs b = 1, from by_cases @@ -99,13 +98,11 @@ section show nat_abs b = 1, from (root_irrational npos (pos_of_ne_zero this) H₂ H₁)), show b = 1, using this, by rewrite [-of_nat_nat_abs_of_nonneg (le_of_lt !denom_pos), this] - exit - theorem eq_num_pow_of_pow_eq {q : ℚ} {n : ℕ} {c : ℤ} (npos : n > 0) (H : q^n = c) : c = (num q)^n := have denom q = 1, from denom_eq_one_of_pow_eq npos H, - have of_int c = (num q)^n, using this, - by rewrite [-H, eq_num_div_denom q at {1}, this, div_one, of_int_pow], + have of_int c = of_int ((num q)^n), using this, + by krewrite [-H, eq_num_div_denom q at {1}, this, div_one, of_int_pow], show c = (num q)^n , from of_int.inj this end @@ -121,11 +118,11 @@ section (suppose p = 0, show false, by let H := (pos_of_prime primep); rewrite this at H; exfalso; exact !lt.irrefl H), - have agtz : a > 0, from pos_of_ne_zero + assert agtz : a > 0, from pos_of_ne_zero (suppose a = 0, - show false, using npos pnez, by revert peq; rewrite [this, zero_pow npos]; exact pnez), + show false, using npos pnez, by revert peq; krewrite [this, zero_pow npos]; exact pnez), have n * mult p a = 1, from calc - n * mult p a = mult p (a^n) : using agtz, by rewrite [mult_pow n agtz primep] + n * mult p a = mult p (a^n) : begin krewrite [mult_pow n agtz primep] end ... = mult p p : peq ... = 1 : mult_self (gt_one_of_prime primep), have n ∣ 1, from dvd_of_mul_right_eq this, @@ -163,7 +160,7 @@ section have a * a = c * b * b, by rewrite -mul.assoc at H; apply H, have a div (gcd a b) = c * b div gcd (c * b) a, from div_gcd_eq_div_gcd this bpos apos, have a = c * b div gcd c a, - using this, by revert this; rewrite [↑coprime at co, co, div_one, H₁]; intros; assumption, + using this, by revert this; krewrite [↑coprime at co, co, int.div_one, H₁]; intros; assumption, have a = b * (c div gcd c a), using this, by revert this; rewrite [mul.comm, !mul_div_assoc !gcd_dvd_left]; intros; assumption,