lean2/library/data/int/gcd.lean
2015-12-05 23:50:01 -08:00

350 lines
14 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/-
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Leonardo de Moura
Definitions and properties of gcd, lcm, and coprime.
-/
import .div data.nat.gcd
open eq.ops
namespace int
/- gcd -/
definition gcd (a b : ) : := of_nat (nat.gcd (nat_abs a) (nat_abs b))
theorem gcd_nonneg (a b : ) : gcd a b ≥ 0 :=
of_nat_nonneg (nat.gcd (nat_abs a) (nat_abs b))
theorem gcd.comm (a b : ) : gcd a b = gcd b a :=
by rewrite [↑gcd, nat.gcd.comm]
theorem gcd_zero_right (a : ) : gcd a 0 = abs a :=
by rewrite [↑gcd, nat_abs_zero, nat.gcd_zero_right, of_nat_nat_abs]
theorem gcd_zero_left (a : ) : gcd 0 a = abs a :=
by rewrite [gcd.comm, gcd_zero_right]
theorem gcd_one_right (a : ) : gcd a 1 = 1 :=
by rewrite [↑gcd, nat_abs_one, nat.gcd_one_right]
theorem gcd_one_left (a : ) : gcd 1 a = 1 :=
by rewrite [gcd.comm, gcd_one_right]
theorem gcd_abs_left (a b : ) : gcd (abs a) b = gcd a b :=
by rewrite [↑gcd, *nat_abs_abs]
theorem gcd_abs_right (a b : ) : gcd (abs a) b = gcd a b :=
by rewrite [↑gcd, *nat_abs_abs]
theorem gcd_abs_abs (a b : ) : gcd (abs a) (abs b) = gcd a b :=
by rewrite [↑gcd, *nat_abs_abs]
section
open nat
theorem gcd_of_ne_zero (a : ) {b : } (H : b ≠ 0) : gcd a b = gcd b (abs a % abs b) :=
have nat_abs b ≠ 0, from assume H', H (eq_zero_of_nat_abs_eq_zero H'),
have nat_abs b > 0, from pos_of_ne_zero this,
assert nat.gcd (nat_abs a) (nat_abs b) = (nat.gcd (nat_abs b) (nat_abs a % nat_abs b)),
from @nat.gcd_of_pos (nat_abs a) (nat_abs b) this,
calc
gcd a b = nat.gcd (nat_abs b) (nat_abs a % nat_abs b) : by rewrite [↑gcd, this]
... = gcd (abs b) (abs a % abs b) : by rewrite [↑gcd, -*of_nat_nat_abs, of_nat_mod]
... = gcd b (abs a % abs b) : by rewrite [↑gcd, *nat_abs_abs]
end
theorem gcd_of_pos (a : ) {b : } (H : b > 0) : gcd a b = gcd b (abs a % b) :=
by rewrite [!gcd_of_ne_zero (ne_of_gt H), abs_of_pos H]
theorem gcd_of_nonneg_of_pos {a b : } (H1 : a ≥ 0) (H2 : b > 0) : gcd a b = gcd b (a % b) :=
by rewrite [!gcd_of_pos H2, abs_of_nonneg H1]
theorem gcd_self (a : ) : gcd a a = abs a :=
by rewrite [↑gcd, nat.gcd_self, of_nat_nat_abs]
theorem gcd_dvd_left (a b : ) : gcd a b a :=
have gcd a b abs a,
by rewrite [↑gcd, -of_nat_nat_abs, of_nat_dvd_of_nat_iff]; apply nat.gcd_dvd_left,
iff.mp !dvd_abs_iff this
theorem gcd_dvd_right (a b : ) : gcd a b b :=
by rewrite gcd.comm; apply gcd_dvd_left
theorem dvd_gcd {a b c : } : a b → a c → a gcd b c :=
begin
rewrite [↑gcd, -*(abs_dvd_iff a), -(dvd_abs_iff _ b), -(dvd_abs_iff _ c), -*of_nat_nat_abs],
rewrite [*of_nat_dvd_of_nat_iff] ,
apply nat.dvd_gcd
end
theorem gcd.assoc (a b c : ) : gcd (gcd a b) c = gcd a (gcd b c) :=
dvd.antisymm !gcd_nonneg !gcd_nonneg
(dvd_gcd
(dvd.trans !gcd_dvd_left !gcd_dvd_left)
(dvd_gcd (dvd.trans !gcd_dvd_left !gcd_dvd_right) !gcd_dvd_right))
(dvd_gcd
(dvd_gcd !gcd_dvd_left (dvd.trans !gcd_dvd_right !gcd_dvd_left))
(dvd.trans !gcd_dvd_right !gcd_dvd_right))
theorem gcd_mul_left (a b c : ) : gcd (a * b) (a * c) = abs a * gcd b c :=
by rewrite [↑gcd, *nat_abs_mul, nat.gcd_mul_left, of_nat_mul, of_nat_nat_abs]
theorem gcd_mul_right (a b c : ) : gcd (a * b) (c * b) = gcd a c * abs b :=
by rewrite [mul.comm a, mul.comm c, mul.comm (gcd a c), gcd_mul_left]
theorem gcd_pos_of_ne_zero_left {a : } (b : ) (H : a ≠ 0) : gcd a b > 0 :=
have gcd a b ≠ 0, from
suppose gcd a b = 0,
have 0 a, from this ▸ gcd_dvd_left a b,
show false, from H (eq_zero_of_zero_dvd this),
lt_of_le_of_ne (gcd_nonneg a b) (ne.symm this)
theorem gcd_pos_of_ne_zero_right (a : ) {b : } (H : b ≠ 0) : gcd a b > 0 :=
by rewrite gcd.comm; apply !gcd_pos_of_ne_zero_left H
theorem eq_zero_of_gcd_eq_zero_left {a b : } (H : gcd a b = 0) : a = 0 :=
decidable.by_contradiction
(suppose a ≠ 0,
have gcd a b > 0, from !gcd_pos_of_ne_zero_left this,
ne_of_lt this H⁻¹)
theorem eq_zero_of_gcd_eq_zero_right {a b : } (H : gcd a b = 0) : b = 0 :=
by rewrite gcd.comm at H; apply !eq_zero_of_gcd_eq_zero_left H
theorem gcd_div {a b c : } (H1 : c a) (H2 : c b) :
gcd (a / c) (b / c) = gcd a b / (abs c) :=
decidable.by_cases
(suppose c = 0,
calc
gcd (a / c) (b / c) = gcd 0 0 : by subst c; rewrite *int.div_zero
... = 0 : gcd_zero_left
... = gcd a b / 0 : int.div_zero
... = gcd a b / (abs c) : by subst c)
(suppose c ≠ 0,
have abs c ≠ 0, from assume H', this (eq_zero_of_abs_eq_zero H'),
eq.symm (int.div_eq_of_eq_mul_left this
(eq.symm (calc
gcd (a / c) (b / c) * abs c = gcd (a / c * c) (b / c * c) : gcd_mul_right
... = gcd a (b / c * c) : int.div_mul_cancel H1
... = gcd a b : int.div_mul_cancel H2))))
theorem gcd_dvd_gcd_mul_left (a b c : ) : gcd a b gcd (c * a) b :=
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₂ = a₂ * b₁)
(H1 : b₁ ≠ 0) (H2 : b₂ ≠ 0) (H3 : a₁ ≥ 0) (H4 : a₂ ≥ 0) :
a₁ / (gcd a₁ b₁) = a₂ / (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, mul.comm b₁]
end
theorem div_gcd_eq_div_gcd {a₁ b₁ a₂ b₂ : } (H : a₁ * b₂ = a₂ * b₁) (H1 : b₁ > 0) (H2 : b₂ > 0) :
a₁ / (gcd a₁ b₁) = a₂ / (gcd a₂ b₂) :=
or.elim (le_or_gt 0 a₁)
(assume H3 : a₁ ≥ 0,
have H4 : a₂ * b₁ ≥ 0, by rewrite -H; apply mul_nonneg H3 (le_of_lt H2),
have H5 : a₂ ≥ 0, from nonneg_of_mul_nonneg_right 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 : a₂ * b₁ < 0, by rewrite -H; apply mul_neg_of_neg_of_pos H3 H2,
assert H5 : a₂ < 0, from neg_of_mul_neg_right H4 (le_of_lt H1),
assert H6 : abs a₁ / (gcd (abs a₁) (abs b₁)) = abs a₂ / (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_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₁ / (gcd a₁ b₁) = -a₂ / (gcd a₂ b₂),
begin
rewrite [-abs_of_neg H3, -abs_of_neg H5, -gcd_abs_abs a₁],
rewrite [-gcd_abs_abs a₂ b₂],
exact H6
end,
calc
a₁ / (gcd a₁ b₁) = -(-a₁ / (gcd a₁ b₁)) :
by rewrite [neg_div_of_dvd !gcd_dvd_left, neg_neg]
... = -(-a₂ / (gcd a₂ b₂)) : H7
... = a₂ / (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))
theorem lcm_nonneg (a b : ) : lcm a b ≥ 0 :=
of_nat_nonneg (nat.lcm (nat_abs a) (nat_abs b))
theorem lcm.comm (a b : ) : lcm a b = lcm b a :=
by rewrite [↑lcm, nat.lcm.comm]
theorem lcm_zero_left (a : ) : lcm 0 a = 0 :=
by rewrite [↑lcm, nat_abs_zero, nat.lcm_zero_left]
theorem lcm_zero_right (a : ) : lcm a 0 = 0 :=
!lcm.comm ▸ !lcm_zero_left
theorem lcm_one_left (a : ) : lcm 1 a = abs a :=
by rewrite [↑lcm, nat_abs_one, nat.lcm_one_left, of_nat_nat_abs]
theorem lcm_one_right (a : ) : lcm a 1 = abs a :=
!lcm.comm ▸ !lcm_one_left
theorem lcm_abs_left (a b : ) : lcm (abs a) b = lcm a b :=
by rewrite [↑lcm, *nat_abs_abs]
theorem lcm_abs_right (a b : ) : lcm (abs a) b = lcm a b :=
by rewrite [↑lcm, *nat_abs_abs]
theorem lcm_abs_abs (a b : ) : lcm (abs a) (abs b) = lcm a b :=
by rewrite [↑lcm, *nat_abs_abs]
theorem lcm_self (a : ) : lcm a a = abs a :=
by rewrite [↑lcm, nat.lcm_self, of_nat_nat_abs]
theorem dvd_lcm_left (a b : ) : a lcm a b :=
by rewrite [↑lcm, -abs_dvd_iff, -of_nat_nat_abs, of_nat_dvd_of_nat_iff]; apply nat.dvd_lcm_left
theorem dvd_lcm_right (a b : ) : b lcm a b :=
!lcm.comm ▸ !dvd_lcm_left
theorem gcd_mul_lcm (a b : ) : gcd a b * lcm a b = abs (a * b) :=
begin
rewrite [↑gcd, ↑lcm, -of_nat_nat_abs, -of_nat_mul, of_nat_eq_of_nat_iff, nat_abs_mul],
apply nat.gcd_mul_lcm
end
theorem lcm_dvd {a b c : } : a c → b c → lcm a b c :=
begin
rewrite [↑lcm, -(abs_dvd_iff a), -(abs_dvd_iff b), -*(dvd_abs_iff _ c), -*of_nat_nat_abs],
rewrite [*of_nat_dvd_of_nat_iff] ,
apply nat.lcm_dvd
end
theorem lcm_assoc (a b c : ) : lcm (lcm a b) c = lcm a (lcm b c) :=
dvd.antisymm !lcm_nonneg !lcm_nonneg
(lcm_dvd
(lcm_dvd !dvd_lcm_left (dvd.trans !dvd_lcm_left !dvd_lcm_right))
(dvd.trans !dvd_lcm_right !dvd_lcm_right))
(lcm_dvd
(dvd.trans !dvd_lcm_left !dvd_lcm_left)
(lcm_dvd (dvd.trans !dvd_lcm_right !dvd_lcm_left) !dvd_lcm_right))
/- coprime -/
abbreviation coprime (a b : ) : Prop := gcd a b = 1
theorem coprime_swap {a b : } (H : coprime b a) : coprime a b :=
!gcd.comm ▸ H
theorem dvd_of_coprime_of_dvd_mul_right {a b c : } (H1 : coprime c b) (H2 : c a * b) : c a :=
assert H3 : gcd (a * c) (a * b) = abs a, from
calc
gcd (a * c) (a * b) = abs a * gcd c b : gcd_mul_left
... = abs a * 1 : H1
... = abs a : mul_one,
assert H4 : (c gcd (a * c) (a * b)), from dvd_gcd !dvd_mul_left H2,
by rewrite [-dvd_abs_iff, -H3]; apply H4
theorem dvd_of_coprime_of_dvd_mul_left {a b c : } (H1 : coprime c a) (H2 : c a * b) : c b :=
dvd_of_coprime_of_dvd_mul_right H1 (!mul.comm ▸ H2)
theorem gcd_mul_left_cancel_of_coprime {c : } (a : ) {b : } (H : coprime c b) :
gcd (c * a) b = gcd a b :=
begin
revert H, unfold [coprime, gcd],
rewrite [-of_nat_one],
rewrite [+of_nat_eq_of_nat_iff, nat_abs_mul],
apply nat.gcd_mul_left_cancel_of_coprime,
end
theorem gcd_mul_right_cancel_of_coprime (a : ) {c b : } (H : coprime c b) :
gcd (a * c) b = gcd a b :=
!mul.comm ▸ !gcd_mul_left_cancel_of_coprime H
theorem gcd_mul_left_cancel_of_coprime_right {c a : } (b : ) (H : coprime c a) :
gcd a (c * b) = gcd a b :=
!gcd.comm ▸ !gcd.comm ▸ !gcd_mul_left_cancel_of_coprime H
theorem gcd_mul_right_cancel_of_coprime_right {c a : } (b : ) (H : coprime c a) :
gcd a (b * c) = gcd a b :=
!gcd.comm ▸ !gcd.comm ▸ !gcd_mul_right_cancel_of_coprime H
theorem coprime_div_gcd_div_gcd {a b : } (H : gcd a b ≠ 0) :
coprime (a / gcd a b) (b / gcd a b) :=
calc
gcd (a / gcd a b) (b / gcd a b)
= gcd a b / abs (gcd a b) : gcd_div !gcd_dvd_left !gcd_dvd_right
... = 1 : by rewrite [abs_of_nonneg !gcd_nonneg, int.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 / gcd a b) * gcd a b, from (int.div_mul_cancel !gcd_dvd_left)⁻¹,
have H2 : b = (b / gcd a b) * gcd a b, from (int.div_mul_cancel !gcd_dvd_right)⁻¹,
exists.intro _ (exists.intro _ (and.intro (coprime_div_gcd_div_gcd H) (and.intro H1 H2)))
theorem coprime_mul {a b c : } (H1 : coprime a c) (H2 : coprime b c) : coprime (a * b) c :=
calc
gcd (a * b) c = gcd b c : !gcd_mul_left_cancel_of_coprime H1
... = 1 : H2
theorem coprime_mul_right {c a b : } (H1 : coprime c a) (H2 : coprime c b) : coprime c (a * b) :=
coprime_swap (coprime_mul (coprime_swap H1) (coprime_swap H2))
theorem coprime_of_coprime_mul_left {c a b : } (H : coprime (c * a) b) : coprime a b :=
have H1 : (gcd a b gcd (c * a) b), from !gcd_dvd_gcd_mul_left,
eq_one_of_dvd_one !gcd_nonneg (H ▸ H1)
theorem coprime_of_coprime_mul_right {c a b : } (H : coprime (a * c) b) : coprime a b :=
coprime_of_coprime_mul_left (!mul.comm ▸ H)
theorem coprime_of_coprime_mul_left_right {c a b : } (H : coprime a (c * b)) : coprime a b :=
coprime_swap (coprime_of_coprime_mul_left (coprime_swap H))
theorem coprime_of_coprime_mul_right_right {c a b : } (H : coprime a (b * c)) : coprime a b :=
coprime_of_coprime_mul_left_right (!mul.comm ▸ H)
theorem exists_eq_prod_and_dvd_and_dvd {a b c : } (H : c a * b) :
∃ a' b', c = a' * b' ∧ a' a ∧ b' b :=
decidable.by_cases
(suppose gcd c a = 0,
have c = 0, from eq_zero_of_gcd_eq_zero_left `gcd c a = 0`,
have a = 0, from eq_zero_of_gcd_eq_zero_right `gcd c a = 0`,
have c = 0 * b, from `c = 0` ⬝ !zero_mul⁻¹,
have 0 a, from `a = 0`⁻¹ ▸ !dvd.refl,
have b b, from !dvd.refl,
exists.intro _ (exists.intro _ (and.intro `c = 0 * b` (and.intro `0 a` `b b`))))
(suppose gcd c a ≠ 0,
have gcd c a c, from !gcd_dvd_left,
have H3 : c / gcd c a (a * b) / gcd c a, from div_dvd_div this H,
have H4 : (a * b) / gcd c a = (a / gcd c a) * b, from
calc
a * b / gcd c a = b * a / gcd c a : mul.comm
... = b * (a / gcd c a) : !int.mul_div_assoc !gcd_dvd_right
... = a / gcd c a * b : mul.comm,
have H5 : c / gcd c a (a / gcd c a) * b, from H4 ▸ H3,
have H6 : coprime (c / gcd c a) (a / gcd c a), from coprime_div_gcd_div_gcd `gcd c a ≠ 0`,
have H7 : c / gcd c a b, from dvd_of_coprime_of_dvd_mul_left H6 H5,
have H8 : c = gcd c a * (c / gcd c a), from (int.mul_div_cancel' `gcd c a c`)⁻¹,
exists.intro _ (exists.intro _ (and.intro H8 (and.intro !gcd_dvd_right H7))))
end int