From e59400b58c1f962c35078c70a9a5506c720ebaa0 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Mon, 8 Jun 2015 22:43:51 +1000 Subject: [PATCH] feat(library/data/int/{div,gcd}): add some theorems, to reduce rationals --- library/algebra/ordered_ring.lean | 30 +++++++++++++++++++ library/data/int/div.lean | 27 +++++++++++++++++ library/data/int/gcd.lean | 49 +++++++++++++++++++++++++++++++ 3 files changed, 106 insertions(+) diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean index 8361a49c5..57bcfb158 100644 --- a/library/algebra/ordered_ring.lean +++ b/library/algebra/ordered_ring.lean @@ -154,6 +154,36 @@ section (assume H2 : a ≤ 0, have H3 : a * b ≤ 0, from mul_nonpos_of_nonpos_of_nonneg H2 H1, not_lt_of_ge H3 H) + + theorem nonneg_of_mul_nonneg_left (H : 0 ≤ a * b) (H1 : 0 < a) : 0 ≤ b := + le_of_not_gt + (assume H2 : b < 0, + not_le_of_gt (mul_neg_of_pos_of_neg H1 H2) H) + + theorem nonneg_of_mul_nonneg_right (H : 0 ≤ a * b) (H1 : 0 < b) : 0 ≤ a := + le_of_not_gt + (assume H2 : a < 0, + not_le_of_gt (mul_neg_of_neg_of_pos H2 H1) H) + + theorem neg_of_mul_neg_left (H : a * b < 0) (H1 : 0 ≤ a) : b < 0 := + lt_of_not_ge + (assume H2 : b ≥ 0, + not_lt_of_ge (mul_nonneg H1 H2) H) + + theorem neg_of_mul_neg_right (H : a * b < 0) (H1 : 0 ≤ b) : a < 0 := + lt_of_not_ge + (assume H2 : a ≥ 0, + not_lt_of_ge (mul_nonneg H2 H1) H) + + theorem nonpos_of_mul_nonpos_left (H : a * b ≤ 0) (H1 : 0 < a) : b ≤ 0 := + le_of_not_gt + (assume H2 : b > 0, + not_le_of_gt (mul_pos H1 H2) H) + + theorem nonpos_of_mul_nonpos_right (H : a * b ≤ 0) (H1 : 0 < b) : a ≤ 0 := + le_of_not_gt + (assume H2 : a > 0, + not_le_of_gt (mul_pos H2 H1) H) end structure ordered_ring [class] (A : Type) extends ring A, ordered_comm_group A, zero_ne_one_class A := diff --git a/library/data/int/div.lean b/library/data/int/div.lean index cdf31f084..5ae626e4b 100644 --- a/library/data/int/div.lean +++ b/library/data/int/div.lean @@ -539,6 +539,14 @@ theorem div_eq_of_eq_mul_left {a b c : ℤ} (H1 : b ≠ 0) (H2 : a = c * b) : a div b = c := div_eq_of_eq_mul_right H1 (!mul.comm ▸ H2) +theorem neg_div_of_dvd {a b : ℤ} (H : b ∣ a) : -a div b = -(a div b) := +decidable.by_cases + (assume H1 : b = 0, by rewrite [H1, *div_zero, neg_zero]) + (assume H1 : b ≠ 0, + dvd.elim H + (take c, assume H' : a = b * c, + by rewrite [H', neg_mul_eq_mul_neg, *!mul_div_cancel_left H1])) + /- div and ordering -/ theorem div_mul_le (a : ℤ) {b : ℤ} (H : b ≠ 0) : a div b * b ≤ a := @@ -613,4 +621,23 @@ theorem le_mul_of_div_le_of_div {a b c : ℤ} (H1 : b > 0) (H2 : b ∣ a) (H3 : a ≤ c * b := iff.mp (!div_le_iff_le_mul_of_div H1 H2) H3 +theorem div_pos_of_pos_of_dvd {a b : ℤ} (H1 : a > 0) (H2 : b ≥ 0) (H3 : b ∣ a) : a div b > 0 := +have H4 : b ≠ 0, from + (assume H5 : b = 0, + have H6 : a = 0, from eq_zero_of_zero_dvd (H5 ▸ H3), + ne_of_gt H1 H6), +have H6 : (a div b) * b > 0, by rewrite (div_mul_cancel H3); apply H1, +pos_of_mul_pos_right H6 H2 + +theorem div_eq_div_of_dvd_of_dvd {a b c d : ℤ} (H1 : b ∣ a) (H2 : d ∣ c) (H3 : b ≠ 0) + (H4 : d ≠ 0) (H5 : a * d = b * c) : + a div b = c div d := +begin + apply div_eq_of_eq_mul_right H3, + rewrite [-!mul_div_assoc H2], + apply eq.symm, + apply div_eq_of_eq_mul_left H4, + apply eq.symm H5 +end + end int diff --git a/library/data/int/gcd.lean b/library/data/int/gcd.lean index 608fde21c..828de3075 100644 --- a/library/data/int/gcd.lean +++ b/library/data/int/gcd.lean @@ -133,6 +133,55 @@ dvd_gcd (dvd.trans !gcd_dvd_left !dvd_mul_left) !gcd_dvd_right theorem gcd_dvd_gcd_mul_right (a b c : ℤ) : gcd a b ∣ gcd (a * c) b := !mul.comm ▸ !gcd_dvd_gcd_mul_left +theorem div_gcd_eq_div_gcd_of_nonneg {a₁ b₁ a₂ b₂ : ℤ} (H : a₁ * b₂ = b₁ * a₂) + (H1 : b₁ ≠ 0) (H2 : b₂ ≠ 0) (H3 : a₁ ≥ 0) (H4 : a₂ ≥ 0) : + a₁ div (gcd a₁ b₁) = a₂ div (gcd a₂ b₂) := +begin + apply div_eq_div_of_dvd_of_dvd, + repeat (apply gcd_dvd_left), + intro H', apply H1, apply eq_zero_of_gcd_eq_zero_right H', + intro H', apply H2, apply eq_zero_of_gcd_eq_zero_right H', + rewrite [-abs_of_nonneg H3 at {1}, -abs_of_nonneg H4 at {2}], + rewrite [-gcd_mul_left, -gcd_mul_right, H] +end + +theorem div_gcd_eq_div_gcd {a₁ b₁ a₂ b₂ : ℤ} (H : a₁ * b₂ = b₁ * a₂) (H1 : b₁ > 0) (H2 : b₂ > 0) : + a₁ div (gcd a₁ b₁) = a₂ div (gcd a₂ b₂) := +or.elim (le_or_gt 0 a₁) + (assume H3 : a₁ ≥ 0, + have H4 : b₁ * a₂ ≥ 0, by rewrite -H; apply mul_nonneg H3 (le_of_lt H2), + have H5 : a₂ ≥ 0, from nonneg_of_mul_nonneg_left H4 H1, + div_gcd_eq_div_gcd_of_nonneg H (ne_of_gt H1) (ne_of_gt H2) H3 H5) + (assume H3 : a₁ < 0, + have H4 : b₁ * a₂ < 0, by rewrite -H; apply mul_neg_of_neg_of_pos H3 H2, + assert H5 : a₂ < 0, from neg_of_mul_neg_left H4 (le_of_lt H1), + assert H6 : abs a₁ div (gcd (abs a₁) (abs b₁)) = abs a₂ div (gcd (abs a₂) (abs b₂)), + begin + apply div_gcd_eq_div_gcd_of_nonneg, + rewrite [abs_of_pos H1, abs_of_pos H2, abs_of_neg H3, abs_of_neg H5], + rewrite [-neg_mul_eq_mul_neg, -neg_mul_eq_neg_mul, H], + apply ne_of_gt (abs_pos_of_pos H1), + apply ne_of_gt (abs_pos_of_pos H2), + repeat (apply abs_nonneg) + end, + have H7 : -a₁ div (gcd a₁ b₁) = -a₂ div (gcd a₂ b₂), + begin +-- TODO: if you uncomment the next two lines, and comment out the three after it, +-- it takes Lean 40 seconds to process the file. (The rewrites are succeed, +-- but do not finish off the goal.) +-- rewrite [-abs_of_neg H3, -abs_of_neg H5, -gcd_abs_abs a₁], +-- rewrite [-gcd_abs_abs a₂ b₂], + revert H6, + rewrite [abs_of_neg H3 at {1}, abs_of_neg H5 at {1}, *gcd_abs_abs], + intro H6, apply H6 + end, + calc + a₁ div (gcd a₁ b₁) = -(-a₁ div (gcd a₁ b₁)) : + by rewrite [neg_div_of_dvd !gcd_dvd_left, neg_neg] + ... = -(-a₂ div (gcd a₂ b₂)) : H7 + ... = a₂ div (gcd a₂ b₂) : + by rewrite [neg_div_of_dvd !gcd_dvd_left, neg_neg]) + /- lcm -/ definition lcm (a b : ℤ) : ℤ := of_nat (nat.lcm (nat_abs a) (nat_abs b))