succ_order and pred_order design

Stream: maths

[Violeta Hernández]

So, @Yaël Dillies and I have been discussing about the design of the docs#succ_order and docs#pred_order typeclasses

[Violeta Hernández]

Currently, succ_order is defined so that succ a covers a unless a is maximal, in which case succ a is some other order-indistinguishable maximal element

[Violeta Hernández]

Of course the mental model is that we're working within a partial order, so that for a maximal element, succ a = a.

[Violeta Hernández]

We have the notion of an docs#is_succ_limit, which is a value that isn't the successor of any value other than possibly itself

[Violeta Hernández]

Think omega on ordinals, or the top in with_top nat

[Violeta Hernández]

Now here's the thing

[Violeta Hernández]

As I proved in #15614, any succ_order has a certain predecessor-like function that I'm calling pred', defined such that pred' a = a on successor limits a, and pred' (succ a) = a for non-maximal a.

[Violeta Hernández]

In a partial order that's also is_succ_archimedean, this function can be used to build a pred_order that satisfies is_pred_archimedean

[Violeta Hernández]

Which means that right off the bat, in the cases we care about, these two classes are actually equivalent

[Violeta Hernández]

Now, Yaël raised the concern that succ_order and pred_order might actually be too strict, if pred' is only a valid predecessor function in the Archimedean case.

[Violeta Hernández]

After all, we do use a predecessor function like this in a non-archimedean order at least once: docs#ordinal.pred

[Violeta Hernández]

Of course, if pred' can be built from any partial succ_order and is a valid predecessor function, then we need to question whether it's even worth having succ_order and pred_order be separate classes.

[Violeta Hernández]

So the first question I'd like to answer is: do we want every succ_order to also be a pred_order and viceversa?

[Violeta Hernández]

These typeclasses don't really correspond to anything in the math library, even though they're undeniably useful to have in mathlib, so we get to make up our own answers here.

[Violeta Hernández]

At the same time, I don't think there's a need to fix what isn't broken. We can have both these typeclasses, and define the functions order.succ' and order.pred' when you want a weaker notion of a successor or predecessor given the other.

[Violeta Hernández]

If we do want to unify these typeclasses, then the next question would be what the new assumptions would become.

[Violeta Hernández]

So yeah, opinions welcome.

[Eric Rodriguez]

we definitely want definitional control of both

[Eric Rodriguez]

I think we could pretty much set them to the obvious things

[Eric Rodriguez]

like just merge it into one class

[Violeta Hernández]

That much is true

[Violeta Hernández]

We could have a single succ_pred_order class with two data fields succ and pred and constructors for one given the other when you don't care about the def-eq

[Violeta Hernández]

But of course we do have reasonable ways to fill out both in most cases, e.g. nat.succ and nat.pred, or int.succ and int.pred

[Violeta Hernández]

The exceptions here would be ordinals and cardinals where there's not a "nice" way to define the predecessor

[Violeta Hernández]

Not that we don't care about it

[Violeta Hernández]

Something else that I just realized regarding succ' and pred': I imagine that these functions would still satisfy many of the properties of succ and pred, leading to a lot of API duplication

[Violeta Hernández]

So that's another point towards merging

[Violeta Hernández]

If we were to merge succ_order and pred_order, what would the new Prop fields be? I imagine they could be like the current ones but with is_max replaced with is_pred_limit

[Violeta Hernández]

Yeah actually that sounds like a really elegant approach

[Violeta Hernández]

And the nice thing is that is_succ_archimedean implies that all predecessor limits are maximums

[Violeta Hernández]

Here's a small but noteworthy issue with this new approach

[Violeta Hernández]

We can't state is_succ_limit without succ

[Violeta Hernández]

Which means we'd need to spell it out in full in the definition, which means no dot notation

[Violeta Hernández]

Unless we were to make separate has_succ and has_pred typeclasses used for the sole purpose of defining is_succ_limit and is_pred_limit, and being extended by succ_pred_order

[Violeta Hernández]

Actually there's another problem, it's not trivial that you can build a pred_order from a succ_order, you need a bunch of extra results

[Violeta Hernández]

Maybe we could keep succ_order and pred_order, just changing is_max to is_pred_limit, and making succ_pred_order extend both?

[Violeta Hernández]

Then in practice, most results would be stated in terms of this latter typeclass

[Violeta Hernández]

That seems like shoddy design though, since succ_order and pred_order wouldn't be meant to be used

[Yaël Dillies]

It is actually very easy to define is_succ_limit without succ.

def is_succ_limit {α : Type*} [preorder α] (a : α) : Prop := ∀ ⦃b⦄, b < a → ∃ c, b < c ∧ c < a

[Yaël Dillies]

Or, even,

