From b11064a90e6f5a704da561dc6ea0163a9f65b31e Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Sat, 3 Jan 2015 17:10:15 -0500
Subject: [PATCH] fix(library/data/nat,int): fix instance declarations for nat
 and int

---
 library/data/int/basic.lean | 18 +++++++-----------
 library/data/int/order.lean | 26 +++++++++++---------------
 library/data/nat/basic.lean |  8 ++++----
 3 files changed, 22 insertions(+), 30 deletions(-)

diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index d359d6655..3f2dba25a 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -597,22 +597,18 @@ or_of_or_of_imp_of_imp H3
   (assume H : (nat_abs a) = nat.zero, nat_abs_eq_zero H)
   (assume H : (nat_abs b) = nat.zero, nat_abs_eq_zero H)
 
-protected definition integral_domain : algebra.integral_domain int :=
-algebra.integral_domain.mk add add.assoc zero zero_add add_zero neg add.left_inv
-add.comm mul mul.assoc (of_num 1) one_mul mul_one mul.left_distrib mul.right_distrib
-zero_ne_one mul.comm @eq_zero_or_eq_zero_of_mul_eq_zero
+section
+  open [classes] algebra
 
---namespace algebra
---  open algebra    -- TODO: why do we have to do this?
---  instance [persistent] int.integral_domain
---end algebra
+  protected definition integral_domain [instance] : algebra.integral_domain int :=
+  algebra.integral_domain.mk add add.assoc zero zero_add add_zero neg add.left_inv
+  add.comm mul mul.assoc (of_num 1) one_mul mul_one mul.left_distrib mul.right_distrib
+  zero_ne_one mul.comm @eq_zero_or_eq_zero_of_mul_eq_zero
+end
 
 /- instantiate ring theorems to int -/
 
 section port_algebra
-  open algebra
-  instance int.integral_domain  -- TODO: why didn't the setting above persist?
-
   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
   theorem add.left_comm : ∀a b c : ℤ, a + (b + c) = b + (a + c) := algebra.add.left_comm
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index 1c21ce864..d51c45081 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -211,23 +211,19 @@ lt.intro
         ... = of_nat (succ (succ n * m + n))   : nat.add_succ
         ... = 0 + succ (succ n * m + n)        : zero_add))
 
-protected definition linear_ordered_comm_ring : algebra.linear_ordered_comm_ring int :=
-algebra.linear_ordered_comm_ring.mk add add.assoc zero zero_add add_zero neg add.left_inv
-  add.comm mul mul.assoc (of_num 1) one_mul mul_one mul.left_distrib mul.right_distrib
-  zero_ne_one le le.refl @le.trans @le.antisymm lt lt_iff_le_and_ne @add_le_add_left
-  @mul_nonneg @mul_pos le_iff_lt_or_eq le.total mul.comm
+section
+  open [classes] algebra
+
+  protected definition linear_ordered_comm_ring [instance] : algebra.linear_ordered_comm_ring int :=
+  algebra.linear_ordered_comm_ring.mk add add.assoc zero zero_add add_zero neg add.left_inv
+    add.comm mul mul.assoc (of_num 1) one_mul mul_one mul.left_distrib mul.right_distrib
+    zero_ne_one le le.refl @le.trans @le.antisymm lt lt_iff_le_and_ne @add_le_add_left
+    @mul_nonneg @mul_pos le_iff_lt_or_eq le.total mul.comm
+end
 
 /- instantiate ordered ring theorems to int -/
 
-namespace algebra
-  open algebra
-  instance [persistent] int.linear_ordered_comm_ring
-end algebra
-
 section port_algebra
-  open algebra
-  instance int.linear_ordered_comm_ring
-
   definition ge (a b : ℤ) := algebra.has_le.ge a b
   definition gt (a b : ℤ) := algebra.has_lt.gt a b
   infix >= := int.ge
@@ -452,8 +448,8 @@ section port_algebra
     @algebra.mul_pos_of_neg_of_neg _ _
 
   theorem mul_self_nonneg : ∀a : ℤ, a * a ≥ 0 := algebra.mul_self_nonneg
-  theorem zero_le_one : #int 0 ≤ 1 := @algebra.zero_le_one int int.linear_ordered_comm_ring
-  theorem zero_lt_one : #int 0 < 1 := @algebra.zero_lt_one int int.linear_ordered_comm_ring
+  theorem zero_le_one : #int 0 ≤ 1 := trivial
+  theorem zero_lt_one : #int 0 < 1 := trivial
   theorem pos_and_pos_or_neg_and_neg_of_mul_pos : ∀{a b : ℤ}, a * b > 0 →
     (a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0) := @algebra.pos_and_pos_or_neg_and_neg_of_mul_pos _ _
 end port_algebra
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index b5ac3d461..5cb61eec0 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -289,15 +289,16 @@ cases_on n
              ... = succ (succ n' * m' + n') : add_succ)⁻¹)
           !succ_ne_zero))
 
-section port_algebra
-
-  open algebra
+section
+  open [classes] algebra
 
   protected definition comm_semiring [instance] : 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
 
@@ -325,7 +326,6 @@ section port_algebra
   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