lean2/library/theories/number_theory/bezout.lean

117 lines
3.9 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) 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