Zulip Chat Archive

Stream: general

Topic: Typeclass strangeness

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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