From 95d79e7bda4067069d1cde86c2fea4e454043a36 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Sun, 1 Feb 2015 09:55:12 -0500
Subject: [PATCH] refactor(library/data/nat): merge comm_semiring, make minor
 fixes

---
 library/data/nat/basic.lean         | 48 +++++++++++++++++++++++-
 library/data/nat/comm_semiring.lean | 58 -----------------------------
 library/data/nat/default.lean       | 11 +++---
 library/data/nat/div.lean           |  4 +-
 library/data/nat/order.lean         |  3 +-
 library/data/nat/sub.lean           |  4 +-
 6 files changed, 57 insertions(+), 71 deletions(-)
 delete mode 100644 library/data/nat/comm_semiring.lean

diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index 6b95cab24..20b6aed2c 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -7,7 +7,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 binary eq.ops
 
 namespace nat
@@ -286,4 +286,50 @@ cases_on n
              ... = succ n' * m' + succ n' : mul_succ
              ... = succ (succ n' * m' + n') : add_succ)⁻¹)
           !succ_ne_zero))
+
+section
+  open [classes] algebra
+
+  protected definition comm_semiring [instance] [reducible] : algebra.comm_semiring nat :=
+  algebra.comm_semiring.mk add add.assoc zero zero_add add_zero add.comm
+    mul mul.assoc (succ zero) one_mul mul_one mul.left_distrib mul.right_distrib
+    zero_mul mul_zero (ne.symm (succ_ne_zero zero)) mul.comm
+end
+
+section port_algebra
+  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 * c = b), a | b := @algebra.dvd.intro _ _
+  theorem dvd.intro_left : ∀{a b c : ℕ} (H : c * a = b), a | b := @algebra.dvd.intro_left _ _
+  theorem exists_eq_mul_right_of_dvd : ∀{a b : ℕ} (H : a | b), ∃c, b = a * c :=
+    @algebra.exists_eq_mul_right_of_dvd _ _
+  theorem dvd.elim : ∀{P : Prop} {a b : ℕ} (H₁ : a | b) (H₂ : ∀c, b = a * c → P), P :=
+    @algebra.dvd.elim _ _
+  theorem exists_eq_mul_left_of_dvd : ∀{a b : ℕ} (H : a | b), ∃c, b = c * a :=
+    @algebra.exists_eq_mul_left_of_dvd _ _
+  theorem dvd.elim_left : ∀{P : Prop} {a b : ℕ} (H₁ : a | b) (H₂ : ∀c, b = c * a → P), P :=
+    @algebra.dvd.elim_left _ _
+  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/comm_semiring.lean b/library/data/nat/comm_semiring.lean
deleted file mode 100644
index 0d2cb7b87..000000000
--- a/library/data/nat/comm_semiring.lean
+++ /dev/null
@@ -1,58 +0,0 @@
-/-
-Copyright (c) 2014 Floris van Doorn. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.nat.comm_semiring
-Author: Jeremy Avigad
-
-ℕ is a comm_semiring.
--/
-import data.nat.basic algebra.binary algebra.ring
-open binary
-
-namespace nat
-section
-  open [classes] algebra
-
-  protected definition comm_semiring [instance] [reducible] : algebra.comm_semiring nat :=
-  algebra.comm_semiring.mk add add.assoc zero zero_add add_zero add.comm
-    mul mul.assoc (succ zero) one_mul mul_one mul.left_distrib mul.right_distrib
-    zero_mul mul_zero (ne.symm (succ_ne_zero zero)) mul.comm
-end
-
-section port_algebra
-  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 * c = b), a | b := @algebra.dvd.intro _ _
-  theorem dvd.intro_left : ∀{a b c : ℕ} (H : c * a = b), a | b := @algebra.dvd.intro_left _ _
-  theorem exists_eq_mul_right_of_dvd : ∀{a b : ℕ} (H : a | b), ∃c, b = a * c :=
-    @algebra.exists_eq_mul_right_of_dvd _ _
-  theorem dvd.elim : ∀{P : Prop} {a b : ℕ} (H₁ : a | b) (H₂ : ∀c, b = a * c → P), P :=
-    @algebra.dvd.elim _ _
-  theorem exists_eq_mul_left_of_dvd : ∀{a b : ℕ} (H : a | b), ∃c, b = c * a :=
-    @algebra.exists_eq_mul_left_of_dvd _ _
-  theorem dvd.elim_left : ∀{P : Prop} {a b : ℕ} (H₁ : a | b) (H₂ : ∀c, b = c * a → P), P :=
-    @algebra.dvd.elim_left _ _
-  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/default.lean b/library/data/nat/default.lean
index 958b36316..0ef7dd722 100644
--- a/library/data/nat/default.lean
+++ b/library/data/nat/default.lean
@@ -1,5 +1,6 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Jeremy Avigad
-
-import .basic .order .sub .div .bquant .comm_semiring
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Jeremy Avigad
+-/
+import .basic .order .sub .div .bquant
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index da20824b0..d0ccdf72a 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -8,7 +8,7 @@ Authors: Jeremy Avigad, Leonardo de Moura
 Definitions of div, mod, and gcd on the natural numbers.
 -/
 
-import data.nat.sub data.nat.comm_semiring tools.fake_simplifier
+import data.nat.sub tools.fake_simplifier
 open eq.ops well_founded decidable fake_simplifier prod
 
 namespace nat
@@ -357,7 +357,7 @@ or.elim (eq_zero_or_pos k)
     calc
       m * n div k = m * n div 0   : H1
               ... = 0             : div_zero
-              ... = m * 0         : mul_zero m    -- TODO: why do we have to specify m here?
+              ... = m * 0         : mul_zero m
               ... = m * (n div 0) : div_zero
               ... = m * (n div k) : H1)
   (assume H1 : k > 0,
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 3762f481d..d7cc39b10 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -7,8 +7,7 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad
 
 The order relation on the natural numbers.
 -/
-
-import data.nat.basic data.nat.comm_semiring algebra.ordered_ring
+import data.nat.basic algebra.ordered_ring
 open eq.ops
 
 namespace nat
diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean
index f959a784c..4efa45bb7 100644
--- a/library/data/nat/sub.lean
+++ b/library/data/nat/sub.lean
@@ -7,10 +7,8 @@ Module: data.nat.sub
 
 Subtraction on the natural numbers, as well as min, max, and distance.
 -/
-
 import .order
 import tools.fake_simplifier
-
 open eq.ops
 open fake_simplifier
 
@@ -143,7 +141,7 @@ induction_on m
                    ... = n * k - (l * k + k)  : sub_sub
                    ... = n * k - (succ l * k) : succ_mul)
 
-theorem mul_sub_distr_left (n m k : ℕ) : n * (m - k) = n * m - n * k :=
+theorem mul_sub_left_distrib (n m k : ℕ) : n * (m - k) = n * m - n * k :=
 calc
   n * (m - k) = (m - k) * n   : !mul.comm
           ... = m * n - k * n : !mul_sub_right_distrib