Ordinal.inductionOn

Stream: mathlib4

[Violeta Hernández]

A pet peeve of mine is that we currently have docs#Ordinal.inductionOn, which is not induction on ordinals or any variant of it, but rather just a specialized docs#Quotient.inductionOn. Is there anything else we could rename it to?

[Violeta Hernández]

Or maybe we can just remove it? It's pretty much just Quotient.inductionOn + rintro

[Eric Wieser]

We have it because the fact Ordinal is implemented with Quotient is an implementation detail

[Eric Wieser]

It's no different to how WithTop has a separate induction principle to Option, right?

[Violeta Hernández]

Hm, fair enough. Then all we really need is a docstring clarifying this situation.

[Eric Wieser]

It should probably be tagged with induction_eliminator and cases_eliminator

[Violeta Hernández]

Actually, I don't think Ordinal.inductionOn can be justified by analogy to WithTop. The declaration doesn't give you nicer rewriting or anything like that. In fact, it just gives you more variables to introduce.

[Violeta Hernández]

Somewhat confusingly, the file uses Quotient.inductionOn₂ and Quotient.inductionOn₃ all over the place. Trying to write the analogous Ordinal.inductionOn₂ and Ordinal.inductionOn₃ reveals why: it's just much less convenient!

[Violeta Hernández]

Consider this proof within Ordinal.partialOrder

Quotient.inductionOn₃ a b c fun _ _ _ ⟨f⟩ ⟨g⟩ => ⟨f.trans g⟩

versus what would be

Ordinal.inductionOn₃ a b c fun _ _ _ _ _ _ _ _ _ _ ⟨f⟩ ⟨g⟩ => ⟨f.trans g⟩

[Violeta Hernández]

Ordinals being quotients is mostly an implementation detail you can forget about once you've proven all the basic results, so I think it's fine to just remove Ordinal.inductionOn too and rewrite the few theorems that use it using rintro or whatnot.

[Violeta Hernández]

#16185

[Eric Wieser]

Violeta Hernández said:

Actually, I don't think Ordinal.inductionOn can be justified by analogy to WithTop. The declaration doesn't give you nicer rewriting or anything like that. In fact, it just gives you more variables to introduce.

How about docs#Sym2.ind as a comparison?

[Violeta Hernández]

I think the difference between those two is that Sym2.ind is just more widely useful. Once you've proven the basic results on ordinal arithmetic, their definition as a quotient of well-orders just kinda fades in the background.

[Violeta Hernández]

If the only files where you use Ordinal.inductionOn are also using all sorts of other stuff like Quotient.inductionOn₂, Quotient.liftOn, etc, then I don't see reason not to use Quotient.inductionOn too.

[Violeta Hernández]

To clarify, the only files using Ordinal.inductionOn are Ordinal/Basic, the first half of Ordinal/Arithmetic, Cardinal/Cofinality (which also already uses Quotient.inductionOn in a few places), and Cardinal/Ordinal (in a single definition).