Zulip Chat Archive

Stream: general

Topic: Conditional complete lattice cleanup

Violeta Hernández (Jun 05 2022 at 23:00):

Currently, complete_lattice.lean and conditionally_complete_lattice.lean are two very different files with very different structures, even if they have a lot of analogous theorems. A few times already I've wanted to use some result on conditional complete lattices that has only been proved on complete lattices. I want to embark on a refactor to match these two APIs.

Of course, the best way to assure that these APIs remain matched in the future would be to put them in a single file, perhaps even putting analogous statements together. This would also get rid of a few redundant statements like Sup_singleton and cSup_singleton, but it would yield a 2k line file, so I don't know if that's the best idea.

Yaël Dillies (Jun 06 2022 at 00:14):

I don't think merging the two files would be a good idea. If the files are separate, you can diff them. Try that out on file#data/set/pointwise and file#data/finset/pointwise. This should be instructive.

Violeta Hernández (Jun 06 2022 at 02:09):

Well, if GitHub allows for this to be done easily, then there shouldn't be an issue with keeping the files separate

Wrenna Robson (Jun 06 2022 at 09:34):

I agree with this and I'd be happy to help with such a refactor. I think there are questions about the best way to do it though.

As I have remarked elsewhere, defining conditionally complete lattices in terms of their relationship with the lattice completion means that we could simply have theorems on CCLs as special cases of theorems on CLs, which, to me, makes sense. This has the benefit of making it easy to define other partially-complete structures, some of which naturally occur in applications.

Wrenna Robson (Jun 06 2022 at 09:35):

Even if we don't do this, however, I agree that a refactor would be useful.

Wrenna Robson (Jun 06 2022 at 09:38):

I have some other ideas for things that this could/should include but I won't get fully into it - I'm just keen and happy to be involved.

Last updated: Dec 20 2023 at 11:08 UTC