Zulip Chat Archive

Stream: general

Topic: Strange instance problem with distributive lattice


Chase Meadors (Jun 10 2021 at 11:25):

The following gives a strange type mismatch error:

import order.complete_lattice
example {α : Type*} [distrib_lattice α] [complete_lattice α] {x y z : α} :
  x  (y  z) = x  y  x  z := inf_sup_left

Replacing inf_sup_left with the more explicit @inf_sup_left α _ x y z yields a very very long type mismatch error.

Upon inspection, removing the [complete_lattice α] instance from the hypothesis makes everything fine. What could be going on here?

Sebastien Gouezel (Jun 10 2021 at 11:27):

You have two different lattice structures (coming from your two instances), for which the operations are completely unrelated. So Lean is confused.

Chase Meadors (Jun 10 2021 at 11:36):

Hm, the class tree is a bit complicated here, but I thought both extended has_sup and has_inf all the way down, so that these operators would be unambiguous. My ignorance of the more technical aspects of type classes might be showing here though; I'm not 100% sure what you mean.
In context, I'd like to work with a complete lattice that is distributive, and rewrite somewhere with this lemma.

Eric Wieser (Jun 10 2021 at 11:39):

The fact that both extend has_sup is exactly the problem. Your lemma doesn't have anything that says the two sups are the same.

Eric Wieser (Jun 10 2021 at 11:40):

Just like if you take two integers as an argument, lean won't assume they are equal

Chase Meadors (Jun 10 2021 at 11:41):

Oh, I see! That makes sense. I'm specifying two (potentially completely unrelated) structures on α.

Rémy Degenne (Jun 10 2021 at 11:41):

There is a docs#complete_distrib_lattice class, which might interest you

Rémy Degenne (Jun 10 2021 at 11:42):

for other code that you may have I mean. It is not useful for that example.

Chase Meadors (Jun 10 2021 at 11:44):

Right. In my case I want to specifically avoid the _infinite_ distributive property, as that's part of / related to the conclusions. But this discussion clears things up and I think I can find a way to make things work now.


Last updated: Dec 20 2023 at 11:08 UTC