Ordinal technical debt

Stream: mathlib4

[Violeta Hernández]

There's a few weird idiosyncrasies in our treatment of ordinals that are biting us back now that others have tried using that file.

[Violeta Hernández]

One of them is Ordinal.sup. This is totally synonymous with iSup, which has way more lemmas and notation. I imagine the intention was for the former to have its universes constrained so that it always exists (instead of defaulting to 0) but this condition should be imposed on the theorems that require it instead.

[Violeta Hernández]

Another one has to do with Ordinal.bsup. The intention of that definition was to be able to call Ordinal.sup with families that nominally are indexed by a higher universe. But really this isn't needed, all we'd have to do is create some theorem stating that the supremum of families with a small range (like Iio o -> a) are in fact the supremum (larger than all elements of the family, etc.)

[Violeta Hernández]

Getting rid of the ad-hoc notion of BFamilies would go a long way in removing code duplication throughout all these files.

[Violeta Hernández]

Just to be sure: do we all agree on this? Should I attempt to remove Ordinal.sup and Ordinal.bsup in that order?

[Yaël Dillies]

Yes, I agree

[Violeta Hernández]

What should happen to Ordinal.lsub? I've found it decently useful in definitions such as e.g. the rank of a well-founded order, or the natural operations on ordinals, so I don't want to ditch it entirely. Maybe its lemmas should be moved elsewhere? They could be generalized to ConditionallyCompleteLattice + SuccOrder.

[Violeta Hernández]

But doing this would require us to write down the generalizations for CompleteLattice + SuccOrder, and the order dual forms. Are these useful anywhere else?

[Violeta Hernández]

I guess the alternative of just writing down ⨆ i, succ (f i) isn't all too bad

[Violeta Hernández]

Can we keep the name lsub in lemmas though? Just explaining with a note somewhere

[Violeta Hernández]

Another question, for lemmas like this:

example {ι : Type u} (f : ι → Ordinal.{max u v}) : ∀ i, f i ≤ ⨆ i, f i :=
  le_ciSup (bddAbove_range f)

What should the name be? The current name is le_sup. I think it should be changed to le_iSup, or to le_ciSup, making the theorem protected in the latter case.

[Violeta Hernández]

Or actually, should we even have these lemmas that are just lemmas from conditionally complete lattices + bddAbove_range?

[Violeta Hernández]

I don't think the convenience of not writing a few characters outweighs all the API duplication.

[Violeta Hernández]

In fact, there's a few lemmas on ordinals that seem to be missing in the more general case, like Ordinal.lt_sup and Ordinal.ne_sup_iff_lt_sup

[Violeta Hernández]

ciSup_eq_bot_iff also seems to be missing

[Violeta Hernández]

@Yaël Dillies think you could help out with those? You're much more familiar with those files than I am

[Mario Carneiro]

(Don't wait for my approval on this topic, I won't have time to review it)

[Violeta Hernández]

I think I'll simply deprecate these le_sup, etc. lemmas for now. Removing sup and removing all the now redundant lemmas can be two separate refactors

[Eric Wieser]

Probably sup, bsup, and lsub should be done as separate refactors

[Violeta Hernández]

Is there a way to turn off deprecation warnings for a file?

[Eric Wieser]

You can turn them off one lemma at a time with set_option linter.deprecated false in

[Eric Wieser]

Per-file is risky, because then people can add lemmas and not realize the linter isn't running on them

[Violeta Hernández]

Yeah, I'll stick that over Ordinal.lean for now

[Eric Wieser]

If you just want to do it temporarily, put set_option linter.deprecated false at the top

[Violeta Hernández]

My current goal is simply to have Mathlib compile without Ordinal.sup

[Violeta Hernández]

I'm expecting that this alone will require changes across hundreds of lines

[Violeta Hernández]

Cleaning up what's left behind is going to be a separate step

[Violeta Hernández]

On that note, is it ok if I leave a bunch of TODO comments throughout the file?

[Violeta Hernández]

(deleted)

[Yaël Dillies]

Violeta Hernández said:

Can we keep the name lsub in lemmas though? Just explaining with a note somewhere

I personally would never know what it stands for

[Yaël Dillies]

Violeta Hernández said:

I'm expecting that this alone will require changes across hundreds of lines

I don't think ordinals are even used in hundreds of files!

[Yaël Dillies]

Violeta Hernández said:

Yaël Dillies think you could help out with those? You're much more familiar with those files than I am

Sure, but looks like you're faring well already

[Violeta Hernández]

Yaël Dillies said:
I don't think ordinals are even used in hundreds of files!

But the ordinal supremum is definitely used a few hundred times across those files!

[Yaël Dillies]

Sorry, I clearly need to change glasses :nerd:

[Violeta Hernández]

Yeah! The Ordinal.Arithmetic file compiles

[Violeta Hernández]

Hopefully that was the hardest part

[Violeta Hernández]

I made a preliminary PR at #15820, I still got a lot of files to comb through though!

[Violeta Hernández]

Violeta Hernández said:

I think I'll simply deprecate these le_sup, etc. lemmas for now. Removing sup and removing all the now redundant lemmas can be two separate refactors

Actually, I changed my mind on this. The most basic theorems like le_sup and such are useful in this version, so I'll keep those

[Violeta Hernández]

I think it's fine having them be protected lemmas. It's important to be careful when using them, or you'll accidentally needlessly restrict the universes of your result.

