Ordinal.pred

Stream: mathlib4

[Violeta Hernández]

I've always been a bit puzzled about what to make of docs#Ordinal.pred. To me it seems like a definition that can obviously be generalized, except that there's no obvious target for generalization, and maybe we don't even need it anyways?

[Violeta Hernández]

To get some obvious ideas out of the way:

• This can't be turned into a docs#PredOrder instance, since it doesn't satisfy min_of_le_pred (pred ω = ω but ¬ IsMin ω)
• In general pred x ≠ x - 1 (e.g. pred (ω + 1) = ω but (ω + 1) - 1 = ω + 1 because ordinal subtraction is right subtraction)

[Violeta Hernández]

Ordinal.pred satisfies a pretty nice property: it forms a Galois connection with Order.succ. That is, pred a ≤ b ↔ a ≤ succ b.

[Violeta Hernández]

And in fact, this property generalizes to the analogous function defined on any linear order without a maximum:

Proof

import Mathlib.Order.SuccPred.Limit

open Order

variable {α} [LinearOrder α] [SuccOrder α]

open Classical in
noncomputable def pred' (x : α) : α :=
  isSuccPrelimitRecOn x (fun a _ ↦ a) (fun a _ ↦ a)

@[simp]
theorem pred'_succ (x : α) [NoMaxOrder α] : pred' (succ x) = x :=
  isSuccPrelimitRecOn_succ ..

theorem pred'_of_isSuccPrelimit {x : α} : IsSuccPrelimit x → pred' x = x :=
  isSuccPrelimitRecOn_of_isSuccPrelimit _ _

theorem pred'_succ_gc [NoMaxOrder α] : GaloisConnection (α := α) pred' succ := by
  intro x y
  obtain ⟨x, rfl⟩ | hx := Order.mem_range_succ_or_isSuccPrelimit x
  · simp
  · rw [pred'_of_isSuccPrelimit hx, hx.le_succ_iff]

[Violeta Hernández]

So this shows (in my opinion) that there's at least some mathematical value in this definition. Perhaps that warrants giving it a proper name and some API?

[Violeta Hernández]

On the other hand, Ordinal.pred is almost completely unused. It only ever appears in the definition of docs#Ordinal.log, where it could easily be inlined or removed.

[Violeta Hernández]

So I'm stuck on what should be done.

[Violeta Hernández]

(if we do want to keep Ordinal.pred, I opened #21751 cleaning up its API)

[Floris van Doorn]

I would not eagerly generalize a rarely used definition, just for the sake of generalization, if you have no application for it (and unifying with Nat.pred is not a good enough reason, since that will be defined in Lean Core anyway). If there are compelling other places we already want it, we could generalize it.

[Violeta Hernández]

I have to agree. I guess the thing that really irks me is that there's no reason for pred not to be defined for other structures like cardinals. But if you actually follow that line of thought there's little reason for it to be defined on ordinals either.