Typeclass strangeness

Stream: general

[Neil Strickland]

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]

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]

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]

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.