def is_succ_limit {α : Type*} [preorder α] (a : α) : Prop := ∀ b, ¬ b ⋖ a

[Violeta Hernández]

Oh wow

[Violeta Hernández]

Btw, I just realized that maybe we do still want to keep succ_order and pred_order even if we make a new class that combines them

[Violeta Hernández]

Since that way we'd still have succ_order.of_succ_le_iff_of_le_lt_succ and such to help build the successor function without having to build the predecessor one

[Violeta Hernández]

If we switch to this new definition of `is
Yaël Dillies said:

Or, even,

def is_succ_limit {α : Type*} [preorder α] (a : α) : Prop := ∀ b, ¬ b ⋖ a

This approach seems clearly better than the current one. But we'd have to rename is_succ_limit to something else, since we're no longer making explicit reference to the successor.

[Violeta Hernández]

Darn it, a PR is merged and two days later I already need to refactor it :sweat_smile:

[Violeta Hernández]

Maybe is_left_dense and is_right_dense?

[Violeta Hernández]

This seems simple enough to have a name in the literature but I can't find anything by googling

[Yaël Dillies]

I think the names still make sense, because the generalisation I was talking about means that succ and pred could be defined in any linear order (at least).

[Violeta Hernández]

Are you talking about the same generalization as me? i.e. changing is_max to is_pred_limit and viceversa

[Yaël Dillies]

Yes, because then either an element is a pred limit, or there's an element that covers it.

[Violeta Hernández]

Yeah, I can see how every linear order would have a successor and predecessor. They'd essentially boil down to "the next element if it exists, itself otherwise"

[Violeta Hernández]

Well, I support this refactor

[Violeta Hernández]

The only problem is that I don't know how to do this refactor without changing 1k lines of code at once

[Violeta Hernández]

I guess I could start by generalizing is_succ_limit, then what?

[Yaël Dillies]

Oh btw this still makes succ monotone.

[Violeta Hernández]

Ah by the way, your new definition of is_succ_limit isn't equivalent to the old one

[Violeta Hernández]

...in preorders, so who cares :stuck_out_tongue:

[Violeta Hernández]

You could have a < b ⋚ c with succ a = b, succ b = c, succ c = c, so that c is a successor order under the old definition, but not under the new definition

[Violeta Hernández]

Honestly it seems better this new way

[Violeta Hernández]

Namespace stuff

[Violeta Hernández]

I want to move is_succ_limit to the order/cover.lean file, but that file isn't contained in the order namespace

[Violeta Hernández]

Which means is_succ_limit will no longer be in the order namespace by default

[Violeta Hernández]

Should I do something about it?

[Yaël Dillies]

I think this is fine. The reason for succ and pred being in the order namespace is to avoid conflicting with nat.succ.

[Violeta Hernández]

I should note, basically everything about is_succ_limit no longer works on preorders, since we don't have covby.succ_eq

[Violeta Hernández]

Again, not a problem, just noteworthy

[Yaël Dillies]

That's surprising. You don't get succ a = b, but you still have antisymm_rel (≤) (succ a) b so most results should still be true.

[Violeta Hernández]

The problem is that the old is_succ_limit had succ a = b in the definition itself

[Yaël Dillies]

Sure. But your results should still be true if you replace = by antisymm_rel (≤).

[Violeta Hernández]

Oh sure, but then they're no longer very useful

[Violeta Hernández]

Ah, there is another inconvenience with the is_succ_limit refactor

[Violeta Hernández]

Our def-eq abuse no longer works

[Violeta Hernández]

is_succ_limit a is no longer def-eq to is_pred_limit (to_dual a)

[Violeta Hernández]

I guess we could remedy this by defining to_pred_limit as the order-dual of is_succ_limit, though

[Violeta Hernández]

The definition would look weird when unfolded, but just don't do that I guess

[Yaël Dillies]

Simply prove is_succ_order.dual.

[Violeta Hernández]

I did prove it, but since the entire is_pred_limit API consists entirely of def-eq conversions, it means that I now have to change all of that to be done "properly"

[Violeta Hernández]

Or, I could just do this

def is_pred_limit (a : α) : Prop := is_succ_limit (to_dual a)

[Yaël Dillies]

Yeah, this is not proper.

[Violeta Hernández]

Well, time to do things the right way then

[Violeta Hernández]

Oh wait, I see what you mean

[Violeta Hernández]

I don't need to do that much extra work, just use h.dual instead of h for my is_pred_limit hypotheses throughout

[Violeta Hernández]

#15655

[Violeta Hernández]

Here's the PR redefining is_succ_limit

[Violeta Hernández]

As for succ_order and pred_order, here's what I think should be done:

• Redefine succ_order by changing max_of_succ_le to is_pred_limit_of_succ_le.
• Create a new typeclass succ_pred_order extending succ_order and pred_order.
• Make constructors from this new typeclass from either succ_order or pred_order on a partial_order.
• Use succ_order and pred_order only to prove the results necessary to create this constructor, and for auxiliary constructors such as succ_order.of_succ_le_iff_of_le_lt_succ. Use succ_pred_order for everything else.

[Violeta Hernández]

Regarding is_succ_archimedean and is_pred_archimedean, we could either merge them into a single typeclass, or use this same approach of having both structures to prove auxiliary results, and only use the combined structure after that.

[Violeta Hernández]

Though actually, I don't know if the auxiliary constructors for succ_order will be all that useful now that any linear order is a successor order period. nvm they can still be used to give better def-eqs

[Violeta Hernández]

By the way, this reminds me of our situation with docs#complete_semilattice_Sup

[Violeta Hernández]

I guess the difference is that in that case, that typeclass is exactly mathematically identical to docs#complete_lattice, and it's not hard to prove so, while in our case succ_order and succ_pred_order are only almost always mathematically identical, and it takes some API development to prove it

[Violeta Hernández]

And also there's shortcuts to building succ_order while there's not really any shortcuts for complete_semilattice_Sup - it IS the shortcut.

[Violeta Hernández]

I started working on the first part, changing is_max to is_pred_limit

[Violeta Hernández]

I can proudly say, when you change is_max into is_pred_limit, every result about succ-preorders remains true

[Violeta Hernández]

Of course, the results on no_max_order no longer work, period

[Violeta Hernández]

But that's where is_succ_archimedean comes in: in a succ-archimedean order, every predecessor limit is minimal, which means that we can still recover some form of these results

[Violeta Hernández]

This is honestly amazing, for most results you can just replace is_max by is_pred_limit and it just immediately works

[Violeta Hernández]

I'm thinking

[Violeta Hernández]

succ_order isn't really badly behaved on preorders

[Violeta Hernández]

And neither is is_pred_limit

[Violeta Hernández]

For the latter, you can prove a congruence lemma of the form antisymm_rel (≤) a b → (is_pred_limit a ↔ is_pred_limit b)

[Violeta Hernández]

So maybe it's not even worth it to merge succ_order and pred_order

[Violeta Hernández]

Even though we should totally document that on a partial order either instance gives you the other

[Violeta Hernández]

Idea

[Violeta Hernández]

Now that is_pred_limit is part of the definition of a succ_order, surely there's no reason for order/succ_pred/limit.lean to be a separate file?

[Violeta Hernández]

On the other hand, all the stuff about archimedean orders is going to grow a lot in size now that the results that were previously stated for no_max_order and such are moved there, so maybe that should get its own file?

[Violeta Hernández]

https://github.com/leanprover-community/mathlib/tree/succ_pred_refactor_REAL

[Violeta Hernández]

Here's the start of the is_max → is_pred_limit refactor

[Violeta Hernández]

I commented out everything that was nontrivial to fix

[Violeta Hernández]

Wait, I just realized something

[Violeta Hernández]

From the module docstring:

The stricter condition of every element having a sensible successor can be obtained through the combination of succ_order α and no_max_order α.

If we do this refactor, we will no longer have a spelling for this exactly. Is that a problem?

[Violeta Hernández]

Also, now that is_succ_limit has a much simpler and natural definition, maybe we do want a no_succ_limit typeclass? It would be niche, but it would be by far the easiest way to patch up the API

[Violeta Hernández]

That way, we will actually have a spelling for "has a sensible successor function" that doesn't just work on naturals and integers

[Violeta Hernández]

Yeah you know, it would be weird not to automatically have that e.g. the successor function on ordinals is strictly monotone

[Violeta Hernández]

Potential dealbreaker

[Violeta Hernández]

Alright, before I go to sleep, I'll summarize my current plan with this refactor. All comments apply to the respective order duals.

1. Redefine is_succ_limit in terms of the covering relation.
2. Introduce a no_succ_limit typeclass.
3. Generalize succ_order by changing max_of_succ_le to is_pred_order_of_succ_le
4. Prove that a partial succ_order is also a pred_order.
5. Prove that a partial is_succ_archimedean order is also is_pred_archimedean.

[Violeta Hernández]

I just realized

[Violeta Hernández]

With this redefinition, you can actually define a predecessor order from any successor order

[Violeta Hernández]

For a successor limit you define the predecessor as itself, otherwise you define it as some element covered by it

[Violeta Hernández]

It's just that this element is not generally unique in a preorder

[Violeta Hernández]

Yeah you know, I think I'm against merging succ_order + pred_order and is_succ_archimedean + is_pred_archimedean

[Violeta Hernández]

There's little cost in just using the constructors for one from the other