very slow elaboration for structure instances #1986
Comments
|
There is some sorried data in the above; unsorrying it seems to make elaboration quicker, but it's still noticeably slow (a couple of seconds on a fast machine). I also removed everything which was a theorem, so it's only data now. universe u v
instance {ι : Type u} {α : ι → Type v} [∀ i, LE (α i)] : LE (∀ i, α i) where
le x y := ∀ i, x i ≤ y i
class Top (α : Type u) where
top : α
class Bot (α : Type u) where
bot : α
notation "⊤" => Top.top
notation "⊥" => Bot.bot
class Preorder (α : Type u) extends LE α, LT α where
le_refl : ∀ a : α, a ≤ a
le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
lt := λ a b => a ≤ b ∧ ¬ b ≤ a
lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a)
class PartialOrder (α : Type u) extends Preorder α :=
(le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b)
def Set (α : Type u) := α → Prop
def setOf {α : Type u} (p : α → Prop) : Set α :=
p
namespace Set
variable {α ι : Type _}
protected def Mem (a : α) (s : Set α) : Prop :=
s a
instance : Membership α (Set α) :=
⟨Set.Mem⟩
def range (f : ι → α) : Set α :=
setOf (λ x => ∃ y, f y = x)
end Set
class InfSet (α : Type _) where
infₛ : Set α → α
class SupSet (α : Type _) where
supₛ : Set α → α
export SupSet (supₛ)
export InfSet (infₛ)
open Set
def supᵢ {α : Type _} [SupSet α] {ι} (s : ι → α) : α :=
supₛ (range s)
def infᵢ {α : Type _} [InfSet α] {ι} (s : ι → α) : α :=
infₛ (range s)
class HasSup (α : Type u) where
sup : α → α → α
class HasInf (α : Type u) where
inf : α → α → α
@[inherit_doc]
infixl:68 " ⊔ " => HasSup.sup
@[inherit_doc]
infixl:69 " ⊓ " => HasInf.inf
class SemilatticeSup (α : Type u) extends HasSup α, PartialOrder α where
protected le_sup_left : ∀ a b : α, a ≤ a ⊔ b
protected le_sup_right : ∀ a b : α, b ≤ a ⊔ b
protected sup_le : ∀ a b c : α, a ≤ c → b ≤ c → a ⊔ b ≤ c
class SemilatticeInf (α : Type u) extends HasInf α, PartialOrder α where
protected inf_le_left : ∀ a b : α, a ⊓ b ≤ a
protected inf_le_right : ∀ a b : α, a ⊓ b ≤ b
protected le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c
class Lattice (α : Type u) extends SemilatticeSup α, SemilatticeInf α
class CompleteSemilatticeInf (α : Type _) extends PartialOrder α, InfSet α where
infₛ_le : ∀ s, ∀ a, a ∈ s → infₛ s ≤ a
le_infₛ : ∀ s a, (∀ b, b ∈ s → a ≤ b) → a ≤ infₛ s
class CompleteSemilatticeSup (α : Type _) extends PartialOrder α, SupSet α where
le_supₛ : ∀ s, ∀ a, a ∈ s → a ≤ supₛ s
supₛ_le : ∀ s a, (∀ b, b ∈ s → b ≤ a) → supₛ s ≤ a
class CompleteLattice (α : Type _) extends Lattice α, CompleteSemilatticeSup α,
CompleteSemilatticeInf α, Top α, Bot α where
protected le_top : ∀ x : α, x ≤ ⊤
protected bot_le : ∀ x : α, ⊥ ≤ x
class Frame (α : Type _) extends CompleteLattice α where
class Coframe (α : Type _) extends CompleteLattice α where
infᵢ_sup_le_sup_infₛ (a : α) (s : Set α) : (infᵢ (λ b => a ⊔ b)) ≤ a ⊔ infₛ s
-- should be ⨅ b ∈ s but I had problems with notation
class CompleteDistribLattice (α : Type _) extends Frame α where
infᵢ_sup_le_sup_infₛ : ∀ a s, (infᵢ (λ b => a ⊔ b)) ≤ a ⊔ infₛ s
-- similarly this is not quite right mathematically but this doesn't matter
-- See note [lower instance priority]
instance (priority := 100) CompleteDistribLattice.toCoframe {α : Type _} [CompleteDistribLattice α] :
Coframe α :=
{ ‹CompleteDistribLattice α› with }
class OrderTop (α : Type u) [LE α] extends Top α where
le_top : ∀ a : α, a ≤ ⊤
class OrderBot (α : Type u) [LE α] extends Bot α where
bot_le : ∀ a : α, ⊥ ≤ a
class BoundedOrder (α : Type u) [LE α] extends OrderTop α, OrderBot α
instance(priority := 100) CompleteLattice.toBoundedOrder {α : Type _} [h : CompleteLattice α] :
BoundedOrder α :=
{ h with }
namespace Pi
variable {ι : Type _} {α' : ι → Type _}
instance [∀ i, Bot (α' i)] : Bot (∀ i, α' i) :=
⟨fun _ => ⊥⟩
instance [∀ i, Top (α' i)] : Top (∀ i, α' i) :=
⟨fun _ => ⊤⟩
protected instance LE {ι : Type u} {α : ι → Type v} [∀ i, LE (α i)] : LE (∀ i, α i) where
le x y := ∀ i, x i ≤ y i
instance Preorder {ι : Type u} {α : ι → Type v} [∀ i, Preorder (α i)] : Preorder (∀ i, α i) :=
{ Pi.LE with
le_refl := sorry
le_trans := sorry
lt_iff_le_not_le := sorry }
instance PartialOrder {ι : Type u} {α : ι → Type v} [∀ i, PartialOrder (α i)] :
PartialOrder (∀ i, α i) :=
{ Pi.Preorder with
le_antisymm := sorry }
instance semilatticeSup [∀ i, SemilatticeSup (α' i)] : SemilatticeSup (∀ i, α' i) where
le_sup_left _ _ _ := SemilatticeSup.le_sup_left _ _
le_sup_right _ _ _ := SemilatticeSup.le_sup_right _ _
sup_le _ _ _ ac bc i := SemilatticeSup.sup_le _ _ _ (ac i) (bc i)
instance semilatticeInf [∀ i, SemilatticeInf (α' i)] : SemilatticeInf (∀ i, α' i) where
inf_le_left _ _ _ := SemilatticeInf.inf_le_left _ _
inf_le_right _ _ _ := SemilatticeInf.inf_le_right _ _
le_inf _ _ _ ac bc i := SemilatticeInf.le_inf _ _ _ (ac i) (bc i)
instance lattice [∀ i, Lattice (α' i)] : Lattice (∀ i, α' i) :=
{ Pi.semilatticeSup, Pi.semilatticeInf with }
instance orderTop [∀ i, LE (α' i)] [∀ i, OrderTop (α' i)] : OrderTop (∀ i, α' i) :=
{ inferInstanceAs (Top (∀ i, α' i)) with le_top := sorry }
instance orderBot [∀ i, LE (α' i)] [∀ i, OrderBot (α' i)] : OrderBot (∀ i, α' i) :=
{ inferInstanceAs (Bot (∀ i, α' i)) with bot_le := sorry }
instance boundedOrder [∀ i, LE (α' i)] [∀ i, BoundedOrder (α' i)] : BoundedOrder (∀ i, α' i) :=
{ Pi.orderTop, Pi.orderBot with }
instance SupSet {α : Type _} {β : α → Type _} [∀ i, SupSet (β i)] : SupSet (∀ i, β i) :=
⟨fun s i => supᵢ (λ (f : {f : ∀ i, β i // f ∈ s}) => f.1 i)⟩
instance InfSet {α : Type _} {β : α → Type _} [∀ i, InfSet (β i)] : InfSet (∀ i, β i) :=
⟨fun s i => infᵢ (λ (f : {f : ∀ i, β i // f ∈ s}) => f.1 i)⟩
instance completeLattice {α : Type _} {β : α → Type _} [∀ i, CompleteLattice (β i)] :
CompleteLattice (∀ i, β i) :=
{ Pi.boundedOrder, Pi.lattice with
le_supₛ := sorry
infₛ_le := sorry
supₛ_le := sorry
le_infₛ := sorry
}
instance frame {ι : Type _} {π : ι → Type _} [∀ i, Frame (π i)] : Frame (∀ i, π i) :=
{ Pi.completeLattice with }
instance coframe {ι : Type _} {π : ι → Type _} [∀ i, Coframe (π i)] : Coframe (∀ i, π i) :=
{ Pi.completeLattice with infᵢ_sup_le_sup_infₛ := sorry }
end Pi
-- very quick (instantaneous) in Lean 4
instance Pi.completeDistribLattice' {ι : Type _} {π : ι → Type _}
[∀ i, CompleteDistribLattice (π i)] : CompleteDistribLattice (∀ i, π i) :=
CompleteDistribLattice.mk (Pi.coframe.infᵢ_sup_le_sup_infₛ)
-- takes around 2 seconds wall clock time on my PC (but very quick in Lean 3)
instance Pi.completeDistribLattice'' {ι : Type _} {π : ι → Type _}
[∀ i, CompleteDistribLattice (π i)] : CompleteDistribLattice (∀ i, π i) :=
{ Pi.frame, Pi.coframe with }
-- quick Lean 3 version:
-- https://github.com/leanprover-community/mathlib/blob/b26e15a46f1a713ce7410e016d50575bb0bc3aa4/src/order/complete_boolean_algebra.lean#L210 |
|
def foo {ι : Type _} {π : ι → Type _} [∀ i, CompleteDistribLattice (π i)] :=
@CompleteDistribLattice.mk ((i : ι) → π i)
(@Frame.mk ((i : ι) → π i) (@Frame.toCompleteLattice ((i : ι) → π i) inferInstance))
(@Pi.completeDistribLattice''.proof_1 ι π inferInstance) |
|
A partially unfolded trace with timings (edit: ...milliseconds, not seconds): |
|
The tragic line is |
|
Gabriel points out on Zulip that changing the definitions of class Frame (α : Type _) extends LE α, CompleteLattice α where
class Coframe (α : Type _) extends LE α, CompleteLattice α where
infᵢ_sup_le_sup_infₛ (a : α) (s : Set α) : (infᵢ (λ b => a ⊔ b)) ≤ a ⊔ infₛ smakes both instances very quick (both in the example above and in |
|
Here's another one: in mathlib (where the classes are actually slightly more complex -- I didn't want to have to minimise a bunch of stuff about -- See https://github.com/leanprover-community/mathlib4/blob/489f10454a7ae53fdc6a95d2ac237cbc20e69b36/Mathlib/Algebra/Order/Positive/Field.lean#L42-L46
-- for the actual mathlib problem, which is even slower
universe u
class Preorder (α : Type u) extends LE α, LT α where
le_refl : ∀ a : α, a ≤ a
le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
lt := λ a b => a ≤ b ∧ ¬ b ≤ a
lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) := by intros; rfl
class PartialOrder (α : Type u) extends Preorder α :=
(le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b)
class LinearOrder (α : Type u) extends PartialOrder α, Min α, Max α :=
/-- A linear order is total. -/
le_total (a b : α) : a ≤ b ∨ b ≤ a
decidable_le : DecidableRel (. ≤ . : α → α → Prop)
min := fun a b => if a ≤ b then a else b
max := fun a b => if a ≤ b then b else a
/-- The minimum function is equivalent to the one you get from `minOfLe`. -/
min_def : ∀ a b, min a b = if a ≤ b then a else b := by intros; rfl
/-- The minimum function is equivalent to the one you get from `maxOfLe`. -/
max_def : ∀ a b, max a b = if a ≤ b then b else a := by intros; rfl
instance {α : Type u} [LinearOrder α] : DecidableRel (. ≤ . : α → α → Prop) := LinearOrder.decidable_le
instance {α : Type u} [LinearOrder α] (x y : α) : Decidable (x ≤ y) := LinearOrder.decidable_le x y
class Zero (α : Type u) where
zero : α
instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
ofNat := ‹Zero α›.1
instance Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
zero := 0
class One (α : Type u) where
one : α
instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
ofNat := ‹One α›.1
instance One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
one := 1
class Nontrivial (α : Type _) : Prop where
exists_pair_ne : ∃ x y : α, x ≠ y
class MulZeroClass (M₀ : Type _) extends Mul M₀, Zero M₀ where
zero_mul : ∀ a : M₀, 0 * a = 0
mul_zero : ∀ a : M₀, a * 0 = 0
class AddSemigroup (G : Type u) extends Add G where
/-- Addition is associative -/
add_assoc : ∀ a b c : G, a + b + c = a + (b + c)
class Semigroup (G : Type u) extends Mul G where
mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)
class CommSemigroup (G : Type u) extends Semigroup G where
mul_comm : ∀ a b : G, a * b = b * a
class AddCommSemigroup (G : Type u) extends AddSemigroup G where
add_comm : ∀ a b : G, a + b = b + a
class SemigroupWithZero (S₀ : Type _) extends Semigroup S₀, MulZeroClass S₀
class MulOneClass (M : Type u) extends One M, Mul M where
one_mul : ∀ a : M, 1 * a = a
mul_one : ∀ a : M, a * 1 = a
class AddZeroClass (M : Type u) extends Zero M, Add M where
/-- Zero is a left neutral element for addition -/
zero_add : ∀ a : M, 0 + a = a
/-- Zero is a right neutral element for addition -/
add_zero : ∀ a : M, a + 0 = a
class MulZeroOneClass (M₀ : Type u) extends MulOneClass M₀, MulZeroClass M₀
class AddMonoid (M : Type u) extends AddSemigroup M, AddZeroClass M where
class Monoid (M : Type u) extends Semigroup M, MulOneClass M where
class AddCommMonoid (M : Type u) extends AddMonoid M, AddCommSemigroup M
class CommMonoid (M : Type u) extends Monoid M, CommSemigroup M
class MonoidWithZero (M₀ : Type u) extends Monoid M₀, MulZeroOneClass M₀, SemigroupWithZero M₀
class IsLeftCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] : Prop where
protected mul_left_cancel_of_ne_zero : ∀ {a b c : M₀}, a ≠ 0 → a * b = a * c → b = c
class IsRightCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] : Prop where
class IsCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀]
extends IsLeftCancelMulZero M₀, IsRightCancelMulZero M₀ : Prop
class CancelMonoidWithZero (M₀ : Type _) extends MonoidWithZero M₀, IsCancelMulZero M₀
class CommMonoidWithZero (M₀ : Type _) extends CommMonoid M₀, MonoidWithZero M₀
class Inv (α : Type u) where
inv : α → α
postfix:max "⁻¹" => Inv.inv
class DivInvMonoid (G : Type u) extends Monoid G, Inv G, Div G where
div a b := a * b⁻¹
/-- `a / b := a * b⁻¹` -/
div_eq_mul_inv : ∀ a b : G, a / b = a * b⁻¹ := by intros; rfl
class SubNegMonoid (G : Type u) extends AddMonoid G, Neg G, Sub G where
sub a b := a + -b
sub_eq_add_neg : ∀ a b : G, a - b = a + -b := by intros; rfl
class GroupWithZero (G₀ : Type u) extends MonoidWithZero G₀, DivInvMonoid G₀, Nontrivial G₀ where
inv_zero : (0 : G₀)⁻¹ = 0
mul_inv_cancel (a : G₀) : a ≠ 0 → a * a⁻¹ = 1
class Distrib (R : Type _) extends Mul R, Add R where
protected left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
protected right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c
class CommGroupWithZero (G₀ : Type _) extends CommMonoidWithZero G₀, GroupWithZero G₀
class NonUnitalNonAssocSemiring (α : Type u) extends AddCommMonoid α, Distrib α, MulZeroClass α
class NonUnitalSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, SemigroupWithZero α
class AddMonoidWithOne (R : Type u) extends AddMonoid R, One R where
class AddCommMonoidWithOne (R : Type _) extends AddMonoidWithOne R, AddCommMonoid R
class NonAssocSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, MulZeroOneClass α,
AddCommMonoidWithOne α
class Semiring (α : Type u) extends NonUnitalSemiring α, NonAssocSemiring α, MonoidWithZero α
class NonUnitalCommSemiring (α : Type u) extends NonUnitalSemiring α, CommSemigroup α
class CommSemiring (R : Type u) extends Semiring R, CommMonoid R
instance (priority := 100) CommSemiring.toNonUnitalCommSemiring (α : Type u) [CommSemiring α] :
NonUnitalCommSemiring α :=
{ inferInstanceAs (CommMonoid α), inferInstanceAs (CommSemiring α) with }
instance (priority := 100) CommSemiring.toCommMonoidWithZero (α : Type u) [CommSemiring α] :
CommMonoidWithZero α :=
{ inferInstanceAs (CommMonoid α), inferInstanceAs (CommSemiring α) with }
class Group (G : Type u) extends DivInvMonoid G where
mul_left_inv : ∀ a : G, a⁻¹ * a = 1
/-- An `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.
There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.
-/
class AddGroup (A : Type u) extends SubNegMonoid A where
add_left_neg : ∀ a : A, -a + a = 0
class AddGroupWithOne (R : Type u) extends AddMonoidWithOne R, AddGroup R where
class AddCommGroup (G : Type u) extends AddGroup G, AddCommMonoid G
class CommGroup (G : Type u) extends Group G, CommMonoid G
class NonUnitalNonAssocRing (α : Type u) extends AddCommGroup α, NonUnitalNonAssocSemiring α
class NonUnitalRing (α : Type _) extends NonUnitalNonAssocRing α, NonUnitalSemiring α
class NonAssocRing (α : Type _) extends NonUnitalNonAssocRing α, NonAssocSemiring α,
AddGroupWithOne α
class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R
class NonUnitalCommRing (α : Type u) extends NonUnitalRing α, CommSemigroup α
instance (priority := 100) NonUnitalCommRing.toNonUnitalCommSemiring (α : Type u) [s : NonUnitalCommRing α] :
NonUnitalCommSemiring α :=
{ s with }
class CommRing (α : Type u) extends Ring α, CommMonoid α
instance (priority := 100) CommRing.toCommSemiring (α : Type u) [s : CommRing α] : CommSemiring α :=
{ s with }
instance (priority := 100) CommRing.toNonUnitalCommRing (α : Type u) [s : CommRing α] : NonUnitalCommRing α :=
{ s with }
class DivisionSemiring (α : Type _) extends Semiring α, GroupWithZero α
class DivisionRing (K : Type u) extends Ring K, DivInvMonoid K, Nontrivial K where
protected mul_inv_cancel : ∀ (a : K), a ≠ 0 → a * a⁻¹ = 1
protected inv_zero : (0 : K)⁻¹ = 0
-- ℚ stuff deleted for simplicity
class Semifield (α : Type _) extends CommSemiring α, DivisionSemiring α, CommGroupWithZero α
class Field (K : Type u) extends CommRing K, DivisionRing K
class OrderedCommMonoid (α : Type _) extends CommMonoid α, PartialOrder α where
protected mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b
class OrderedAddCommMonoid (α : Type _) extends AddCommMonoid α, PartialOrder α where
protected add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b
class OrderedAddCommGroup (α : Type u) extends AddCommGroup α, PartialOrder α where
protected add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b
class OrderedCommGroup (α : Type u) extends CommGroup α, PartialOrder α where
protected mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b
class OrderedCancelAddCommMonoid (α : Type u) extends AddCommMonoid α, PartialOrder α where
protected add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b
protected le_of_add_le_add_left : ∀ a b c : α, a + b ≤ a + c → b ≤ c
class OrderedCancelCommMonoid (α : Type u) extends CommMonoid α, PartialOrder α where
protected mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b
protected le_of_mul_le_mul_left : ∀ a b c : α, a * b ≤ a * c → b ≤ c
class LinearOrderedAddCommMonoid (α : Type _) extends LinearOrder α, OrderedAddCommMonoid α
class LinearOrderedCommMonoid (α : Type _) extends LinearOrder α, OrderedCommMonoid α
class LinearOrderedCancelAddCommMonoid (α : Type u) extends OrderedCancelAddCommMonoid α,
LinearOrderedAddCommMonoid α
class LinearOrderedCancelCommMonoid (α : Type u) extends OrderedCancelCommMonoid α,
LinearOrderedCommMonoid α
class LinearOrderedAddCommGroup (α : Type u) extends OrderedAddCommGroup α, LinearOrder α
class LinearOrderedCommGroup (α : Type u) extends OrderedCommGroup α, LinearOrder α
class OrderedSemiring (α : Type u) extends Semiring α, OrderedAddCommMonoid α where
protected zero_le_one : (0 : α) ≤ 1
protected mul_le_mul_of_nonneg_left : ∀ a b c : α, a ≤ b → 0 ≤ c → c * a ≤ c * b
protected mul_le_mul_of_nonneg_right : ∀ a b c : α, a ≤ b → 0 ≤ c → a * c ≤ b * c
class OrderedCommSemiring (α : Type u) extends OrderedSemiring α, CommSemiring α
class OrderedRing (α : Type u) extends Ring α, OrderedAddCommGroup α where
protected zero_le_one : 0 ≤ (1 : α)
protected mul_nonneg : ∀ a b : α, 0 ≤ a → 0 ≤ b → 0 ≤ a * b
class OrderedCommRing (α : Type u) extends OrderedRing α, CommRing α
class StrictOrderedSemiring (α : Type u) extends Semiring α, OrderedCancelAddCommMonoid α,
Nontrivial α where
protected zero_le_one : (0 : α) ≤ 1
protected mul_lt_mul_of_pos_left : ∀ a b c : α, a < b → 0 < c → c * a < c * b
protected mul_lt_mul_of_pos_right : ∀ a b c : α, a < b → 0 < c → a * c < b * c
class StrictOrderedCommSemiring (α : Type u) extends StrictOrderedSemiring α, CommSemiring α
class StrictOrderedRing (α : Type u) extends Ring α, OrderedAddCommGroup α, Nontrivial α where
protected zero_le_one : 0 ≤ (1 : α)
protected mul_pos : ∀ a b : α, 0 < a → 0 < b → 0 < a * b
class StrictOrderedCommRing (α : Type _) extends StrictOrderedRing α, CommRing α
class LinearOrderedSemiring (α : Type u) extends StrictOrderedSemiring α,
LinearOrderedAddCommMonoid α
class LinearOrderedCommSemiring (α : Type _) extends StrictOrderedCommSemiring α,
LinearOrderedSemiring α
class LinearOrderedRing (α : Type u) extends StrictOrderedRing α, LinearOrder α
class LinearOrderedCommRing (α : Type u) extends LinearOrderedRing α, CommMonoid α
instance (priority := 100) LinearOrderedCommSemiring.toLinearOrderedCancelAddCommMonoid
(α : Type u) [LinearOrderedCommSemiring α] : LinearOrderedCancelAddCommMonoid α :=
{ ‹LinearOrderedCommSemiring α› with }
section StrictOrderedRing
variable (α : Type u) [StrictOrderedRing α] {a b c : α}
instance (priority := 100) StrictOrderedRing.toStrictOrderedSemiring : StrictOrderedSemiring α :=
{ ‹StrictOrderedRing α›, (Ring.toSemiring : Semiring α) with
le_of_add_le_add_left := sorry,
mul_lt_mul_of_pos_left := sorry,
mul_lt_mul_of_pos_right := sorry }
@[reducible]
def StrictOrderedRing.toOrderedRing' [@DecidableRel α (· ≤ ·)] : OrderedRing α :=
{ ‹StrictOrderedRing α›, (Ring.toSemiring : Semiring α) with
mul_nonneg := sorry }
instance (priority := 100) StrictOrderedRing.toOrderedRing : OrderedRing α :=
{ ‹StrictOrderedRing α› with
mul_nonneg := sorry }
end StrictOrderedRing
section LinearOrderedRing
variable (α : Type u) [LinearOrderedRing α] {a b c : α}
--attribute [local instance] LinearOrderedRing.decidable_le LinearOrderedRing.decidable_lt
instance (priority := 100) LinearOrderedRing.toLinearOrderedSemiring (α : Type u) [LinearOrderedRing α] : LinearOrderedSemiring α :=
{ ‹LinearOrderedRing α›, StrictOrderedRing.toStrictOrderedSemiring α with }
instance (priority := 100) LinearOrderedRing.toLinearOrderedAddCommGroup :
LinearOrderedAddCommGroup α :=
{ ‹LinearOrderedRing α› with }
end LinearOrderedRing
class LinearOrderedSemifield (α : Type _) extends LinearOrderedCommSemiring α, Semifield α
class LinearOrderedField (α : Type _) extends LinearOrderedCommRing α, Field α
instance (priority := 100) LinearOrderedField.toLinearOrderedSemifield (α : Type u) [LinearOrderedField α] :
LinearOrderedSemifield α :=
{ LinearOrderedRing.toLinearOrderedSemiring α, ‹LinearOrderedField α› with }
open Function
variable {ι α β : Type _}
section LinearOrderedSemifield
variable [LinearOrderedSemifield α] {a : α}
theorem inv_pos : 0 < a⁻¹ ↔ 0 < a := sorry
end LinearOrderedSemifield
class HasSup (α : Type u) where
sup : α → α → α
class HasInf (α : Type u) where
inf : α → α → α
@[inherit_doc]
infixl:68 " ⊔ " => HasSup.sup
@[inherit_doc]
infixl:69 " ⊓ " => HasInf.inf
/-- Transfer a `Preorder` on `β` to a `Preorder` on `α` using a function `f : α → β`.
See note [reducible non-instances]. -/
@[reducible]
def Preorder.lift {α β} [Preorder β] (f : α → β) : Preorder α where
le x y := f x ≤ f y
le_refl _ := sorry
le_trans _ _ _ := sorry
lt x y := f x < f y
lt_iff_le_not_le _ _ := sorry
def Function.Injective (f : α → β) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
/-- Transfer a `PartialOrder` on `β` to a `PartialOrder` on `α` using an injective
function `f : α → β`. See note [reducible non-instances]. -/
@[reducible]
def PartialOrder.lift {α β} [PartialOrder β] (f : α → β) (inj : Injective f) : PartialOrder α :=
{ Preorder.lift f with le_antisymm := sorry }
@[reducible]
def LinearOrder.lift {α β} [LinearOrder β] [HasSup α] [HasInf α] (f : α → β) (inj : Injective f)
(hsup : ∀ x y, f (x ⊔ y) = max (f x) (f y)) (hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y)) :
LinearOrder α :=
{ PartialOrder.lift f inj with
le_total := fun x y => le_total (f x) (f y)
decidable_le := fun x y => (inferInstance : Decidable (f x ≤ f y))
min := (· ⊓ ·)
max := (· ⊔ ·)
min_def := sorry
max_def := sorry }
namespace Subtype
instance preorder [Preorder α] (p : α → Prop) : Preorder (Subtype p) :=
Preorder.lift (fun (a : Subtype p) => (a : α))
instance partialOrder [PartialOrder α] (p : α → Prop) : PartialOrder (Subtype p) :=
PartialOrder.lift (fun (a : Subtype p) => (a : α)) sorry
theorem coe_injective {p : α → Prop} : Injective (fun (a : Subtype p) => (a : α)) := sorry
instance linearOrder [LinearOrder α] (p : α → Prop) : LinearOrder (Subtype p) :=
@LinearOrder.lift (Subtype p) _ _ ⟨fun x y => ⟨max x y, sorry⟩⟩
⟨fun x y => ⟨min x y, sorry⟩⟩ (fun (a : Subtype p) => (a : α))
Subtype.coe_injective (fun _ _ => rfl) fun _ _ => rfl
end Subtype
namespace Function
namespace Injective
variable {M₁ : Type _} {M₂ : Type _} [Mul M₁]
protected def semigroup [Semigroup M₂] (f : M₁ → M₂) (hf : Injective f)
(mul : ∀ x y, f (x * y) = f x * f y) : Semigroup M₁ :=
{ ‹Mul M₁› with mul_assoc := sorry }
@[reducible]
protected def commSemigroup [CommSemigroup M₂] (f : M₁ → M₂) (hf : Injective f)
(mul : ∀ x y, f (x * y) = f x * f y) : CommSemigroup M₁ :=
{ hf.semigroup f mul with mul_comm := sorry }
variable [One M₁]
protected def mulOneClass [MulOneClass M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1)
(mul : ∀ x y, f (x * y) = f x * f y) : MulOneClass M₁ :=
{ ‹One M₁›, ‹Mul M₁› with
one_mul := sorry,
mul_one := sorry }
@[reducible]
protected def monoid [Monoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1)
(mul : ∀ x y, f (x * y) = f x * f y) : Monoid M₁ :=
{ hf.mulOneClass f one mul, hf.semigroup f mul with }
protected def commMonoid [Mul M₁] [CommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1)
(mul : ∀ x y, f (x * y) = f x * f y) :
CommMonoid M₁ :=
{ hf.commSemigroup f mul, hf.monoid f one mul with }
end Injective
end Function
namespace Positive
section Mul
variable {R : Type _} [StrictOrderedSemiring R]
instance [Nontrivial R] : One { x : R // 0 < x } :=
⟨⟨1, sorry⟩⟩
theorem val_one [Nontrivial R] : ((1 : { x : R // 0 < x }) : R) = 1 :=
rfl
instance : Mul { x : R // 0 < x } :=
⟨fun x y => ⟨x * y, sorry⟩⟩
@[simp]
theorem val_mul (x y : { x : R // 0 < x }) : ↑(x * y) = (x * y : R) :=
rfl
end Mul
instance orderedCommMonoid {R : Type _} [StrictOrderedCommSemiring R] [Nontrivial R] :
OrderedCommMonoid { x : R // 0 < x } :=
{ Subtype.partialOrder (λ (x : R) => 0 < x),
Subtype.coe_injective.commMonoid (Subtype.val) val_one val_mul with
mul_le_mul_left := sorry }
instance linearOrderedCancelCommMonoid {R : Type _} [LinearOrderedCommSemiring R] :
LinearOrderedCancelCommMonoid { x : R // 0 < x } :=
{ Subtype.linearOrder _, Positive.orderedCommMonoid with
le_of_mul_le_mul_left := sorry }
variable {K : Type _} [LinearOrderedField K]
instance Subtype.inv : Inv { x : K // 0 < x } :=
⟨fun x => ⟨x⁻¹, sorry⟩⟩
-- super-slow (in actual mathlib the classes are slightly more complex (I removed
-- all the nat, int, rat cast stuff) and this instance
-- actually times out unless maxheartbeats is increased)
-- See https://github.com/leanprover-community/mathlib4/blob/489f10454a7ae53fdc6a95d2ac237cbc20e69b36/Mathlib/Algebra/Order/Positive/Field.lean#L42-L46
instance : LinearOrderedCommGroup { x : K // 0 < x } :=
{ Positive.Subtype.inv, Positive.linearOrderedCancelCommMonoid with
mul_left_inv := sorry }
end Positive |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Prerequisites
Description
We're building the mathlib structure "tower" and some instances are taking a lot longer to compile in Lean 4 than in Lean 3. Here is a rather large MWE, where I build a bunch of the order hierarchy and then at the very bottom I construct an instance in two ways, one very quick and one very slow. I know other examples where I don't have an analogue of the "quick" way because the
mkconstructor is not so convenient. The slowness is really striking: there are three instances of these in the mathlib4 fileMathlib.Order.CompleteBooleanAlgebraand the entire file compiles essentially instantaneously apart from these instances which are super-slow. Here I give three super-quick workarounds for the instances in Mathlib4 but this has come up again in another file and no doubt it will show up more.The text was updated successfully, but these errors were encountered: