Zulip Chat Archive

Stream: maths

Topic: succ_order and pred_order design


Violeta Hernández (Jul 23 2022 at 21:42):

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 (Jul 23 2022 at 21:45):

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 (Jul 23 2022 at 21:47):

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 (Jul 23 2022 at 21:49):

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 (Jul 23 2022 at 21:50):

Think omega on ordinals, or the top in with_top nat

Violeta Hernández (Jul 23 2022 at 21:51):

Now here's the thing

Violeta Hernández (Jul 23 2022 at 21:53):

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 (Jul 23 2022 at 21:53):

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 (Jul 23 2022 at 21:54):

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

Violeta Hernández (Jul 23 2022 at 21:56):

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 (Jul 23 2022 at 21:57):

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

Violeta Hernández (Jul 23 2022 at 21:58):

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 (Jul 23 2022 at 22:01):

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 (Jul 23 2022 at 22:02):

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 (Jul 23 2022 at 22:03):

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 (Jul 23 2022 at 22:04):

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

Violeta Hernández (Jul 23 2022 at 22:05):

So yeah, opinions welcome.

Eric Rodriguez (Jul 23 2022 at 22:09):

we definitely want definitional control of both

Eric Rodriguez (Jul 23 2022 at 22:09):

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

Eric Rodriguez (Jul 23 2022 at 22:09):

like just merge it into one class

Violeta Hernández (Jul 23 2022 at 22:15):

That much is true

Violeta Hernández (Jul 23 2022 at 22:15):

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 (Jul 23 2022 at 22:16):

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 (Jul 23 2022 at 22:17):

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

Violeta Hernández (Jul 23 2022 at 22:17):

Not that we don't care about it

Violeta Hernández (Jul 23 2022 at 22:18):

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 (Jul 23 2022 at 22:19):

So that's another point towards merging

Violeta Hernández (Jul 23 2022 at 22:23):

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 (Jul 23 2022 at 22:27):

Yeah actually that sounds like a really elegant approach

Violeta Hernández (Jul 23 2022 at 22:37):

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

Violeta Hernández (Jul 23 2022 at 23:28):

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

Violeta Hernández (Jul 23 2022 at 23:28):

We can't state is_succ_limit without succ

Violeta Hernández (Jul 23 2022 at 23:29):

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

Violeta Hernández (Jul 23 2022 at 23:29):

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 (Jul 23 2022 at 23:39):

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 (Jul 23 2022 at 23:40):

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 (Jul 23 2022 at 23:40):

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

Violeta Hernández (Jul 23 2022 at 23:40):

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

Yaël Dillies (Jul 23 2022 at 23:40):

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 (Jul 23 2022 at 23:41):

Or, even,

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

Violeta Hernández (Jul 23 2022 at 23:42):

Oh wow

Violeta Hernández (Jul 23 2022 at 23:42):

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 (Jul 23 2022 at 23:43):

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 (Jul 23 2022 at 23:45):

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 (Jul 23 2022 at 23:45):

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

Violeta Hernández (Jul 23 2022 at 23:51):

Maybe is_left_dense and is_right_dense?

Violeta Hernández (Jul 23 2022 at 23:55):

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

Yaël Dillies (Jul 23 2022 at 23:58):

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 (Jul 24 2022 at 00:00):

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

Yaël Dillies (Jul 24 2022 at 00:03):

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

Violeta Hernández (Jul 24 2022 at 00:03):

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 (Jul 24 2022 at 00:04):

Well, I support this refactor

Violeta Hernández (Jul 24 2022 at 00:04):

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 (Jul 24 2022 at 00:04):

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

Yaël Dillies (Jul 24 2022 at 00:16):

Oh btw this still makes succ monotone.

Violeta Hernández (Jul 24 2022 at 00:27):

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

Violeta Hernández (Jul 24 2022 at 00:27):

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

Violeta Hernández (Jul 24 2022 at 00:29):

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 (Jul 24 2022 at 00:29):

Honestly it seems better this new way

Violeta Hernández (Jul 24 2022 at 00:33):

Namespace stuff

Violeta Hernández (Jul 24 2022 at 00:33):

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 (Jul 24 2022 at 00:33):

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

