From e0ef14ed727010d4457ef55fb1f9407d78235d63 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Thu, 9 May 2024 10:59:45 +0200 Subject: [PATCH] lower instance priorities, add scoped higher prio versions --- Mathlib/Algebra/Order/Field/Defs.lean | 12 +++++++++ Mathlib/Algebra/Order/Group/Defs.lean | 13 ++++++++++ Mathlib/Algebra/Order/Group/Units.lean | 1 + .../Order/GroupWithZero/Canonical.lean | 12 +++++++++ Mathlib/Algebra/Order/Monoid/Basic.lean | 1 + .../Algebra/Order/Monoid/Canonical/Defs.lean | 2 ++ Mathlib/Algebra/Order/Monoid/Defs.lean | 10 +++++++ Mathlib/Algebra/Order/Monoid/OrderDual.lean | 1 + Mathlib/Algebra/Order/Ring/Defs.lean | 26 +++++++++++++++++++ 9 files changed, 78 insertions(+) diff --git a/Mathlib/Algebra/Order/Field/Defs.lean b/Mathlib/Algebra/Order/Field/Defs.lean index ed2ba88ec97d0..8c9306f519b2b 100644 --- a/Mathlib/Algebra/Order/Field/Defs.lean +++ b/Mathlib/Algebra/Order/Field/Defs.lean @@ -26,6 +26,8 @@ A linear ordered (semi)field is a (semi)field equipped with a linear order such -- Guard against import creep. assert_not_exists MonoidHom +open scoped AlgebraOrderInstances + variable {α : Type*} /-- A linear ordered semifield is a field with a linear order respecting the operations. -/ @@ -101,3 +103,13 @@ lemma zpow_pos_of_pos (ha : 0 < a) : ∀ n : ℤ, 0 < a ^ n | (n : ℕ) => by rw [zpow_natCast]; exact pow_pos ha _ | -(n + 1 : ℕ) => by rw [zpow_neg, inv_pos, zpow_natCast]; exact pow_pos ha _ #align zpow_pos_of_pos zpow_pos_of_pos + +-- lower instance priorities to avoid instance synthesis trying this early +attribute [instance 50] LinearOrderedSemifield.toSemifield +attribute [instance 50] LinearOrderedField.toField + +-- add higer-priority versions in scope `AlgebraOrderInstances` +namespace AlgebraOrderInstances +attribute [scoped instance 1000] LinearOrderedSemifield.toSemifield +attribute [scoped instance 1000] LinearOrderedField.toField +end AlgebraOrderInstances diff --git a/Mathlib/Algebra/Order/Group/Defs.lean b/Mathlib/Algebra/Order/Group/Defs.lean index fda928b560d21..ed832a8105f3c 100644 --- a/Mathlib/Algebra/Order/Group/Defs.lean +++ b/Mathlib/Algebra/Order/Group/Defs.lean @@ -21,6 +21,7 @@ may differ between the multiplicative and the additive version of a lemma. The reason is that we did not want to change existing names in the library. -/ +open scoped AlgebraOrderInstances open Function @@ -1291,6 +1292,18 @@ theorem StrictAntiOn.inv (hf : StrictAntiOn f s) : StrictMonoOn (fun x => (f x) end +-- lower instance priorities to avoid instance synthesis trying this early +attribute [instance 50] OrderedAddCommGroup.toAddCommGroup +attribute [instance 50] OrderedCommGroup.toCommGroup +attribute [instance 50] LinearOrderedAddCommGroupWithTop.toSubNegMonoid + +-- add higer-priority versions in scope `AlgebraOrderInstances` +namespace AlgebraOrderInstances +attribute [scoped instance 1000] OrderedAddCommGroup.toAddCommGroup +attribute [scoped instance 1000] OrderedCommGroup.toCommGroup +attribute [scoped instance 1000] LinearOrderedAddCommGroupWithTop.toSubNegMonoid +end AlgebraOrderInstances + /- `NeZero` should not be needed at this point in the ordered algebraic hierarchy. -/ diff --git a/Mathlib/Algebra/Order/Group/Units.lean b/Mathlib/Algebra/Order/Group/Units.lean index 3eecf660ebf36..1346aa831e759 100644 --- a/Mathlib/Algebra/Order/Group/Units.lean +++ b/Mathlib/Algebra/Order/Group/Units.lean @@ -13,6 +13,7 @@ import Mathlib.Algebra.Order.Monoid.Units # The units of an ordered commutative monoid form an ordered commutative group -/ +open scoped AlgebraOrderInstances variable {α : Type*} diff --git a/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean b/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean index 14d9e4649c34b..210d1f6f73fc0 100644 --- a/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean +++ b/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean @@ -31,6 +31,8 @@ whereas it is a very common target for valuations. The solutions is to use a typeclass, and that is exactly what we do in this file. -/ +open scoped AlgebraOrderInstances + variable {α : Type*} /-- A linearly ordered commutative monoid with a zero element. -/ @@ -470,3 +472,13 @@ instance instLinearOrderedCommGroupWithZero [LinearOrderedCommGroup α] : __ := commGroupWithZero end WithZero + +-- lower instance priorities to avoid instance synthesis trying this early +attribute [instance 50] LinearOrderedCommMonoidWithZero.toCommMonoidWithZero +attribute [instance 50] LinearOrderedCommGroupWithZero.toCommGroupWithZero + +-- add higer-priority versions in scope `AlgebraOrderInstances` +namespace AlgebraOrderInstances +attribute [scoped instance 1000] LinearOrderedCommMonoidWithZero.toCommMonoidWithZero +attribute [scoped instance 1000] LinearOrderedCommGroupWithZero.toCommGroupWithZero +end AlgebraOrderInstances diff --git a/Mathlib/Algebra/Order/Monoid/Basic.lean b/Mathlib/Algebra/Order/Monoid/Basic.lean index 069e2dfa9c9ab..f32b2cdf5c26d 100644 --- a/Mathlib/Algebra/Order/Monoid/Basic.lean +++ b/Mathlib/Algebra/Order/Monoid/Basic.lean @@ -15,6 +15,7 @@ import Mathlib.Order.Hom.Basic This file develops some additional material on ordered monoids. -/ +open scoped AlgebraOrderInstances open Function diff --git a/Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean b/Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean index 20ee35c53af0d..dfea87317ebae 100644 --- a/Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean +++ b/Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean @@ -14,6 +14,8 @@ import Mathlib.Algebra.Order.Monoid.Defs # Canonically ordered monoids -/ +open scoped AlgebraOrderInstances + universe u variable {α : Type u} diff --git a/Mathlib/Algebra/Order/Monoid/Defs.lean b/Mathlib/Algebra/Order/Monoid/Defs.lean index a7d0c68cf6fe0..4b833bcd0595b 100644 --- a/Mathlib/Algebra/Order/Monoid/Defs.lean +++ b/Mathlib/Algebra/Order/Monoid/Defs.lean @@ -186,3 +186,13 @@ theorem mul_self_le_one_iff : a * a ≤ 1 ↔ a ≤ 1 := by simp [← not_iff_no @[to_additive (attr := simp)] theorem mul_self_lt_one_iff : a * a < 1 ↔ a < 1 := by simp [← not_iff_not] + +-- lower instance priorities to avoid instance synthesis trying this early +attribute [instance 50] OrderedAddCommMonoid.toAddCommMonoid +attribute [instance 50] OrderedCommMonoid.toCommMonoid + +-- add higer-priority versions in scope `AlgebraOrderInstances` +namespace AlgebraOrderInstances +attribute [scoped instance 1000] OrderedAddCommMonoid.toAddCommMonoid +attribute [scoped instance 1000] OrderedCommMonoid.toCommMonoid +end AlgebraOrderInstances diff --git a/Mathlib/Algebra/Order/Monoid/OrderDual.lean b/Mathlib/Algebra/Order/Monoid/OrderDual.lean index 57b507e561317..4df79911e9cef 100644 --- a/Mathlib/Algebra/Order/Monoid/OrderDual.lean +++ b/Mathlib/Algebra/Order/Monoid/OrderDual.lean @@ -10,6 +10,7 @@ import Mathlib.Algebra.Order.Monoid.Defs /-! # Ordered monoid structures on the order dual. -/ +open scoped AlgebraOrderInstances universe u diff --git a/Mathlib/Algebra/Order/Ring/Defs.lean b/Mathlib/Algebra/Order/Ring/Defs.lean index cc528564a9301..fe79bd99ee04b 100644 --- a/Mathlib/Algebra/Order/Ring/Defs.lean +++ b/Mathlib/Algebra/Order/Ring/Defs.lean @@ -106,6 +106,8 @@ immediate predecessors and what conditions are added to each of them. - `CommRing` & `IsDomain` & linear order structure -/ +open scoped AlgebraOrderInstances + open Function universe u @@ -1327,4 +1329,28 @@ instance (priority := 100) LinearOrderedCommRing.toLinearOrderedCommSemiring @[deprecated] alias zero_lt_mul_left := mul_pos_iff_of_pos_left @[deprecated] alias zero_lt_mul_right := mul_pos_iff_of_pos_right +-- lower instance priorities to avoid instance synthesis trying this early +attribute [instance 50] OrderedSemiring.toSemiring +attribute [instance 50] OrderedCommSemiring.toCommSemiring +attribute [instance 50] OrderedRing.toRing +attribute [instance 50] OrderedCommRing.toCommRing +attribute [instance 50] StrictOrderedSemiring.toSemiring +attribute [instance 50] StrictOrderedCommSemiring.toCommSemiring +attribute [instance 50] StrictOrderedRing.toRing +attribute [instance 50] StrictOrderedCommRing.toCommRing +attribute [instance 50] LinearOrderedCommRing.toCommMonoid + +-- add higer-priority versions in scope `AlgebraOrderInstances` +namespace AlgebraOrderInstances +attribute [scoped instance 1000] OrderedSemiring.toSemiring +attribute [scoped instance 1000] OrderedCommSemiring.toCommSemiring +attribute [scoped instance 1000] OrderedRing.toRing +attribute [scoped instance 1000] OrderedCommRing.toCommRing +attribute [scoped instance 1000] StrictOrderedSemiring.toSemiring +attribute [scoped instance 1000] StrictOrderedCommSemiring.toCommSemiring +attribute [scoped instance 1000] StrictOrderedRing.toRing +attribute [scoped instance 1000] StrictOrderedCommRing.toCommRing +attribute [scoped instance 1000] LinearOrderedCommRing.toCommMonoid +end AlgebraOrderInstances + assert_not_exists MonoidHom