Zulip Chat Archive

Stream: Is there code for X?

Topic: Bilattices


view this post on Zulip Simon Marynissen (Jan 22 2021 at 14:44):

I started playing around with Lean, and I wonder if there is code for https://en.wiktionary.org/wiki/bilattice

view this post on Zulip Johan Commelin (Jan 22 2021 at 14:45):

Nope, I don't think so.

view this post on Zulip Johan Commelin (Jan 22 2021 at 14:45):

We have all sorts of lattices, but not two on the same object.

view this post on Zulip Simon Marynissen (Jan 22 2021 at 14:47):

That's unfortunate, It would be nice to use \le\_1 and \le\_2 for the orders. But I think \le is reserved.

view this post on Zulip Floris van Doorn (Jan 22 2021 at 18:15):

\le is reserved indeed, but you can definitely define new notations \le\1 and \le\2 and use that notation for your definition of bilattice.

view this post on Zulip Floris van Doorn (Jan 22 2021 at 18:17):

Though - thinking about it - it might be inconvenient to apply lemmas about lattices for these structures, since lattices use the notation \le.

view this post on Zulip Floris van Doorn (Jan 22 2021 at 18:20):

Another approach is to do something similar to docs#opposite (see module doc) to get two orders on the same type. However, with opposite we tend to not mix the two different operations, while in bilattices we definitely want to mix them. That might get inconvenient.
I think it's a tricky question how to do bilattices cleanly in mathlib.

view this post on Zulip Floris van Doorn (Jan 22 2021 at 19:23):

Oh, a better idea: make \le\1 and similar local notation for \le with a specific instance.
Example:

import order.lattice

variables (α : Type*) (h1 : lattice α) (h2 : lattice α)

local infix ` ≤₁ `:50 := @has_le.le α { .. h1 }
local infix ` ≤₁ `:50 := @has_le.le α { .. h2 }
local infix ` ⊓₁ `:70 := @has_inf.inf α { .. h1 }
local infix ` ⊔₂ `:65 := @has_sup.sup α { .. h2 }
-- etc.

class bilattice :=
  (example_axiom :  x y : α, x ⊓₁ y = x ⊔₂ y)
-- I don't know the actual axioms for bilattices

variables {α h1 h2}

lemma example_axiom [bilattice α h1 h2] (x y : α) : x ⊓₁ y = x ⊔₂ y :=
bilattice.example_axiom x y

view this post on Zulip Aaron Anderson (Jan 22 2021 at 20:49):

I would think that a bilattice would be best modeled as just a bijection between two lattices, but also I don't really think we should create an API for them until someone has something they'd like to prove.

view this post on Zulip Floris van Doorn (Jan 22 2021 at 21:18):

Oh, that is probably a better idea. I agree we shouldn't put them in mathlib until they are used, but I think it's good to think about whether our current API (about lattices) is future proof in the sense that we can define other concepts (bilattices) on top of them.

view this post on Zulip Patrick Massot (Jan 22 2021 at 21:21):

We need to be very careful when messing up with lattices because they are used a lot.

view this post on Zulip Simon Marynissen (Jan 23 2021 at 15:36):

Bilattices are used for semantics of logic programming. It would be nice to be able to use all the results for lattices. The question was not to ask support for it in mathlib.
Wouldn't it make difficult to work with it if it is represented as a bijection between two lattices. What for example with structures that combine multiple different structures like for example topological groups or trilattices. In order to keep modularity I suppose we should not change lattices in any way.

view this post on Zulip Aaron Anderson (Jan 23 2021 at 17:50):

It'd be a bit of a pain, at least at first, to work with the bijection, but based on how much the syntax in mathlib is based on referring to THE <-relation or THE lattice structure on a type, if you put both lattice structures on the same type, you'll have no way of distinguishing them, and it'll be intractable.

view this post on Zulip Aaron Anderson (Jan 23 2021 at 17:51):

And if you want to talk about, say, <1 and <2, with corresponding meets, joins, etc., you have to copy basically every statement you want about lattices for each separate lattice structure manually (or metaprogram this process)

view this post on Zulip Aaron Anderson (Jan 23 2021 at 17:52):

There are already several well-developed APIs where you have multiple structures of the same kind on the same object in mathlib - but they're nearly always through some bijection - I believe the best term for this would be a "type synonym".

view this post on Zulip Aaron Anderson (Jan 23 2021 at 17:54):

For instance, there is already a bilattice in mathlib, it's just not called that. There is a bijection between every lattice and its order_dual, which has its own lattice structure.


Last updated: May 19 2021 at 03:22 UTC