Cantor Normal Form

Stream: mathlib4

[Violeta Hernández]

I did a complete rewrite of docs#NONote in my own ordinal notations repository about a year ago. I kind of left it at that since I figured no one would want to review a rewrite this big, but I just came across #27187 by @Miyahara Kō.

[Violeta Hernández]

I'm wondering, should I PR this to Mathlib? The file gets rewritten completely and (in my opinion) improved in a bunch of ways. Copying from the docstring:

• ONote is renamed to PreCantor and NONote is renamed to Cantor.
• The Preorder instance is no longer defined in terms of repr, thus making it computable.
• NFBelow is disposed of, and NF is no longer a typeclass.

• The definition of opow is heavily simplified, avoiding multiple auxiliary definitions and
  instead relying only on natOpow.

• Most proofs are golfed substantially by relying on new lemmas for ordinal arithmetic (in
  particular, I got rid of those hideous simp only says).

[Violeta Hernández]

(In retrospective maybe NF should stay as a typeclass, but everything else is to me an improvement)

[Violeta Hernández]

I can try to tweak my code to make it a bit closer to what's in Mathlib currently, but I don't think there's a way to do my refactor without either temporarily removing a lot of the functionality from ONOte and PRing it back gradually, or doing a huge 1000-line PR at once.

[Miyahara Kō]

I took a look at your repository and it seems you have a library for Veblen ordinal notation. Since this is a strict superset of Cantor's ordinal notation, and because ordinal notation can be very useful—especially for things like an ordinal version of the norm_num tactic as the notations grow—I'd suggest replacing the current NONote with your Veblen ordinal notation rather than the Cantor one.
I'm not an reviewer, but I’ve made over 300 PRs so far, and non-reviewer feedback is welcome, so I’ll be happy to review it!

[Violeta Hernández]

My Veblen ordinal notation is incomplete, unfortunately. I was trying to create a more general framework for ordinal notations, noting that most of them have the form of an inductive lists of lists, but I never really completed that project.

[Violeta Hernández]

In truth I think the ideal scenario would be to have multiple ordinal notations for multiple uses. Veblen's ordinal notation is far from the most general one; there's Veblen's Klammersymbolen, there's Buchholz's notation, and a lot of more esoteric stuff.

[Violeta Hernández]

Maybe it's best to have all of them available rather than just trying to do the single most powerful one

[Miyahara Kō]

I see. In any case, a PR refactoring Cantor's ordinal notation is very welcome!

[Violeta Hernández]

I'll assemble the PR. I'll see if there's a way to minimize it.