From 768ba1c363dfa3110a16a096afa50259831e8349 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Feb 2016 14:30:00 -0800 Subject: [PATCH] refactor(library/hott): remove more unnecessary annotations --- hott/algebra/field.hlean | 3 +-- hott/algebra/group.hlean | 12 ++++-------- hott/algebra/order.hlean | 7 +++---- hott/algebra/ordered_field.hlean | 3 +-- hott/algebra/ordered_group.hlean | 4 ++-- hott/algebra/ordered_ring.hlean | 10 +++------- hott/algebra/ring.hlean | 4 ++-- hott/types/int/basic.hlean | 2 +- hott/types/nat/basic.hlean | 2 +- hott/types/nat/order.hlean | 2 +- library/algebra/complete_lattice.lean | 4 ++-- library/algebra/field.lean | 2 +- library/algebra/group.lean | 10 ++++------ library/algebra/order.lean | 6 +++--- library/algebra/ordered_field.lean | 3 +-- library/algebra/ordered_group.lean | 7 +++---- library/algebra/ordered_ring.lean | 8 ++++---- library/algebra/ring.lean | 4 ++-- library/data/complex.lean | 2 +- library/data/int/basic.lean | 2 +- library/data/int/order.lean | 2 +- library/data/nat/basic.lean | 2 +- library/data/nat/order.lean | 2 +- library/data/rat/basic.lean | 2 +- library/data/rat/order.lean | 2 +- library/data/real/division.lean | 2 +- library/data/real/order.lean | 2 +- library/data/set/filter.lean | 2 +- library/theories/analysis/complex_norm.lean | 2 +- library/theories/analysis/inner_product.lean | 2 +- library/theories/analysis/normed_space.lean | 5 ++--- library/theories/analysis/real_limit.lean | 4 ++-- library/theories/measure_theory/extended_real.lean | 12 ++++-------- library/theories/measure_theory/sigma_algebra.lean | 2 +- library/theories/topology/basic.lean | 4 ++-- library/theories/topology/order_topology.lean | 2 +- 36 files changed, 63 insertions(+), 83 deletions(-) diff --git a/hott/algebra/field.hlean b/hott/algebra/field.hlean index d23c7286e..5816a2274 100644 --- a/hott/algebra/field.hlean +++ b/hott/algebra/field.hlean @@ -334,8 +334,7 @@ section discrete_field (suppose x ≠ 0, sum.inr (by rewrite [-one_mul, -(inv_mul_cancel this), mul.assoc, H, mul_zero])) - definition discrete_field.to_integral_domain [trans_instance] [reducible] : - integral_domain A := + definition discrete_field.to_integral_domain [trans_instance] : integral_domain A := ⦃ integral_domain, s, eq_zero_sum_eq_zero_of_mul_eq_zero := discrete_field.eq_zero_sum_eq_zero_of_mul_eq_zero⦄ diff --git a/hott/algebra/group.hlean b/hott/algebra/group.hlean index ffecca5e2..b13ae81db 100644 --- a/hott/algebra/group.hlean +++ b/hott/algebra/group.hlean @@ -316,13 +316,11 @@ section group ... = x ∘c b : Py ... = a : Px) - definition group.to_left_cancel_semigroup [trans_instance] [reducible] : - left_cancel_semigroup A := + definition group.to_left_cancel_semigroup [trans_instance] : left_cancel_semigroup A := ⦃ left_cancel_semigroup, s, mul_left_cancel := @mul_left_cancel A s ⦄ - definition group.to_right_cancel_semigroup [trans_instance] [reducible] : - right_cancel_semigroup A := + definition group.to_right_cancel_semigroup [trans_instance] : right_cancel_semigroup A := ⦃ right_cancel_semigroup, s, mul_right_cancel := @mul_right_cancel A s ⦄ @@ -444,13 +442,11 @@ section add_group ... = (c + b) + -b : H ... = c : add_neg_cancel_right - definition add_group.to_left_cancel_semigroup [trans_instance] [reducible] : - add_left_cancel_semigroup A := + definition add_group.to_left_cancel_semigroup [trans_instance] : 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 [trans_instance] [reducible] : - add_right_cancel_semigroup A := + definition add_group.to_add_right_cancel_semigroup [trans_instance] : add_right_cancel_semigroup A := ⦃ add_right_cancel_semigroup, s, add_right_cancel := @add_right_cancel A s ⦄ diff --git a/hott/algebra/order.hlean b/hott/algebra/order.hlean index acebf3616..d0b6049b8 100644 --- a/hott/algebra/order.hlean +++ b/hott/algebra/order.hlean @@ -109,7 +109,7 @@ section private theorem lt_trans (s' : order_pair A) (a b c: A) (lt_ab : a < b) (lt_bc : b < c) : a < c := lt_of_lt_of_le lt_ab (le_of_lt lt_bc) - definition order_pair.to_strict_order [trans_instance] [reducible] : strict_order A := + definition order_pair.to_strict_order [trans_instance] : strict_order A := ⦃ strict_order, s, lt_irrefl := lt_irrefl s, lt_trans := lt_trans s ⦄ definition gt_of_gt_of_ge [trans] (H1 : a > b) (H2 : b ≥ c) : a > c := lt_of_le_of_lt H2 H1 @@ -179,8 +179,7 @@ have ne_ac : a ≠ c, from show empty, from ne_of_lt' lt_bc eq_bc, show a < c, from iff.mpr (lt_iff_le_prod_ne) (pair le_ac ne_ac) -definition strong_order_pair.to_order_pair [trans_instance] [reducible] - [s : strong_order_pair A] : order_pair A := +definition strong_order_pair.to_order_pair [trans_instance] [s : strong_order_pair A] : order_pair A := ⦃ order_pair, s, lt_irrefl := lt_irrefl', le_of_lt := le_of_lt', @@ -194,7 +193,7 @@ structure linear_order_pair [class] (A : Type) extends order_pair A, linear_weak structure linear_strong_order_pair [class] (A : Type) extends strong_order_pair A, linear_weak_order A -definition linear_strong_order_pair.to_linear_order_pair [trans_instance] [reducible] +definition linear_strong_order_pair.to_linear_order_pair [trans_instance] [s : linear_strong_order_pair A] : linear_order_pair A := ⦃ linear_order_pair, s, strong_order_pair.to_order_pair ⦄ diff --git a/hott/algebra/ordered_field.hlean b/hott/algebra/ordered_field.hlean index c07086aaf..3404b681e 100644 --- a/hott/algebra/ordered_field.hlean +++ b/hott/algebra/ordered_field.hlean @@ -384,8 +384,7 @@ section discrete_linear_ordered_field (assume H' : ¬ y < x, decidable.inl (le.antisymm (le_of_not_gt H') (le_of_not_gt H)))) - definition discrete_linear_ordered_field.to_discrete_field [trans_instance] [reducible] - : discrete_field A := + definition discrete_linear_ordered_field.to_discrete_field [trans_instance] : discrete_field A := ⦃ discrete_field, s, has_decidable_eq := dec_eq_of_dec_lt⦄ theorem pos_of_one_div_pos (H : 0 < 1 / a) : 0 < a := diff --git a/hott/algebra/ordered_group.hlean b/hott/algebra/ordered_group.hlean index 11a9eaeeb..6b9db1ab6 100644 --- a/hott/algebra/ordered_group.hlean +++ b/hott/algebra/ordered_group.hlean @@ -209,7 +209,7 @@ theorem ordered_comm_group.lt_of_add_lt_add_left [s : ordered_comm_group A] {a b assert H' : -a + (a + b) < -a + (a + c), from ordered_comm_group.add_lt_add_left _ _ H _, by rewrite *neg_add_cancel_left at H'; exact H' -definition ordered_comm_group.to_ordered_cancel_comm_monoid [trans_instance] [reducible] +definition ordered_comm_group.to_ordered_cancel_comm_monoid [trans_instance] [s : ordered_comm_group A] : ordered_cancel_comm_monoid A := ⦃ ordered_cancel_comm_monoid, s, add_left_cancel := @add.left_cancel A _, @@ -581,7 +581,7 @@ structure decidable_linear_ordered_comm_group [class] (A : Type) (add_lt_add_left : Π a b, lt a b → Π c, lt (add c a) (add c b)) definition decidable_linear_ordered_comm_group.to_ordered_comm_group - [trans_instance] [reducible] + [trans_instance] (A : Type) [s : decidable_linear_ordered_comm_group A] : ordered_comm_group A := ⦃ ordered_comm_group, s, le_of_lt := @le_of_lt A _, diff --git a/hott/algebra/ordered_ring.hlean b/hott/algebra/ordered_ring.hlean index 55605590d..c04220716 100644 --- a/hott/algebra/ordered_ring.hlean +++ b/hott/algebra/ordered_ring.hlean @@ -234,9 +234,7 @@ begin exact (iff.mp !sub_pos_iff_lt H2) end -definition ordered_ring.to_ordered_semiring [trans_instance] [reducible] - [s : ordered_ring A] : - ordered_semiring A := +definition ordered_ring.to_ordered_semiring [trans_instance] [s : ordered_ring A] : ordered_semiring A := ⦃ ordered_semiring, s, mul_zero := mul_zero, zero_mul := zero_mul, @@ -316,9 +314,7 @@ structure linear_ordered_ring [class] (A : Type) extends ordered_ring A, linear_strong_order_pair A := (zero_lt_one : lt zero one) -definition linear_ordered_ring.to_linear_ordered_semiring [trans_instance] [reducible] - [s : linear_ordered_ring A] : - linear_ordered_semiring A := +definition linear_ordered_ring.to_linear_ordered_semiring [trans_instance] [s : linear_ordered_ring A] : linear_ordered_semiring A := ⦃ linear_ordered_semiring, s, mul_zero := mul_zero, zero_mul := zero_mul, @@ -370,7 +366,7 @@ lt.by_cases end)) -- Linearity implies no zero divisors. Doesn't need commutativity. -definition linear_ordered_comm_ring.to_integral_domain [trans_instance] [reducible] +definition linear_ordered_comm_ring.to_integral_domain [trans_instance] [s: linear_ordered_comm_ring A] : integral_domain A := ⦃ integral_domain, s, eq_zero_sum_eq_zero_of_mul_eq_zero := diff --git a/hott/algebra/ring.hlean b/hott/algebra/ring.hlean index af18dc083..af8a823e4 100644 --- a/hott/algebra/ring.hlean +++ b/hott/algebra/ring.hlean @@ -172,7 +172,7 @@ have 0 * a + 0 = 0 * a + 0 * a, from calc ... = 0 * a + 0 * a : by rewrite {_*a}ring.right_distrib, show 0 * a = 0, from (add.left_cancel this)⁻¹ -definition ring.to_semiring [trans_instance] [reducible] [s : ring A] : semiring A := +definition ring.to_semiring [trans_instance] [s : ring A] : semiring A := ⦃ semiring, s, mul_zero := ring.mul_zero, zero_mul := ring.zero_mul ⦄ @@ -260,7 +260,7 @@ end structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A -definition comm_ring.to_comm_semiring [trans_instance] [reducible] [s : comm_ring A] : comm_semiring A := +definition comm_ring.to_comm_semiring [trans_instance] [s : comm_ring A] : comm_semiring A := ⦃ comm_semiring, s, mul_zero := mul_zero, zero_mul := zero_mul ⦄ diff --git a/hott/types/int/basic.hlean b/hott/types/int/basic.hlean index 153955441..5ef9784a3 100644 --- a/hott/types/int/basic.hlean +++ b/hott/types/int/basic.hlean @@ -553,7 +553,7 @@ protected theorem eq_zero_sum_eq_zero_of_mul_eq_zero {a b : ℤ} (H : a * b = 0) sum.imp eq_zero_of_nat_abs_eq_zero eq_zero_of_nat_abs_eq_zero (eq_zero_sum_eq_zero_of_mul_eq_zero (by rewrite [-nat_abs_mul, H])) -protected definition integral_domain [reducible] [trans_instance] : integral_domain int := +protected definition integral_domain [trans_instance] : integral_domain int := ⦃integral_domain, add := int.add, add_assoc := int.add_assoc, diff --git a/hott/types/nat/basic.hlean b/hott/types/nat/basic.hlean index 40cfdece1..565340ea9 100644 --- a/hott/types/nat/basic.hlean +++ b/hott/types/nat/basic.hlean @@ -287,7 +287,7 @@ nat.cases_on n ... = succ (succ n' * m' + n') : add_succ)⁻¹ !succ_ne_zero)) -protected definition comm_semiring [reducible] [trans_instance] : comm_semiring nat := +protected definition comm_semiring [trans_instance] : comm_semiring nat := ⦃comm_semiring, add := nat.add, add_assoc := nat.add_assoc, diff --git a/hott/types/nat/order.hlean b/hott/types/nat/order.hlean index 987b2a2ca..d296c5c84 100644 --- a/hott/types/nat/order.hlean +++ b/hott/types/nat/order.hlean @@ -90,7 +90,7 @@ protected theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) /- nat is an instance of a linearly ordered semiring and a lattice -/ -protected definition decidable_linear_ordered_semiring [reducible] [trans_instance] : +protected definition decidable_linear_ordered_semiring [trans_instance] : decidable_linear_ordered_semiring nat := ⦃ decidable_linear_ordered_semiring, nat.comm_semiring, add_left_cancel := @nat.add_left_cancel, diff --git a/library/algebra/complete_lattice.lean b/library/algebra/complete_lattice.lean index 63313c587..d42bd042c 100644 --- a/library/algebra/complete_lattice.lean +++ b/library/algebra/complete_lattice.lean @@ -113,7 +113,7 @@ definition complete_lattice_Inf_to_complete_lattice_Sup [C : complete_lattice_In ⦃ complete_lattice_Sup, C ⦄ -- Every complete_lattice_Inf is a complete_lattice -definition complete_lattice_Inf_to_complete_lattice [trans_instance] [reducible] [C : complete_lattice_Inf A] : +definition complete_lattice_Inf_to_complete_lattice [trans_instance] [C : complete_lattice_Inf A] : complete_lattice A := ⦃ complete_lattice, C ⦄ @@ -179,7 +179,7 @@ definition complete_lattice_Sup_to_complete_lattice_Inf [C : complete_lattice_Su -- Every complete_lattice_Sup is a complete_lattice section -definition complete_lattice_Sup_to_complete_lattice [trans_instance] [reducible] [C : complete_lattice_Sup A] : +definition complete_lattice_Sup_to_complete_lattice [trans_instance] [C : complete_lattice_Sup A] : complete_lattice A := ⦃ complete_lattice, C ⦄ end diff --git a/library/algebra/field.lean b/library/algebra/field.lean index e890353a8..b296fbcf2 100644 --- a/library/algebra/field.lean +++ b/library/algebra/field.lean @@ -313,7 +313,7 @@ section discrete_field (suppose x ≠ 0, or.inr (by rewrite [-one_mul, -(inv_mul_cancel this), mul.assoc, H, mul_zero])) - definition discrete_field.to_integral_domain [trans_instance] [reducible] : + definition discrete_field.to_integral_domain [trans_instance] : integral_domain A := ⦃ integral_domain, s, eq_zero_or_eq_zero_of_mul_eq_zero := discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero⦄ diff --git a/library/algebra/group.lean b/library/algebra/group.lean index c83988ef0..a6a69eccb 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -288,12 +288,12 @@ section group end group -definition group.to_left_cancel_semigroup [trans_instance] [reducible] [s : group A] : +definition group.to_left_cancel_semigroup [trans_instance] [s : group A] : left_cancel_semigroup A := ⦃ left_cancel_semigroup, s, mul_left_cancel := @mul_left_cancel A s ⦄ -definition group.to_right_cancel_semigroup [trans_instance] [reducible] [s : group A] : +definition group.to_right_cancel_semigroup [trans_instance] [s : group A] : right_cancel_semigroup A := ⦃ right_cancel_semigroup, s, mul_right_cancel := @mul_right_cancel A s ⦄ @@ -410,13 +410,11 @@ section add_group assert a + b + -b = a, by inst_simp, by inst_simp - definition add_group.to_left_cancel_semigroup [trans_instance] [reducible] : - add_left_cancel_semigroup A := + definition add_group.to_left_cancel_semigroup [trans_instance] : 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 [trans_instance] [reducible] : - add_right_cancel_semigroup A := + definition add_group.to_add_right_cancel_semigroup [trans_instance] : 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 587450b7e..bfe0a67e8 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -111,7 +111,7 @@ section private theorem lt_trans (s' : order_pair A) (a b c: A) (lt_ab : a < b) (lt_bc : b < c) : a < c := lt_of_lt_of_le lt_ab (le_of_lt lt_bc) - definition order_pair.to_strict_order [trans_instance] [reducible] : strict_order A := + definition order_pair.to_strict_order [trans_instance] : strict_order A := ⦃ strict_order, s, lt_irrefl := lt_irrefl s, lt_trans := lt_trans s ⦄ theorem gt_of_gt_of_ge [trans] (H1 : a > b) (H2 : b ≥ c) : a > c := lt_of_le_of_lt H2 H1 @@ -181,7 +181,7 @@ have ne_ac : a ≠ c, from show false, from ne_of_lt' lt_bc eq_bc, show a < c, from iff.mpr (lt_iff_le_and_ne) (and.intro le_ac ne_ac) -definition strong_order_pair.to_order_pair [trans_instance] [reducible] +definition strong_order_pair.to_order_pair [trans_instance] [s : strong_order_pair A] : order_pair A := ⦃ order_pair, s, lt_irrefl := lt_irrefl', @@ -196,7 +196,7 @@ structure linear_order_pair [class] (A : Type) extends order_pair A, linear_weak structure linear_strong_order_pair [class] (A : Type) extends strong_order_pair A, linear_weak_order A -definition linear_strong_order_pair.to_linear_order_pair [trans_instance] [reducible] +definition linear_strong_order_pair.to_linear_order_pair [trans_instance] [s : linear_strong_order_pair A] : linear_order_pair A := ⦃ linear_order_pair, s, strong_order_pair.to_order_pair ⦄ diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean index d89bf112f..93d6197df 100644 --- a/library/algebra/ordered_field.lean +++ b/library/algebra/ordered_field.lean @@ -393,8 +393,7 @@ section discrete_linear_ordered_field (assume H' : ¬ y < x, decidable.inl (le.antisymm (le_of_not_gt H') (le_of_not_gt H)))) - definition discrete_linear_ordered_field.to_discrete_field [trans_instance] [reducible] - : discrete_field A := + definition discrete_linear_ordered_field.to_discrete_field [trans_instance] : discrete_field A := ⦃ discrete_field, s, has_decidable_eq := dec_eq_of_dec_lt⦄ theorem pos_of_one_div_pos (H : 0 < 1 / a) : 0 < a := diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index 23d6fb91f..d80a4a1e4 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -249,8 +249,7 @@ theorem ordered_comm_group.lt_of_add_lt_add_left [ordered_comm_group A] {a b c : assert H' : -a + (a + b) < -a + (a + c), from ordered_comm_group.add_lt_add_left _ _ H _, by rewrite *neg_add_cancel_left at H'; exact H' -definition ordered_comm_group.to_ordered_cancel_comm_monoid [trans_instance] [reducible] - [s : ordered_comm_group A] : ordered_cancel_comm_monoid A := +definition ordered_comm_group.to_ordered_cancel_comm_monoid [trans_instance] [s : ordered_comm_group A] : ordered_cancel_comm_monoid A := ⦃ ordered_cancel_comm_monoid, s, add_left_cancel := @add.left_cancel A _, add_right_cancel := @add.right_cancel A _, @@ -621,7 +620,7 @@ structure decidable_linear_ordered_comm_group [class] (A : Type) (add_lt_add_left : ∀ a b, lt a b → ∀ c, lt (add c a) (add c b)) definition decidable_linear_ordered_comm_group.to_ordered_comm_group - [trans_instance] [reducible] + [trans_instance] (A : Type) [s : decidable_linear_ordered_comm_group A] : ordered_comm_group A := ⦃ ordered_comm_group, s, le_of_lt := @le_of_lt A _, @@ -629,7 +628,7 @@ definition decidable_linear_ordered_comm_group.to_ordered_comm_group lt_of_lt_of_le := @lt_of_lt_of_le A _ ⦄ definition decidable_linear_ordered_comm_group.to_decidable_linear_ordered_cancel_comm_monoid - [trans_instance] [reducible] (A : Type) [s : decidable_linear_ordered_comm_group A] : + [trans_instance] (A : Type) [s : decidable_linear_ordered_comm_group A] : decidable_linear_ordered_cancel_comm_monoid A := ⦃ decidable_linear_ordered_cancel_comm_monoid, s, @ordered_comm_group.to_ordered_cancel_comm_monoid A _ ⦄ diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean index 489a4f6a3..e3ed6ca41 100644 --- a/library/algebra/ordered_ring.lean +++ b/library/algebra/ordered_ring.lean @@ -242,7 +242,7 @@ begin exact (iff.mp !sub_pos_iff_lt H2) end -definition ordered_ring.to_ordered_semiring [trans_instance] [reducible] +definition ordered_ring.to_ordered_semiring [trans_instance] [s : ordered_ring A] : ordered_semiring A := ⦃ ordered_semiring, s, @@ -324,7 +324,7 @@ structure linear_ordered_ring [class] (A : Type) extends ordered_ring A, linear_strong_order_pair A := (zero_lt_one : lt zero one) -definition linear_ordered_ring.to_linear_ordered_semiring [trans_instance] [reducible] +definition linear_ordered_ring.to_linear_ordered_semiring [trans_instance] [s : linear_ordered_ring A] : linear_ordered_semiring A := ⦃ linear_ordered_semiring, s, @@ -378,7 +378,7 @@ lt.by_cases end)) -- Linearity implies no zero divisors. Doesn't need commutativity. -definition linear_ordered_comm_ring.to_integral_domain [trans_instance] [reducible] +definition linear_ordered_comm_ring.to_integral_domain [trans_instance] [s: linear_ordered_comm_ring A] : integral_domain A := ⦃ integral_domain, s, eq_zero_or_eq_zero_of_mul_eq_zero := @@ -464,7 +464,7 @@ structure decidable_linear_ordered_comm_ring [class] (A : Type) extends linear_o decidable_linear_ordered_comm_group A definition decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_semiring - [trans_instance] [reducible] [s : decidable_linear_ordered_comm_ring A] : + [trans_instance] [s : decidable_linear_ordered_comm_ring A] : decidable_linear_ordered_semiring A := ⦃decidable_linear_ordered_semiring, s, @linear_ordered_ring.to_linear_ordered_semiring A _⦄ diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index ed24a92d5..56089450f 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -174,7 +174,7 @@ have 0 * a + 0 = 0 * a + 0 * a, from calc ... = 0 * a + 0 * a : by rewrite right_distrib, show 0 * a = 0, from (add.left_cancel this)⁻¹ -definition ring.to_semiring [trans_instance] [reducible] [s : ring A] : semiring A := +definition ring.to_semiring [trans_instance] [s : ring A] : semiring A := ⦃ semiring, s, mul_zero := ring.mul_zero, zero_mul := ring.zero_mul ⦄ @@ -255,7 +255,7 @@ end structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A -definition comm_ring.to_comm_semiring [trans_instance] [reducible] [s : comm_ring A] : comm_semiring A := +definition comm_ring.to_comm_semiring [trans_instance] [s : comm_ring A] : comm_semiring A := ⦃ comm_semiring, s, mul_zero := mul_zero, zero_mul := zero_mul ⦄ diff --git a/library/data/complex.lean b/library/data/complex.lean index c284d34a4..e70eb3560 100644 --- a/library/data/complex.lean +++ b/library/data/complex.lean @@ -278,7 +278,7 @@ take z w, classical.prop_decidable (z = w) protected theorem zero_ne_one : (0 : ℂ) ≠ 1 := assume H, zero_ne_one (eq_of_of_real_eq_of_real H) -protected noncomputable definition discrete_field [reducible][trans_instance] : +protected noncomputable definition discrete_field [trans_instance] : discrete_field ℂ := ⦃ discrete_field, complex.comm_ring, mul_inv_cancel := @complex.mul_inv_cancel, diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 358752196..7fd6c9567 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -515,7 +515,7 @@ protected theorem eq_zero_or_eq_zero_of_mul_eq_zero {a b : ℤ} (H : a * b = 0) or.imp eq_zero_of_nat_abs_eq_zero eq_zero_of_nat_abs_eq_zero (eq_zero_or_eq_zero_of_mul_eq_zero (by rewrite [-nat_abs_mul, H])) -protected definition integral_domain [reducible] [trans_instance] : integral_domain int := +protected definition integral_domain [trans_instance] : integral_domain int := ⦃integral_domain, add := int.add, add_assoc := int.add_assoc, diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 2d1b8260c..a128432e5 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -232,7 +232,7 @@ protected theorem lt_of_le_of_lt {a b c : ℤ} (Hab : a ≤ b) (Hbc : b < c) : (iff.mpr !int.lt_iff_le_and_ne) (and.intro Hac (assume Heq, int.not_le_of_gt (Heq⁻¹ ▸ Hbc) Hab)) -protected definition linear_ordered_comm_ring [reducible] [trans_instance] : +protected definition linear_ordered_comm_ring [trans_instance] : linear_ordered_comm_ring int := ⦃linear_ordered_comm_ring, int.integral_domain, le := int.le, diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index aa9db5fed..dd73228de 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -237,7 +237,7 @@ nat.cases_on n (by simp) (show succ (succ n' * m' + n') = 0, by simp) !succ_ne_zero)) -protected definition comm_semiring [reducible] [trans_instance] : comm_semiring nat := +protected definition comm_semiring [trans_instance] : comm_semiring nat := ⦃comm_semiring, add := nat.add, add_assoc := nat.add_assoc, diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 61a2f976e..766579146 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -90,7 +90,7 @@ protected theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) /- nat is an instance of a linearly ordered semiring and a lattice -/ -protected definition decidable_linear_ordered_semiring [reducible] [trans_instance] : +protected definition decidable_linear_ordered_semiring [trans_instance] : decidable_linear_ordered_semiring nat := ⦃ decidable_linear_ordered_semiring, nat.comm_semiring, add_left_cancel := @nat.add_left_cancel, diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean index 3dd17dc7f..96d3af46f 100644 --- a/library/data/rat/basic.lean +++ b/library/data/rat/basic.lean @@ -550,7 +550,7 @@ decidable.by_cases end)) -protected definition discrete_field [reducible] [trans_instance] : discrete_field rat := +protected definition discrete_field [trans_instance] : discrete_field rat := ⦃discrete_field, add := rat.add, add_assoc := rat.add_assoc, diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean index a8b0966cb..fa7959d79 100644 --- a/library/data/rat/order.lean +++ b/library/data/rat/order.lean @@ -301,7 +301,7 @@ let H' := rat.le_of_lt H in (take Heq, let Heq' := add_left_cancel Heq in !rat.lt_irrefl (Heq' ▸ H))) -protected definition discrete_linear_ordered_field [reducible] [trans_instance] : +protected definition discrete_linear_ordered_field [trans_instance] : discrete_linear_ordered_field rat := ⦃discrete_linear_ordered_field, rat.discrete_field, diff --git a/library/data/real/division.lean b/library/data/real/division.lean index e6bc53852..1c8b780c1 100644 --- a/library/data/real/division.lean +++ b/library/data/real/division.lean @@ -639,7 +639,7 @@ noncomputable definition dec_lt : decidable_rel real.lt := apply prop_decidable end -protected noncomputable definition discrete_linear_ordered_field [reducible] [trans_instance]: +protected noncomputable definition discrete_linear_ordered_field [trans_instance]: discrete_linear_ordered_field ℝ := ⦃ discrete_linear_ordered_field, real.comm_ring, real.ordered_ring, le_total := real.le_total, diff --git a/library/data/real/order.lean b/library/data/real/order.lean index edeec7082..25ada2763 100644 --- a/library/data/real/order.lean +++ b/library/data/real/order.lean @@ -1092,7 +1092,7 @@ protected theorem le_of_lt_or_eq (x y : ℝ) : x < y ∨ x = y → x ≤ y := apply (or.inr (quot.exact H')) end))) -definition ordered_ring [reducible] [trans_instance] : ordered_ring ℝ := +definition ordered_ring [trans_instance] : ordered_ring ℝ := ⦃ ordered_ring, real.comm_ring, le_refl := real.le_refl, le_trans := @real.le_trans, diff --git a/library/data/set/filter.lean b/library/data/set/filter.lean index d7621eb68..e96c826f5 100644 --- a/library/data/set/filter.lean +++ b/library/data/set/filter.lean @@ -287,7 +287,7 @@ namespace complete_lattice Sup_le (λ G GS, GS F FS) end complete_lattice -protected definition complete_lattice [reducible] [trans_instance] : complete_lattice (filter A) := +protected definition complete_lattice [trans_instance] : complete_lattice (filter A) := ⦃ complete_lattice, le := complete_lattice.le, le_refl := complete_lattice.le_refl, diff --git a/library/theories/analysis/complex_norm.lean b/library/theories/analysis/complex_norm.lean index 1a161308c..94e8cd04f 100644 --- a/library/theories/analysis/complex_norm.lean +++ b/library/theories/analysis/complex_norm.lean @@ -63,7 +63,7 @@ namespace complex local attribute complex.real_inner_product_space [trans_instance] - protected definition normed_vector_space [trans_instance] [reducible] : normed_vector_space ℂ := + protected definition normed_vector_space [trans_instance] : normed_vector_space ℂ := _ theorem norm_squared_eq_cmod (z : ℂ) : ∥ z ∥^2 = cmod z := by rewrite norm_squared diff --git a/library/theories/analysis/inner_product.lean b/library/theories/analysis/inner_product.lean index c294d8bd3..9501b1e4d 100644 --- a/library/theories/analysis/inner_product.lean +++ b/library/theories/analysis/inner_product.lean @@ -172,7 +172,7 @@ have (ip_norm (u + v))^2 ≤ (ip_norm u + ip_norm v)^2, from mul.comm (ip_norm v) (ip_norm u)], le_of_squared_le_squared (add_nonneg !ip_norm_nonneg !ip_norm_nonneg) this -definition inner_product_space.to_normed_space [trans_instance] [reducible] : +definition inner_product_space.to_normed_space [trans_instance] : normed_vector_space V := ⦃ normed_vector_space, _inst_1, norm := ip_norm, diff --git a/library/theories/analysis/normed_space.lean b/library/theories/analysis/normed_space.lean index 21c9e46f7..2d94782bc 100644 --- a/library/theories/analysis/normed_space.lean +++ b/library/theories/analysis/normed_space.lean @@ -103,7 +103,7 @@ section private lemma nvs_dist_comm (u v : V) : nvs_dist u v = nvs_dist v u := by rewrite [↑nvs_dist, -norm_neg, neg_sub] - definition normed_vector_space_to_metric_space [reducible] [trans_instance] + definition normed_vector_space_to_metric_space [trans_instance] (V : Type) [nvsV : normed_vector_space V] : metric_space V := ⦃ metric_space, @@ -132,8 +132,7 @@ structure banach_space [class] (V : Type) extends nvsV : normed_vector_space V : (complete : ∀ X, @analysis.cauchy V (@normed_vector_space_to_metric_space V nvsV) X → @analysis.converges_seq V (@normed_vector_space_to_metric_space V nvsV) X) -definition banach_space_to_metric_space [reducible] [trans_instance] - (V : Type) [bsV : banach_space V] : +definition banach_space_to_metric_space [trans_instance] (V : Type) [bsV : banach_space V] : complete_metric_space V := ⦃ complete_metric_space, normed_vector_space_to_metric_space V, complete := banach_space.complete diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean index 28fb9800d..552dc637e 100644 --- a/library/theories/analysis/real_limit.lean +++ b/library/theories/analysis/real_limit.lean @@ -221,7 +221,7 @@ exists.intro l end analysis -definition complete_metric_space_real [reducible] [trans_instance] : +definition complete_metric_space_real [trans_instance] : complete_metric_space ℝ := ⦃complete_metric_space, metric_space_real, complete := @analysis.converges_seq_of_cauchy @@ -238,7 +238,7 @@ definition real_vector_space_real : real_vector_space ℝ := one_smul := one_mul ⦄ -definition banach_space_real [trans_instance] [reducible] : banach_space ℝ := +definition banach_space_real [trans_instance] : banach_space ℝ := ⦃ banach_space, real_vector_space_real, norm := abs, norm_zero := abs_zero, diff --git a/library/theories/measure_theory/extended_real.lean b/library/theories/measure_theory/extended_real.lean index 778d2008c..035762f04 100644 --- a/library/theories/measure_theory/extended_real.lean +++ b/library/theories/measure_theory/extended_real.lean @@ -281,8 +281,7 @@ by krewrite [ereal.mul_comm, ereal.one_mul] -- Note that distributivity fails, e.g. ∞ ⬝ (-1 + 1) ≠ ∞ * -1 + ∞ * 1 -protected definition comm_monoid [reducible] [trans_instance] : - comm_monoid ereal := +protected definition comm_monoid [trans_instance] : comm_monoid ereal := ⦃comm_monoid, mul := ereal.mul, mul_assoc := ereal.mul_assoc, @@ -292,8 +291,7 @@ protected definition comm_monoid [reducible] [trans_instance] : mul_comm := ereal.mul_comm ⦄ -protected definition add_comm_monoid [reducible] [trans_instance] : - add_comm_monoid ereal := +protected definition add_comm_monoid [trans_instance] : add_comm_monoid ereal := ⦃add_comm_monoid, add := ereal.add, add_assoc := ereal.add_assoc, @@ -313,8 +311,7 @@ protected definition le : ereal → ereal → Prop | ∞ (of_real y) := false | ∞ -∞ := false -definition ereal_has_le [instance] [priority ereal.prio] : - has_le ereal := +definition ereal_has_le [instance] [priority ereal.prio] : has_le ereal := has_le.mk ereal.le theorem of_real_le_of_real (x y : real) : of_real x ≤ of_real y ↔ x ≤ y := @@ -393,8 +390,7 @@ theorem neg_infty_lt_of_real (x : real) : -∞ < of_real x := and.intro trivial theorem of_real_lt_infty (x : real) : of_real x < ∞ := and.intro trivial (ne.symm !infty_ne_of_real) -protected definition decidable_linear_order [reducible] [trans_instance] : - decidable_linear_order ereal := +protected definition decidable_linear_order [trans_instance] : decidable_linear_order ereal := ⦃decidable_linear_order, le := ereal.le, le_refl := ereal.le_refl, diff --git a/library/theories/measure_theory/sigma_algebra.lean b/library/theories/measure_theory/sigma_algebra.lean index 872c33e45..340f11443 100644 --- a/library/theories/measure_theory/sigma_algebra.lean +++ b/library/theories/measure_theory/sigma_algebra.lean @@ -200,7 +200,7 @@ protected theorem Sup_le {N : sigma_algebra X} {MS : set (sigma_algebra X)} (H : have (⋃ M ∈ MS, @sets _ M) ⊆ @sets _ N, from bUnion_subset H, sets_generated_by_initial this -protected definition complete_lattice [reducible] [trans_instance] : +protected definition complete_lattice [trans_instance] : complete_lattice (sigma_algebra X) := ⦃complete_lattice, le := sigma_algebra.le, diff --git a/library/theories/topology/basic.lean b/library/theories/topology/basic.lean index 4561249b0..b543e1880 100644 --- a/library/theories/topology/basic.lean +++ b/library/theories/topology/basic.lean @@ -166,7 +166,7 @@ end topology structure T1_space [class] (X : Type) extends topology X := (T1 : ∀ {x y}, x ≠ y → ∃ U, U ∈ opens ∧ x ∈ U ∧ y ∉ U) -protected definition T0_space.of_T1 [reducible] [trans_instance] {X : Type} [T : T1_space X] : +protected definition T0_space.of_T1 [trans_instance] {X : Type} [T : T1_space X] : T0_space X := ⦃T0_space, T, T0 := abstract @@ -208,7 +208,7 @@ end topology structure T2_space [class] (X : Type) extends topology X := (T2 : ∀ {x y}, x ≠ y → ∃ U V, U ∈ opens ∧ V ∈ opens ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = ∅) -protected definition T1_space.of_T2 [reducible] [trans_instance] {X : Type} [T : T2_space X] : +protected definition T1_space.of_T2 [trans_instance] {X : Type} [T : T2_space X] : T1_space X := ⦃T1_space, T, T1 := abstract diff --git a/library/theories/topology/order_topology.lean b/library/theories/topology/order_topology.lean index a43a98b5f..fe7a19058 100644 --- a/library/theories/topology/order_topology.lean +++ b/library/theories/topology/order_topology.lean @@ -57,7 +57,7 @@ section exists.intro y (exists.intro x (and.intro (and.intro `x < y` `x < y`) this)) end -protected definition T2_space.of_linorder_topology [reducible] [trans_instance] : +protected definition T2_space.of_linorder_topology [trans_instance] : T2_space X := ⦃ T2_space, linorder_topology, T2 := abstract