Violeta Hernández (Jul 24 2022 at 00:33):

Should I do something about it?

Yaël Dillies (Jul 24 2022 at 00:34):

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 (Jul 24 2022 at 00:39):

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 (Jul 24 2022 at 00:39):

Again, not a problem, just noteworthy

Yaël Dillies (Jul 24 2022 at 00:41):

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 (Jul 24 2022 at 00:43):

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

Yaël Dillies (Jul 24 2022 at 00:43):

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

Violeta Hernández (Jul 24 2022 at 00:44):

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

Violeta Hernández (Jul 24 2022 at 01:06):

Ah, there is another inconvenience with the is_succ_limit refactor

Violeta Hernández (Jul 24 2022 at 01:06):

Our def-eq abuse no longer works

Violeta Hernández (Jul 24 2022 at 01:06):

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

Violeta Hernández (Jul 24 2022 at 01:07):

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

Violeta Hernández (Jul 24 2022 at 01:07):

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

Yaël Dillies (Jul 24 2022 at 01:08):

Simply prove is_succ_order.dual.

Violeta Hernández (Jul 24 2022 at 01:10):

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 (Jul 24 2022 at 01:11):

Or, I could just do this

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

Yaël Dillies (Jul 24 2022 at 01:11):

Yeah, this is not proper.

Violeta Hernández (Jul 24 2022 at 01:12):

Well, time to do things the right way then

Violeta Hernández (Jul 24 2022 at 01:15):

Oh wait, I see what you mean

Violeta Hernández (Jul 24 2022 at 01:15):

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 (Jul 24 2022 at 01:47):

#15655

Violeta Hernández (Jul 24 2022 at 01:47):

Here's the PR redefining is_succ_limit

Violeta Hernández (Jul 24 2022 at 01:55):

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 (Jul 24 2022 at 01:56):

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 (Jul 24 2022 at 01:57):

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 (Jul 24 2022 at 02:25):

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

Violeta Hernández (Jul 24 2022 at 02:26):

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 (Jul 24 2022 at 02:29):

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 (Jul 24 2022 at 03:36):

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

Violeta Hernández (Jul 24 2022 at 03:36):

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

Violeta Hernández (Jul 24 2022 at 03:37):

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

Violeta Hernández (Jul 24 2022 at 03:39):

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 (Jul 24 2022 at 03:47):

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 (Jul 24 2022 at 04:08):

I'm thinking

Violeta Hernández (Jul 24 2022 at 04:09):

succ_order isn't really badly behaved on preorders

Violeta Hernández (Jul 24 2022 at 04:10):

And neither is is_pred_limit

Violeta Hernández (Jul 24 2022 at 04:11):

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 (Jul 24 2022 at 04:12):

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

Violeta Hernández (Jul 24 2022 at 04:14):

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

Violeta Hernández (Jul 24 2022 at 04:25):

Idea

Violeta Hernández (Jul 24 2022 at 04:26):

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 (Jul 24 2022 at 04:26):

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 (Jul 24 2022 at 05:25):

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

Violeta Hernández (Jul 24 2022 at 05:25):

Here's the start of the is_max → is_pred_limit refactor

Violeta Hernández (Jul 24 2022 at 05:26):

I commented out everything that was nontrivial to fix

Violeta Hernández (Jul 24 2022 at 05:29):

Wait, I just realized something

Violeta Hernández (Jul 24 2022 at 05:31):

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 (Jul 24 2022 at 05:36):

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 (Jul 24 2022 at 05:37):

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 (Jul 24 2022 at 05:39):

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 (Jul 24 2022 at 05:39):

Potential dealbreaker

Violeta Hernández (Jul 24 2022 at 05:53):

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 (Jul 24 2022 at 12:43):

I just realized

Violeta Hernández (Jul 24 2022 at 12:44):

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

Violeta Hernández (Jul 24 2022 at 12:45):

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

Violeta Hernández (Jul 24 2022 at 12:46):

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

Violeta Hernández (Jul 24 2022 at 14:09):

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

Violeta Hernández (Jul 24 2022 at 14:10):

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


Last updated: Dec 20 2023 at 11:08 UTC