michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor/feat(library/data/nat): fix up sub and div, rename theorems, add theorems

Browse source
This commit is contained in:
Jeremy Avigad 2015-01-13 11:56:25 -05:00
parent 0dcf06000b
commit b68ce77650
3 changed files with 152 additions and 160 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/data/nat/comm_semiring.lean
View file

@ -2,10 +2,10 @@
Copyright (c) 2014 Floris van Doorn. All rights reserved. Copyright (c) 2014 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE. Released under Apache 2.0 license as described in the file LICENSE.
Module: data.nat.algebra Module: data.nat.comm_semiring
Authors: Jeremy Avigad Author: Jeremy Avigad
nat is a comm_semiring ℕ is a comm_semiring.
-/ -/
import data.nat.basic algebra.binary algebra.ring import data.nat.basic algebra.binary algebra.ring
open binary open binary

288
library/data/nat/div.lean
View file

@ -1,4 +1,4 @@
/- /-
Copyright (c) 2014 Jeremy Avigad. All rights reserved. Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE. Released under Apache 2.0 license as described in the file LICENSE.
@ -8,25 +8,21 @@ Authors: Jeremy Avigad, Leonardo de Moura
Definitions of div, mod, and gcd on the natural numbers. Definitions of div, mod, and gcd on the natural numbers.
-/ -/
import data.nat.sub data.nat.comm_semiring logic import data.nat.sub data.nat.comm_semiring tools.fake_simplifier
import algebra.relation
import tools.fake_simplifier
open eq.ops well_founded decidable fake_simplifier prod open eq.ops well_founded decidable fake_simplifier prod
open relation relation.iff_ops
namespace nat namespace nat
-- Auxiliary lemma used to justify div /- 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 := private definition div_rec_lemma {x y : nat} (H : 0 < y ∧ y ≤ x) : x - y < x :=
and.rec_on H (λ ypos ylex, and.rec_on H (λ ypos ylex, sub_lt (lt_of_lt_of_le ypos ylex) ypos)
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 := 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 if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y + 1 else zero
definition divide (x y : nat) := definition divide (x y : nat) := fix div.F x y
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 := 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 congr_fun (fix_eq div.F x) y
@ -36,22 +32,25 @@ notation a div b := divide a b
theorem div_zero (a : ℕ) : a div 0 = 0 := theorem div_zero (a : ℕ) : a div 0 = 0 :=
divide_def a 0 ⬝ if_neg (!not_and_of_not_left (lt.irrefl 0)) divide_def a 0 ⬝ if_neg (!not_and_of_not_left (lt.irrefl 0))
theorem div_less {a b : ℕ} (h : a < b) : a div b = 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)) divide_def a b ⬝ if_neg (!not_and_of_not_right (not_le_of_lt h))
theorem zero_div (b : ℕ) : 0 div b = 0 := 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))) 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_rec {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a div b = succ ((a - b) div b) := 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₂) divide_def a b ⬝ if_pos (and.intro h₁ h₂)
theorem div_add_self_right {x z : ℕ} (H : z > 0) : (x + z) div z = succ (x div z) := theorem add_div_left {x z : ℕ} (H : z > 0) : (x + z) div z = succ (x div z) :=
calc calc
(x + z) div z = if 0 < z ∧ z ≤ x + z then (x + z - z) div z + 1 else 0 : !divide_def (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)) ... = (x + z - z) div z + 1 : if_pos (and.intro H (le_add_left z x))
... = succ (x div z) : add_sub_cancel ... = succ (x div z) : add_sub_cancel
theorem div_add_mul_self_right {x y z : ℕ} (H : z > 0) : (x + y * z) div z = x div z + y := theorem add_div_right {x z : ℕ} (H : x > 0) : (x + z) div x = succ (z div x) :=
!add.comm ▸ add_div_left H
theorem add_mul_div_left {x y z : ℕ} (H : z > 0) : (x + y * z) div z = x div z + y :=
induction_on y induction_on y
(calc (x + zero * z) div z = (x + zero) div z : zero_mul (calc (x + zero * z) div z = (x + zero) div z : zero_mul
... = x div z : add_zero ... = x div z : add_zero
@ -59,14 +58,16 @@ induction_on y
(take y, (take y,
assume IH : (x + y * z) div z = x div z + y, calc 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 (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 ... = succ ((x + y * z) div z) : add_div_left H
... = x div z + succ y : by simp) ... = x div z + succ y : by simp)
theorem add_mul_div_right {x y z : ℕ} (H : y > 0) : (x + y * z) div y = x div y + z :=
!mul.comm ▸ add_mul_div_left H
private definition mod.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat := 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 if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y else x
definition modulo (x y : nat) := definition modulo (x y : nat) := fix mod.F x y
fix mod.F x y
notation a mod b := modulo a b notation a mod b := modulo a b
@ -76,22 +77,25 @@ congr_fun (fix_eq mod.F x) y
theorem mod_zero (a : ℕ) : a mod 0 = a := theorem mod_zero (a : ℕ) : a mod 0 = a :=
modulo_def a 0 ⬝ if_neg (!not_and_of_not_left (lt.irrefl 0)) modulo_def a 0 ⬝ if_neg (!not_and_of_not_left (lt.irrefl 0))
theorem mod_less {a b : ℕ} (h : a < b) : a mod b = a := 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)) modulo_def a b ⬝ if_neg (!not_and_of_not_right (not_le_of_lt h))
theorem zero_mod (b : ℕ) : 0 mod b = 0 := 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))) 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_rec {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a mod b = (a - b) mod b := 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₂) modulo_def a b ⬝ if_pos (and.intro h₁ h₂)
theorem mod_add_self_right {x z : ℕ} (H : z > 0) : (x + z) mod z = x mod z := theorem add_mod_left {x z : ℕ} (H : z > 0) : (x + z) mod z = x mod z :=
calc (x + z) mod z calc
= if 0 < z ∧ z ≤ x + z then (x + z - z) mod z else _ : modulo_def (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 + z - z) mod z : if_pos (and.intro H (le_add_left z x))
... = x mod z : add_sub_cancel ... = x mod z : add_sub_cancel
theorem mod_add_mul_self_right {x y z : ℕ} (H : z > 0) : (x + y * z) mod z = x mod z := 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_left {x y z : ℕ} (H : z > 0) : (x + y * z) mod z = x mod z :=
induction_on y induction_on y
(calc (x + zero * z) mod z = (x + zero) mod z : zero_mul (calc (x + zero * z) mod z = (x + zero) mod z : zero_mul
... = x mod z : add_zero) ... = x mod z : add_zero)
@ -100,23 +104,20 @@ induction_on y
calc calc
(x + succ y * z) mod z = (x + (y * z + z)) mod z : succ_mul (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 + z) mod z : add.assoc
... = (x + y * z) mod z : mod_add_self_right H ... = (x + y * z) mod z : add_mod_left H
... = x mod z : IH) ... = x mod z : IH)
theorem mod_mul_self_right {m n : ℕ} : (m * n) mod n = 0 := theorem add_mul_mod_right {x y z : ℕ} (H : y > 0) : (x + y * z) mod y = x mod y :=
!mul.comm ▸ add_mul_mod_left H
theorem mul_mod_left {m n : ℕ} : (m * n) mod n = 0 :=
by_cases_zero_pos n (by simp) by_cases_zero_pos n (by simp)
(take n, (take n,
assume npos : n > 0, assume npos : n > 0,
(by simp) ▸ (@mod_add_mul_self_right 0 m _ npos)) (by simp) ▸ (@add_mul_mod_left 0 m _ npos))
-- add_rewrite mod_mul_self_right theorem mul_mod_right {m n : ℕ} : (m * n) mod m = 0 :=
!mul.comm ▸ !mul_mod_left
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 := theorem mod_lt {x y : ℕ} (H : y > 0) : x mod y < y :=
case_strong_induction_on x case_strong_induction_on x
@ -126,16 +127,19 @@ case_strong_induction_on x
show succ x mod y < y, from show succ x mod y < y, from
by_cases -- (succ x < y) by_cases -- (succ x < y)
(assume H1 : succ x < y, (assume H1 : succ x < y,
have H2 : succ x mod y = succ x, from mod_less H1, have H2 : succ x mod y = succ x, from mod_eq_of_lt H1,
show succ x mod y < y, from H2⁻¹ ▸ H1) show succ x mod y < y, from H2⁻¹ ▸ H1)
(assume H1 : ¬ succ x < y, (assume H1 : ¬ succ x < y,
have H2 : y ≤ succ x, from le_of_not_lt H1, have H2 : y ≤ succ x, from le_of_not_lt H1,
have H3 : succ x mod y = (succ x - y) mod y, from mod_rec H H2, 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 H4 : succ x - y < succ x, from sub_lt !succ_pos H,
have H5 : succ x - y ≤ x, from le_of_lt_succ H4, have H5 : succ x - y ≤ x, from le_of_lt_succ H4,
show succ x mod y < y, from H3⁻¹ ▸ IH _ H5)) show succ x mod y < y, from H3⁻¹ ▸ IH _ H5))
theorem div_mod_eq {x y : ℕ} : x = x div y * y + x mod y := /- 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 by_cases_zero_pos y
(show x = x div 0 * 0 + x mod 0, from (show x = x div 0 * 0 + x mod 0, from
(calc (calc
@ -152,45 +156,45 @@ by_cases_zero_pos y
show succ x = succ x div y * y + succ x mod y, from show succ x = succ x div y * y + succ x mod y, from
by_cases -- (succ x < y) by_cases -- (succ x < y)
(assume H1 : succ x < y, (assume H1 : succ x < y,
have H2 : succ x div y = 0, from div_less H1, have H2 : succ x div y = 0, from div_eq_zero_of_lt H1,
have H3 : succ x mod y = succ x, from mod_less H1, have H3 : succ x mod y = succ x, from mod_eq_of_lt H1,
by simp) by simp)
(assume H1 : ¬ succ x < y, (assume H1 : ¬ succ x < y,
have H2 : y ≤ succ x, from le_of_not_lt H1, 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_rec H H2, 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_rec 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 H5 : succ x - y < succ x, from sub_lt !succ_pos H,
have H6 : succ x - y ≤ x, from le_of_lt_succ H5, have H6 : succ x - y ≤ x, from le_of_lt_succ H5,
(calc (calc
succ x div y * y + succ x mod y = succ ((succ x - y) div y) * y + succ x mod y : H3 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 mod y : succ_mul
... = ((succ x - y) div y) * y + y + (succ x - y) mod y : H4 ... = ((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) div y) * y + (succ x - y) mod y + y : add.right_comm
... = succ x - y + y : {!(IH _ H6)⁻¹} ... = succ x - y + y : {!(IH _ H6)⁻¹}
... = succ x : sub_add_cancel H2)⁻¹))) ... = succ x : sub_add_cancel H2)⁻¹)))
theorem mod_le {x y : ℕ} : x mod y ≤ x := theorem mod_le {x y : ℕ} : x mod y ≤ x :=
div_mod_eq⁻¹ ▸ !le_add_left eq_div_mul_add_mod⁻¹ ▸ !le_add_left
--- a good example where simplifying using the context causes problems theorem eq_remainder {y : ℕ} (H : y > 0) {q1 r1 q2 r2 : ℕ} (H1 : r1 < y) (H2 : r2 < y)
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 := (H3 : q1 * y + r1 = q2 * y + r2) : r1 = r2 :=
calc calc
r1 = r1 mod y : by simp r1 = r1 mod y : by simp
... = (r1 + q1 * y) mod y : (mod_add_mul_self_right H)⁻¹ ... = (r1 + q1 * y) mod y : (add_mul_mod_left H)⁻¹
... = (q1 * y + r1) mod y : add.comm ... = (q1 * y + r1) mod y : add.comm
... = (r2 + q2 * y) mod y : by simp ... = (r2 + q2 * y) mod y : by simp
... = r2 mod y : mod_add_mul_self_right H ... = r2 mod y : add_mul_mod_left H
... = r2 : by simp ... = r2 : by simp
theorem quotient_unique {y : ℕ} (H : y > 0) {q1 r1 q2 r2 : ℕ} (H1 : r1 < y) (H2 : r2 < y) 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 := (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 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 H5 : q1 * y = q2 * y, from add.cancel_right H4,
have H6 : y > 0, from lt_of_le_of_lt !zero_le H1, 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 show q1 = q2, from eq_of_mul_eq_mul_right H6 H5
theorem div_mul_mul {z x y : ℕ} (zpos : z > 0) : (z * x) div (z * y) = x div y := theorem mul_div_mul_left {z x y : ℕ} (zpos : z > 0) : (z * x) div (z * y) = x div y :=
by_cases -- (y = 0) by_cases -- (y = 0)
(assume H : y = 0, by simp) (assume H : y = 0, by simp)
(assume H : y ≠ 0, (assume H : y ≠ 0,
@ -198,16 +202,17 @@ by_cases -- (y = 0)
have zypos : z * y > 0, from mul_pos zpos ypos, have zypos : z * y > 0, from mul_pos zpos ypos,
have H1 : (z * x) mod (z * y) < z * y, from mod_lt zypos, 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, have H2 : z * (x mod y) < z * y, from mul_lt_mul_of_pos_left (mod_lt ypos) zpos,
quotient_unique zypos H1 H2 eq_quotient zypos H1 H2
(calc (calc
((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : div_mod_eq ((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) : div_mod_eq ... = 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 ... = z * (x div y * y) + z * (x mod y) : mul.left_distrib
... = (x div y) * (z * y) + z * (x mod y) : mul.left_comm)) ... = (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) := 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 : ℕ} (zpos : z > 0) : (z * x) mod (z * y) = z * (x mod y) :=
by_cases -- (y = 0) by_cases -- (y = 0)
(assume H : y = 0, by simp) (assume H : y = 0, by simp)
(assume H : y ≠ 0, (assume H : y ≠ 0,
@ -215,106 +220,60 @@ by_cases -- (y = 0)
have zypos : z * y > 0, from mul_pos zpos ypos, have zypos : z * y > 0, from mul_pos zpos ypos,
have H1 : (z * x) mod (z * y) < z * y, from mod_lt zypos, 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, have H2 : z * (x mod y) < z * y, from mul_lt_mul_of_pos_left (mod_lt ypos) zpos,
remainder_unique zypos H1 H2 eq_remainder zypos H1 H2
(calc (calc
((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : div_mod_eq ((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) : div_mod_eq ... = 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 ... = z * (x div y * y) + z * (x mod y) : mul.left_distrib
... = (x div y) * (z * y) + z * (x mod y) : mul.left_comm)) ... = (x div y) * (z * y) + z * (x mod y) : mul.left_comm))
theorem mul_mod_mul_right {x z y : ℕ} (zpos : z > 0) : (x * z) mod (y * z) = (x mod y) * z :=
mul.comm z x ▸ mul.comm z y ▸ !mul.comm ▸ mul_mod_mul_left zpos
theorem mod_one (x : ℕ) : x mod 1 = 0 := theorem mod_one (x : ℕ) : x mod 1 = 0 :=
have H1 : x mod 1 < 1, from mod_lt !succ_pos, have H1 : x mod 1 < 1, from mod_lt !succ_pos,
eq_zero_of_le_zero (le_of_lt_succ H1) eq_zero_of_le_zero (le_of_lt_succ H1)
-- add_rewrite mod_one
theorem mod_self (n : ℕ) : n mod n = 0 := theorem mod_self (n : ℕ) : n mod n = 0 :=
cases_on n (by simp) cases_on n (by simp)
(take n, (take n,
have H : (succ n * 1) mod (succ n * 1) = succ n * (1 mod 1), have H : (succ n * 1) mod (succ n * 1) = succ n * (1 mod 1),
from mod_mul_mul !succ_pos, from mul_mod_mul_left !succ_pos,
(by simp) ▸ H) (by simp) ▸ H)
-- add_rewrite mod_self
theorem div_one (n : ℕ) : n div 1 = n := theorem div_one (n : ℕ) : n div 1 = n :=
have H : n div 1 * 1 + n mod 1 = n, from div_mod_eq⁻¹, have H : n div 1 * 1 + n mod 1 = n, from eq_div_mul_add_mod⁻¹,
(by simp) ▸ H (by simp) ▸ H
-- add_rewrite div_one 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,
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 (by simp) ▸ H1
-- add_rewrite pos_div_self theorem div_mul_eq_of_mod_eq_zero {x y : ℕ} (H : x mod y = 0) : x div y * y = x :=
-- 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 :=
-- iff.of_eq rfl
theorem mod_eq_zero_imp_div_mul_eq {x y : ℕ} (H : x mod y = 0) : x div y * y = x :=
(calc (calc
x = x div y * y + x mod y : div_mod_eq x = x div y * y + x mod y : eq_div_mul_add_mod
... = x div y * y + 0 : H ... = x div y * y + 0 : H
... = x div y * y : !add_zero)⁻¹ ... = x div y * y : !add_zero)⁻¹
-- add_rewrite dvd_imp_div_mul_eq /- divides -/
theorem mul_eq_imp_mod_eq_zero {z x y : ℕ} (H : z * y = x) : x mod y = 0 :=
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_right_distrib
... = x mod y + x div y * y - x div y * y : H1
... = x mod y : add_sub_cancel,
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,
calc
x mod y = x mod 0 : yz
... = x : mod_zero
... = 0 : xz)
(assume ynz : y ≠ 0,
have ypos : y > 0, from pos_of_ne_zero ynz,
have H3 : (z - x div y) * y < y, from H2⁻¹ ▸ mod_lt ypos,
have H4 : (z - x div y) * y < 1 * y, from !one_mul⁻¹ ▸ H3,
have H5 : z - x div y < 1, from lt_of_mul_lt_mul_right H4,
have H6 : z - x div y = 0, from eq_zero_of_le_zero (le_of_lt_succ H5),
calc
x mod y = (z - x div y) * y : H2
... = 0 * y : H6
... = 0 : zero_mul)
theorem dvd_of_mod_eq_zero {x y : ℕ} (H : y mod x = 0) : x | y := theorem dvd_of_mod_eq_zero {x y : ℕ} (H : y mod x = 0) : x | y :=
dvd.intro (!mul.comm ▸ mod_eq_zero_imp_div_mul_eq H) dvd.intro (!mul.comm ▸ div_mul_eq_of_mod_eq_zero H)
theorem mod_eq_zero_of_dvd {x y : ℕ} (H : x | y) : y mod x = 0 := theorem mod_eq_zero_of_dvd {x y : ℕ} (H : x | y) : y mod x = 0 :=
dvd.elim H ( dvd.elim H
take z, (take z,
assume H1 : x * z = y, assume H1 : x * z = y,
mul_eq_imp_mod_eq_zero (!mul.comm ▸ H1)) H1 ▸ !mul_mod_right)
theorem dvd_iff_mod_eq_zero (x y : ℕ) : x | y ↔ y mod x = 0 := theorem dvd_iff_mod_eq_zero (x y : ℕ) : x | y ↔ y mod x = 0 :=
iff.intro mod_eq_zero_of_dvd dvd_of_mod_eq_zero iff.intro mod_eq_zero_of_dvd dvd_of_mod_eq_zero
definition dvd.decidable_rel [instance] : decidable_rel dvd := definition dvd.decidable_rel [instance] : decidable_rel dvd :=
take m n, decidable_of_decidable_of_iff _ (!dvd_iff_mod_eq_zero⁻¹) take m n, decidable_of_decidable_of_iff _ (iff.symm !dvd_iff_mod_eq_zero)
theorem dvd_imp_div_mul_eq {x y : ℕ} (H : y | x) : x div y * y = x := theorem div_mul_eq_of_dvd {x y : ℕ} (H : y | x) : x div y * y = x :=
mod_eq_zero_imp_div_mul_eq (mod_eq_zero_of_dvd H) div_mul_eq_of_mod_eq_zero (mod_eq_zero_of_dvd H)
theorem dvd_of_dvd_add_left {m n1 n2 : ℕ} : m | (n1 + n2) → m | n1 → m | n2 := theorem dvd_of_dvd_add_left {m n1 n2 : ℕ} : m | (n1 + n2) → m | n1 → m | n2 :=
by_cases_zero_pos m by_cases_zero_pos m
@ -331,36 +290,50 @@ by_cases_zero_pos m
assume H1 : m | (n1 + n2), assume H1 : m | (n1 + n2),
assume H2 : m | n1, assume H2 : m | n1,
have H3 : n1 + n2 = n1 + n2 div m * m, from calc have H3 : n1 + n2 = n1 + n2 div m * m, from calc
n1 + n2 = (n1 + n2) div m * m : dvd_imp_div_mul_eq H1 n1 + n2 = (n1 + n2) div m * m : div_mul_eq_of_dvd H1
... = (n1 div m * m + n2) div m * m : dvd_imp_div_mul_eq H2 ... = (n1 div m * m + n2) div m * m : div_mul_eq_of_dvd H2
... = (n2 + n1 div m * m) div m * m : add.comm ... = (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 + n1 div m) * m : add_mul_div_left mpos
... = n2 div m * m + n1 div m * m : mul.right_distrib ... = n2 div m * m + n1 div m * m : mul.right_distrib
... = n1 div m * m + n2 div m * m : add.comm ... = n1 div m * m + n2 div m * m : add.comm
... = n1 + n2 div m * m : dvd_imp_div_mul_eq H2, ... = n1 + n2 div m * m : div_mul_eq_of_dvd H2,
have H4 : n2 = n2 div m * m, from add.cancel_left H3, have H4 : n2 = n2 div m * m, from add.cancel_left H3,
have H5 : m * (n2 div m) = n2, from !mul.comm ▸ H4⁻¹, have H5 : m * (n2 div m) = n2, from !mul.comm ▸ H4⁻¹,
dvd.intro H5) dvd.intro H5)
theorem dvd_add_cancel_right {m n1 n2 : ℕ} (H : m | (n1 + n2)) : m | n2 → m | n1 := 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) dvd_of_dvd_add_left (!add.comm ▸ H)
theorem dvd_sub {m n1 n2 : ℕ} (H1 : m | n1) (H2 : m | n2) : m | (n1 - n2) := theorem dvd_sub {m n1 n2 : ℕ} (H1 : m | n1) (H2 : m | n2) : m | (n1 - n2) :=
by_cases by_cases
(assume H3 : n1 ≥ n2, (assume H3 : n1 ≥ n2,
have H4 : n1 = n1 - n2 + n2, from (sub_add_cancel H3)⁻¹, have H4 : n1 = n1 - n2 + n2, from (sub_add_cancel H3)⁻¹,
show m | n1 - n2, from dvd_add_cancel_right (H4 ▸ H1) H2) show m | n1 - n2, from dvd_of_dvd_add_right (H4 ▸ H1) H2)
(assume H3 : ¬ (n1 ≥ n2), (assume H3 : ¬ (n1 ≥ n2),
have H4 : n1 - n2 = 0, from sub_eq_zero_of_le (le_of_lt (lt_of_not_le H3)), 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 _) show m | n1 - n2, from H4⁻¹ ▸ dvd_zero _)
-- Gcd and lcm 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 : m * k = n), from dvd.ex H1,
obtain l (Hl : n * l = m), from dvd.ex 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))
/- gcd and lcm -/
private definition pair_nat.lt : nat × nat → nat × nat → Prop := measure pr₂ private definition pair_nat.lt : nat × nat → nat × nat → Prop := measure pr₂
private definition pair_nat.lt.wf : well_founded pair_nat.lt := private definition pair_nat.lt.wf : well_founded pair_nat.lt :=
intro_k (measure.wf pr₂) 20 -- Remark: we use intro_k to be able to execute gcd efficiently in the kernel intro_k (measure.wf pr₂) 20 -- we use intro_k to be able to execute gcd efficiently in the kernel
instance pair_nat.lt.wf -- Remark: instance will not be saved in .olean
instance pair_nat.lt.wf -- instance will not be saved in .olean
infixl [local] `≺`:50 := pair_nat.lt infixl [local] `≺`:50 := pair_nat.lt
private definition gcd.lt.dec (x y₁ : nat) : (succ y₁, x mod succ y₁) ≺ (x, succ y₁) := private definition gcd.lt.dec (x y₁ : nat) : (succ y₁, x mod succ y₁) ≺ (x, succ y₁) :=
@ -371,8 +344,7 @@ prod.cases_on p₁ (λx y, cases_on y
(λ f, x) (λ f, x)
(λ y₁ (f : Πp₂, p₂ ≺ (x, succ y₁) → nat), f (succ y₁, x mod succ y₁) !gcd.lt.dec)) (λ y₁ (f : Πp₂, p₂ ≺ (x, succ y₁) → nat), f (succ y₁, x mod succ y₁) !gcd.lt.dec))
definition gcd (x y : nat) := definition gcd (x y : nat) := fix gcd.F (pair x y)
fix gcd.F (pair x y)
theorem gcd_zero (x : nat) : gcd x 0 = x := theorem gcd_zero (x : nat) : gcd x 0 = x :=
well_founded.fix_eq gcd.F (x, 0) well_founded.fix_eq gcd.F (x, 0)
@ -390,10 +362,10 @@ cases_on y
(calc gcd x 0 = x : gcd_zero x (calc gcd x 0 = x : gcd_zero x
... = if 0 = 0 then x else gcd zero (x mod zero) : (if_pos rfl)⁻¹) ... = if 0 = 0 then x else gcd zero (x mod zero) : (if_pos rfl)⁻¹)
(λy₁, calc (λy₁, calc
gcd x (succ y₁) = gcd (succ y₁) (x mod succ y₁) : gcd_succ x y₁ 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₁))⁻¹) ... = if succ y₁ = 0 then x else gcd (succ y₁) (x mod succ y₁) : (if_neg (succ_ne_zero y₁))⁻¹)
theorem gcd_pos (m : ℕ) {n : ℕ} (H : n > 0) : gcd m n = gcd n (m mod n) := theorem gcd_rec (m : ℕ) {n : ℕ} (H : n > 0) : gcd m n = gcd n (m mod n) :=
gcd_def m n ⬝ if_neg (ne_zero_of_pos H) gcd_def m n ⬝ if_neg (ne_zero_of_pos H)
theorem gcd_self (n : ℕ) : gcd n n = n := theorem gcd_self (n : ℕ) : gcd n n = n :=
@ -412,11 +384,11 @@ cases_on n
... = gcd (succ n₁) 0 : zero_mod ... = gcd (succ n₁) 0 : zero_mod
... = (succ n₁) : gcd_zero) ... = (succ n₁) : gcd_zero)
theorem gcd_induct {P : ℕ → ℕ → Prop} theorem gcd.induction {P : ℕ → ℕ → Prop}
(m n : ℕ) (m n : ℕ)
(H0 : ∀m, P m 0) (H0 : ∀m, P m 0)
(H1 : ∀m n, 0 < n → P n (m mod n) → P m n) (H1 : ∀m n, 0 < n → P n (m mod n) → P m n) :
: P m n := P m n :=
let Q : nat × nat → Prop := λ p : nat × nat, P (pr₁ p) (pr₂ p) in let Q : nat × nat → Prop := λ p : nat × nat, P (pr₁ p) (pr₂ p) in
have aux : Q (m, n), from have aux : Q (m, n), from
well_founded.induction (m, n) (λp, prod.cases_on p well_founded.induction (m, n) (λp, prod.cases_on p
@ -431,7 +403,7 @@ have aux : Q (m, n), from
aux aux
theorem gcd_dvd (m n : ℕ) : (gcd m n | m) ∧ (gcd m n | n) := theorem gcd_dvd (m n : ℕ) : (gcd m n | m) ∧ (gcd m n | n) :=
gcd_induct m n gcd.induction m n
(take m, (take m,
show (gcd m 0 | m) ∧ (gcd m 0 | 0), by simp) show (gcd m 0 | m) ∧ (gcd m 0 | 0), by simp)
(take m n, (take m n,
@ -439,16 +411,16 @@ gcd_induct m n
assume IH : (gcd n (m mod n) | n) ∧ (gcd n (m mod n) | (m mod 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 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), dvd_add (dvd.trans (and.elim_left IH) !dvd_mul_left) (and.elim_right IH),
have H1 : gcd n (m mod n) | m, from div_mod_eq⁻¹ ▸ H, 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_pos _ npos)⁻¹, have gcd_eq : gcd n (m mod n) = gcd m n, from (gcd_rec _ npos)⁻¹,
show (gcd m n | m) ∧ (gcd m n | n), from gcd_eq ▸ (and.intro H1 (and.elim_left IH))) 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_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 gcd_dvd_right (m n : ℕ) : (gcd m n | n) := and.elim_right !gcd_dvd
theorem gcd_greatest {m n k : ℕ} : k | m → k | n → k | (gcd m n) := theorem dvd_gcd {m n k : ℕ} : k | m → k | n → k | (gcd m n) :=
gcd_induct m n gcd.induction m n
(take m, assume (h₁ : k | m) (h₂ : k | 0), (take m, assume (h₁ : k | m) (h₂ : k | 0),
show k | gcd m 0, from !gcd_zero⁻¹ ▸ h₁) show k | gcd m 0, from !gcd_zero⁻¹ ▸ h₁)
(take m n, (take m n,
@ -456,9 +428,23 @@ gcd_induct m n
assume IH : k | n → k | (m mod n) → k | gcd n (m mod n), assume IH : k | n → k | (m mod n) → k | gcd n (m mod n),
assume H1 : k | m, assume H1 : k | m,
assume H2 : k | n, assume H2 : k | n,
have H3 : k | m div n * n + m mod n, from div_mod_eq ▸ H1, 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 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_pos _ npos)⁻¹, have gcd_eq : gcd n (m mod n) = gcd m n, from (gcd_rec _ npos)⁻¹,
show k | gcd m n, from gcd_eq ▸ IH H2 H4) 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))
end nat end nat

18
library/data/nat/order.lean
View file

@ -411,17 +411,17 @@ have H4 : m ≤ k, from le_of_mul_le_mul_left H2 Hn,
have H5 : k ≤ m, from le_of_mul_le_mul_left H3 Hn, have H5 : k ≤ m, from le_of_mul_le_mul_left H3 Hn,
le.antisymm H4 H5 le.antisymm H4 H5
theorem eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) : n = k :=
eq_of_mul_eq_mul_left Hm (!mul.comm ▸ !mul.comm ▸ H)
theorem eq_zero_or_eq_of_mul_eq_mul_left {n m k : ℕ} (H : n * m = n * k) : n = 0 ∨ m = k := theorem eq_zero_or_eq_of_mul_eq_mul_left {n m k : ℕ} (H : n * m = n * k) : n = 0 ∨ m = k :=
or_of_or_of_imp_right zero_or_pos or_of_or_of_imp_right zero_or_pos
(assume Hn : n > 0, eq_of_mul_eq_mul_left Hn H) (assume Hn : n > 0, eq_of_mul_eq_mul_left Hn H)
theorem eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) : n = k :=
eq_of_mul_eq_mul_left Hm (!mul.comm ▸ !mul.comm ▸ H)
theorem eq_zero_or_eq_of_mul_eq_mul_right {n m k : ℕ} (H : n * m = k * m) : m = 0 ∨ n = k := theorem eq_zero_or_eq_of_mul_eq_mul_right {n m k : ℕ} (H : n * m = k * m) : m = 0 ∨ n = k :=
eq_zero_or_eq_of_mul_eq_mul_left (!mul.comm ▸ !mul.comm ▸ H) eq_zero_or_eq_of_mul_eq_mul_left (!mul.comm ▸ !mul.comm ▸ H)
theorem eq_one_of_mul_eq_one_left {n m : ℕ} (H : n * m = 1) : n = 1 := theorem eq_one_of_mul_eq_one_right {n m : ℕ} (H : n * m = 1) : n = 1 :=
have H2 : n * m > 0, from H⁻¹ ▸ !succ_pos, have H2 : n * m > 0, from H⁻¹ ▸ !succ_pos,
have H3 : n > 0, from pos_of_mul_pos_right H2, have H3 : n > 0, from pos_of_mul_pos_right H2,
have H4 : m > 0, from pos_of_mul_pos_left H2, have H4 : m > 0, from pos_of_mul_pos_left H2,
@ -433,7 +433,13 @@ or.elim (le_or_gt n 1)
have H7 : 1 ≥ 2, from !mul_one ▸ H ▸ H6, have H7 : 1 ≥ 2, from !mul_one ▸ H ▸ H6,
absurd !self_lt_succ (not_lt_of_le H7)) absurd !self_lt_succ (not_lt_of_le H7))
theorem eq_one_of_mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1 := theorem eq_one_of_mul_eq_one_left {n m : ℕ} (H : n * m = 1) : m = 1 :=
eq_one_of_mul_eq_one_left (!mul.comm ▸ H) eq_one_of_mul_eq_one_right (!mul.comm ▸ H)
theorem eq_one_of_mul_eq_self_left {n m : ℕ} (Hpos : n > 0) (H : m * n = n) : m = 1 :=
eq_of_mul_eq_mul_right Hpos (H ⬝ !one_mul⁻¹)
theorem eq_one_of_mul_eq_self_right {n m : ℕ} (Hpos : m > 0) (H : m * n = m) : n = 1 :=
eq_one_of_mul_eq_self_left Hpos (!mul.comm ▸ H)
end nat end nat