Code for CompleteLinearOrder

Stream: general

[Yijun Yuan]

In mathlib, CompleteLinearOrder = CompleteOrder + BiheytingAlgebra. I'm just confused why the following code doesn't work?

instance {α : Type*} [h1 : CompleteLattice α] [h2 : LinearOrder α] : CompleteLinearOrder α :=
{
  h1, h2.toBiheytingAlgebra with
}

Lean is just complaining about LinearOrder.toBiheytingAlgebra requires BoundedOrder, but why it can't be automatically inferred by CompleteLattice, i.e. h1 in the above code?

[Andrew Yang]

Both CompleteLattice and LinearOrder extends PartialOrder, so {α : Type*} [h1 : CompleteLattice α] [h2 : LinearOrder α] actually means let α be a type, equipped with an order h1 that makes it into a complete lattice, and another totally unrelated order h2 that makes it into a linear order.

[Yijun Yuan]

I understand the situation, but what is the correct way to do so?

[Kenny Lau]

@Yijun Yuan this might be an #xy problem, what are you actually trying to do?

[Floris van Doorn]

Yijun Yuan said:

I understand the situation, but what is the correct way to do so?

Never assume [h1 : CompleteLattice α] [h2 : LinearOrder α]. Just assume [CompleteLinearOrder α] directly.

[Yijun Yuan]

I figured it out by myself. Maybe I should do

noncomputable instance {α : Type*} [h1 : CompleteLattice α] [DecidableEq α] [DecidableLE α] [DecidableLT α] [h2 : IsTotal _ h1.toLE.le] : CompleteLinearOrder α := {
    h1, (Lattice.toLinearOrder α).toBiheytingAlgebra with
    le_total := h2.total
    toDecidableLE := inferInstance
  }