# Zulip Chat Archive

## Stream: general

### Topic: Typeclass strangeness

#### Neil Strickland (Feb 23 2019 at 19:01):

Can anyone suggest how to fix this?

namespace lattice open lattice instance {α : Type*} [decidable_linear_order α] [order_bot α] [order_top α] : bounded_lattice α := { top := order_top.top α, bot := order_bot.bot α, le_top := @order_top.le_top α _, bot_le := @order_bot.bot_le α _, .. (lattice.lattice_of_decidable_linear_order) }

The definitions of `le_top`

and `bot_le`

are rejected, with rather complex error messages. The problem seems to be that Lean is pushing around order relations through some complicated pattern of typeclass inferences involving `lattice`

, `partial_order`

, `preorder`

, `order_top`

and so on, and it has decided that `@order_top.le_top α _`

refers to a different order relation than the one that is needed for the `le_top`

field, although in fact there is only one order relation on `α`

that could possibly be relevant. I have not been able to work out what to do about that.

I only care immediately about the case `α = with_bot (with_top (fin n))`

, but it seems best to do the general thing.

#### Kenny Lau (Feb 23 2019 at 19:02):

The order in `[decidable_linear_order \a]`

and the order in `[order_bot \a]`

and the order in `[order_top \a]`

are not the same

#### Neil Strickland (Feb 23 2019 at 19:25):

OK, I see that I was confused: the `order_bot`

instance is not dependent on the `decidable_linear_order`

instance and contains its own order relation that is completely independent of the previous one. So I'm not sure what's the best thing to do about that. One could define a `bounded_decidable_linear_order`

class extending `decidable_linear_order`

, and then define an instance to convert one of those to a `bounded_distrib_lattice`

. But this seems to be asking for diamond problems, and I am sure that other people know better than me how to think about that.

#### Sebastien Gouezel (Feb 23 2019 at 20:05):

I think `order_bot`

should be modified, to be an additional property of a given `preorder`

instead of containing an order by itself. Then the current theorems about `order_bot`

would have a slightly more complicated statement since they would need two assumptions `[preorder α] [order_bot α]`

, but on the other hand it would be much more convenient to define new properties of orders.

Last updated: May 15 2021 at 00:39 UTC