Ordinal.succ

Stream: mathlib4

[Kenny Lau]

Why do we not have Ordinal.succ defeq to Order.succ (currently Ordinal.succ does not exist)?

[Aaron Liu]

Are you proposing to add

def Ordinal.succ (o : Ordinal) : Ordinal := Order.succ o

for the dot notation?

[Mario Carneiro]

note that Ordinal.succ used to exist, it was removed with the order refactor

[Kenny Lau]

hmm probably the same reason why we don't want A+B as ideal then

[Aaron Liu]

Why can't you just add one?

[Mario Carneiro]

Addition is not commutative, so you have to be a bit careful there.

[Mario Carneiro]

but I think o + 1 is equal to o.succ

[Aaron Liu]

Yeah, do o + 1 I mean

[Aaron Liu]

1 + o = o for o infinite

[Mario Carneiro]

but I think it's the same as for Nat, succ is in some ways more basic

[Mario Carneiro]

and they aren't defeq

[Kenny Lau]

wait how can o+1 not be defeq to succ o

[Aaron Liu]

Mario Carneiro said:

and they aren't defeq

Don't we have a typeclass for this? It's docs#SuccAddOrder

[Kenny Lau]

oh is succ defined classically?

[Kenny Lau]

wait no succ is an explicit argument there

[Kenny Lau]

instance : SuccOrder Ordinal.{u} :=
  SuccOrder.ofSuccLeIff (fun o => o + 1) succ_le_iff'

[Aaron Liu]

Oh, so it is defeq?

[Kenny Lau]

import Mathlib

universe u

example (o : Ordinal.{u}) : Order.succ o = o + 1 := rfl

[Kenny Lau]

it is defeq!

[Kenny Lau]

brb refactoring all succ lemmas to +1

[Aaron Liu]

maybe make sure we want this first before putting in all the work

[Kenny Lau]

@loogle Ordinal, Order.succ

[loogle]

:search: Ordinal.succ_ne_zero, Cardinal.lt_ord_succ_card, and 165 more

[Aaron Liu]

oh so it's not that much

[Kenny Lau]

Aaron Liu said:

maybe make sure we want this first before putting in all the work

(that was a joke, i don't have the time to refactor 165 lemmas)

[Kevin Buzzard]

You could just get a language model to do it for you, if everything is defeq it would stand a good chance.

[Violeta Hernández]

Hi! Sorry for the late reply. The plan is to turn docs#SuccAddOrder.succ_eq_add_one into a simp lemma, and stop using Order.succ directly in the Ordinal files. I just haven't been able to do this yet.

[Violeta Hernández]

Kenny Lau said:

brb refactoring all succ lemmas to +1

If you do find the time to do this, please go ahead!