From ae7b5a9bc916ea31397e5e7cac1d31815baa5aff Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 Jan 2015 15:53:56 -0800 Subject: [PATCH] fix(library/algebra): add missing `[reducible]` It addresses issues raised at #403 --- library/algebra/group.lean | 8 ++++---- library/algebra/order.lean | 6 +++--- library/algebra/ordered_group.lean | 2 +- library/algebra/ordered_ring.lean | 12 ++++++------ library/algebra/ring.lean | 6 +++--- 5 files changed, 17 insertions(+), 17 deletions(-) diff --git a/library/algebra/group.lean b/library/algebra/group.lean index 577560137..1360b1b31 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -261,11 +261,11 @@ section group ... = (c * b) * b⁻¹ : H ... = c : mul_inv_cancel_right - definition group.to_left_cancel_semigroup [instance] [coercion] : left_cancel_semigroup A := + definition group.to_left_cancel_semigroup [instance] [coercion] [reducible] : left_cancel_semigroup A := ⦃ left_cancel_semigroup, s, mul_left_cancel := @mul_left_cancel A s ⦄ - definition group.to_right_cancel_semigroup [instance] [coercion] : right_cancel_semigroup A := + definition group.to_right_cancel_semigroup [instance] [coercion] [reducible] : right_cancel_semigroup A := ⦃ right_cancel_semigroup, s, mul_right_cancel := @mul_right_cancel A s ⦄ @@ -388,12 +388,12 @@ section add_group ... = (c + b) + -b : H ... = c : add_neg_cancel_right - definition add_group.to_left_cancel_semigroup [instance] [coercion] : + definition add_group.to_left_cancel_semigroup [instance] [coercion] [reducible] : add_left_cancel_semigroup A := ⦃ add_left_cancel_semigroup, s, add_left_cancel := @add_left_cancel A s ⦄ - definition add_group.to_add_right_cancel_semigroup [instance] [coercion] : + definition add_group.to_add_right_cancel_semigroup [instance] [coercion] [reducible] : add_right_cancel_semigroup A := ⦃ add_right_cancel_semigroup, s, add_right_cancel := @add_right_cancel A s ⦄ diff --git a/library/algebra/order.lean b/library/algebra/order.lean index dd15625d9..cee587b5a 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -157,7 +157,7 @@ section ne_ab eq_ab, show a < c, from lt_of_le_of_ne le_ac ne_ac - definition order_pair.to_strict_order [instance] [coercion] [s : order_pair A] : strict_order A := + definition order_pair.to_strict_order [instance] [coercion] [reducible] [s : order_pair A] : strict_order A := ⦃ strict_order, s, lt_irrefl := lt_irrefl s, lt_trans := lt_trans s ⦄ theorem lt_of_lt_of_le : a < b → b ≤ c → a < c := @@ -242,7 +242,7 @@ iff.intro iff.mp !strict_order_with_le.le_iff_lt_or_eq (and.elim_left H), show a < b, from or_resolve_left H1 (and.elim_right H)) -definition strict_order_with_le.to_order_pair [instance] [coercion] [s : strict_order_with_le A] : +definition strict_order_with_le.to_order_pair [instance] [coercion] [reducible] [s : strict_order_with_le A] : strong_order_pair A := ⦃ strong_order_pair, s, le_refl := le_refl s, @@ -277,7 +277,7 @@ section (assume H, H1 H) (assume H, or.elim H (assume H', H2 H') (assume H', H3 H')) - definition linear_strong_order_pair.to_linear_order_pair [instance] [coercion] + definition linear_strong_order_pair.to_linear_order_pair [instance] [coercion] [reducible] [s : linear_strong_order_pair A] : linear_order_pair A := ⦃ linear_order_pair, s ⦄ diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index f3a0d45ff..2c9860bb2 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -203,7 +203,7 @@ theorem ordered_comm_group.le_of_add_le_add_left [s : ordered_comm_group A] {a b have H' : -a + (a + b) ≤ -a + (a + c), from ordered_comm_group.add_le_add_left _ _ H _, !neg_add_cancel_left ▸ !neg_add_cancel_left ▸ H' -definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [coercion] +definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [coercion] [reducible] [s : ordered_comm_group A] : ordered_cancel_comm_monoid A := ⦃ ordered_cancel_comm_monoid, s, add_left_cancel := @add.left_cancel A s, diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean index cd620bf02..d478620cd 100644 --- a/library/algebra/ordered_ring.lean +++ b/library/algebra/ordered_ring.lean @@ -154,7 +154,7 @@ have H1 : 0 < b - a, from iff.elim_right !sub_pos_iff_lt Hab, have H2 : 0 < (b - a) * c, from ordered_ring.mul_pos _ _ H1 Hc, iff.mp !sub_pos_iff_lt (!mul_sub_right_distrib ▸ H2) -definition ordered_ring.to_ordered_semiring [instance] [coercion] [s : ordered_ring A] : +definition ordered_ring.to_ordered_semiring [instance] [coercion] [reducible] [s : ordered_ring A] : ordered_semiring A := ⦃ ordered_semiring, s, mul_zero := mul_zero, @@ -209,7 +209,7 @@ structure linear_ordered_ring [class] (A : Type) extends ordered_ring A, linear_ -- print fields linear_ordered_semiring -definition linear_ordered_ring.to_linear_ordered_semiring [instance] [coercion] +definition linear_ordered_ring.to_linear_ordered_semiring [instance] [coercion] [reducible] [s : linear_ordered_ring A] : linear_ordered_semiring A := ⦃ linear_ordered_semiring, s, @@ -245,7 +245,7 @@ lt.by_cases absurd (H ▸ show 0 < a * b, from mul_pos_of_neg_of_neg Ha Hb) (lt.irrefl 0))) -- Linearity implies no zero divisors. Doesn't need commutativity. -definition linear_ordered_comm_ring.to_integral_domain [instance] [coercion] +definition linear_ordered_comm_ring.to_integral_domain [instance] [coercion] [reducible] [s: linear_ordered_comm_ring A] : integral_domain A := ⦃ integral_domain, s, eq_zero_or_eq_zero_of_mul_eq_zero := @@ -359,11 +359,11 @@ section (assume H1 : 0 < a, calc sign (-a) = -1 : sign_of_neg (neg_neg_of_pos H1) - ... = -(sign a) : {(sign_of_pos H1)⁻¹}) + ... = -(sign a) : sign_of_pos H1) (assume H1 : 0 = a, calc sign (-a) = sign (-0) : H1 - ... = sign 0 : {neg_zero} -- TODO: why do we need {}? + ... = sign 0 : neg_zero ... = 0 : sign_zero ... = -0 : neg_zero ... = -(sign 0) : sign_zero @@ -372,7 +372,7 @@ section calc sign (-a) = 1 : sign_of_pos (neg_pos_of_neg H1) ... = -(-1) : neg_neg - ... = -(sign a) : {(sign_of_neg H1)⁻¹}) + ... = -(sign a) : sign_of_neg H1) -- hopefully, will be quick with the simplifier theorem sign_mul (a b : A) : sign (a * b) = sign a * sign b := sorry diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 947c68220..a07e30724 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -166,7 +166,7 @@ have H : 0 * a + 0 = 0 * a + 0 * a, from calc ... = 0 * a + 0 * a : ring.right_distrib, show 0 * a = 0, from (add.left_cancel H)⁻¹ -definition ring.to_semiring [instance] [coercion] [s : ring A] : semiring A := +definition ring.to_semiring [instance] [coercion] [reducible] [s : ring A] : semiring A := ⦃ semiring, s, mul_zero := ring.mul_zero, zero_mul := ring.zero_mul ⦄ @@ -199,7 +199,7 @@ section theorem neg_eq_neg_one_mul : -a = -1 * a := calc - -a = -(1 * a) : one_mul a ▸ rfl + -a = -(1 * a) : one_mul ... = -1 * a : neg_mul_eq_neg_mul theorem mul_sub_left_distrib : a * (b - c) = a * b - a * c := @@ -228,7 +228,7 @@ end structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A -definition comm_ring.to_comm_semiring [instance] [coercion] [s : comm_ring A] : comm_semiring A := +definition comm_ring.to_comm_semiring [instance] [coercion] [reducible] [s : comm_ring A] : comm_semiring A := ⦃ comm_semiring, s, mul_zero := mul_zero, zero_mul := zero_mul ⦄