Plain not distributive lattices

[hivert]

In file https://github.com/math-comp/finmap/blob/master/order.v:

latticeType == the type of distributive lattices

I.E.: all lattices are assumed to be distributive. There is a lot to say on non-distributive lattices. I'd love to have them.

[pi8027]

Recently, I started to generalize interval.v on top of order.v and proved that intervals on a latticeType are a (non-distributive) lattice, where the meet operator is the intersection and the join operator is the convex hull. To prove some properties of the intersection operator, the non-distributive lattice theory seems to be really useful. For example, x \in i (where i is an interval) is equivalent to X <= i where X := [x, x], so x \in itv_meet i1 i2 = (x \in i1) && (x \in i2) is equivalent to (itv_meet X (itv_meet i1 i2) == X) = (X <= i1) && (X <= i2) which seems to be proved easily by using the non-distributive lattice theory. So now I'm motivated to add the non-distributive lattice structure to MathComp. I intend to do it after math-comp/math-comp#270 is merged.

[hivert]

Excellent ! Each times I'm trying to insert something inside the hierarchy, I end up in a nightmare with canonical wishing there where really some ghostbuster around ;-) Tell me If I can be of any help extending the theory.

[strub]

Hi,

With Xavier Allamigeon, we also need non-distributive lattices, inf-semi lattices and graded posets (and some combinations of the 3 previous ones). I just started adding graded posets to order.v. It would be delightful to see somebody adding the non-distributive lattices structure to order.v

[CohenCyril]

@pi8027

So now I'm motivated to add the non-distributive lattice structure to MathComp. I intend to do it after math-comp/math-comp#270 is merged.

@hivert

Each times I'm trying to insert something inside the hierarchy, I end up in a nightmare with canonical wishing there where really some ghostbuster around ;-)

I really hope that we could start generating hierarchies very soon. The burden of inserting new structures in a hierarchy has reached is limits...

[strub]

@pi8027

So now I'm motivated to add the non-distributive lattice structure to MathComp. I intend to do it after math-comp/math-comp#270 is merged.

@hivert

Each times I'm trying to insert something inside the hierarchy, I end up in a nightmare with canonical wishing there where really some ghostbuster around ;-)

I really hope that we could start generating hierarchies very soon. The burden of inserting new structures in a hierarchy has reached is limits...

Is there an on-going project for solving this? This would be great!

[amahboubi]

Is there an on-going project for solving this? This would be great!

May be this?

[strub]

Ok, thx. I am discovering Coq ELPI at the same time.

[pi8027]

After spending a day for this, I have obtained 4 non-distributive lattice structures:

• ndlatticeType: plain non-distributive lattices,
• ndblatticeType: non-distributive lattices with bottom,
• ndtblatticeType: non-distributive lattices with bottom and top, and
• finNDlatticeType: finite non-distributive lattices (with bottom and top).

Currently, I don't have complemented non-distributive lattice structures. My experimental implementation can be found here: https://github.com/pi8027/math-comp/tree/experiment/order-nondistr-lattice. I probably should contain this to math-comp/math-comp#270 but it would delay the review process. :(

I really hope that we could start generating hierarchies very soon. The burden of inserting new structures in a hierarchy has reached is limits...

I hope so too, but just adding non-distributive lattice structures and reshuffling theorems was not so hard. (I needed to check and fix how small pack notations and factories interact with displays, and also needed to put some record-eta expansions to fix factories. Those were the hard parts for me.)

[strub]

@pi8027 That was fast. In that case, I am going to rebase my graded poset structure on top of your branch and will start using the non-distributive bottom lattices ASAP in our development

[pi8027]

@hivert

Excellent ! Each times I'm trying to insert something inside the hierarchy, I end up in a nightmare with canonical wishing there where really some ghostbuster around ;-) Tell me If I can be of any help extending the theory.

If you understand the invariants of packed classes correctly, you can use my tool hierarchy.ml to detect and fix implementation errors of implicit coercions and canonical projections. https://github.com/math-comp/math-comp/blob/master/etc/utils/hierarchy.ml

• One can use the following command in the mathcomp directory to generate the exhaustive set of assertions for canonical projections that implement inheritances of packed classes.

  $ ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp -lib all.all > hierarchy_test.v

• One can also generate the hierarchy diagram of MathComp as follows (graphviz required). This is sometimes useful to find missing inheritance paths.

  $ ocaml ../etc/utils/hierarchy.ml -canonicals blue -R . mathcomp -lib all.all | dot -Tpdf -o hierarchy.pdf

More details can be found by giving the -help option and in my proposal, slides, and demo for the Coq Workshop 2019.

@strub That would be helpful to improve the quality of my work! I think there are still some glitches. If you find them please ask me and @CohenCyril.

[pi8027]

@strub @hivert I put my non-distributive lattice structures branch as a PR math-comp/math-comp#388. So if you find something wrong, missing things, etc., please report them as comments of that PR. I intend to do some more improvements this week.