diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 7a4f5ff821..c62089bd8c 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -326,7 +326,8 @@ theorem eq_zero_or_eq_zero_of_mul_eq_zero {A : Type} [s : no_zero_divisors A] {a (H : a * b = 0) : a = 0 ∨ b = 0 := !no_zero_divisors.eq_zero_or_eq_zero_of_mul_eq_zero H -structure integral_domain [class] (A : Type) extends comm_ring A, no_zero_divisors A +structure integral_domain [class] (A : Type) extends comm_ring A, no_zero_divisors A, + zero_ne_one_class A section variables [s : integral_domain A] (a b c d e : A) diff --git a/library/algebra/ring_power.lean b/library/algebra/ring_power.lean index 9a0a49df2d..b011cc5bbc 100644 --- a/library/algebra/ring_power.lean +++ b/library/algebra/ring_power.lean @@ -3,17 +3,57 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Jeremy Avigad -Properties of the power operation in an ordered ring. +Properties of the power operation in an ordered ring or field. (Right now, this file is just a stub. More soon.) -/ -import .group_power +import .group_power .ordered_field open nat namespace algebra variable {A : Type} +section semiring +variable [s : semiring A] +include s + +theorem zero_pow {m : ℕ} (mpos : m > 0) : 0^m = (0 : A) := +have h₁ : ∀ m, 0^succ m = (0 : A), + from take m, nat.induction_on m + (show 0^1 = 0, by rewrite pow_one) + (take m, suppose 0^(succ m) = 0, + show 0^(succ (succ m)) = 0, from !zero_mul), +obtain m' (h₂ : m = succ m'), from exists_eq_succ_of_pos mpos, +show 0^m = 0, by rewrite h₂; apply h₁ + +end semiring + +section integral_domain +variable [s : integral_domain A] +include s + +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, + by rewrite [`m = 0` at H, pow_zero at H]; apply absurd H (ne.symm zero_ne_one)) + (suppose m > 0, + have h₁ : ∀ m, a^succ m = 0 → a = 0, + begin + intro m, + induction m with m ih, + {rewrite pow_one; intros; assumption}, + rewrite pow_succ, + intro H, + cases eq_zero_or_eq_zero_of_mul_eq_zero H with h₃ h₄, + assumption, + exact ih h₄ + end, + obtain m' (h₂ : m = succ m'), from exists_eq_succ_of_pos `m > 0`, + show a = 0, by rewrite h₂ at H; apply h₁ m' H) + +end integral_domain + section linear_ordered_semiring variable [s : linear_ordered_semiring A] include s @@ -27,14 +67,14 @@ end theorem pow_nonneg_of_nonneg {x : A} (i : ℕ) (H : x ≥ 0) : x^i ≥ 0 := begin - induction i with [j, ih], + induction i with j ih, {show (1 : A) ≥ 0, from le_of_lt zero_lt_one}, {show x^(succ j) ≥ 0, from mul_nonneg H ih} end theorem pow_le_pow_of_le {x y : A} (i : ℕ) (H₁ : 0 ≤ x) (H₂ : x ≤ y) : x^i ≤ y^i := begin - induction i with [i, ih], + induction i with i ih, {rewrite *pow_zero, apply le.refl}, rewrite *pow_succ, have H : 0 ≤ x^i, from pow_nonneg_of_nonneg i H₁, @@ -45,8 +85,6 @@ theorem pow_ge_one {x : A} (i : ℕ) (xge1 : x ≥ 1) : x^i ≥ 1 := assert H : x^i ≥ 1^i, from pow_le_pow_of_le i (le_of_lt zero_lt_one) xge1, by rewrite one_pow at H; exact H -set_option formatter.hide_full_terms false - theorem pow_gt_one {x : A} {i : ℕ} (xgt1 : x > 1) (ipos : i > 0) : x^i > 1 := assert xpos : x > 0, from lt.trans zero_lt_one xgt1, begin @@ -60,4 +98,31 @@ end end linear_ordered_semiring +section decidable_linear_ordered_comm_ring +variable [s : decidable_linear_ordered_comm_ring A] +include s + +theorem abs_pow (a : A) (n : ℕ) : abs (a^n) = abs a^n := +begin + induction n with n ih, + rewrite [*pow_zero, (abs_of_nonneg zero_le_one : abs (1 : A) = 1)], + rewrite [*pow_succ, abs_mul, ih] +end + +end decidable_linear_ordered_comm_ring + +section discrete_field +variable [s : discrete_field A] +include s + +theorem div_pow (a : A) {b : A} {n : ℕ} (bnz : b ≠ 0) : (a / b)^n = a^n / b^n := +begin + induction n with n ih, + rewrite [*pow_zero, div_one], + have bnnz : b^n ≠ 0, from suppose b^n = 0, bnz (eq_zero_of_pow_eq_zero this), + rewrite [*pow_succ, ih, div_mul_div bnz bnnz] +end + +end discrete_field + end algebra diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index a4773c0e5f..74737951d0 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -126,7 +126,7 @@ definition nat_abs (a : ℤ) : ℕ := int.cases_on a function.id succ theorem nat_abs_of_nat (n : ℕ) : nat_abs n = n := rfl -theorem nat_abs_eq_zero : Π {a : ℤ}, nat_abs a = 0 → a = 0 +theorem eq_zero_of_nat_abs_eq_zero : Π {a : ℤ}, nat_abs a = 0 → a = 0 | (of_nat m) H := congr_arg of_nat H | -[1+ m'] H := absurd H !succ_ne_zero @@ -375,7 +375,7 @@ calc theorem nat_abs_add_le (a b : ℤ) : nat_abs (a + b) ≤ nat_abs a + nat_abs b := calc - nat_abs (a + b) = pabs (repr (a + b)) : nat_abs_eq_pabs_repr + nat_abs (a + b) = pabs (repr (a + b)) : nat_abs_eq_pabs_repr ... = pabs (padd (repr a) (repr b)) : pabs_congr !repr_add ... ≤ pabs (repr a) + pabs (repr b) : dist_add_add_le_add_dist_dist ... = pabs (repr a) + nat_abs b : nat_abs_eq_pabs_repr @@ -469,7 +469,7 @@ theorem one_mul (a : ℤ) : 1 * a = a := mul.comm a 1 ▸ 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) = + ((a1+b1)*c1+(a2+b2)*c2, (a1+b1)*c2+(a2+b2)*c1) = (a1*c1+a2*c2+(b1*c1+b2*c2), a1*c2+a2*c1+(b1*c2+b2*c1)) := by rewrite[+mul.right_distrib] ⬝ (!congr_arg2 !add.comm4 !add.comm4) @@ -494,7 +494,8 @@ 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 := -or.imp nat_abs_eq_zero nat_abs_eq_zero (eq_zero_or_eq_zero_of_mul_eq_zero (H ▸ (nat_abs_mul a b)⁻¹)) +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 (H ▸ (nat_abs_mul a b)⁻¹)) section migrate_algebra open [classes] algebra @@ -517,6 +518,7 @@ section migrate_algebra 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⦄ local attribute int.integral_domain [instance] @@ -526,7 +528,7 @@ section migrate_algebra notation [priority int.prio] a ∣ b := dvd a b migrate from algebra with int - replacing sub → sub, dvd → dvd + replacing sub → sub, dvd → dvd end migrate_algebra /- additional properties -/ diff --git a/library/data/int/div.lean b/library/data/int/div.lean index b5a8bacee2..d23eef5844 100644 --- a/library/data/int/div.lean +++ b/library/data/int/div.lean @@ -581,6 +581,18 @@ decidable.by_cases have abs a ∣ a, from abs_dvd_of_dvd !dvd.refl, eq.symm (iff.mpr (!div_eq_iff_eq_mul_left `abs a ≠ 0` this) !eq_sign_mul_abs)) +theorem le_of_dvd {a b : ℤ} (bpos : b > 0) (H : a ∣ b) : a ≤ b := +or.elim !le_or_gt + (suppose a ≤ 0, le.trans this (le_of_lt bpos)) + (suppose a > 0, + obtain c (Hc : b = a * c), from exists_eq_mul_right_of_dvd H, + have a * c > 0, by rewrite -Hc; exact bpos, + have c > 0, from int.pos_of_mul_pos_left this (le_of_lt `a > 0`), + show a ≤ b, from calc + a = a * 1 : mul_one + ... ≤ a * c : mul_le_mul_of_nonneg_left (add_one_le_of_lt `c > 0`) (le_of_lt `a > 0`) + ... = b : Hc) + /- div and ordering -/ theorem div_mul_le (a : ℤ) {b : ℤ} (H : b ≠ 0) : a div b * b ≤ a := diff --git a/library/data/int/gcd.lean b/library/data/int/gcd.lean index e9ae3449fb..502c00bb09 100644 --- a/library/data/int/gcd.lean +++ b/library/data/int/gcd.lean @@ -42,7 +42,7 @@ theorem gcd_abs_abs (a b : ℤ) : gcd (abs a) (abs b) = gcd a b := by rewrite [↑gcd, *nat_abs_abs] theorem gcd_of_ne_zero (a : ℤ) {b : ℤ} (H : b ≠ 0) : gcd a b = gcd b (abs a mod abs b) := -have nat_abs b ≠ nat.zero, from assume H', H (nat_abs_eq_zero H'), +have nat_abs b ≠ nat.zero, from assume H', H (eq_zero_of_nat_abs_eq_zero H'), have (#nat nat_abs b > nat.zero), from nat.pos_of_ne_zero this, assert nat.gcd (nat_abs a) (nat_abs b) = (#nat nat.gcd (nat_abs b) (nat_abs a mod nat_abs b)), from @nat.gcd_of_pos (nat_abs a) (nat_abs b) this, @@ -284,6 +284,14 @@ calc = gcd a b div abs (gcd a b) : gcd_div !gcd_dvd_left !gcd_dvd_right ... = 1 : by rewrite [abs_of_nonneg !gcd_nonneg, div_self H] +theorem not_coprime_of_dvd_of_dvd {m n d : ℤ} (dgt1 : d > 1) (Hm : d ∣ m) (Hn : d ∣ n) : + ¬ coprime m n := +assume co : coprime m n, +assert d ∣ gcd m n, from dvd_gcd Hm Hn, +have d ∣ 1, by rewrite [↑coprime at co, co at this]; apply this, +have d ≤ 1, from le_of_dvd dec_trivial this, +show false, from not_lt_of_ge `d ≤ 1` `d > 1` + theorem exists_coprime {a b : ℤ} (H : gcd a b ≠ 0) : exists a' b', coprime a' b' ∧ a = a' * gcd a b ∧ b = b' * gcd a b := have H1 : a = (a div gcd a b) * gcd a b, from (div_mul_cancel !gcd_dvd_left)⁻¹, diff --git a/library/data/int/order.lean b/library/data/int/order.lean index b081aed7cb..8916e98231 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -267,9 +267,9 @@ section migrate_algebra definition ge [reducible] (a b : ℤ) := algebra.has_le.ge a b definition gt [reducible] (a b : ℤ) := algebra.has_lt.gt a b - infix >= := int.ge - infix ≥ := int.ge - infix > := int.gt + infix [priority int.prio] >= := int.ge + infix [priority int.prio] ≥ := int.ge + infix [priority int.prio] > := int.gt definition decidable_ge [instance] (a b : ℤ) : decidable (a ≥ b) := show decidable (b ≤ a), from _ definition decidable_gt [instance] (a b : ℤ) : decidable (a > b) := @@ -280,7 +280,7 @@ section migrate_algebra definition sign : ℤ → ℤ := algebra.sign migrate from algebra with int - replacing has_le.ge → ge, has_lt.gt → gt, dvd → dvd, sub → sub, min → min, max → max, + replacing dvd → dvd, sub → sub, has_le.ge → ge, has_lt.gt → gt, min → min, max → max, abs → abs, sign → sign attribute le.trans ge.trans lt.trans gt.trans [trans] diff --git a/library/data/int/power.lean b/library/data/int/power.lean index dcfd2a8378..3dcb7748ec 100644 --- a/library/data/int/power.lean +++ b/library/data/int/power.lean @@ -5,7 +5,7 @@ Author: Jeremy Avigad The power function on the integers. -/ -import data.int.basic data.int.order data.int.div algebra.group_power +import data.int.basic data.int.order data.int.div algebra.group_power data.nat.power namespace int @@ -18,13 +18,27 @@ section migrate_algebra definition pow (a : ℤ) (n : ℕ) : ℤ := algebra.pow a n infix [priority int.prio] ^ := pow + definition nmul (n : ℕ) (a : ℤ) : ℤ := algebra.nmul n a + infix [priority int.prio] `⬝` := nmul + definition imul (i : ℤ) (a : ℤ) : ℤ := algebra.imul i a migrate from algebra with int - replacing dvd → dvd, has_le.ge → ge, has_lt.gt → gt, pow → pow + replacing dvd → dvd, sub → sub, has_le.ge → ge, has_lt.gt → gt, min → min, max → max, + abs → abs, sign → sign, pow → pow, nmul → nmul, imul → imul hiding add_pos_of_pos_of_nonneg, add_pos_of_nonneg_of_pos, add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg, le_add_of_nonneg_of_le, le_add_of_le_of_nonneg, lt_add_of_nonneg_of_lt, lt_add_of_lt_of_nonneg, lt_of_mul_lt_mul_left, lt_of_mul_lt_mul_right, pos_of_mul_pos_left, pos_of_mul_pos_right end migrate_algebra +section + open nat + theorem of_nat_pow (a n : ℕ) : of_nat (a^n) = (of_nat a)^n := + begin + induction n with n ih, + apply eq.refl, + rewrite [pow_succ, nat.pow_succ, of_nat_mul, ih] + end +end + end int diff --git a/library/data/nat/gcd.lean b/library/data/nat/gcd.lean index 82164cf081..f3e07ca5ce 100644 --- a/library/data/nat/gcd.lean +++ b/library/data/nat/gcd.lean @@ -300,6 +300,14 @@ calc gcd (m div gcd m n) (n div gcd m n) = gcd m n div gcd m n : gcd_div !gcd_dvd_left !gcd_dvd_right ... = 1 : div_self H +theorem not_coprime_of_dvd_of_dvd {m n d : ℕ} (dgt1 : d > 1) (Hm : d ∣ m) (Hn : d ∣ n) : + ¬ coprime m n := +assume co : coprime m n, +assert d ∣ gcd m n, from dvd_gcd Hm Hn, +have d ∣ 1, by rewrite [↑coprime at co, co at this]; apply this, +have d ≤ 1, from le_of_dvd dec_trivial this, +show false, from not_lt_of_ge `d ≤ 1` `d > 1` + theorem exists_coprime {m n : ℕ} (H : gcd m n > 0) : exists m' n', coprime m' n' ∧ m = m' * gcd m n ∧ n = n' * gcd m n := have H1 : m = (m div gcd m n) * gcd m n, from (div_mul_cancel !gcd_dvd_left)⁻¹, diff --git a/library/data/nat/parity.lean b/library/data/nat/parity.lean index 2d5e2e7ea5..663dd99136 100644 --- a/library/data/nat/parity.lean +++ b/library/data/nat/parity.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura Parity -/ -import data.nat.div logic.identities +import data.nat.power logic.identities namespace nat open decidable @@ -229,6 +229,32 @@ suppose odd (n * n), have even (n * n), from !even_mul_of_even_left this, show false, from `odd (n * n)` this +lemma odd_pow {n m} (h : odd n) : odd (n^m) := +nat.induction_on m + (show odd (n^0), from dec_trivial) + (take m, suppose odd (n^m), + show odd (n^(m+1)), from odd_mul_of_odd_of_odd h this) + +lemma even_pow {n m} (mpos : m > 0) (h : even n) : even (n^m) := +have h₁ : ∀ m, even (n^succ m), + from take m, nat.induction_on m + (show even (n^1), by rewrite pow_one; apply h) + (take m, suppose even (n^succ m), + show even (n^(succ (succ m))), from !even_mul_of_even_left h), +obtain m' (h₂ : m = succ m'), from exists_eq_succ_of_pos mpos, +show even (n^m), by rewrite h₂; apply h₁ + +lemma odd_of_odd_pow {n m} (mpos : m > 0) (h : odd (n^m)) : odd n := +suppose even n, +have even (n^m), from even_pow mpos this, +show false, from `odd (n^m)` this + +lemma even_of_even_pow {n m} (h : even (n^m)) : even n := +by_contradiction + (suppose odd n, + have odd (n^m), from odd_pow this, + show false, from this `even (n^m)`) + lemma eq_of_div2_of_even {n m : nat} : n div 2 = m div 2 → (even n ↔ even m) → n = m := assume h₁ h₂, or.elim (em (even n)) diff --git a/library/data/nat/power.lean b/library/data/nat/power.lean index 5487455a7f..e794585f56 100644 --- a/library/data/nat/power.lean +++ b/library/data/nat/power.lean @@ -29,6 +29,25 @@ section migrate_algebra pow_nonneg_of_nonneg end migrate_algebra +theorem eq_zero_of_pow_eq_zero {a m : ℕ} (H : a^m = 0) : a = 0 := +or.elim (eq_zero_or_pos m) + (suppose m = 0, + by rewrite [`m = 0` at H, pow_zero at H]; contradiction) + (suppose m > 0, + have h₁ : ∀ m, a^succ m = 0 → a = 0, + begin + intro m, + induction m with m ih, + {rewrite pow_one; intros; assumption}, + rewrite pow_succ, + intro H, + cases eq_zero_or_eq_zero_of_mul_eq_zero H with h₃ h₄, + assumption, + exact ih h₄ + end, + obtain m' (h₂ : m = succ m'), from exists_eq_succ_of_pos `m > 0`, + show a = 0, by rewrite h₂ at H; apply h₁ m' H) + -- generalize to semirings? theorem le_pow_self {x : ℕ} (H : x > 1) : ∀ i, i ≤ x^i | 0 := !zero_le diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean index 60079e6f8b..b584aaa01f 100644 --- a/library/data/rat/basic.lean +++ b/library/data/rat/basic.lean @@ -533,9 +533,12 @@ section migrate_algebra definition pow (a : ℚ) (n : ℕ) : ℚ := algebra.pow a n infix [priority rat.prio] ^ := pow + definition nmul (n : ℕ) (a : ℚ) : ℚ := algebra.nmul n a + infix [priority rat.prio] `⬝` := nmul + definition imul (i : ℤ) (a : ℚ) : ℚ := algebra.imul i a migrate from algebra with rat - replacing sub → rat.sub, divide → divide, dvd → dvd, pow → pow + replacing sub → rat.sub, divide → divide, dvd → dvd, pow → pow, nmul → nmul, imul → imul end migrate_algebra @@ -555,4 +558,11 @@ decidable.by_cases by rewrite [Hc, !int.mul_div_cancel_left bnz, mul.comm]), iff.mpr (eq_div_iff_mul_eq bnz') H') +theorem of_int_pow (a : ℤ) (n : ℕ) : of_int (a^n) = (of_int a)^n := +begin + induction n with n ih, + apply eq.refl, + rewrite [pow_succ, int.pow_succ, of_int_mul, ih] +end + end rat diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean index 751eba0b4a..3ffb228165 100644 --- a/library/data/rat/order.lean +++ b/library/data/rat/order.lean @@ -228,7 +228,7 @@ iff.intro (suppose a < b, and.left (iff.mp !lt_iff_le_and_ne this)) (suppose a = b, this ▸ !le.refl)) -theorem to_nonneg : a ≥ 0 → nonneg a := +private theorem to_nonneg : a ≥ 0 → nonneg a := by intros; rewrite -sub_zero; eassumption theorem add_le_add_left (H : a ≤ b) (c : ℚ) : c + a ≤ c + b := @@ -240,7 +240,7 @@ theorem mul_nonneg (H1 : a ≥ (0 : ℚ)) (H2 : b ≥ (0 : ℚ)) : a * b ≥ (0 have nonneg (a * b), from nonneg_mul (to_nonneg H1) (to_nonneg H2), !sub_zero⁻¹ ▸ this -theorem to_pos : a > 0 → pos a := +private theorem to_pos : a > 0 → pos a := by intros; rewrite -sub_zero; eassumption theorem mul_pos (H1 : a > (0 : ℚ)) (H2 : b > (0 : ℚ)) : a * b > (0 : ℚ) := @@ -314,8 +314,9 @@ section migrate_algebra definition sign : ℚ → ℚ := algebra.sign migrate from algebra with rat - replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, dvd → dvd, - divide → divide, max → max, min → min, abs → abs, sign → sign + replacing sub → sub, dvd → dvd, has_le.ge → ge, has_lt.gt → gt, + divide → divide, max → max, min → min, abs → abs, sign → sign, + nmul → nmul, imul → imul attribute le.trans lt.trans lt_of_lt_of_le lt_of_le_of_lt ge.trans gt.trans gt_of_gt_of_ge gt_of_ge_of_gt [trans] @@ -328,6 +329,52 @@ int.induction_on a (take b, abs_of_nonneg (!of_nat_nonneg)) (take b, by rewrite [this, abs_neg, abs_of_nonneg (!of_nat_nonneg)]) +section + open int + + set_option pp.coercions true + + theorem num_nonneg_of_nonneg {q : ℚ} (H : q ≥ 0) : num q ≥ 0 := + have of_int (num q) ≥ of_int 0, + begin + rewrite [-mul_denom], + apply mul_nonneg H, + rewrite [of_int_le_of_int], + exact int.le_of_lt !denom_pos + end, + show num q ≥ 0, from iff.mp !of_int_le_of_int this + + theorem num_pos_of_pos {q : ℚ} (H : q > 0) : num q > 0 := + have of_int (num q) > of_int 0, + begin + rewrite [-mul_denom], + apply mul_pos H, + rewrite [of_int_lt_of_int], + exact !denom_pos + end, + show num q > 0, from iff.mp !of_int_lt_of_int this + + theorem num_neg_of_neg {q : ℚ} (H : q < 0) : num q < 0 := + have of_int (num q) < of_int 0, + begin + rewrite [-mul_denom], + apply mul_neg_of_neg_of_pos H, + rewrite [of_int_lt_of_int], + exact !denom_pos + end, + show num q < 0, from iff.mp !of_int_lt_of_int this + + theorem num_nonpos_of_nonpos {q : ℚ} (H : q ≤ 0) : num q ≤ 0 := + have of_int (num q) ≤ of_int 0, + begin + rewrite [-mul_denom], + apply mul_nonpos_of_nonpos_of_nonneg H, + rewrite [of_int_le_of_int], + exact int.le_of_lt !denom_pos + end, + show num q ≤ 0, from iff.mp !of_int_le_of_int this +end + definition ubound : ℚ → ℕ := λ a : ℚ, nat.succ (int.nat_abs (num a)) theorem ubound_ge (a : ℚ) : of_nat (ubound a) ≥ a := diff --git a/library/data/real/division.lean b/library/data/real/division.lean index 3b3c6d6f13..b91cdfb364 100644 --- a/library/data/real/division.lean +++ b/library/data/real/division.lean @@ -647,7 +647,7 @@ section migrate_algebra migrate from algebra with real replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, abs → abs, sign → sign, dvd → dvd, - divide → divide, max → max, min → min + divide → divide, max → max, min → min, pow → pow, nmul → nmul, imul → imul end migrate_algebra infix / := divide diff --git a/library/data/real/order.lean b/library/data/real/order.lean index b5e62b87b3..627b324832 100644 --- a/library/data/real/order.lean +++ b/library/data/real/order.lean @@ -1122,9 +1122,15 @@ section migrate_algebra infix [priority real.prio] - := real.sub definition dvd (a b : ℝ) : Prop := algebra.dvd a b notation [priority real.prio] a ∣ b := real.dvd a b + definition pow (a : ℝ) (n : ℕ) : ℝ := algebra.pow a n + notation [priority real.prio] a^n := real.pow a n + definition nmul (n : ℕ) (a : ℝ) : ℝ := algebra.nmul n a + infix [priority real.prio] `⬝` := nmul + definition imul (i : ℤ) (a : ℝ) : ℝ := algebra.imul i a migrate from algebra with real - replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, dvd → dvd, divide → divide + replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, dvd → dvd, divide → divide, + pow → pow, nmul → nmul, imul → imul attribute le.trans lt.trans lt_of_lt_of_le lt_of_le_of_lt ge.trans gt.trans gt_of_gt_of_ge gt_of_ge_of_gt [trans] diff --git a/library/theories/number_theory/irrational_roots.lean b/library/theories/number_theory/irrational_roots.lean new file mode 100644 index 0000000000..d291f1c11d --- /dev/null +++ b/library/theories/number_theory/irrational_roots.lean @@ -0,0 +1,165 @@ +/- +Copyright (c) 2015 Jeremy Avigad. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Jeremy Avigad + +A proof that if n > 1 and a > 0, then the nth root of a is irrational, unless a is a perfect nth power. +-/ +import data.rat .prime_factorization +open eq.ops + +/- First, a textbook proof that sqrt 2 is irrational. -/ + +section + open nat + + theorem sqrt_two_irrational {a b : ℕ} (co : coprime a b) : a^2 ≠ 2 * b^2 := + assume H : a^2 = 2 * b^2, + have even (a^2), from even_of_exists (exists.intro _ H), + have even a, from even_of_even_pow this, + obtain c (aeq : a = 2 * c), from exists_of_even this, + have 2 * (2 * c^2) = 2 * b^2, by rewrite [-H, aeq, *pow_two, mul.assoc, mul.left_comm c], + have 2 * c^2 = b^2, from eq_of_mul_eq_mul_left dec_trivial this, + have even (b^2), from even_of_exists (exists.intro _ (eq.symm this)), + have even b, from even_of_even_pow this, + have 2 ∣ gcd a b, from dvd_gcd (dvd_of_even `even a`) (dvd_of_even `even b`), + have 2 ∣ 1, from co ▸ this, + absurd `2 ∣ 1` dec_trivial +end + +/- + Replacing 2 by an arbitrary prime and the power 2 by any n ≥ 1 yields the stronger result + that the nth root of an integer is irrational, unless the integer is already a perfect nth + power. +-/ + +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 := + have bpos : b > 0, from pos_of_ne_zero + (suppose b = 0, + have a^n = 0, by rewrite [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⁻¹), + 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, + 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 b < 2, from by_contradiction + (suppose ¬ b < 2, + 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 `b < 2`) (succ_le_of_lt `b > 0`)) +end + +/- + Here we state this in terms of the rationals, ℚ. The main difficulty is casting between ℕ, ℤ, + and ℚ. +-/ + +section + open rat int nat decidable + + 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 : (#rat b^n ≠ 0), from assume bneqz, bnz (eq_zero_of_pow_eq_zero bneqz), + have a^n / b^n = c, using bnz, by rewrite [*of_int_pow, -(!div_pow bnz), -eq_num_div_denom, -H], + have a^n = c * 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, + have (abs a)^n = abs c * (abs b)^n, + using this, by rewrite [-int.abs_pow, this, int.abs_mul, int.abs_pow], + have H₁ : (nat_abs a)^n = nat_abs c * (nat_abs b)^n, + using this, + by apply of_nat.inj; rewrite [int.of_nat_mul, +of_nat_pow, +of_nat_nat_abs]; assumption, + 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 + (suppose q = 0, by rewrite this) + (suppose q ≠ 0, + have a ≠ 0, from suppose a = 0, `q ≠ 0` (by rewrite [eq_num_div_denom, `a = 0`, zero_div]), + have nat_abs a ≠ 0, from suppose nat_abs a = 0, `a ≠ 0` (eq_zero_of_nat_abs_eq_zero this), + 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] + + 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], + show c = (num q)^n , from of_int.inj this +end + +/- As a corollary, for n > 1, the nth root of a prime is irrational. -/ + +section + open nat + + theorem not_eq_pow_of_prime {p n : ℕ} (a : ℕ) (ngt1 : n > 1) (primep : prime p) : p ≠ a^n := + assume peq : p = a^n, + have npos : n > 0, from lt.trans dec_trivial ngt1, + have pnez : p ≠ 0, from + (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 + (suppose a = 0, + show false, using npos pnez, by revert peq; rewrite [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] + ... = mult p p : peq + ... = 1 : mult_self (gt_one_of_prime primep), + have n ∣ 1, from dvd_of_mul_right_eq this, + have n = 1, from eq_one_of_dvd_one this, + show false, using this, by rewrite this at ngt1; exact !lt.irrefl ngt1 + + open int rat + + theorem root_prime_irrational {p n : ℕ} {q : ℚ} (qnonneg : q ≥ 0) (ngt1 : n > 1) + (primep : prime p) : + q^n ≠ p := + have numq : num q ≥ 0, from num_nonneg_of_nonneg qnonneg, + have npos : n > 0, from lt.trans dec_trivial ngt1, + suppose q^n = p, + have p = (num q)^n, from eq_num_pow_of_pow_eq npos this, + have p = (nat_abs (num q))^n, using this numq, + by apply of_nat.inj; rewrite [this, of_nat_pow, of_nat_nat_abs_of_nonneg numq], + show false, from not_eq_pow_of_prime _ ngt1 primep this +end + +/- + Thaetetus, who lives in the fourth century BC, is said to have proved the irrationality of square + roots up to seventeen. In Chapter 4 of /Why Prove it Again/, John Dawson notes that Thaetetus may + have used an approach similar to the one below. (See data/nat/gcd.lean for the key theorem, + "div_gcd_eq_div_gcd".) +-/ + +section + open int + + example {a b c : ℤ} (co : coprime a b) (apos : a > 0) (bpos : b > 0) + (H : a * a = c * (b * b)) : + b = 1 := + assert H₁ : gcd (c * b) a = gcd c a, from gcd_mul_right_cancel_of_coprime _ (coprime_swap co), + 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, + have a = b * (c div gcd c a), + using this, + by revert this; rewrite [mul.comm, !mul_div_assoc !gcd_dvd_left]; intros; assumption, + have b ∣ a, from dvd_of_mul_right_eq this⁻¹, + have b ∣ gcd a b, from dvd_gcd this !dvd.refl, + have b ∣ 1, using this, by rewrite [↑coprime at co, co at this]; apply this, + show b = 1, from eq_one_of_dvd_one (le_of_lt bpos) this +end diff --git a/library/theories/number_theory/number_theory.md b/library/theories/number_theory/number_theory.md index 43445957a7..072dd2d9bd 100644 --- a/library/theories/number_theory/number_theory.md +++ b/library/theories/number_theory/number_theory.md @@ -4,4 +4,4 @@ theories.number_theory * [primes](primes.lean) * [bezout](bezout.lean) : Bezout's theorem * [prime_factorization](prime_factorization.lean) : prime divisors and multiplicity -* [square_root_irrational](square_root_irrational.lean) : quadratic surds \ No newline at end of file +* [irrational_roots](irrational_roots.lean) : irrationality of nth roots \ No newline at end of file diff --git a/library/theories/number_theory/prime_factorization.lean b/library/theories/number_theory/prime_factorization.lean index 9b8efd4a68..82c9fa7b61 100644 --- a/library/theories/number_theory/prime_factorization.lean +++ b/library/theories/number_theory/prime_factorization.lean @@ -130,6 +130,9 @@ end theorem mult_pow_self {p : ℕ} (i : ℕ) (pgt1 : p > 1) : mult p (p^i) = i := by rewrite [-(mul_one (p^i)), mult_pow_mul i pgt1 zero_lt_one, mult_one_right] +theorem mult_self {p : ℕ} (pgt1 : p > 1) : mult p p = 1 := +by rewrite [-pow_one p at {2}]; apply mult_pow_self 1 pgt1 + theorem le_mult {p i n : ℕ} (pgt1 : p > 1) (npos : n > 0) (pidvd : p^i ∣ n) : i ≤ mult p n := dvd.elim pidvd (take m, @@ -168,6 +171,13 @@ calc ... = mult p m + mult p n : by rewrite [!mult_pow_mul `p > 1` m'n'pos, multm'n'] +theorem mult_pow {p m : ℕ} (n : ℕ) (mpos : m > 0) (primep : prime p) : mult p (m^n) = n * mult p m := +begin + induction n with n ih, + rewrite [pow_zero, mult_one_right, zero_mul], + rewrite [pow_succ, mult_mul primep mpos (!pow_pos_of_pos mpos), ih, succ_mul, add.comm] +end + theorem dvd_of_forall_prime_mult_le {m n : ℕ} (mpos : m > 0) (H : ∀ {p}, prime p → mult p m ≤ mult p n) : m ∣ n := @@ -178,7 +188,7 @@ begin {intros, rewrite meq, apply one_dvd}, have mgt1 : m > 1, from lt_of_le_of_ne (succ_le_of_lt mpos) (ne.symm mneq), have mge2 : m ≥ 2, from succ_le_of_lt mgt1, - have hpd : ∃ p, prime p ∧ p ∣ m, from ex_prime_and_dvd mge2, + have hpd : ∃ p, prime p ∧ p ∣ m, from exists_prime_and_dvd mge2, cases hpd with [p, H1], cases H1 with [primep, pdvdm], intro n, diff --git a/library/theories/number_theory/primes.lean b/library/theories/number_theory/primes.lean index c77a462375..30d005dbc9 100644 --- a/library/theories/number_theory/primes.lean +++ b/library/theories/number_theory/primes.lean @@ -83,7 +83,7 @@ obtain `m ∣ n` (h₅ : ¬ (m = 1 ∨ m = n)), from iff.mp !not_implies_iff_and have ¬ m = 1 ∧ ¬ m = n, from iff.mp !not_or_iff_not_and_not h₅, subtype.tag m (and.intro `m ∣ n` this) -theorem ex_dvd_of_not_prime {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n := +theorem exists_dvd_of_not_prime {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n := assume h₁ h₂, ex_of_sub (sub_dvd_of_not_prime h₁ h₂) definition sub_dvd_of_not_prime2 {n : nat} : n ≥ 2 → ¬ prime n → {m | m ∣ n ∧ m ≥ 2 ∧ m < n} := @@ -100,7 +100,7 @@ begin exact lt_of_le_and_ne m_le_n m_ne_n} end -theorem ex_dvd_of_not_prime2 {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≥ 2 ∧ m < n := +theorem exists_dvd_of_not_prime2 {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≥ 2 ∧ m < n := assume h₁ h₂, ex_of_sub (sub_dvd_of_not_prime2 h₁ h₂) definition sub_prime_and_dvd {n : nat} : n ≥ 2 → {p | prime p ∧ p ∣ n} := @@ -116,7 +116,7 @@ nat.strong_rec_on n have p ∣ n, from dvd.trans p_dvd_m m_dvd_n, subtype.tag p (and.intro hp this))) -lemma ex_prime_and_dvd {n : nat} : n ≥ 2 → ∃ p, prime p ∧ p ∣ n := +lemma exists_prime_and_dvd {n : nat} : n ≥ 2 → ∃ p, prime p ∧ p ∣ n := assume h, ex_of_sub (sub_prime_and_dvd h) open eq.ops diff --git a/library/theories/number_theory/square_root_irrational.lean b/library/theories/number_theory/square_root_irrational.lean deleted file mode 100644 index 29a72b584d..0000000000 --- a/library/theories/number_theory/square_root_irrational.lean +++ /dev/null @@ -1,52 +0,0 @@ -/- -Copyright (c) 2015 Jeremy Avigad. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Jeremy Avigad - -A proof that the square root of an integer is irrational, unless the integer is a perfect square. --/ -import data.rat -open nat eq.ops - -/- First, a textbook proof that sqrt 2 is irrational. -/ - -theorem sqrt_two_irrational_aux {a b : ℕ} (co : coprime a b) : a * a ≠ 2 * (b * b) := -assume H : a * a = 2 * (b * b), -have even (a * a), from even_of_exists (exists.intro _ H), -have even a, from even_of_even_mul_self this, -obtain c (aeq : a = 2 * c), from exists_of_even this, -have 2 * (2 * (c * c)) = 2 * (b * b), by rewrite [-H, aeq, mul.assoc, mul.left_comm c], -have 2 * (c * c) = b * b, from eq_of_mul_eq_mul_left dec_trivial this, -have even (b * b), from even_of_exists (exists.intro _ (eq.symm this)), -have even b, from even_of_even_mul_self this, -have 2 ∣ gcd a b, from dvd_gcd (dvd_of_even `even a`) (dvd_of_even `even b`), -have 2 ∣ 1, from co ▸ this, -absurd `2 ∣ 1` dec_trivial - -/- Let's state this in terms of rational numbers. The problem is that we now have to mediate between - rat, int, and nat. -/ - -section - open rat int - - theorem sqrt_two_irrational (q : ℚ): q^2 ≠ 2 := - suppose q^2 = 2, - let a := num q, b := denom q in - have b ≠ 0, from ne_of_gt (denom_pos q), - assert bnz : b ≠ (0 : ℚ), from assume H, `b ≠ 0` (of_int.inj H), - have b * b ≠ (0 : ℚ), from rat.mul_ne_zero bnz bnz, - have (a * a) / (b * b) = 2, - by rewrite [*of_int_mul, -div_mul_div bnz bnz, -eq_num_div_denom, -this, rat.pow_two], - have a * a = 2 * (b * b), from eq.symm (mul_eq_of_eq_div `b * b ≠ (0 : ℚ)` this⁻¹), - assert a * a = 2 * (b * b), from of_int.inj this, -- now in the integers - let a' := nat_abs a, b' := nat_abs b in - have H : a' * a' = 2 * (b' * b'), - begin - apply of_nat.inj, - rewrite [-+nat_abs_mul, int.of_nat_mul, +of_nat_nat_abs, +int.abs_mul_self], - exact this, - end, - have coprime a b, from !coprime_num_denom, - have nat.coprime a' b', from of_nat.inj this, - show false, from sqrt_two_irrational_aux this H -end