Bilattices

Stream: Is there code for X?

[Simon Marynissen]

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

[Johan Commelin]

Nope, I don't think so.

[Johan Commelin]

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

[Simon Marynissen]

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

[Floris van Doorn]

\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.

[Floris van Doorn]

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

[Floris van Doorn]

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.

[Floris van Doorn]

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

[Aaron Anderson]

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.

[Floris van Doorn]

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.

[Patrick Massot]

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

[Simon Marynissen]

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.

[Aaron Anderson]

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.

[Aaron Anderson]

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)

[Aaron Anderson]

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".

[Aaron Anderson]

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.