Recursion on ordinals

Stream: new members

[Nir Paz]

I want to construct something with transfinite induction, so I want to use induction on the ordinals to define it. I found Ordinal.induction, but

induction' o using Ordinal.induction with o IH

doesn't work when constructing a non-prop term (type mismatch when assigning motive, expected Ordinal → Prop, got Ordinal → Type).

MWE:

import Mathlib

def fasd : Ordinal → ℕ := fun o ↦ by
  induction' o using Ordinal.induction with o IH --type mismatch

Is there an easy way to do this?

[Mario Carneiro]

I think docs#Ordinal.recOn exists?

[Mario Carneiro]

it doesn't, but Ordinal is well founded so you can use the equation compiler to define functions by well founded recursion

[Mario Carneiro]

docs#Ordinal.limitRecOn exists if you want to define the function by cases on zero/succ/limit ordinals

[Nir Paz]

Thanks!

[George Kojonis]

Nir Paz Hi and sorry about that, but would you mind sharing your ordinal recursion solution? I could really use a concrete example (and I am sure other people could too, in the future).

[Nir Paz]

@George Kojonis I'm not in front of a computer, but I'll send it soon!

[Nir Paz]

@George Kojonis apparantly for this project I ended up using recursion on a minimal well order on a type, rather than ordinals directly, and the code is broken now anyways since something changed with simp. I have this simpe example though, defining the aleph function with docs#Ordinal.limitRecOn and proving it's equivalent to the definition in mathlib:

import Mathlib

noncomputable section

open Ordinal Cardinal

def myAleph (o : Ordinal) : Cardinal :=
  Ordinal.limitRecOn o
    (Cardinal.aleph0) -- myAleph 0
    (fun o alepho ↦ Order.succ alepho) -- myAleph (o + 1)
    (fun o oLim ih ↦ sSup {κ : Cardinal | ∃ p plto, ih p plto = κ}) -- myAleph of limit

theorem alpeh_eq : ∀ o, myAleph o = aleph o := fun o ↦
  Ordinal.limitRecOn (C := fun o ↦ myAleph o = aleph o) o
  (by simp [myAleph]) -- proof for o = 0
  (by                 -- proof for o + 1
    intro p ih
    simpa [myAleph])
  (by                 -- proof for limit o
    intro p pLim ih
    simp at ih
    dsimp [myAleph]
    rw [limitRecOn_limit] --using definition of myAleph at limit points
    simp
    rw [aleph_limit pLim]
    congr
    ext x; constructor
    · rintro ⟨q, qltp, hq⟩
      use ⟨q, qltp⟩
      simp
      convert hq
      change aleph q = myAleph q
      exact (ih q qltp).symm
    · rintro ⟨q, hq⟩
      use q
      aesop
    exact pLim)

Basically using docs#Ordinal.limitRecOn to define stuff and then using docs#Ordinal.limitRecOn_zero, docs#Ordinal.limitRecOn_succ and docs#Ordinal.limitRecOn_limit to prove things about them. It can get messy so feel free to ask for help if you want (:

[Nir Paz]

Anyways if you end up doing induction directly on a well order on a type (which is usually best if your function isn't doing set theory stuff) you can use docs#IsWellFounded.fix to define it and docs#IsWellFounded.fix_eq to work with it.

[George Kojonis]

Thanks! This was very helpful!