[Violeta Hernández]

The good news is that I think this first refactor is done

[Violeta Hernández]

The bad news is that GitHub is down :frown:

[Violeta Hernández]

It builds!

[Violeta Hernández]

Now to appease the linter...

[Violeta Hernández]

Alright, this is ready for review at #15820

[finegeometer]

You've been discussing the fact that Ordinal.sup is equivalent to iSup, but with more restrictive universe levels.
You've argued that restricting the universe levels like this is not useful.

I notice that Ordinal.mex has exactly the same type signature as Ordinal.sup. Should its type signature similarly be relaxed?

[Violeta Hernández]

Ordinal.mexis weird. Ideally I'd want to generalize it to other conditionally complete linear orders so that these API concerns can be delegated, but unfortunately I don't think it's a very useful definition outside of Nim. For that reason, it might be better to just remove it altogether and inline it wherever needed.

[Violeta Hernández]

But if we are to keep it, then yeah, at some point we should do this analogous refactor.

[Violeta Hernández]

Just to clarify, I do think restricting the universe levels in lemmas about sup can be useful. But restricting the universes within the definition itself has caused a lot of needless API pain.

[Yaël Dillies]

Also you don't need to restrict the universe lemmas in lemmas at all: Instead of having ι : Type u, you can have ι : Type* + Small.{u} ι

[Violeta Hernández]

You're right! That's so much more useful

[Violeta Hernández]

That way you don't have to annoyingly cast across equivShrink

[Violeta Hernández]

I don't think I can implement this quite yet, without making the diff like 300 lines larger. But I'll add it in the PR list of future refactors.

[finegeometer]

Violeta Hernández said:

Ordinal.mexis weird. Ideally I'd want to generalize it to other conditionally complete linear orders so that these API concerns can be delegated, but unfortunately I don't think it's a very useful definition outside of Nim. For that reason, it might be better to just remove it altogether and inline it wherever needed.

I'm not even sure it makes sense for general conditionally complete linear orders. Or, at least, the name doesn't. "Mex" stands for "minimum excluded", yet the only reasonable candidate for the mex of (-∞,0] ⊆ ℝ is zero, which isn't "excluded". So while mex makes sense for well-orders, generalizing any farther makes the name "mex" confusing.

I want to say I like your suggestion of removing mex entirely. But I suspect that if it hadn't been there, I'd be asking on this exact forum why it's missing. Maybe it should be deprecated rather than removed, so searching mex in the docs leads to an explanation of why it's not there anymore?

[Violeta Hernández]

It makes sense for ConditionallyCompleteLinearOrderBot. Of which the only relevant instances are ℕ, Cardinal, and Ordinal. But the case for Ordinal basically subsumes the case for ℕ, and I've never come across the Cardinal mex.

[Violeta Hernández]

I'm not sure if I like the idea of simply deprecating it and keeping it there. The "minimum viable API" for even a basic definition like this is decently large. We'd need versions of theorems for both an indexed and a set version of mex, plus helper lemmas in the case where the indexed type is Small. And the only benefit (?) is that we don't have to write sInf sᶜ.

[Violeta Hernández]

That's my same reasoning to removing the much more useful lsub. The cost of maintaining the API outweighs the keystrokes of just writing the definition in full.

[finegeometer]

What's bothering me is that if Ordinal.mex hadn't been there, I would have been confused why it wasn't. So I was looking for a way to make searching mex lead the user to a note that reminds them that they can just use sInf sᶜ. It's not that I want the API to exist; it's that I want the search bar in the docs to point the user in the right direction.

[Violeta Hernández]

If there's a way to do that, then I'm all for it

[Violeta Hernández]

So we wouldn't even make an API then? Just a single deprecated definition

[finegeometer]

That's basically what I was thinking. Is it a sensible thing to do?

[Violeta Hernández]

No idea. But if there's any precedent for this, then we definitely should do it

[Violeta Hernández]

In fact, I think this refactor should be largely orthogonal to the sup refactor

[Violeta Hernández]

I could do it soon-ish

[Violeta Hernández]

finegeometer said:

I notice that Ordinal.mex has exactly the same type signature as Ordinal.sup. Should its type signature similarly be relaxed?

I've been working with nimbers these past few days and I can safely say, we don't need mex

[Violeta Hernández]

sInf sᶜ has worked perfectly for everything. And in fact, I now have an example where mex would be substantially worse than it

[Violeta Hernández]

The definition of the nimber inverse a⁻¹ is as the minimum excluded value in the set S, recursively defined as the least set so that 0 ∈ S and (1 + (a' + a) * b) / a ∈ S for 0 < a' < a and b ∈ S

[Violeta Hernández]

With sInf, it's not hard to get this definition to work:

def inv' (a : Nimber) : Nimber :=
  sInf (⋂₀ {s | 0 ∈ s ∧ ∀ a' < a, a' ≠ 0 → ∀ b ∈ s, (1 + (a + a') * b) * inv' a' ∈ s})ᶜ
termination_by a

[Violeta Hernández]

Now, proving that this is set is nonempty (and thus the infimum isn't just a dummy value) is somewhat difficult, as you need to build a function from a small type that contains these values in its range. But the nice thing is that this is a separate concern from the definition, inv' is already defined by now.

[Violeta Hernández]

With mex, you'd be forced to do these two things at once. I have no idea if that could even be made to work.