From 5bc6dd84cfb09ce08584a969fa22c471dd60640d Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Tue, 23 Dec 2014 19:46:48 -0500 Subject: [PATCH] feat(library/data/nat): make nat an instance of comm_semiring --- library/algebra/ring.lean | 2 +- library/data/int/basic.lean | 2 +- library/data/nat/basic.lean | 72 ++++++++++++---------- library/data/nat/bquant.lean | 4 +- library/data/nat/default.lean | 2 +- library/data/nat/div.lean | 112 ++++++++++++---------------------- library/data/nat/nat.md | 1 + 7 files changed, 88 insertions(+), 107 deletions(-) diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 47c4d87f87..b5b92aec9f 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -99,7 +99,7 @@ section comm_semiring ... = b * e : H₃ ... = c : H₄))) - theorem eq_zero_of_zero_dvd {H : 0 | a} : a = 0 := + theorem eq_zero_of_zero_dvd {a : A} (H : 0 | a) : a = 0 := dvd.elim H (take c, assume H' : 0 * c = a, (H')⁻¹ ⬝ !zero_mul) theorem dvd_zero : a | 0 := dvd.intro !mul_zero diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index cb2d77d33c..e4a1f1ba44 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -692,7 +692,7 @@ context port_algebra @algebra.dvd.elim _ _ theorem dvd.refl : ∀a : ℤ, a | a := algebra.dvd.refl theorem dvd.trans : ∀{a b c : ℤ} (H₁ : a | b) (H₂ : b | c), a | c := @algebra.dvd.trans _ _ - theorem eq_zero_of_zero_dvd : ∀(a : ℤ) {H : 0 | a}, a = 0 := @algebra.eq_zero_of_zero_dvd _ _ + theorem eq_zero_of_zero_dvd : ∀{a : ℤ} (H : 0 | a), a = 0 := @algebra.eq_zero_of_zero_dvd _ _ theorem dvd_zero : ∀a : ℤ, a | 0 := algebra.dvd_zero theorem one_dvd : ∀a : ℤ, 1 | a := algebra.one_dvd theorem dvd_mul_right : ∀a b : ℤ, a | a * b := algebra.dvd_mul_right diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index f7fbb85ba1..32c606dd70 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -8,7 +8,7 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad Basic operations on the natural numbers. -/ -import logic.connectives data.num algebra.binary +import logic.connectives data.num algebra.binary algebra.ring open eq.ops binary @@ -67,10 +67,6 @@ induction_on n (take m IH, or.inr (show succ m = succ (pred (succ m)), from congr_arg succ !pred.succ⁻¹)) ---theorem eq_zero_or_exists_eq_succ (n : ℕ) : n = 0 ∨ ∃k, n = succ k := ---or_of_or_of_imp_of_imp (eq_zero_or_eq_succ_pred n) (assume H, H) --- (assume H : n = succ (pred n), exists.intro (pred n) H) - theorem succ.inj {n m : ℕ} (H : succ n = succ m) : n = m := no_confusion H (λe, e) @@ -106,13 +102,6 @@ have general : ∀m, P n m, from induction_on n cases_on m (H2 k) (take l, (H3 k l (IH l)))), general m -/- - discriminate - (assume Hm : m = 0, Hm⁻¹ ▸ (H2 k)) - (take l : ℕ, assume Hm : m = succ l, Hm⁻¹ ▸ (H3 k l (IH l)))), -general m --/ - /- addition -/ theorem add.right_id (n : ℕ) : n + 0 = n := @@ -150,9 +139,6 @@ induction_on m theorem succ_add_eq_add_succ (n m : ℕ) : succ n + m = n + succ m := !add.succ_left ⬝ !add_succ⁻¹ --- theorem add.comm_succ (n m : ℕ) : n + succ m = m + succ n := --- !succ_add_eq_add_succ⁻¹ ⬝ !add.comm - theorem add.assoc (n m k : ℕ) : (n + m) + k = n + (m + k) := induction_on k (!add.right_id ▸ !add.right_id) @@ -169,8 +155,6 @@ left_comm add.comm add.assoc n m k theorem add.right_comm (n m k : ℕ) : n + m + k = n + k + m := right_comm add.comm add.assoc n m k --- ### cancelation - theorem add.cancel_left {n m k : ℕ} : n + m = n + k → m = k := induction_on n (take H : 0 + m = 0 + k, @@ -205,19 +189,12 @@ eq_zero_of_add_eq_zero_right (!add.comm ⬝ H) theorem add.eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0 := and.intro (eq_zero_of_add_eq_zero_right H) (eq_zero_of_add_eq_zero_left H) --- ### misc - theorem add_one (n : ℕ) : n + 1 = succ n := !add.right_id ▸ !add_succ theorem one_add (n : ℕ) : 1 + n = succ n := !add.left_id ▸ !add.succ_left --- TODO: rename? remove? --- theorem induction_plus_one {P : nat → Prop} (a : ℕ) (H1 : P 0) --- (H2 : ∀ (n : ℕ) (IH : P n), P (n + 1)) : P a := --- nat.rec H1 (take n IH, !add.one ▸ (H2 n IH)) a - /- multiplication -/ theorem mul_zero (n : ℕ) : n * 0 = 0 := @@ -228,7 +205,7 @@ rfl irreducible mul --- ### commutativity, distributivity, associativity, identity +-- commutativity, distributivity, associativity, identity theorem zero_mul (n : ℕ) : 0 * n = 0 := induction_on n @@ -291,12 +268,6 @@ induction_on k ... = n * (m * l + m) : mul.left_distrib ... = n * (m * succ l) : mul_succ) -theorem mul.left_comm (n m k : ℕ) : n * (m * k) = m * (n * k) := -left_comm mul.comm mul.assoc n m k - -theorem mul.right_comm (n m k : ℕ) : n * m * k = n * k * m := -right_comm mul.comm mul.assoc n m k - theorem mul.right_id (n : ℕ) : n * 1 = n := calc n * 1 = n * 0 + n : mul_succ @@ -323,4 +294,43 @@ cases_on n ... = succ (succ n' * m' + n') : add_succ)⁻¹) !succ_ne_zero)) +section port_algebra + + open algebra + + protected definition comm_semiring [instance] : algebra.comm_semiring nat := + algebra.comm_semiring.mk add add.assoc zero add.left_id add.right_id add.comm + mul mul.assoc (succ zero) mul.left_id mul.right_id mul.left_distrib mul.right_distrib + zero_mul mul_zero (ne.symm (succ_ne_zero zero)) mul.comm + + theorem mul.left_comm : ∀a b c : ℕ, a * (b * c) = b * (a * c) := algebra.mul.left_comm + theorem mul.right_comm : ∀a b c : ℕ, (a * b) * c = (a * c) * b := algebra.mul.right_comm + + definition dvd (a b : ℕ) : Prop := algebra.dvd a b + infix `|` := dvd + theorem dvd.intro : ∀{a b c : ℕ} (H : a * b = c), a | c := @algebra.dvd.intro _ _ + theorem dvd.ex : ∀{a b : ℕ} (H : a | b), ∃c, a * c = b := @algebra.dvd.ex _ _ + theorem dvd.elim : ∀{P : Prop} {a b : ℕ} (H₁ : a | b) (H₂ : ∀c, a * c = b → P), P := + @algebra.dvd.elim _ _ + theorem dvd.refl : ∀a : ℕ, a | a := algebra.dvd.refl + theorem dvd.trans : ∀{a b c : ℕ} (H₁ : a | b) (H₂ : b | c), a | c := @algebra.dvd.trans _ _ + theorem eq_zero_of_zero_dvd : ∀{a : ℕ} (H : 0 | a), a = 0 := @algebra.eq_zero_of_zero_dvd _ _ + theorem dvd_zero : ∀a : ℕ, a | 0 := algebra.dvd_zero + theorem one_dvd : ∀a : ℕ, 1 | a := algebra.one_dvd + theorem dvd_mul_right : ∀a b : ℕ, a | a * b := algebra.dvd_mul_right + theorem dvd_mul_left : ∀a b : ℕ, a | b * a := algebra.dvd_mul_left + theorem dvd_mul_of_dvd_left : ∀{a b : ℕ} (H : a | b) (c : ℕ), a | b * c := + @algebra.dvd_mul_of_dvd_left _ _ + theorem dvd_mul_of_dvd_right : ∀{a b : ℕ} (H : a | b) (c : ℕ), a | c * b := + @algebra.dvd_mul_of_dvd_right _ _ + theorem mul_dvd_mul : ∀{a b c d : ℕ}, a | b → c | d → a * c | b * d := + @algebra.mul_dvd_mul _ _ + theorem dvd_of_mul_right_dvd : ∀{a b c : ℕ}, a * b | c → a | c := + @algebra.dvd_of_mul_right_dvd _ _ + theorem dvd_of_mul_left_dvd : ∀{a b c : ℕ}, a * b | c → b | c := + @algebra.dvd_of_mul_left_dvd _ _ + theorem dvd_add : ∀{a b c : ℕ}, a | b → a | c → a | b + c := @algebra.dvd_add _ _ + +end port_algebra + end nat diff --git a/library/data/nat/bquant.lean b/library/data/nat/bquant.lean index e95de8e3ab..12233bb573 100644 --- a/library/data/nat/bquant.lean +++ b/library/data/nat/bquant.lean @@ -1,6 +1,8 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. + +Module: data.nat.bquant Author: Leonardo de Moura Show that "bounded" quantifiers: (∃x, x < n ∧ P x) and (∀x, x < n → P x) @@ -14,7 +16,7 @@ without assuming classical axioms. More importantly, they can be reduced inside of the Lean kernel. -/ -import data.nat +import data.nat.order namespace nat definition bex (n : nat) (P : nat → Prop) : Prop := diff --git a/library/data/nat/default.lean b/library/data/nat/default.lean index 89b96899f1..c6d7dfb735 100644 --- a/library/data/nat/default.lean +++ b/library/data/nat/default.lean @@ -2,4 +2,4 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Jeremy Avigad -import .basic .order .sub .div +import .basic .order .sub .div .bquant diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 9d32f4e087..cb4cd9c86e 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -1,12 +1,13 @@ ---- Copyright (c) 2014 Jeremy Avigad. All rights reserved. ---- Released under Apache 2.0 license as described in the file LICENSE. ---- Author: Jeremy Avigad, Leonardo de Moura +/- +Copyright (c) 2014 Jeremy Avigad. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. --- 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. +Module: data.nat.div +Authors: Jeremy Avigad, Leonardo de Moura + +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 data.nat.sub logic import algebra.relation @@ -251,22 +252,23 @@ have H1 : (n * 1) div (n * 1) = 1 div 1, from div_mul_mul H, -- Divides -- ------- -definition dvd (x y : ℕ) : Prop := y mod x = 0 -infix `|` := dvd +-- definition dvd (x y : ℕ) : Prop := y mod x = 0 -theorem dvd_iff_mod_eq_zero {x y : ℕ} : x | y ↔ y mod x = 0 := -iff.of_eq rfl +-- infix `|` := dvd -theorem dvd_imp_div_mul_eq {x y : ℕ} (H : y | x) : x div y * y = x := +-- 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 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 + 0 : H ... = x div y * y : !add.right_id)⁻¹ -- add_rewrite dvd_imp_div_mul_eq -theorem mul_eq_imp_dvd {z x y : ℕ} (H : z * y = x) : y | x := +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 @@ -297,69 +299,34 @@ show x mod y = 0, from ... = 0 * y : H6 ... = 0 : zero_mul) -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_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) -theorem dvd_zero {n : ℕ} : n | 0 := -zero_mod n +theorem mod_eq_zero_of_dvd {x y : ℕ} (H : x | y) : y mod x = 0 := +dvd.elim H ( + take z, + assume H1 : x * z = y, + mul_eq_imp_mod_eq_zero (!mul.comm ▸ H1)) --- add_rewrite dvd_zero +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 -theorem zero_dvd_eq (n : ℕ) : (0 | n) = (n = 0) := -mod_zero n ▸ eq.refl (0 | n) +theorem dvd.decidable_rel [instance] : decidable_rel dvd := +take m n, decidable_of_decidable_of_iff _ (!dvd_iff_mod_eq_zero⁻¹) --- add_rewrite zero_dvd_iff +theorem dvd_imp_div_mul_eq {x y : ℕ} (H : y | x) : x div y * y = x := +mod_eq_zero_imp_div_mul_eq (mod_eq_zero_of_dvd H) -theorem one_dvd (n : ℕ) : 1 | n := -mod_one n - --- add_rewrite one_dvd - -theorem dvd_self (n : ℕ) : n | n := -mod_self n - --- add_rewrite dvd_self - -theorem dvd_mul_self_left (m n : ℕ) : m | (m * n) := -!mod_mul_self_left - --- add_rewrite dvd_mul_self_left - -theorem dvd_mul_self_right (m n : ℕ) : m | (n * m) := -!mod_mul_self_right - --- 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, from (dvd_imp_div_mul_eq H1)⁻¹, -have H4 : k = k div n * (n div m) * m, from calc - k = k div n * n : dvd_imp_div_mul_eq H2 - ... = 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, from calc - (n1 div m + n2 div m) * m = n1 div m * m + n2 div m * m : mul.right_distrib - ... = n1 + n2 div m * m : dvd_imp_div_mul_eq H1 - ... = n1 + n2 : dvd_imp_div_mul_eq H2, -mp (!dvd_iff_exists_mul⁻¹) (exists.intro _ H) - -theorem dvd_add_cancel_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 := case_zero_pos m (assume (H1 : 0 | n1 + n2) (H2 : 0 | n1), - have H3 : n1 + n2 = 0, from (zero_dvd_eq (n1 + n2)) ▸ H1, - have H4 : n1 = 0, from (zero_dvd_eq n1) ▸ H2, + 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 : add.left_id ... = n1 + n2 : H4 ... = 0 : H3, - show 0 | n2, from H5 ▸ dvd_self n2) + show 0 | n2, from H5 ▸ dvd.refl n2) (take m, assume mpos : m > 0, assume H1 : m | (n1 + n2), @@ -373,10 +340,11 @@ case_zero_pos m ... = n1 div m * m + n2 div m * m : add.comm ... = n1 + n2 div m * m : dvd_imp_div_mul_eq H2, have H4 : n2 = n2 div m * m, from add.cancel_left H3, - mp (!dvd_iff_exists_mul⁻¹) (exists.intro _ (H4⁻¹))) + have H5 : m * (n2 div m) = n2, from !mul.comm ▸ H4⁻¹, + dvd.intro H5) theorem dvd_add_cancel_right {m n1 n2 : ℕ} (H : m | (n1 + n2)) : m | n2 → m | n1 := -dvd_add_cancel_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) := by_cases @@ -385,7 +353,7 @@ by_cases 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) + show m | n1 - n2, from H4⁻¹ ▸ dvd_zero _) -- Gcd and lcm -- ----------- @@ -471,7 +439,7 @@ gcd_induct 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), + 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 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))) @@ -490,7 +458,7 @@ gcd_induct m 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 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)⁻¹, show k | gcd m n, from gcd_eq ▸ IH H2 H4) diff --git a/library/data/nat/nat.md b/library/data/nat/nat.md index 182d18633a..de5fa6ba99 100644 --- a/library/data/nat/nat.md +++ b/library/data/nat/nat.md @@ -5,5 +5,6 @@ The natural numbers. * [basic](basic.lean) : the natural numbers, with succ, pred, addition, and multiplication * [order](order.lean) : less-than, less-then-or-equal, etc. +* [bquant](bquant.lean) : bounded quantifiers * [sub](sub.lean) : subtraction, and distance * [div](div.lean) : div, mod, gcd, and lcm \ No newline at end of file