conditional lattice refactor

Stream: general

[Violeta Hernández]

I've decided to finally start work on matching the APIs on complete lattices and conditionally complete lattices

[Violeta Hernández]

Here's one sticking point I've quickly noticed: what's up with complete_semilattice_Sup and complete_semilattice_Inf?

[Violeta Hernández]

They unconditionally imply complete_lattice, so surely it makes no sense to have them in the typeclass hierarchy?

[Yaël Dillies]

Those two classes should be completely removed from the hierarchy, and docs#boolean_algebra.core as well. They are alternative constructors, not mathematically meaningful typeclasses.

[Violeta Hernández]

Then that's a good starting point for the refactor

[Violeta Hernández]

I'm on it

[Eric Wieser]

Note that docs#complete_semilattice_Sup was added somewhat recently in #6797 by @Scott Morrison; I would wait for their opinion before pushing for removing it

[Eric Wieser]

(Of course, you can still play around with removing it to understand what breaks before that)

[Violeta Hernández]

I opened a draft PR #14863

[Eric Wieser]

I edited its description to link back here

[Wrenna Robson]

Ooh cool. Violeta, I think those typeclasses are meant to have a purpose but they are misdefined. I worked it out the other day but I can't remember where I got to - but essentially if you add the right caveat to le_Sup etc. they make sense.

[Violeta Hernández]

That to me just suggests that there's other potentially useful typeclasses, which doesn't change that the current ones should be removed.

[Violeta Hernández]

I'm curious as to what your proposal is though

[Wrenna Robson]

Oh I totally agree they need to be removed.

[Wrenna Robson]

OK, let me try and put my thoughts together.

You can think of many classes in the order hierarchy as "failing to be complete" in various ways, or "succeeding at being complete" in certain cases. Certain sets have Sups and Inf, by which I mean well-behaved ones, obviously: when I say "a set has an Inf" I mean "for that set s, Inf s is a glb for s, a la complete_lattice_of_Inf, and obviously analogously for Sup`.

For instance, an order_top has Inf for the empty set/Sup for set.univ. An order_bot vice versa. A bounded_order for both. A lattice has them both for every non-empty finite set. A semilattice_inf has only Inf for the same. You get the picture.

We even have some stuff that doesn't use the same notation but which fits into this view. An omega_complete_partial_order essentially has Sups for every chain. There are concepts which I think we don't have but which fit into this framework - a directed-complete partial order is a porder where each directed subset has a Sup.

Obviously, a conditionally_complete_lattice is a porder where every non-empty bounded above set has a Sup, and vice versa for Inf. So it also fits into this view. We also have conditionally_complete_linear_order_bot, which is described as "nonempty subset which is bounded above has a supremum, and every nonempty subset (necessarily bounded below) has an infimum", though this isn't quite true: an empty subset has a sensible Sup (see is_lub_cSup' and note the lack of requirement of s to be nonempty). So actually a conditionally_complete_linear_order_bot has "bounded above Sups and nonempty Infs", and indeed I think these are dual to one another? We don't seem to have a conditionally_complete_linear_order_top but I hope it's clear what that would be.

complete_semilattice_Inf should be "you have as much Inf as you can without completing the lattice", I guess was my thought. If you have every Inf except the Inf of the empty set, I think that's actually conditionally_complete_linear_order_bot, though, and every Inf for bounded below sets" should be "conditionally_complete_linear_order_top`", though we don't have it, as I say.

My overall point is this, which I think you should take into account in this refactor: there is a general paradigm here where there is some sensible set of sets on which Infs or Sups make sense, and the lattice of this set of sets corresponds to the lattice of differently complete structures that we have.

We also have types like with_bot and with_top. These are a bit different. They are used sometimes in two different ways:

• Sometimes they are used like closure operators. That is to say, "with_top nat" is "doing the minimal you want to do to nat in order to make it an order_top". In theory, given any of the semicomplete structures mentioned above, and a partial order, you could apply a closure operator using that structure to your partial order in order to produce a new partial order that is in a precise sense minimal with respect to that structure. In the extreme case of "closure over complete_lattice", this is the Dedekind–MacNeille completion, which we have using order.concept, and I wonder (speculation!) that maybe the work of Yaël in order.concept might provide a general framework to define such a "closure via a semicompletion".
• Sometimes we use with_bot etc. not like closure operators. nat is already an order_bot, but with_bot nat is a different type with its own uses! So here it is... I don't know how to say it, really just a type constructor but not a closure operator of any kind. My claim is not that this is bad, but that conceptually it's a different thing. While it would be work, perhaps more than it's worth, we could try to separate out these two different uses. I have a theory that they probably cause some trouble in some places.

