lean2/library/data/nat/div.lean

700 lines
26 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.
--- Author: Jeremy Avigad
-- div.lean
-- ========
--
-- This is a continuation of the development of the natural numbers, with a general way of
-- defining recursive functions, and definitions of div, mod, and gcd.
import logic .sub algebra.relation data.prod
import tools.fake_simplifier
open nat relation relation.iff_ops prod
open fake_simplifier decidable
open eq.ops
namespace nat
-- A general recursion principle
-- -----------------------------
--
-- Data:
--
-- dom, codom : Type
-- default : codom
-- measure : dom →
-- rec_val : dom → (dom → codom) → codom
--
-- and a proof
--
-- rec_decreasing : ∀m, m ≥ measure x, rec_val x f = rec_val x (restrict f m)
--
-- ... which says that the recursive call only depends on f at values with measure less than x,
-- in the sense that changing other values to the default value doesn't change the result.
--
-- The result is a function f = rec_measure, satisfying
--
-- f x = rec_val x f
definition restrict {dom codom : Type} (default : codom) (measure : dom → ) (f : dom → codom)
(m : ) (x : dom) :=
if measure x < m then f x else default
theorem restrict_lt_eq {dom codom : Type} (default : codom) (measure : dom → ) (f : dom → codom)
(m : ) (x : dom) (H : measure x < m) :
restrict default measure f m x = f x :=
if_pos H
theorem restrict_not_lt_eq {dom codom : Type} (default : codom) (measure : dom → )
(f : dom → codom) (m : ) (x : dom) (H : ¬ measure x < m) :
restrict default measure f m x = default :=
if_neg H
definition rec_measure_aux {dom codom : Type} (default : codom) (measure : dom → )
(rec_val : dom → (dom → codom) → codom) : → dom → codom :=
rec (λx, default) (λm g x, if measure x < succ m then rec_val x g else default)
definition rec_measure {dom codom : Type} (default : codom) (measure : dom → )
(rec_val : dom → (dom → codom) → codom) (x : dom) : codom :=
rec_measure_aux default measure rec_val (succ (measure x)) x
theorem rec_measure_aux_spec {dom codom : Type} (default : codom) (measure : dom → )
(rec_val : dom → (dom → codom) → codom)
(rec_decreasing : ∀g1 g2 x, (∀z, measure z < measure x → g1 z = g2 z) →
rec_val x g1 = rec_val x g2)
(m : ) :
let f' := rec_measure_aux default measure rec_val in
let f := rec_measure default measure rec_val in
∀x, f' m x = restrict default measure f m x :=
let f' := rec_measure_aux default measure rec_val in
let f := rec_measure default measure rec_val in
case_strong_induction_on m
(take x,
have H1 : f' 0 x = default, from rfl,
have H2 : ¬ measure x < 0, from not_lt_zero,
have H3 : restrict default measure f 0 x = default, from if_neg H2,
show f' 0 x = restrict default measure f 0 x, from H1 ⬝ H3⁻¹)
(take m,
assume IH: ∀n, n ≤ m → ∀x, f' n x = restrict default measure f n x,
take x : dom,
show f' (succ m) x = restrict default measure f (succ m) x, from
by_cases -- (measure x < succ m)
(assume H1 : measure x < succ m,
have H2a : ∀z, measure z < measure x → f' m z = f z, from
take z,
assume Hzx : measure z < measure x,
calc
f' m z = restrict default measure f m z : IH m le_refl z
... = f z : restrict_lt_eq _ _ _ _ _ (lt_le_trans Hzx (lt_succ_imp_le H1)),
have H2 : f' (succ m) x = rec_val x f, from
calc
f' (succ m) x = if measure x < succ m then rec_val x (f' m) else default : rfl
... = rec_val x (f' m) : if_pos H1
... = rec_val x f : rec_decreasing (f' m) f x H2a,
let m' := measure x in
have H3a : ∀z, measure z < m' → f' m' z = f z, from
take z,
assume Hzx : measure z < measure x,
calc
f' m' z = restrict default measure f m' z : IH _ (lt_succ_imp_le H1) _
... = f z : restrict_lt_eq _ _ _ _ _ Hzx,
have H3 : restrict default measure f (succ m) x = rec_val x f, from
calc
restrict default measure f (succ m) x = f x : if_pos H1
... = f' (succ m') x : eq.refl _
... = if measure x < succ m' then rec_val x (f' m') else default : rfl
... = rec_val x (f' m') : if_pos self_lt_succ
... = rec_val x f : rec_decreasing _ _ _ H3a,
show f' (succ m) x = restrict default measure f (succ m) x,
from H2 ⬝ H3⁻¹)
(assume H1 : ¬ measure x < succ m,
have H2 : f' (succ m) x = default, from
calc
f' (succ m) x = if measure x < succ m then rec_val x (f' m) else default : rfl
... = default : if_neg H1,
have H3 : restrict default measure f (succ m) x = default,
from if_neg H1,
show f' (succ m) x = restrict default measure f (succ m) x,
from H2 ⬝ H3⁻¹))
theorem rec_measure_spec {dom codom : Type} {default : codom} {measure : dom → }
(rec_val : dom → (dom → codom) → codom)
(rec_decreasing : ∀g1 g2 x, (∀z, measure z < measure x → g1 z = g2 z) →
rec_val x g1 = rec_val x g2)
(x : dom):
let f := rec_measure default measure rec_val in
f x = rec_val x f :=
let f' := rec_measure_aux default measure rec_val in
let f := rec_measure default measure rec_val in
let m := measure x in
have H : ∀z, measure z < measure x → f' m z = f z, from
take z,
assume H1 : measure z < measure x,
calc
f' m z = restrict default measure f m z : rec_measure_aux_spec _ _ _ rec_decreasing m z
... = f z : restrict_lt_eq _ _ _ _ _ H1,
calc
f x = f' (succ m) x : rfl
... = if measure x < succ m then rec_val x (f' m) else default : rfl
... = rec_val x (f' m) : if_pos (self_lt_succ)
... = rec_val x f : rec_decreasing _ _ _ H
-- Div and mod
-- -----------
-- ### the definition of div
-- for fixed y, recursive call for x div y
definition div_aux_rec (y : ) (x : ) (div_aux' : ) : :=
if (y = 0 x < y) then 0 else succ (div_aux' (x - y))
definition div_aux (y : ) : := rec_measure 0 (fun x, x) (div_aux_rec y)
theorem div_aux_decreasing (y : ) (g1 g2 : ) (x : ) (H : ∀z, z < x → g1 z = g2 z) :
div_aux_rec y x g1 = div_aux_rec y x g2 :=
let lhs := div_aux_rec y x g1 in
let rhs := div_aux_rec y x g2 in
show lhs = rhs, from
by_cases -- (y = 0 x < y)
(assume H1 : y = 0 x < y,
calc
lhs = 0 : if_pos H1
... = rhs : (if_pos H1)⁻¹)
(assume H1 : ¬ (y = 0 x < y),
have H2a : y ≠ 0, from assume H, H1 (or.inl H),
have H2b : ¬ x < y, from assume H, H1 (or.inr H),
have ypos : y > 0, from ne_zero_imp_pos H2a,
have xgey : x ≥ y, from not_lt_imp_ge H2b,
have H4 : x - y < x, from sub_lt (lt_le_trans ypos xgey) ypos,
calc
lhs = succ (g1 (x - y)) : if_neg H1
... = succ (g2 (x - y)) : {H _ H4}
... = rhs : (if_neg H1)⁻¹)
theorem div_aux_spec (y : ) (x : ) :
div_aux y x = if (y = 0 x < y) then 0 else succ (div_aux y (x - y)) :=
rec_measure_spec (div_aux_rec y) (div_aux_decreasing y) x
definition idivide (x : ) (y : ) : := div_aux y x
infixl `div` := idivide
theorem div_zero {x : } : x div 0 = 0 :=
div_aux_spec _ _ ⬝ if_pos (or.inl rfl)
-- add_rewrite div_zero
theorem div_less {x y : } (H : x < y) : x div y = 0 :=
div_aux_spec _ _ ⬝ if_pos (or.inr H)
-- add_rewrite div_less
theorem zero_div {y : } : 0 div y = 0 :=
case y div_zero (take y', div_less succ_pos)
-- add_rewrite zero_div
theorem div_rec {x y : } (H1 : y > 0) (H2 : x ≥ y) : x div y = succ ((x - y) div y) :=
have H3 : ¬ (y = 0 x < y), from
not_intro
(assume H4 : y = 0 x < y,
or.elim H4
(assume H5 : y = 0, not_elim lt_irrefl (H5 ▸ H1))
(assume H5 : x < y, not_elim (lt_imp_not_ge H5) H2)),
div_aux_spec _ _ ⬝ if_neg H3
theorem div_add_self_right {x z : } (H : z > 0) : (x + z) div z = succ (x div z) :=
have H1 : z ≤ x + z, by simp,
let H2 := div_rec H H1 in
by simp
theorem div_add_mul_self_right {x y z : } (H : z > 0) : (x + y * z) div z = x div z + y :=
induction_on y (by simp)
(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) : div_add_self_right H
... = x div z + succ y : by simp)
-- ### The definition of mod
-- for fixed y, recursive call for x mod y
definition mod_aux_rec (y : ) (x : ) (mod_aux' : ) : :=
if (y = 0 x < y) then x else mod_aux' (x - y)
definition mod_aux (y : ) : := rec_measure 0 (fun x, x) (mod_aux_rec y)
theorem mod_aux_decreasing (y : ) (g1 g2 : ) (x : ) (H : ∀z, z < x → g1 z = g2 z) :
mod_aux_rec y x g1 = mod_aux_rec y x g2 :=
let lhs := mod_aux_rec y x g1 in
let rhs := mod_aux_rec y x g2 in
show lhs = rhs, from
by_cases -- (y = 0 x < y)
(assume H1 : y = 0 x < y,
calc
lhs = x : if_pos H1
... = rhs : (if_pos H1)⁻¹)
(assume H1 : ¬ (y = 0 x < y),
have H2a : y ≠ 0, from assume H, H1 (or.inl H),
have H2b : ¬ x < y, from assume H, H1 (or.inr H),
have ypos : y > 0, from ne_zero_imp_pos H2a,
have xgey : x ≥ y, from not_lt_imp_ge H2b,
have H4 : x - y < x, from sub_lt (lt_le_trans ypos xgey) ypos,
calc
lhs = g1 (x - y) : if_neg H1
... = g2 (x - y) : H _ H4
... = rhs : (if_neg H1)⁻¹)
theorem mod_aux_spec (y : ) (x : ) :
mod_aux y x = if (y = 0 x < y) then x else mod_aux y (x - y) :=
rec_measure_spec (mod_aux_rec y) (mod_aux_decreasing y) x
definition modulo (x : ) (y : ) : := mod_aux y x
infixl `mod` := modulo
theorem mod_zero {x : } : x mod 0 = x :=
mod_aux_spec _ _ ⬝ if_pos (or.inl rfl)
-- add_rewrite mod_zero
theorem mod_lt_eq {x y : } (H : x < y) : x mod y = x :=
mod_aux_spec _ _ ⬝ if_pos (or.inr H)
-- add_rewrite mod_lt_eq
theorem zero_mod {y : } : 0 mod y = 0 :=
case y mod_zero (take y', mod_lt_eq succ_pos)
-- add_rewrite zero_mod
theorem mod_rec {x y : } (H1 : y > 0) (H2 : x ≥ y) : x mod y = (x - y) mod y :=
have H3 : ¬ (y = 0 x < y), from
not_intro
(assume H4 : y = 0 x < y,
or.elim H4
(assume H5 : y = 0, not_elim lt_irrefl (H5 ▸ H1))
(assume H5 : x < y, not_elim (lt_imp_not_ge H5) H2)),
mod_aux_spec _ _ ⬝ if_neg H3
-- need more of these, add as rewrite rules
theorem mod_add_self_right {x z : } (H : z > 0) : (x + z) mod z = x mod z :=
have H1 : z ≤ x + z, by simp,
let H2 := mod_rec H H1 in
by simp
theorem mod_add_mul_self_right {x y z : } (H : z > 0) : (x + y * z) mod z = x mod z :=
induction_on y (by simp)
(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 : by simp
... = (x + y * z) mod z : mod_add_self_right H
... = x mod z : IH)
theorem mod_mul_self_right {m n : } : (m * n) mod n = 0 :=
case_zero_pos n (by simp)
(take n,
assume npos : n > 0,
(by simp) ▸ (@mod_add_mul_self_right 0 m _ npos))
-- add_rewrite mod_mul_self_right
theorem mod_mul_self_left {m n : } : (m * n) mod m = 0 :=
!mul.comm ▸ mod_mul_self_right
-- add_rewrite mod_mul_self_left
-- ### properties of div and mod together
theorem mod_lt {x y : } (H : y > 0) : x mod y < y :=
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_lt_eq H1,
show succ x mod y < y, from H2⁻¹ ▸ H1)
(assume H1 : ¬ succ x < y,
have H2 : y ≤ succ x, from not_lt_imp_ge H1,
have H3 : succ x mod y = (succ x - y) mod y, from mod_rec H H2,
have H4 : succ x - y < succ x, from sub_lt succ_pos H,
have H5 : succ x - y ≤ x, from lt_succ_imp_le H4,
show succ x mod y < y, from H3⁻¹ ▸ IH _ H5))
theorem div_mod_eq {x y : } : x = x div y * y + x mod y :=
case_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_right}
... = x mod 0 : !add.zero_left
... = x : mod_zero)⁻¹)
(take y,
assume H : y > 0,
show x = x div y * y + x mod y, from
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_less H1,
have H3 : succ x mod y = succ x, from mod_lt_eq H1,
by simp)
(assume H1 : ¬ succ x < y,
have H2 : y ≤ succ x, from not_lt_imp_ge H1,
have H3 : succ x div y = succ ((succ x - y) div y), from div_rec H H2,
have H4 : succ x mod y = (succ x - y) mod y, from mod_rec H H2,
have H5 : succ x - y < succ x, from sub_lt succ_pos H,
have H6 : succ x - y ≤ x, from lt_succ_imp_le 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 : {!mul.succ_left}
... = ((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 : add_sub_ge_left H2)⁻¹)))
theorem mod_le {x y : } : x mod y ≤ x :=
div_mod_eq⁻¹ ▸ le_add_left
--- a good example where simplifying using the context causes problems
theorem remainder_unique {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 : (mod_add_mul_self_right H)⁻¹
... = (q1 * y + r1) mod y : {!add.comm}
... = (r2 + q2 * y) mod y : by simp
... = r2 mod y : mod_add_mul_self_right H
... = r2 : by simp
theorem quotient_unique {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 (remainder_unique H H1 H2 H3) ▸ H3,
have H5 : q1 * y = q2 * y, from add.cancel_right H4,
have H6 : y > 0, from le_lt_trans zero_le H1,
show q1 = q2, from mul_cancel_right H6 H5
theorem div_mul_mul {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 ne_zero_imp_pos 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_left zpos (mod_lt ypos),
quotient_unique zypos H1 H2
(calc
((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : div_mod_eq⁻¹
... = z * (x div y * y + x mod y) : {div_mod_eq}
... = z * (x div y * y) + z * (x mod y) : !mul.distr_left
... = (x div y) * (z * y) + z * (x mod y) : {!mul.left_comm}))
--- something wrong with the term order
--- ... = (x div y) * (z * y) + z * (x mod y) : by simp))
theorem mod_mul_mul {z x y : } (zpos : z > 0) : (z * x) mod (z * y) = z * (x mod y) :=
by_cases -- (y = 0)
(assume H : y = 0, by simp)
(assume H : y ≠ 0,
have ypos : y > 0, from ne_zero_imp_pos 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_left zpos (mod_lt ypos),
remainder_unique zypos H1 H2
(calc
((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : div_mod_eq⁻¹
... = z * (x div y * y + x mod y) : {div_mod_eq}
... = z * (x div y * y) + z * (x mod y) : !mul.distr_left
... = (x div y) * (z * y) + z * (x mod y) : {!mul.left_comm}))
theorem mod_one {x : } : x mod 1 = 0 :=
have H1 : x mod 1 < 1, from mod_lt succ_pos,
le_zero (lt_succ_imp_le H1)
-- add_rewrite mod_one
theorem mod_self {n : } : n mod n = 0 :=
case n (by simp)
(take n,
have H : (succ n * 1) mod (succ n * 1) = succ n * (1 mod 1),
from mod_mul_mul succ_pos,
(by simp) ▸ H)
-- add_rewrite mod_self
theorem div_one {n : } : n div 1 = n :=
have H : n div 1 * 1 + n mod 1 = n, from div_mod_eq⁻¹,
(by simp) ▸ H
-- add_rewrite div_one
theorem pos_div_self {n : } (H : n > 0) : n div n = 1 :=
have H1 : (n * 1) div (n * 1) = 1 div 1, from div_mul_mul H,
(by simp) ▸ H1
-- add_rewrite pos_div_self
-- Divides
-- -------
definition dvd (x y : ) : Prop := y mod x = 0
infix `|` := dvd
theorem dvd_iff_mod_eq_zero {x y : } : x | y ↔ y mod x = 0 :=
refl _
theorem dvd_imp_div_mul_eq {x y : } (H : y | x) : x div y * y = x :=
(calc
x = x div y * y + x mod y : div_mod_eq
... = x div y * y + 0 : {mp dvd_iff_mod_eq_zero H}
... = x div y * y : !add.zero_right)⁻¹
-- add_rewrite dvd_imp_div_mul_eq
theorem mul_eq_imp_dvd {z x y : } (H : z * y = x) : y | x :=
have H1 : z * y = x mod y + x div y * y, from
H ⬝ div_mod_eq ⬝ !add.comm,
have H2 : (z - x div y) * y = x mod y, from
calc
(z - x div y) * y = z * y - x div y * y : mul_sub_distr_right
... = x mod y + x div y * y - x div y * y : {H1}
... = x mod y : sub_add_left,
show x mod y = 0, from
by_cases
(assume yz : y = 0,
have xz : x = 0, from
calc
x = z * y : H⁻¹
... = z * 0 : {yz}
... = 0 : !mul.zero_right,
calc
x mod y = x mod 0 : {yz}
... = x : mod_zero
... = 0 : xz)
(assume ynz : y ≠ 0,
have ypos : y > 0, from ne_zero_imp_pos ynz,
have H3 : (z - x div y) * y < y, from H2⁻¹ ▸ mod_lt ypos,
have H4 : (z - x div y) * y < 1 * y, from !mul.one_left⁻¹ ▸ H3,
have H5 : z - x div y < 1, from mul_lt_cancel_right H4,
have H6 : z - x div y = 0, from le_zero (lt_succ_imp_le H5),
calc
x mod y = (z - x div y) * y : H2⁻¹
... = 0 * y : {H6}
... = 0 : !mul.zero_left)
theorem dvd_iff_exists_mul {x y : } : x | y ↔ ∃z, z * x = y :=
iff.intro
(assume H : x | y,
show ∃z, z * x = y, from exists_intro _ (dvd_imp_div_mul_eq H))
(assume H : ∃z, z * x = y,
obtain (z : ) (zx_eq : z * x = y), from H,
show x | y, from mul_eq_imp_dvd zx_eq)
theorem dvd_zero {n : } : n | 0 := sorry
-- (by simp) (dvd_iff_mod_eq_zero n 0)
-- add_rewrite dvd_zero
theorem zero_dvd_iff {n : } : (0 | n) = (n = 0) := sorry
-- (by simp) (dvd_iff_mod_eq_zero 0 n)
-- add_rewrite zero_dvd_iff
theorem one_dvd {n : } : 1 | n := sorry
-- (by simp) (dvd_iff_mod_eq_zero 1 n)
-- add_rewrite one_dvd
theorem dvd_self {n : } : n | n := sorry
-- (by simp) (dvd_iff_mod_eq_zero n n)
-- add_rewrite dvd_self
theorem dvd_mul_self_left {m n : } : m | (m * n) := sorry
-- (by simp) (dvd_iff_mod_eq_zero m (m * n))
-- add_rewrite dvd_mul_self_left
theorem dvd_mul_self_right {m n : } : m | (n * m) := sorry
-- (by simp) (dvd_iff_mod_eq_zero m (n * m))
-- add_rewrite dvd_mul_self_left
theorem dvd_trans {m n k : } (H1 : m | n) (H2 : n | k) : m | k :=
have H3 : n = n div m * m, by simp,
have H4 : k = k div n * (n div m) * m, from
calc
k = k div n * n : by simp
... = k div n * (n div m * m) : {H3}
... = k div n * (n div m) * m : !mul.assoc⁻¹,
mp (dvd_iff_exists_mul⁻¹) (exists_intro (k div n * (n div m)) (H4⁻¹))
theorem dvd_add {m n1 n2 : } (H1 : m | n1) (H2 : m | n2) : m | (n1 + n2) :=
have H : (n1 div m + n2 div m) * m = n1 + n2, by simp,
mp (dvd_iff_exists_mul⁻¹) (exists_intro _ H)
theorem dvd_add_cancel_left {m n1 n2 : } : m | (n1 + n2) → m | n1 → m | n2 :=
case_zero_pos m
(assume H1 : 0 | n1 + n2,
assume H2 : 0 | n1,
have H3 : n1 + n2 = 0, from zero_dvd_iff ▸ H1,
have H4 : n1 = 0, from zero_dvd_iff ▸ H2,
have H5 : n2 = 0, from mp (by simp) (H4 ▸ H3),
show 0 | n2, by simp)
(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 : by simp
... = (n1 div m * m + n2) div m * m : by simp
... = (n2 + n1 div m * m) div m * m : {!add.comm}
... = (n2 div m + n1 div m) * m : {div_add_mul_self_right mpos}
... = n2 div m * m + n1 div m * m : !mul.distr_right
... = n1 div m * m + n2 div m * m : !add.comm
... = n1 + n2 div m * m : by simp,
have H4 : n2 = n2 div m * m, from add.cancel_left H3,
mp (dvd_iff_exists_mul⁻¹) (exists_intro _ (H4⁻¹)))
theorem dvd_add_cancel_right {m n1 n2 : } (H : m | (n1 + n2)) : m | n2 → m | n1 :=
dvd_add_cancel_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 (add_sub_ge_left H3)⁻¹,
show m | n1 - n2, from dvd_add_cancel_right (H4 ▸ H1) H2)
(assume H3 : ¬ (n1 ≥ n2),
have H4 : n1 - n2 = 0, from le_imp_sub_eq_zero (lt_imp_le (not_le_imp_gt H3)),
show m | n1 - n2, from H4⁻¹ ▸ dvd_zero)
-- Gcd and lcm
-- -----------
-- ### definition of gcd
definition gcd_aux_measure (p : × ) : :=
pr2 p
definition gcd_aux_rec (p : × ) (gcd_aux' : × ) : :=
let x := pr1 p, y := pr2 p in
if y = 0 then x else gcd_aux' (pair y (x mod y))
definition gcd_aux : × := rec_measure 0 gcd_aux_measure gcd_aux_rec
theorem gcd_aux_decreasing (g1 g2 : × ) (p : × )
(H : ∀p', gcd_aux_measure p' < gcd_aux_measure p → g1 p' = g2 p') :
gcd_aux_rec p g1 = gcd_aux_rec p g2 :=
let x := pr1 p, y := pr2 p in
let p' := pair y (x mod y) in
let lhs := gcd_aux_rec p g1 in
let rhs := gcd_aux_rec p g2 in
show lhs = rhs, from
by_cases -- (y = 0)
(assume H1 : y = 0,
calc
lhs = x : if_pos H1
... = rhs : (if_pos H1)⁻¹)
(assume H1 : y ≠ 0,
have ypos : y > 0, from ne_zero_imp_pos H1,
have H2 : gcd_aux_measure p' = x mod y, from pr2_pair _ _,
have H3 : gcd_aux_measure p' < gcd_aux_measure p, from H2⁻¹ ▸ mod_lt ypos,
calc
lhs = g1 p' : if_neg H1
... = g2 p' : H _ H3
... = rhs : (if_neg H1)⁻¹)
theorem gcd_aux_spec (p : × ) : gcd_aux p =
let x := pr1 p, y := pr2 p in
if y = 0 then x else gcd_aux (pair y (x mod y)) :=
rec_measure_spec gcd_aux_rec gcd_aux_decreasing p
definition gcd (x y : ) : := gcd_aux (pair x y)
theorem gcd_def (x y : ) : gcd x y = if y = 0 then x else gcd y (x mod y) :=
let x' := pr1 (pair x y), y' := pr2 (pair x y) in
calc
gcd x y = if y' = 0 then x' else gcd_aux (pair y' (x' mod y'))
: gcd_aux_spec (pair x y)
... = if y = 0 then x else gcd y (x mod y) : rfl
theorem gcd_zero (x : ) : gcd x 0 = x :=
(gcd_def x 0) ⬝ (if_pos rfl)
-- add_rewrite gcd_zero
theorem gcd_pos (m : ) {n : } (H : n > 0) : gcd m n = gcd n (m mod n) :=
gcd_def m n ⬝ if_neg (pos_imp_ne_zero H)
theorem gcd_zero_left (x : ) : gcd 0 x = x :=
case x (by simp) (take x, (gcd_def _ _) ⬝ (by simp))
-- add_rewrite gcd_zero_left
theorem gcd_induct {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 :=
have aux : ∀m, P m n, from
case_strong_induction_on n H0
(take n,
assume IH : ∀k, k ≤ n → ∀m, P m k,
take m,
have H2 : m mod succ n ≤ n, from lt_succ_imp_le (mod_lt succ_pos),
have H3 : P (succ n) (m mod succ n), from IH _ H2 _,
show P m (succ n), from H1 _ _ succ_pos H3),
aux m
theorem gcd_succ (m n : ) : gcd m (succ n) = gcd (succ n) (m mod succ n) :=
!gcd_def ⬝ if_neg !succ_ne_zero
theorem gcd_one (n : ) : gcd n 1 = 1 := sorry
-- (by simp) (gcd_succ n 0)
theorem gcd_self (n : ) : gcd n n = n := sorry
-- case n (by simp) (take n, (by simp) (gcd_succ (succ n) n))
theorem gcd_dvd (m n : ) : (gcd m n | m) ∧ (gcd m n | n) :=
gcd_induct 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_self_right) (and.elim_right IH),
have H1 : gcd n (m mod n) | m, from div_mod_eq⁻¹ ▸ H,
have gcd_eq : gcd n (m mod n) = gcd m n, from (gcd_pos _ npos)⁻¹,
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 _ _)
-- add_rewrite gcd_dvd_left gcd_dvd_right
theorem gcd_greatest {m n k : } : k | m → k | n → k | (gcd m n) :=
gcd_induct m n
(take m, assume H : k | m, sorry) -- by simp)
(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 div_mod_eq ▸ H1,
have H4 : k | m mod n, from dvd_add_cancel_left H3 (dvd_trans H2 (by simp)),
have gcd_eq : gcd n (m mod n) = gcd m n, from (gcd_pos _ npos)⁻¹,
show k | gcd m n, from gcd_eq ▸ IH H2 H4)
end nat