lean2/library/theories/number_theory/bezout.lean

118 lines
3.9 KiB
Text
Raw Normal View History

/-
Copyright (c) 2015 William Peterson. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: William Peterson, Jeremy Avigad
Extended gcd, Bezout's theorem, chinese remainder theorem.
-/
import data.nat.div data.int .primes
/- Bezout's theorem -/
section Bezout
open nat int
open eq.ops well_founded decidable prod
open algebra
private definition pair_nat.lt : × × → Prop := measure pr₂
private definition pair_nat.lt.wf : well_founded pair_nat.lt := intro_k (measure.wf pr₂) 20
local attribute pair_nat.lt.wf [instance]
local infixl `≺`:50 := pair_nat.lt
private definition gcd.lt.dec (x y₁ : ) : (succ y₁, x mod succ y₁) ≺ (x, succ y₁) :=
!nat.mod_lt (succ_pos y₁)
private definition egcd_rec_f (z : ) : × := λ s t, (t, s - t * z)
definition egcd.F : Π (p₁ : × ), (Π p₂ : × , p₂ ≺ p₁ → × ) → ×
| (x, y) := nat.cases_on y
(λ f, (1, 0) )
(λ y₁ (f : Π p₂, p₂ ≺ (x, succ y₁) → × ),
let bz := f (succ y₁, x mod succ y₁) !gcd.lt.dec in
prod.cases_on bz (egcd_rec_f (x div succ y₁)))
definition egcd (x y : ) := fix egcd.F (pair x y)
theorem egcd_zero (x : ) : egcd x 0 = (1, 0) :=
well_founded.fix_eq egcd.F (x, 0)
theorem egcd_succ (x y : ) :
egcd x (succ y) = prod.cases_on (egcd (succ y) (x mod succ y)) (egcd_rec_f (x div succ y)) :=
well_founded.fix_eq egcd.F (x, succ y)
theorem egcd_of_pos (x : ) {y : } (ypos : y > 0) :
let erec := egcd y (x mod y), u := pr₁ erec, v := pr₂ erec in
egcd x y = (v, u - v * (x div y)) :=
obtain (y' : nat) (yeq : y = succ y'), from exists_eq_succ_of_pos ypos,
begin
rewrite [yeq, egcd_succ, -prod.eta (egcd _ _)],
esimp, unfold egcd_rec_f,
rewrite [of_nat_div]
end
theorem egcd_prop (x y : ) : (pr₁ (egcd x y)) * x + (pr₂ (egcd x y)) * y = gcd x y :=
gcd.induction x y
(take m, by krewrite [egcd_zero, algebra.mul_zero, algebra.one_mul])
(take m n,
assume npos : 0 < n,
assume IH,
begin
let H := egcd_of_pos m npos, esimp at H,
rewrite H,
esimp,
rewrite [gcd_rec, -IH],
rewrite [algebra.add.comm],
rewrite [-of_nat_mod],
rewrite [int.modulo.def],
rewrite [+algebra.mul_sub_right_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)
theorem Bezout_aux (x y : ) : ∃ a b : , a * x + b * y = gcd x y :=
exists.intro _ (exists.intro _ (egcd_prop x y))
theorem Bezout (x y : ) : ∃ a b : , a * x + b * y = gcd x y :=
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 [*mul.assoc, -*abs_eq_sign_mul, -*of_nat_nat_abs],
apply H
end
end Bezout
/-
A sample application of Bezout's theorem, namely, an alternative proof that irreducible
implies prime (dvd_or_dvd_of_prime_of_dvd_mul).
-/
namespace nat
open int algebra
example {p x y : } (pp : prime p) (H : p x * y) : p x p y :=
decidable.by_cases
(suppose p x, or.inl this)
(suppose ¬ p x,
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 [-right_distrib, Hab, ↑coprime at cpx, cpx, int.one_mul],
have p y,
begin
apply dvd_of_of_nat_dvd_of_nat,
rewrite [-this],
apply @dvd_add,
{apply dvd_mul_of_dvd_left,
apply dvd_mul_of_dvd_right,
apply dvd.refl},
{rewrite mul.assoc,
apply dvd_mul_of_dvd_right,
apply of_nat_dvd_of_nat_of_dvd H}
end,
or.inr this)
end nat