Separately I think to the above things, but interrelated with the first: some types have the property that for some sets, not only do they have Sups/Infs for some sets, but those Sups/Infs are, for some sets, actually Max/Min (which is to say, they are not just glb/lubs but greatest/least elements of the set). In other types, it might be the case that some sets always have a maximal element but not a greatest element - this I think is more different, but it's another property. And because a Sup is the "greatest of upper bounds", the presence of greatest and and least elements of at least some sets is tied up with Sup/Inf presence.

So, to summarise (I'm sorry this is long but I hope it is useful):

• There is a general paradigm where you have some "semicompleteness/conditional completeness property for a type", which is essentially some predicate on sets which says whether or not you have Sups and/or Infs for sets meeting that predicate. (Is this a filter? I don't understand filters, but it might be.)
• Nearly every structure we have in the pure order hierarchy can be described this way.
• Abstracting this common description might make it easier to use the hierarchy, understand how it fits together, and extend it in future.
• "Closure with respect to a semicompleteness structure" is a meaningful concept and one we might be able to support.
• There are a few lacunae or other issues to consider and this isn't a total view.

Thanks for listening.

[Yaël Dillies]

Wrenna, do you know about categorical limits?

[Wrenna Robson]

Vaguely!

[Wrenna Robson]

I guess what I describe above might be that in a sense? But I didn't want to go too abstract.

[Yaël Dillies]

"Sups in different situations" are exactly limits (or colimits? who cares), and this is the right way to talk about them.

[Yaël Dillies]

I'm afraid you're reinventing category theory, that's it :grinning:

[Wrenna Robson]

Sure, I am not claiming to be doing anything new! And isn't it all category theory really? ;) But just as, say, in an algebraic concept "the algebraic closure of a field" is useful in and of itself, even though I'm sure it has a categorical interpretation, perhaps it is useful to have these things without simply saying "well, it's general abstract nonsense".

[Yaël Dillies]

Abstracting this common description might make it easier to use the hierarchy, understand how it fits together, and extend it in future.

This is what the files in catgeory_theory do.

[Wrenna Robson]

Well - this was a reply to Violeta so I shall see what she thinks.

[Yaël Dillies]

You should look up the correspondence between order and category concepts. Here's the ones I can think of on the spot:

• Preorders and categories
• bottom/top element and initial/final object
• sup/inf and binary limit/colimit
• Sup/Inf and arbitrary limit/colimit
• order dual and opposite category
• Heyting algebras and cartesian closed categories

[Wrenna Robson]

Yes, I do know about these things.

[Violeta Hernández]

I don't really understand category theory but that's a really cool insight into the order hierarchy

[Violeta Hernández]

That said, from a design perspective, I have no idea how we would actually implement this

[Wrenna Robson]

I don't know if you meant my post or Yaël's, though I guess your latter comment applies to either.

[Violeta Hernández]

I mean your post

[Wrenna Robson]

Ah - thank you then :D

[Wrenna Robson]

One idea I had - though it wasn't very popular - was to redefine Sup and Inf so that they go into the complete_lattice completion, and then essentially you're talking about "when is Sup/Inf a principal ideal over there". But that doesn't get to the heart of the matter. (It's a bit like embedding a field in its algebraic completion because then it's easier to talk about "the roots of a polynomial" even when they don't exist in the current field, I guess.)

[Violeta Hernández]

That would certainly be a huge change, I don't know what repercussions it might have to change their types like that

[Wrenna Robson]

Oh it would be massive, it's a terrible idea :D

[Wrenna Robson]

But the nice thing about that is that you don't have any kind of junk value for Inf or Sup - it has some meaning. From wikipedia:

The partially ordered set S is join-dense and meet-dense in the Dedekind–MacNeille completion; that is, every element of the completion is a join of some set of elements of S, and is also the meet of some set of elements in S. The Dedekind–MacNeille completion is characterized among completions of S by this property.

Because members of the completion are cuts, which you can think of as sets where the lower bound of their upper bounds is equal to the set (or the pair of that with the dual), if you think about this a little, those sets which are cuts are I think exactly those that have Sups (or Infs dually). So it really does measure "the degree of Sup/Inf failure".

[Wrenna Robson]

I guess I just feel like we have:
ωSup_le_ωSup_of_le
Sup_le_Sup
cSup_le_cSup

And these are all the same theorem - "on good sets, Sup is monotonic" - but we prove it in three unrelated ways. This is what indicates to me that you could do a deep refactor here. If someone wants to introduce a new notion of "semicomplete partial order" - and as noted, there are such notions - we want them to get all these theorems "for free", ideally.

[Junyan Xu]

There is a general paradigm where you have some "semicompleteness/conditional completeness property for a type", which is essentially some predicate on sets which says whether or not you have Sups and/or Infs for sets meeting that predicate.

Probably best phrased in terms of docs#category_theory.limits.has_limits_of_shape

[Violeta Hernández]

Wrenna Robson said:

And these are all the same theorem - "on good sets, Sup is monotonic" - but we prove it in three unrelated ways.

I fear that even if we proved this general theorem, we'd still want the specific instantiations depending on what the "good sets" are

[Violeta Hernández]

That said there should be a much greater effort in making sure these APIs look approximately the same

[Violeta Hernández]

The refactor builds!

[Violeta Hernández]

It definitely looks much cleaner IMO

[Violeta Hernández]

The other PR I made cleaning up the file builds too, it's on @Yaël Dillies to merge it

[Violeta Hernández]

There's still some cleanup I want to do to this file before moving on to actually match APIs

[Violeta Hernández]

Mostly tweak some simp attributes and remove some redundant or frankly pointless theorems

[Violeta Hernández]

There's still some cleanup I want to do to this file before moving on to actually match APIs

[Wrenna Robson]

Oh I definitely agree we'd want the specific instantiations.

[Wrenna Robson]

But as you say, it's about matching APIs and similar constructions. Well done on the initial refactor - this is the one just removing complete_semilattice_Inf?

[Wrenna Robson]

I think the next thing to do that would be useful is just creating a hasse diagram of the hierarchy here and identifying anything else that is a natural structure you'd want, or things like the omega_complete_partial_order which aren't currently in the hierarchy directly but have a natural place in it?

While in some ideal world, yes, some kind of nice categorical construction would be nice, at the very least we can get a clear picture of what the current state of affairs is. Sorry to maths wikipedia (would be good to get a good non-wiki source on this), but these pages are interesting:

https://en.wikipedia.org/wiki/Complete_partial_order
https://en.wikipedia.org/wiki/Completeness_(order_theory)

The "Completeness in terms of adjunctions" section in the latter looks particularly interesting. Which also contains "The considerations in this section suggest a reformulation of (parts of) order theory in terms of category theory, where properties are usually expressed by referring to the relationships (morphisms, more specifically: adjunctions) between objects, instead of considering their internal structure. For more detailed considerations of this relationship see the article on the categorical formulation of order theory", although said article appears to have been deleted...

[Wrenna Robson]

(The "Introduction to Lattices and Order" book that Yael has mentioned before might provide a good source? Would be good to get feedback from multiple order theorists before doing anything wild maybe.)

[Violeta Hernández]

Just a side comment, but putting these three files (complete_lattice, conditionally_complete_lattice, and omega_complete_lattice) on the same folder would help us keep the API matched

[Violeta Hernández]

And also declutter the huge order folder

[Yaël Dillies]

I was thinking about a more general lattice folder, actually.

[Violeta Hernández]

Even then, maybe these specific files still deserve a subfolder?

[Violeta Hernández]

Even then, maybe these specific files still deserve a subfolder?

[Violeta Hernández]

The whole point is that they should have very similar lemmas, just with somewhat different hypotheses

[Yaël Dillies]

Highly unconvinced. Very similar files are rarely (never?) grouped alone in a subfolder. Instead, they are either spread through similar folders (eg the .interval or .pointwise files) or mixed within a bigger folder (eg algebra.big_operators.).

[Wrenna Robson]

You mean omega_complete_partial_order.

[Wrenna Robson]

It isn't a lattice.

[Wrenna Robson]

@Violeta Hernández This page points out one reason we might keep these structures. https://ncatlab.org/nlab/show/suplattice

Namely, while any complete_semilattice_Sup is a complete_lattice, a Sup-preserving map may not preserve Infs. So the type of structure-preserving maps from these things is different.

[Violeta Hernández]

We have no API whatsoever for maps preserving these structures though, and if we did, surely that would be orthogonal to the typeclasses themselves?

[Violeta Hernández]

e.g. group homomorphisms are defined separately from groups

[Wrenna Robson]

Aye, I am not sure if it's an issue in practice.

[Wrenna Robson]

But at least it is a "why would you ever define such a thing": as ever, the answer is categorical.

[Yaël Dillies]

docs#Sup_hom, docs#Inf_hom, docs#SemilatticeSup, docs#SemilatticeInf

[Violeta Hernández]

Oh nice

[Violeta Hernández]

Guess that settles it

[Yaël Dillies]

But the fact that the same objects with different maps form a different category is an important property and it does not mean that we should make the objects different.

[Violeta Hernández]

On this topic, I was thinking

[Violeta Hernández]

It might be clearer what the relation between these different lattices are if instead of having fields Inf_le and le_Inf separately in the classes, we had a single field is_glb_Inf

[Violeta Hernández]

Same goes for Sup

[Violeta Hernández]

For complete lattices, is_glb (Inf s) always, for conditionally complete lattices this happens for nonempty sets that are bounded above, for conditionally complete linear orders with a bottom element it happens when they're bounded above

[Violeta Hernández]

We can then deduce le_Inf and Inf_le from here

[Violeta Hernández]

If nothing else, this approach is certainly conceptually easier

[Violeta Hernández]

And since is_glb (Inf s) is def-eq to le_Inf s \and Inf_le s it shouldn't make any proofs harder

[Violeta Hernández]

It might fail to make them easier if there's no better ways to prove is_glb though

[Yaël Dillies]

The tendency is to rather split fields (#14556) because it makes things easier to prove.

[Eric Wieser]

is_glb (Inf s) has type α → Prop; what are you intending as the second argument?

[Eric Wieser]

Or did you mean is_glb set.univ (Inf s) or is_glb s (Inf s)?

[Wrenna Robson]

Surely is_glb s (Inf s)is the only thing that makes sense?

[Wrenna Robson]

Personally I think this has much to commend it.

[Wrenna Robson]

the split approach is essentially "Inf s \mem lower_bounds s" and "Inf s \mem upper_bounds (lower_bounds s)". It certainly makes sense to have these as their own theorems. But I'm not sure what's better in terms of defining the structure.

[Yury G. Kudryashov]

I think that is_glb_Inf is a good idea because we already have API about is_glb/is_lub.

[Yury G. Kudryashov]

In case of a conditionally_complete_lattice, the axiom should say that for any bounded from below nonempty set s, we have is_glb s (Inf s).

[Yury G. Kudryashov]

But I don't recommend you to start this refactor before running, e.g., a poll on Zulip.

[Violeta Hernández]

Here's an idea, might be a bad idea, might be a good idea, who knows

[Violeta Hernández]

We could create a structure generalized_lattice that looks like the current conditional_lattice, but with extra fields for the sets of sets for which le_cSup, etc. hold

[Violeta Hernández]

We can then create typeclasses for special cases

[Violeta Hernández]

If these sets are the universal set, it's a complete lattice, it they contain the sets of sets bounded above, then they're a conditional complete lattice, and so on

[Violeta Hernández]

A nice thing about this approach is that we can change the def-eqs: for instance, naturals are a conditionally complete lattice, but we might prefer to use the set.finite predicate instead of bdd_above, and on ordinals, we might prefer to use small instead

[Violeta Hernández]

This approach might also alleviate having to prove the same results over and over for these different types: we can prove whatever version is true in the most general case, then specialize

[Wrenna Robson]

I think that's not too far from what I was thinking about, and I like it.

[Wrenna Robson]

However, it shouldn't be called a generalized lattice.

[Wrenna Robson]

Because a lattice is (in particular) one of these where the sets that have this property etc. are the finite sets.

[Wrenna Robson]

Also it's worth thinking about how the presence of Sups and the presence of Infs is related. Obviously all Infs iff all Sups, but...

[Wrenna Robson]

generalized_conditionally_complete_partial_order might work as a name maybe.

[Eric Wieser]

That suggestion sounds a bit like refactoring field to allow other non-invertibility conditions, which I think I considered before but seemed dubious

[Yaël Dillies]

My opinion is that this is solving a problem we don't have.

[Yaël Dillies]

Our order theoretic library does not fine grain enough on what exactly we are allowed to take a supremum of? This is expected, because order theory is a simple special case of category theory. If you want this fine graining, use categories, not orders.

[Yaël Dillies]

In the opposite direction, you could go as far as ditching lattice because "it's just generalized_conditionally_complete_partial_order α (range $ λ x : α × α, {x.1, x.2}) after all".

[Violeta Hernández]

I think that even if we did have a generalized_conditionally_complete_partial_order, we'd still want lattice and all the other special cases. The difference is that now we'd be proving a lot of theorems on generalized_conditionally_complete_partial_order and then transferring them to these special cases.

[Violeta Hernández]

I'm not sure if "just use categories" is a viable solution here. One because I don't know category theory :frown: and two because surely we still have an interest in speaking in these structures as order structures?

[Yaël Dillies]

That's what I'm not sure about. We are going well without these hypothetical typeclasses.

[Violeta Hernández]

That's a fair point

[Violeta Hernández]

I guess we've done alright without a single unifying class

[Wrenna Robson]

I do think we should consider refactoring omega_complete_partial_order so that it uses the Sup notation, rather than a different notation.

[Violeta Hernández]

It doesn't use Sup?

[Violeta Hernández]

That's a surprise given all we've discussed

[Violeta Hernández]

(note: I've never actually touched that code)

[Wrenna Robson]

let me just double-check

[Violeta Hernández]

docs#omega_complete_partial_order

[Wrenna Robson]

(My computer is always slow first thing in the morning, like its owner.)

[Violeta Hernández]

Yeah, we should totally use Sup there too

[Wrenna Robson]

Well it just works a differently too because the domain of ωSup is chains.

[Wrenna Robson]

Rather than, as Sup works everywhere else, the domain being sets, and then having theorems which say "when this set matches this predicate, Sup of it works"

[Violeta Hernández]

Oh

[Violeta Hernández]

In that case I'm not so sure anymore

[Wrenna Robson]

well I think it may reflect the fact that it was designed differently

[Wrenna Robson]

conceptually it really is the same.

[Wrenna Robson]

https://en.wikipedia.org/wiki/Complete_partial_order

[Wrenna Robson]

I maintain that we should be able to describe the three notions on here, of which I believe we have one (?)

[Violeta Hernández]

I guess there's an alternate universe where suprema of conditionally complete lattices take in the subtype of bounded sets instead of sets

[Wrenna Robson]

Yes.

[Wrenna Robson]

Which I think would... be less good.

[Violeta Hernández]

It would suck not being able to use the theorems on conditionally complete lattices on complete lattices

[Wrenna Robson]

Yes

[Violeta Hernández]

Although there's not really that many common theorems, to be fair

[Violeta Hernández]

Mostly just easy ones like Sup {a} = a and such

[Violeta Hernández]

Do we have any such situations with omega-complete partial orders?

[Wrenna Robson]

In terms of annoyances I've encountered, to be honest in the past it's mostly been things like "it's oddly hard to know what the right way to talk about the minimum of a set of natural numbers are", and that isn't (directly) an issue with Sup

[Wrenna Robson]

Violeta Hernández said:

Do we have any such situations with omega-complete partial orders?

Well, every complete lattice is an omega-complete partial order, so we must have all the theorems of the latter on the former.

[Wrenna Robson]

But yeah - I don't think we have to do this refactor, but while I see Yael's complaint, I'm not necessarily saying we should be able to talk about arbitrary Sups - just that we should make sure we have every commonly-used notion of completeness and they should fit together nicely.

[Wrenna Robson]

Wrenna Robson said:

Well it just works a differently too because the domain of ωSup is chains.

chains btw are omega-chains here, and they aren't actually sets because they're monotone functions from Nat to your type or whatnot

[Violeta Hernández]

My PR broke and I can't figure out why for the life of me

[Violeta Hernández]

Can someone check #14863 and tell me why it suddenly changes how the order in upper_setis defined?

[Anne Baanen]

It's possible that the problem is not that the order is different, but that there are too many metavariables to infer the order.

[Anne Baanen]

What happens if you use @compl_subset_compl instead?

[Violeta Hernández]

I'm almost sure the order changed, since changing the ≤ to ≥ fixes these lemmas

[Violeta Hernández]

I'll still try to provide everything explicitly, give me a sec

[Violeta Hernández]

Yeah look,

@[simp] lemma compl_le_compl : s.compl ≤ t.compl ↔ s ≥ t := compl_subset_compl

this works, the original doesn't

[Violeta Hernández]

I think I see the issue

[Violeta Hernández]

upper_set is getting its ≤ from set_like.partial_order

[Violeta Hernández]

So it seems like my PR accidentally uncovered a diamond

[Violeta Hernández]

@Yaël Dillies

[Yaël Dillies]

Oh wait, set_like provides a partial order by default? :grimacing:

[Violeta Hernández]

Yep

[Violeta Hernández]

I presume that should be a definition rather than an instance?

[Violeta Hernández]

Or maybe the solution is to short-circuit typeclass inference in upper_set?

[Yaël Dillies]

We can probably strip that off because most set-like structures are actually complete lattices (so there's no need for a partial_order instance). If lemmas are stated in the generality of set_like using that default partial order, we can restate them using an order embedding or something of sort.

[Violeta Hernández]

You wanna go ahead? I could try fixing this diamond myself but I've never worked with set_like before and I don't want to screw something up

[Yaël Dillies]

You have at least until I wake tomorrow to try it out!

[Violeta Hernández]

I started a fix attempt at #15411, but I have no idea if it will work

[Eric Wieser]

The original point of set_like is "objects with canonical embedding to sets that preserves order and membership and coercion to sort"

[Eric Wieser]

The current behavior is useful; if it's not useful to you, then it sounds like you need a weaker less_set_like class

[Eric Wieser]

(or to rename the existing one)

[Violeta Hernández]

I'm glad to hear that because turning set_like.partial_order into a def breaks a lot of things I don't really understand

[Violeta Hernández]

So, the solution here would be to remove the set_like instance for upper_set?

[Violeta Hernández]

...or possibly, just use the order-dual to get the reverse ordering Yaël wants

[Violeta Hernández]

...and/or revert #14982

[Eric Wieser]

Yeah, either we need a new typeclass for "a bit less set-like than set_like" to use for upper_set, or we should not have made upper_set less set-like in the first place

[Violeta Hernández]

What's the immediate solution though?

[Violeta Hernández]

This is blocking my PR for no good reason

[Violeta Hernández]

It shouldn't be hard to revert #14982 - we can then figure out what should or shouldn't be done long term

[Violeta Hernández]

I still think that just using the order dual of upper_set is the most elegant solution btw

[Eric Wieser]

Using the order dual in the place where we state the isomorphism, you mean?

[Eric Wieser]

A revert seems reasonable to me, but let's wait to hear from @Yaël Dillies

[Violeta Hernández]

Indeed, and if we want to use this order on filters, use the order dual too

[Violeta Hernández]

That's one of the justifications Yaël originally gave for this

[Eric Wieser]

Filters already have this order

[Eric Wieser]

I don't think you'll persuade anyone that changing the order on filters is a good idea

[Eric Wieser]

Just to be clear; which is "your PR" in question?

[Yaël Dillies]

The original order on upper_set was the result of @Bhavik Mehta being doubtful about not using the inclusion order, but the literature is clear that upper sets and filters should be ordered by reverse inclusion (and Bhavik changed his mind), so I would rather suggest either:

• Getting rid of the set_like → partial_order instance
• Getting rid of the set_like (upper_set α) α instance

[Eric Wieser]

docs#upper_set.set_like is the offending instance I assume?

[Eric Wieser]

If the literature is clear on this, can you edit the docstring to reference it for our choice?

[Wrenna Robson]

I think it makes sense to retain the set_like → partial_order instance (I've used it recently).