lean2/library/data/nat/div.lean
2015-02-11 14:09:25 -08:00

798 lines
34 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.
Module: data.nat.div
Authors: Jeremy Avigad, Leonardo de Moura
Definitions and properties of div, mod, gcd, lcm, coprime. Much of the development follows
Isabelle's library.
-/
import data.nat.sub tools.fake_simplifier
open eq.ops well_founded decidable fake_simplifier prod
namespace nat
/- div and mod -/
-- auxiliary lemma used to justify div
private definition div_rec_lemma {x y : nat} (H : 0 < y ∧ y ≤ x) : x - y < x :=
and.rec_on H (λ ypos ylex, sub_lt (lt_of_lt_of_le ypos ylex) ypos)
private definition div.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=
if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y + 1 else zero
definition divide (x y : nat) := fix div.F x y
theorem divide_def (x y : nat) : divide x y = if 0 < y ∧ y ≤ x then divide (x - y) y + 1 else 0 :=
congr_fun (fix_eq div.F x) y
notation a div b := divide a b
theorem div_zero (a : ) : a div 0 = 0 :=
divide_def a 0 ⬝ if_neg (!not_and_of_not_left (lt.irrefl 0))
theorem div_eq_zero_of_lt {a b : } (h : a < b) : a div b = 0 :=
divide_def a b ⬝ if_neg (!not_and_of_not_right (not_le_of_lt h))
theorem zero_div (b : ) : 0 div b = 0 :=
divide_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt_of_lt_of_le l r) (lt.irrefl 0)))
theorem div_eq_succ_sub_div {a b : } (h₁ : b > 0) (h₂ : a ≥ b) : a div b = succ ((a - b) div b) :=
divide_def a b ⬝ if_pos (and.intro h₁ h₂)
theorem add_div_self_right (x : ) {z : } (H : z > 0) : (x + z) div z = succ (x div z) :=
calc
(x + z) div z = if 0 < z ∧ z ≤ x + z then (x + z - z) div z + 1 else 0 : !divide_def
... = (x + z - z) div z + 1 : if_pos (and.intro H (le_add_left z x))
... = succ (x div z) : {!add_sub_cancel}
theorem add_div_self_left {x : } (z : ) (H : x > 0) : (x + z) div x = succ (z div x) :=
!add.comm ▸ !add_div_self_right H
theorem add_mul_div_self_right {x y z : } (H : z > 0) : (x + y * z) div z = x div z + y :=
nat.induction_on y
(calc (x + zero * z) div z = (x + zero) div z : zero_mul
... = x div z : add_zero
... = x div z + zero : add_zero)
(take y,
assume IH : (x + y * z) div z = x div z + y, calc
(x + succ y * z) div z = (x + y * z + z) div z : by simp
... = succ ((x + y * z) div z) : !add_div_self_right H
... = x div z + succ y : by simp)
theorem add_mul_div_self_left (x z : ) {y : } (H : y > 0) : (x + y * z) div y = x div y + z :=
!mul.comm ▸ add_mul_div_self_right H
theorem mul_div_cancel (m : ) {n : } (H : n > 0) : m * n div n = m :=
calc
m * n div n = (0 + m * n) div n : zero_add
... = 0 div n + m : add_mul_div_self_right H
... = 0 + m : zero_div
... = m : zero_add
theorem mul_div_cancel_left {m : } (n : ) (H : m > 0) : m * n div m = n :=
!mul.comm ▸ !mul_div_cancel H
private definition mod.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=
if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y else x
definition modulo (x y : nat) := fix mod.F x y
notation a mod b := modulo a b
theorem modulo_def (x y : nat) : modulo x y = if 0 < y ∧ y ≤ x then modulo (x - y) y else x :=
congr_fun (fix_eq mod.F x) y
theorem mod_zero (a : ) : a mod 0 = a :=
modulo_def a 0 ⬝ if_neg (!not_and_of_not_left (lt.irrefl 0))
theorem mod_eq_of_lt {a b : } (h : a < b) : a mod b = a :=
modulo_def a b ⬝ if_neg (!not_and_of_not_right (not_le_of_lt h))
theorem zero_mod (b : ) : 0 mod b = 0 :=
modulo_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt_of_lt_of_le l r) (lt.irrefl 0)))
theorem mod_eq_sub_mod {a b : } (h₁ : b > 0) (h₂ : a ≥ b) : a mod b = (a - b) mod b :=
modulo_def a b ⬝ if_pos (and.intro h₁ h₂)
theorem add_mod_left {x z : } (H : z > 0) : (x + z) mod z = x mod z :=
calc
(x + z) mod z = if 0 < z ∧ z ≤ x + z then (x + z - z) mod z else _ : modulo_def
... = (x + z - z) mod z : if_pos (and.intro H (le_add_left z x))
... = x mod z : add_sub_cancel
theorem add_mod_right {x z : } (H : x > 0) : (x + z) mod x = z mod x :=
!add.comm ▸ add_mod_left H
theorem add_mul_mod_self_right {x y z : } (H : z > 0) : (x + y * z) mod z = x mod z :=
nat.induction_on y
(calc (x + zero * z) mod z = (x + zero) mod z : zero_mul
... = x mod z : add_zero)
(take y,
assume IH : (x + y * z) mod z = x mod z,
calc
(x + succ y * z) mod z = (x + (y * z + z)) mod z : succ_mul
... = (x + y * z + z) mod z : add.assoc
... = (x + y * z) mod z : add_mod_left H
... = x mod z : IH)
theorem add_mul_mod_self_left {x y z : } (H : y > 0) : (x + y * z) mod y = x mod y :=
!mul.comm ▸ add_mul_mod_self_right H
theorem mul_mod_left {m n : } : (m * n) mod n = 0 :=
by_cases_zero_pos n (by simp)
(take n,
assume npos : n > 0,
(by simp) ▸ (@add_mul_mod_self_right 0 m _ npos))
theorem mul_mod_right {m n : } : (m * n) mod m = 0 :=
!mul.comm ▸ !mul_mod_left
theorem mod_lt {x y : } (H : y > 0) : x mod y < y :=
nat.case_strong_induction_on x
(show 0 mod y < y, from !zero_mod⁻¹ ▸ H)
(take x,
assume IH : ∀x', x' ≤ x → x' mod y < y,
show succ x mod y < y, from
by_cases -- (succ x < y)
(assume H1 : succ x < y,
have H2 : succ x mod y = succ x, from mod_eq_of_lt H1,
show succ x mod y < y, from H2⁻¹ ▸ H1)
(assume H1 : ¬ succ x < y,
have H2 : y ≤ succ x, from le_of_not_lt H1,
have H3 : succ x mod y = (succ x - y) mod y, from mod_eq_sub_mod H H2,
have H4 : succ x - y < succ x, from sub_lt !succ_pos H,
have H5 : succ x - y ≤ x, from le_of_lt_succ H4,
show succ x mod y < y, from H3⁻¹ ▸ IH _ H5))
/- properties of div and mod together -/
-- the quotient / remainder theorem
theorem eq_div_mul_add_mod {x y : } : x = x div y * y + x mod y :=
by_cases_zero_pos y
(show x = x div 0 * 0 + x mod 0, from
(calc
x div 0 * 0 + x mod 0 = 0 + x mod 0 : mul_zero
... = x mod 0 : zero_add
... = x : mod_zero)⁻¹)
(take y,
assume H : y > 0,
show x = x div y * y + x mod y, from
nat.case_strong_induction_on x
(show 0 = (0 div y) * y + 0 mod y, by simp)
(take x,
assume IH : ∀x', x' ≤ x → x' = x' div y * y + x' mod y,
show succ x = succ x div y * y + succ x mod y, from
by_cases -- (succ x < y)
(assume H1 : succ x < y,
have H2 : succ x div y = 0, from div_eq_zero_of_lt H1,
have H3 : succ x mod y = succ x, from mod_eq_of_lt H1,
by simp)
(assume H1 : ¬ succ x < y,
have H2 : y ≤ succ x, from le_of_not_lt H1,
have H3 : succ x div y = succ ((succ x - y) div y), from div_eq_succ_sub_div H H2,
have H4 : succ x mod y = (succ x - y) mod y, from mod_eq_sub_mod H H2,
have H5 : succ x - y < succ x, from sub_lt !succ_pos H,
have H6 : succ x - y ≤ x, from le_of_lt_succ H5,
(calc
succ x div y * y + succ x mod y =
succ ((succ x - y) div y) * y + succ x mod y : H3
... = ((succ x - y) div y) * y + y + succ x mod y : succ_mul
... = ((succ x - y) div y) * y + y + (succ x - y) mod y : H4
... = ((succ x - y) div y) * y + (succ x - y) mod y + y : add.right_comm
... = succ x - y + y : {!(IH _ H6)⁻¹}
... = succ x : sub_add_cancel H2)⁻¹)))
theorem mod_le {x y : } : x mod y ≤ x :=
eq_div_mul_add_mod⁻¹ ▸ !le_add_left
theorem eq_remainder {y : } (H : y > 0) {q1 r1 q2 r2 : } (H1 : r1 < y) (H2 : r2 < y)
(H3 : q1 * y + r1 = q2 * y + r2) : r1 = r2 :=
calc
r1 = r1 mod y : by simp
... = (r1 + q1 * y) mod y : (add_mul_mod_self_right H)⁻¹
... = (q1 * y + r1) mod y : add.comm
... = (r2 + q2 * y) mod y : by simp
... = r2 mod y : add_mul_mod_self_right H
... = r2 : by simp
theorem eq_quotient {y : } (H : y > 0) {q1 r1 q2 r2 : } (H1 : r1 < y) (H2 : r2 < y)
(H3 : q1 * y + r1 = q2 * y + r2) : q1 = q2 :=
have H4 : q1 * y + r2 = q2 * y + r2, from (eq_remainder H H1 H2 H3) ▸ H3,
have H5 : q1 * y = q2 * y, from add.cancel_right H4,
have H6 : y > 0, from lt_of_le_of_lt !zero_le H1,
show q1 = q2, from eq_of_mul_eq_mul_right H6 H5
theorem mul_div_mul_left {z : } (x y : ) (zpos : z > 0) : (z * x) div (z * y) = x div y :=
by_cases -- (y = 0)
(assume H : y = 0, by simp)
(assume H : y ≠ 0,
have ypos : y > 0, from pos_of_ne_zero H,
have zypos : z * y > 0, from mul_pos zpos ypos,
have H1 : (z * x) mod (z * y) < z * y, from mod_lt zypos,
have H2 : z * (x mod y) < z * y, from mul_lt_mul_of_pos_left (mod_lt ypos) zpos,
eq_quotient zypos H1 H2
(calc
((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : eq_div_mul_add_mod
... = z * (x div y * y + x mod y) : eq_div_mul_add_mod
... = z * (x div y * y) + z * (x mod y) : mul.left_distrib
... = (x div y) * (z * y) + z * (x mod y) : mul.left_comm))
theorem mul_div_mul_right {x z y : } (zpos : z > 0) : (x * z) div (y * z) = x div y :=
!mul.comm ▸ !mul.comm ▸ !mul_div_mul_left zpos
theorem mul_mod_mul_left (z x y : ) : (z * x) mod (z * y) = z * (x mod y) :=
or.elim (eq_zero_or_pos z)
(assume H : z = 0,
calc
(z * x) mod (z * y) = (0 * x) mod (z * y) : H
... = 0 mod (z * y) : zero_mul
... = 0 : zero_mod
... = 0 * (x mod y) : zero_mul
... = z * (x mod y) : H)
(assume zpos : z > 0,
or.elim (eq_zero_or_pos y)
(assume H : y = 0, by simp)
(assume ypos : y > 0,
have zypos : z * y > 0, from mul_pos zpos ypos,
have H1 : (z * x) mod (z * y) < z * y, from mod_lt zypos,
have H2 : z * (x mod y) < z * y, from mul_lt_mul_of_pos_left (mod_lt ypos) zpos,
eq_remainder zypos H1 H2
(calc
((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : eq_div_mul_add_mod
... = z * (x div y * y + x mod y) : eq_div_mul_add_mod
... = z * (x div y * y) + z * (x mod y) : mul.left_distrib
... = (x div y) * (z * y) + z * (x mod y) : mul.left_comm)))
theorem mul_mod_mul_right (x z y : ) : (x * z) mod (y * z) = (x mod y) * z :=
mul.comm z x ▸ mul.comm z y ▸ !mul.comm ▸ !mul_mod_mul_left
theorem mod_one (n : ) : n mod 1 = 0 :=
have H1 : n mod 1 < 1, from mod_lt !succ_pos,
eq_zero_of_le_zero (le_of_lt_succ H1)
theorem mod_self (n : ) : n mod n = 0 :=
nat.cases_on n (by simp)
(take n,
have H : (succ n * 1) mod (succ n * 1) = succ n * (1 mod 1),
from !mul_mod_mul_left,
(by simp) ▸ H)
theorem div_one (n : ) : n div 1 = n :=
have H : n div 1 * 1 + n mod 1 = n, from eq_div_mul_add_mod⁻¹,
(by simp) ▸ H
theorem div_self {n : } (H : n > 0) : n div n = 1 :=
have H1 : (n * 1) div (n * 1) = 1 div 1, from !mul_div_mul_left H,
(by simp) ▸ H1
theorem div_mul_cancel_of_mod_eq_zero {m n : } (H : m mod n = 0) : m div n * n = m :=
(calc
m = m div n * n + m mod n : eq_div_mul_add_mod
... = m div n * n + 0 : H
... = m div n * n : !add_zero)⁻¹
theorem mul_div_cancel_of_mod_eq_zero {m n : } (H : m mod n = 0) : n * (m div n) = m :=
!mul.comm ▸ div_mul_cancel_of_mod_eq_zero H
/- divides -/
theorem dvd_of_mod_eq_zero {m n : } (H : n mod m = 0) : m | n :=
dvd.intro (!mul.comm ▸ div_mul_cancel_of_mod_eq_zero H)
theorem mod_eq_zero_of_dvd {m n : } (H : m | n) : n mod m = 0 :=
dvd.elim H
(take z,
assume H1 : n = m * z,
H1⁻¹ ▸ !mul_mod_right)
theorem dvd_iff_mod_eq_zero (m n : ) : m | n ↔ n mod m = 0 :=
iff.intro mod_eq_zero_of_dvd dvd_of_mod_eq_zero
definition dvd.decidable_rel [instance] : decidable_rel dvd :=
take m n, decidable_of_decidable_of_iff _ (iff.symm !dvd_iff_mod_eq_zero)
theorem div_mul_cancel {m n : } (H : n | m) : m div n * n = m :=
div_mul_cancel_of_mod_eq_zero (mod_eq_zero_of_dvd H)
theorem mul_div_cancel' {m n : } (H : n | m) : n * (m div n) = m :=
!mul.comm ▸ div_mul_cancel H
theorem eq_mul_of_div_eq {m n k : } (H1 : m | n) (H2 : n div m = k) : n = m * k :=
eq.symm (calc
m * k = m * (n div m) : H2
... = n : mul_div_cancel' H1)
theorem eq_div_of_mul_eq {m n k : } (H1 : k > 0) (H2 : n * k = m) : n = m div k :=
calc
n = n * k div k : mul_div_cancel _ H1
... = m div k : H2
theorem dvd_of_dvd_add_left {m n1 n2 : } : m | (n1 + n2) → m | n1 → m | n2 :=
by_cases_zero_pos m
(assume (H1 : 0 | n1 + n2) (H2 : 0 | n1),
have H3 : n1 + n2 = 0, from eq_zero_of_zero_dvd H1,
have H4 : n1 = 0, from eq_zero_of_zero_dvd H2,
have H5 : n2 = 0, from calc
n2 = 0 + n2 : zero_add
... = n1 + n2 : H4
... = 0 : H3,
show 0 | n2, from H5 ▸ dvd.refl n2)
(take m,
assume mpos : m > 0,
assume H1 : m | (n1 + n2),
assume H2 : m | n1,
have H3 : n1 + n2 = n1 + n2 div m * m, from calc
n1 + n2 = (n1 + n2) div m * m : div_mul_cancel H1
... = (n1 div m * m + n2) div m * m : div_mul_cancel H2
... = (n2 + n1 div m * m) div m * m : add.comm
... = (n2 div m + n1 div m) * m : add_mul_div_self_right mpos
... = n2 div m * m + n1 div m * m : mul.right_distrib
... = n1 div m * m + n2 div m * m : add.comm
... = n1 + n2 div m * m : div_mul_cancel H2,
have H4 : n2 = n2 div m * m, from add.cancel_left H3,
have H5 : m * (n2 div m) = n2, from !mul.comm ▸ H4⁻¹,
dvd.intro H5)
theorem dvd_of_dvd_add_right {m n1 n2 : } (H : m | (n1 + n2)) : m | n2 → m | n1 :=
dvd_of_dvd_add_left (!add.comm ▸ H)
theorem dvd_sub {m n1 n2 : } (H1 : m | n1) (H2 : m | n2) : m | (n1 - n2) :=
by_cases
(assume H3 : n1 ≥ n2,
have H4 : n1 = n1 - n2 + n2, from (sub_add_cancel H3)⁻¹,
show m | n1 - n2, from dvd_of_dvd_add_right (H4 ▸ H1) H2)
(assume H3 : ¬ (n1 ≥ n2),
have H4 : n1 - n2 = 0, from sub_eq_zero_of_le (le_of_lt (lt_of_not_le H3)),
show m | n1 - n2, from H4⁻¹ ▸ dvd_zero _)
theorem dvd.antisymm {m n : } : m | n → n | m → m = n :=
by_cases_zero_pos n
(assume H1, assume H2 : 0 | m, eq_zero_of_zero_dvd H2)
(take n,
assume Hpos : n > 0,
assume H1 : m | n,
assume H2 : n | m,
obtain k (Hk : n = m * k), from exists_eq_mul_right_of_dvd H1,
obtain l (Hl : m = n * l), from exists_eq_mul_right_of_dvd H2,
have H3 : n * (l * k) = n, from !mul.assoc ▸ Hl ▸ Hk⁻¹,
have H4 : l * k = 1, from eq_one_of_mul_eq_self_right Hpos H3,
have H5 : k = 1, from eq_one_of_mul_eq_one_left H4,
show m = n, from (mul_one m)⁻¹ ⬝ (H5 ▸ Hk⁻¹))
theorem mul_div_assoc (m : ) {n k : } (H : k | n) : m * n div k = m * (n div k) :=
or.elim (eq_zero_or_pos k)
(assume H1 : k = 0,
calc
m * n div k = m * n div 0 : H1
... = 0 : div_zero
... = m * 0 : mul_zero m
... = m * (n div 0) : div_zero
... = m * (n div k) : H1)
(assume H1 : k > 0,
have H2 : n = n div k * k, from (div_mul_cancel H)⁻¹,
calc
m * n div k = m * (n div k * k) div k : H2
... = m * (n div k) * k div k : mul.assoc
... = m * (n div k) : mul_div_cancel _ H1)
theorem dvd_of_mul_dvd_mul_left {m n k : } (kpos : k > 0) (H : k * m | k * n) : m | n :=
dvd.elim H
(take l,
assume H1 : k * n = k * m * l,
have H2 : n = m * l, from eq_of_mul_eq_mul_left kpos (H1 ⬝ !mul.assoc),
dvd.intro H2⁻¹)
theorem dvd_of_mul_dvd_mul_right {m n k : } (kpos : k > 0) (H : m * k | n * k) : m | n :=
dvd_of_mul_dvd_mul_left kpos (!mul.comm ▸ !mul.comm ▸ H)
theorem div_dvd_div {k m n : } (H1 : k | m) (H2 : m | n) : m div k | n div k :=
have H3 : m = m div k * k, from (div_mul_cancel H1)⁻¹,
have H4 : n = n div k * k, from (div_mul_cancel (dvd.trans H1 H2))⁻¹,
or.elim (eq_zero_or_pos k)
(assume H5 : k = 0,
have H6: n div k = 0, from (congr_arg _ H5 ⬝ !div_zero),
H6⁻¹ ▸ !dvd_zero)
(assume H5 : k > 0,
dvd_of_mul_dvd_mul_right H5 (H3 ▸ H4 ▸ H2))
/- gcd -/
private definition pair_nat.lt : nat × nat → nat × nat → Prop := measure pr₂
private definition pair_nat.lt.wf : well_founded pair_nat.lt :=
intro_k (measure.wf pr₂) 20 -- we use intro_k to be able to execute gcd efficiently in the kernel
local attribute pair_nat.lt.wf [instance] -- instance will not be saved in .olean
local infixl `≺`:50 := pair_nat.lt
private definition gcd.lt.dec (x y₁ : nat) : (succ y₁, x mod succ y₁) ≺ (x, succ y₁) :=
mod_lt (succ_pos y₁)
definition gcd.F (p₁ : nat × nat) : (Π p₂ : nat × nat, p₂ ≺ p₁ → nat) → nat :=
prod.cases_on p₁ (λx y, nat.cases_on y
(λ f, x)
(λ y₁ (f : Πp₂, p₂ ≺ (x, succ y₁) → nat), f (succ y₁, x mod succ y₁) !gcd.lt.dec))
definition gcd (x y : nat) := fix gcd.F (pair x y)
theorem gcd_zero_right (x : nat) : gcd x 0 = x :=
well_founded.fix_eq gcd.F (x, 0)
theorem gcd_succ (x y : nat) : gcd x (succ y) = gcd (succ y) (x mod succ y) :=
well_founded.fix_eq gcd.F (x, succ y)
theorem gcd_one_right (n : ) : gcd n 1 = 1 :=
calc gcd n 1 = gcd 1 (n mod 1) : gcd_succ n zero
... = gcd 1 0 : mod_one
... = 1 : gcd_zero_right
theorem gcd_def (x y : ) : gcd x y = if y = 0 then x else gcd y (x mod y) :=
nat.cases_on y
(calc gcd x 0 = x : gcd_zero_right x
... = if 0 = 0 then x else gcd zero (x mod zero) : (if_pos rfl)⁻¹)
(λy₁, calc
gcd x (succ y₁) = gcd (succ y₁) (x mod succ y₁) : gcd_succ x y₁
... = if succ y₁ = 0 then x else gcd (succ y₁) (x mod succ y₁) : (if_neg (succ_ne_zero y₁))⁻¹)
theorem gcd_self (n : ) : gcd n n = n :=
nat.cases_on n
rfl
(λn₁, calc
gcd (succ n₁) (succ n₁) = gcd (succ n₁) (succ n₁ mod succ n₁) : gcd_succ (succ n₁) n₁
... = gcd (succ n₁) 0 : mod_self (succ n₁)
... = succ n₁ : gcd_zero_right)
theorem gcd_zero_left (n : nat) : gcd 0 n = n :=
nat.cases_on n
rfl
(λ n₁, calc
gcd 0 (succ n₁) = gcd (succ n₁) (0 mod succ n₁) : gcd_succ
... = gcd (succ n₁) 0 : zero_mod
... = (succ n₁) : gcd_zero_right)
theorem gcd_rec_of_pos (m : ) {n : } (H : n > 0) : gcd m n = gcd n (m mod n) :=
gcd_def m n ⬝ if_neg (ne_zero_of_pos H)
theorem gcd_rec (m n : ) : gcd m n = gcd n (m mod n) :=
by_cases_zero_pos n
(calc
gcd m 0 = m : gcd_zero_right
... = gcd 0 m : gcd_zero_left
... = gcd 0 (m mod 0) : mod_zero)
(take n, assume H : 0 < n, gcd_rec_of_pos m H)
theorem gcd.induction {P : → Prop}
(m n : )
(H0 : ∀m, P m 0)
(H1 : ∀m n, 0 < n → P n (m mod n) → P m n) :
P m n :=
let Q : nat × nat → Prop := λ p : nat × nat, P (pr₁ p) (pr₂ p) in
have aux : Q (m, n), from
well_founded.induction (m, n) (λp, prod.cases_on p
(λm n, nat.cases_on n
(λ ih, show P (pr₁ (m, 0)) (pr₂ (m, 0)), from H0 m)
(λ n₁ (ih : ∀p₂, p₂ ≺ (m, succ n₁) → P (pr₁ p₂) (pr₂ p₂)),
have hlt₁ : 0 < succ n₁, from succ_pos n₁,
have hlt₂ : (succ n₁, m mod succ n₁) ≺ (m, succ n₁), from gcd.lt.dec _ _,
have hp : P (succ n₁) (m mod succ n₁), from ih _ hlt₂,
show P m (succ n₁), from
H1 m (succ n₁) hlt₁ hp))),
aux
theorem gcd_dvd (m n : ) : (gcd m n | m) ∧ (gcd m n | n) :=
gcd.induction m n
(take m,
show (gcd m 0 | m) ∧ (gcd m 0 | 0), by simp)
(take m n,
assume npos : 0 < n,
assume IH : (gcd n (m mod n) | n) ∧ (gcd n (m mod n) | (m mod n)),
have H : gcd n (m mod n) | (m div n * n + m mod n), from
dvd_add (dvd.trans (and.elim_left IH) !dvd_mul_left) (and.elim_right IH),
have H1 : gcd n (m mod n) | m, from eq_div_mul_add_mod⁻¹ ▸ H,
have gcd_eq : gcd n (m mod n) = gcd m n, from !gcd_rec⁻¹,
show (gcd m n | m) ∧ (gcd m n | n), from gcd_eq ▸ (and.intro H1 (and.elim_left IH)))
theorem gcd_dvd_left (m n : ) : (gcd m n | m) := and.elim_left !gcd_dvd
theorem gcd_dvd_right (m n : ) : (gcd m n | n) := and.elim_right !gcd_dvd
theorem dvd_gcd {m n k : } : k | m → k | n → k | (gcd m n) :=
gcd.induction m n
(take m, assume (h₁ : k | m) (h₂ : k | 0),
show k | gcd m 0, from !gcd_zero_right⁻¹ ▸ h₁)
(take m n,
assume npos : n > 0,
assume IH : k | n → k | (m mod n) → k | gcd n (m mod n),
assume H1 : k | m,
assume H2 : k | n,
have H3 : k | m div n * n + m mod n, from eq_div_mul_add_mod ▸ H1,
have H4 : k | m mod n, from nat.dvd_of_dvd_add_left H3 (dvd.trans H2 (by simp)),
have gcd_eq : gcd n (m mod n) = gcd m n, from !gcd_rec⁻¹,
show k | gcd m n, from gcd_eq ▸ IH H2 H4)
theorem gcd.comm (m n : ) : gcd m n = gcd n m :=
dvd.antisymm
(dvd_gcd !gcd_dvd_right !gcd_dvd_left)
(dvd_gcd !gcd_dvd_right !gcd_dvd_left)
theorem gcd.assoc (m n k : ) : gcd (gcd m n) k = gcd m (gcd n k) :=
dvd.antisymm
(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_one_left (m : ) : gcd 1 m = 1 :=
!gcd.comm ⬝ !gcd_one_right
theorem gcd_mul_left (m n k : ) : gcd (m * n) (m * k) = m * gcd n k :=
gcd.induction n k
(take n,
calc
gcd (m * n) (m * 0) = gcd (m * n) 0 : mul_zero
... = m * n : gcd_zero_right
... = m * gcd n 0 : gcd_zero_right)
(take n k,
assume H : 0 < k,
assume IH : gcd (m * k) (m * (n mod k)) = m * gcd k (n mod k),
calc
gcd (m * n) (m * k) = gcd (m * k) (m * n mod (m * k)) : !gcd_rec
... = gcd (m * k) (m * (n mod k)) : mul_mod_mul_left
... = m * gcd k (n mod k) : IH
... = m * gcd n k : !gcd_rec)
theorem gcd_mul_right (m n k : ) : gcd (m * n) (k * n) = gcd m k * n :=
calc
gcd (m * n) (k * n) = gcd (n * m) (k * n) : mul.comm
... = gcd (n * m) (n * k) : mul.comm
... = n * gcd m k : gcd_mul_left
... = gcd m k * n : mul.comm
theorem gcd_pos_of_pos_left {m : } (n : ) (mpos : m > 0) : gcd m n > 0 :=
pos_of_dvd_of_pos !gcd_dvd_left mpos
theorem gcd_pos_of_pos_right (m : ) {n : } (npos : n > 0) : gcd m n > 0 :=
pos_of_dvd_of_pos !gcd_dvd_right npos
theorem eq_zero_of_gcd_eq_zero_left {m n : } (H : gcd m n = 0) : m = 0 :=
or.elim (eq_zero_or_pos m)
(assume H1, H1)
(assume H1 : m > 0, absurd H⁻¹ (ne_of_lt (!gcd_pos_of_pos_left H1)))
theorem eq_zero_of_gcd_eq_zero_right {m n : } (H : gcd m n = 0) : n = 0 :=
eq_zero_of_gcd_eq_zero_left (!gcd.comm ▸ H)
theorem gcd_div {m n k : } (H1 : k | m) (H2 : k | n) : gcd (m div k) (n div k) = gcd m n div k :=
or.elim (eq_zero_or_pos k)
(assume H3 : k = 0,
calc
gcd (m div k) (n div k) = gcd (m div 0) (n div k) : H3
... = gcd 0 (n div k) : div_zero
... = n div k : gcd_zero_left
... = n div 0 : H3
... = 0 : div_zero
... = gcd m n div 0 : div_zero
... = gcd m n div k : H3)
(assume H3 : k > 0,
eq_div_of_mul_eq H3
(calc
gcd (m div k) (n div k) * k = gcd (m div k * k) (n div k * k) : gcd_mul_right
... = gcd m (n div k * k) : div_mul_cancel H1
... = gcd m n : div_mul_cancel H2))
theorem gcd_dvd_gcd_mul_left (m n k : ) : gcd m n | gcd (k * m) n :=
dvd_gcd (dvd.trans !gcd_dvd_left !dvd_mul_left) !gcd_dvd_right
theorem gcd_dvd_gcd_mul_right (m n k : ) : gcd m n | gcd (m * k) n :=
!mul.comm ▸ !gcd_dvd_gcd_mul_left
theorem gcd_dvd_gcd_mul_left_right (m n k : ) : gcd m n | gcd m (k * n) :=
dvd_gcd !gcd_dvd_left (dvd.trans !gcd_dvd_right !dvd_mul_left)
theorem gcd_dvd_gcd_mul_right_right (m n k : ) : gcd m n | gcd m (n * k) :=
!mul.comm ▸ !gcd_dvd_gcd_mul_left_right
/- lcm -/
definition lcm (m n : ) : := m * n div (gcd m n)
theorem lcm.comm (m n : ) : lcm m n = lcm n m :=
calc
lcm m n = m * n div gcd m n : rfl
... = n * m div gcd m n : mul.comm
... = n * m div gcd n m : gcd.comm
... = lcm n m : rfl
theorem lcm_zero_left (m : ) : lcm 0 m = 0 :=
calc
lcm 0 m = 0 * m div gcd 0 m : rfl
... = 0 div gcd 0 m : zero_mul
... = 0 : zero_div
theorem lcm_zero_right (m : ) : lcm m 0 = 0 := !lcm.comm ▸ !lcm_zero_left
theorem lcm_one_left (m : ) : lcm 1 m = m :=
calc
lcm 1 m = 1 * m div gcd 1 m : rfl
... = m div gcd 1 m : one_mul
... = m div 1 : gcd_one_left
... = m : div_one
theorem lcm_one_right (m : ) : lcm m 1 = m := !lcm.comm ▸ !lcm_one_left
theorem lcm_self (m : ) : lcm m m = m :=
have H : m * m div m = m, from
by_cases_zero_pos m !div_zero (take m, assume H1 : m > 0, !mul_div_cancel H1),
calc
lcm m m = m * m div gcd m m : rfl
... = m * m div m : gcd_self
... = m : H
theorem dvd_lcm_left (m n : ) : m | lcm m n :=
have H : lcm m n = m * (n div gcd m n), from mul_div_assoc _ !gcd_dvd_right,
dvd.intro H⁻¹
theorem dvd_lcm_right (m n : ) : n | lcm m n :=
!lcm.comm ▸ !dvd_lcm_left
theorem gcd_mul_lcm (m n : ) : gcd m n * lcm m n = m * n :=
eq.symm (eq_mul_of_div_eq (dvd.trans !gcd_dvd_left !dvd_mul_right) rfl)
theorem lcm_dvd {m n k : } (H1 : m | k) (H2 : n | k) : lcm m n | k :=
or.elim (eq_zero_or_pos k)
(assume kzero : k = 0, !kzero⁻¹ ▸ !dvd_zero)
(assume kpos : k > 0,
have mpos : m > 0, from pos_of_dvd_of_pos H1 kpos,
have npos : n > 0, from pos_of_dvd_of_pos H2 kpos,
have gcd_pos : gcd m n > 0, from !gcd_pos_of_pos_left mpos,
obtain p (km : k = m * p), from exists_eq_mul_right_of_dvd H1,
obtain q (kn : k = n * q), from exists_eq_mul_right_of_dvd H2,
have ppos : p > 0, from pos_of_mul_pos_left (km ▸ kpos),
have qpos : q > 0, from pos_of_mul_pos_left (kn ▸ kpos),
have H3 : p * q * (m * n * gcd p q) = p * q * (gcd m n * k), from
calc
p * q * (m * n * gcd p q) = p * (q * (m * n * gcd p q)) : mul.assoc
... = p * (q * (m * (n * gcd p q))) : mul.assoc
... = p * (m * (q * (n * gcd p q))) : mul.left_comm
... = p * m * (q * (n * gcd p q)) : mul.assoc
... = p * m * (q * n * gcd p q) : mul.assoc
... = m * p * (q * n * gcd p q) : mul.comm
... = k * (q * n * gcd p q) : km
... = k * (n * q * gcd p q) : mul.comm
... = k * (k * gcd p q) : kn
... = k * gcd (k * p) (k * q) : gcd_mul_left
... = k * gcd (n * q * p) (k * q) : kn
... = k * gcd (n * q * p) (m * p * q) : km
... = k * gcd (n * (q * p)) (m * p * q) : mul.assoc
... = k * gcd (n * (q * p)) (m * (p * q)) : mul.assoc
... = k * gcd (n * (p * q)) (m * (p * q)) : mul.comm
... = k * (gcd n m * (p * q)) : gcd_mul_right
... = gcd n m * (p * q) * k : mul.comm
... = p * q * gcd n m * k : mul.comm
... = p * q * (gcd n m * k) : mul.assoc
... = p * q * (gcd m n * k) : gcd.comm,
have H4 : m * n * gcd p q = gcd m n * k,
from !eq_of_mul_eq_mul_left (mul_pos ppos qpos) H3,
have H5 : gcd m n * (lcm m n * gcd p q) = gcd m n * k,
from !mul.assoc ▸ !gcd_mul_lcm⁻¹ ▸ H4,
have H6 : lcm m n * gcd p q = k,
from !eq_of_mul_eq_mul_left gcd_pos H5,
dvd.intro H6)
theorem lcm_assoc (m n k : ) : lcm (lcm m n) k = lcm m (lcm n k) :=
dvd.antisymm
(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 -/
definition coprime [reducible] (m n : ) : Prop := gcd m n = 1
theorem coprime_swap {m n : } (H : coprime n m) : coprime m n :=
!gcd.comm ▸ H
theorem dvd_of_coprime_of_dvd_mul_right {m n k : } (H1 : coprime k n) (H2 : k | m * n) : k | m :=
have H3 : gcd (m * k) (m * n) = m, from
calc
gcd (m * k) (m * n) = m * gcd k n : gcd_mul_left
... = m * 1 : H1
... = m : mul_one,
have H4 : k | gcd (m * k) (m * n), from dvd_gcd !dvd_mul_left H2,
H3 ▸ H4
theorem dvd_of_coprime_of_dvd_mul_left {m n k : } (H1 : coprime k m) (H2 : k | m * n) : k | n :=
dvd_of_coprime_of_dvd_mul_right H1 (!mul.comm ▸ H2)
theorem gcd_mul_left_cancel_of_coprime {k : } (m : ) {n : } (H : coprime k n) :
gcd (k * m) n = gcd m n :=
have H1 : coprime (gcd (k * m) n) k, from
calc
gcd (gcd (k * m) n) k = gcd k (gcd (k * m) n) : gcd.comm
... = gcd (gcd k (k * m)) n : gcd.assoc
... = gcd (gcd (k * 1) (k * m)) n : mul_one
... = gcd (k * gcd 1 m) n : gcd_mul_left
... = gcd (k * 1) n : gcd_one_left
... = gcd k n : mul_one
... = 1 : H,
dvd.antisymm
(dvd_gcd (dvd_of_coprime_of_dvd_mul_left H1 !gcd_dvd_left) !gcd_dvd_right)
(dvd_gcd (dvd.trans !gcd_dvd_left !dvd_mul_left) !gcd_dvd_right)
theorem gcd_mul_right_cancel_of_coprime (m : ) {k n : } (H : coprime k n) :
gcd (m * k) n = gcd m n :=
!mul.comm ▸ !gcd_mul_left_cancel_of_coprime H
theorem gcd_mul_left_cancel_of_coprime_right {k m : } (n : ) (H : coprime k m) :
gcd m (k * n) = gcd m n :=
!gcd.comm ▸ !gcd.comm ▸ !gcd_mul_left_cancel_of_coprime H
theorem gcd_mul_right_cancel_of_coprime_right {k m : } (n : ) (H : coprime k m) :
gcd m (n * k) = gcd m n :=
!gcd.comm ▸ !gcd.comm ▸ !gcd_mul_right_cancel_of_coprime H
theorem coprime_div_gcd_div_gcd {m n : } (H : gcd m n > 0) :
coprime (m div gcd m n) (n div gcd m n) :=
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 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)⁻¹,
have H2 : n = (n div gcd m n) * gcd m n, from (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 {m n k : } (H1 : coprime m k) (H2 : coprime n k) : coprime (m * n) k :=
calc
gcd (m * n) k = gcd n k : !gcd_mul_left_cancel_of_coprime H1
... = 1 : H2
theorem coprime_mul_right {k m n : } (H1 : coprime k m) (H2 : coprime k n) : coprime k (m * n) :=
coprime_swap (coprime_mul (coprime_swap H1) (coprime_swap H2))
theorem coprime_of_coprime_mul_left {k m n : } (H : coprime (k * m) n) : coprime m n :=
have H1 : gcd m n | gcd (k * m) n, from !gcd_dvd_gcd_mul_left,
eq_one_of_dvd_one (H ▸ H1)
theorem coprime_of_coprime_mul_right {k m n : } (H : coprime (m * k) n) : coprime m n :=
coprime_of_coprime_mul_left (!mul.comm ▸ H)
theorem coprime_of_coprime_mul_left_right {k m n : } (H : coprime m (k * n)) : coprime m n :=
coprime_swap (coprime_of_coprime_mul_left (coprime_swap H))
theorem coprime_of_coprime_mul_right_right {k m n : } (H : coprime m (n * k)) : coprime m n :=
coprime_of_coprime_mul_left_right (!mul.comm ▸ H)
theorem exists_eq_prod_and_dvd_and_dvd {m n k} (H : k | m * n) :
∃ m' n', k = m' * n' ∧ m' | m ∧ n' | n :=
or.elim (eq_zero_or_pos (gcd k m))
(assume H1 : gcd k m = 0,
have H2 : k = 0, from eq_zero_of_gcd_eq_zero_left H1,
have H3 : m = 0, from eq_zero_of_gcd_eq_zero_right H1,
have H4 : k = 0 * n, from H2 ⬝ !zero_mul⁻¹,
have H5 : 0 | m, from H3⁻¹ ▸ !dvd.refl,
have H6 : n | n, from !dvd.refl,
exists.intro _ (exists.intro _ (and.intro H4 (and.intro H5 H6))))
(assume H1 : gcd k m > 0,
have H2 : gcd k m | k, from !gcd_dvd_left,
have H3 : k div gcd k m | (m * n) div gcd k m, from div_dvd_div H2 H,
have H4 : (m * n) div gcd k m = (m div gcd k m) * n, from
calc
m * n div gcd k m = n * m div gcd k m : mul.comm
... = n * (m div gcd k m) : !mul_div_assoc !gcd_dvd_right
... = m div gcd k m * n : mul.comm,
have H5 : k div gcd k m | (m div gcd k m) * n, from H4 ▸ H3,
have H6 : coprime (k div gcd k m) (m div gcd k m), from coprime_div_gcd_div_gcd H1,
have H7 : k div gcd k m | n, from dvd_of_coprime_of_dvd_mul_left H6 H5,
have H8 : k = gcd k m * (k div gcd k m), from (mul_div_cancel' H2)⁻¹,
exists.intro _ (exists.intro _ (and.intro H8 (and.intro !gcd_dvd_right H7))))
end nat