Very slow LinearOrderedCommGroup instance

slow.lean

-- 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