feat(library/data/nat): make nat an instance of comm_semiring

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

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

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

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 :=

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

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)
 

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