mathlib3 documentation

set_theory.ordinal.notation

Ordinal notation #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Constructive ordinal arithmetic for ordinals below ε₀.

We define a type onote, with constructors 0 : onote and onote.oadd e n a representing ω ^ e * n + a. We say that o is in Cantor normal form - onote.NF o - if either o = 0 or o = ω ^ e * n + a with a < ω ^ e and a in Cantor normal form.

The type nonote is the type of ordinals below ε₀ in Cantor normal form. Various operations (addition, subtraction, multiplication, power function) are defined on onote and nonote.

inductive onote :

zero : onote
oadd : onote → ℕ+ → onote → onote

Recursive definition of an ordinal notation. zero denotes the ordinal 0, and oadd e n a is intended to refer to ω^e * n + a. For this to be valid Cantor normal form, we must have the exponents decrease to the right, but we can't state this condition until we've defined repr, so it is a separate definition NF.

Instances for onote

@[protected, instance]

def onote.decidable_eq :

decidable_eq onote

@[protected, instance]

def onote.has_zero :

Notation for 0

Equations

onote.has_zero = {zero := onote.zero}

@[simp]

theorem onote.zero_def :

@[protected, instance]

def onote.inhabited :

inhabited onote

Equations

onote.inhabited = {default := 0}

@[protected, instance]

def onote.has_one :

Notation for 1

Equations

onote.has_one = {one := 0.oadd 1 0}

def onote.omega :

Notation for ω

Equations

onote.omega = 1.oadd 1 0

@[simp]

noncomputable def onote.repr :

onote → ordinal

The ordinal denoted by a notation

Equations

(e.oadd n a).repr = ordinal.omega ^ e.repr * ↑n + a.repr
0.repr = 0

def onote.to_string_aux1 (e : onote) (n : ℕ) (s : string) :

Auxiliary definition to print an ordinal notation

Equations

e.to_string_aux1 n s = ite (e = 0) (to_string n) (ite (e = 1) "ω" ("ω^(" ++ s ++ ")") ++ ite (n = 1) "" ("*" ++ to_string n))

def onote.to_string :

onote → string

Print an ordinal notation

Equations

(e.oadd n (ᾰ.oadd ᾰ_1 ᾰ_2)).to_string = e.to_string_aux1 ↑n e.to_string ++ " + " ++ (ᾰ.oadd ᾰ_1 ᾰ_2).to_string
(e.oadd n 0).to_string = e.to_string_aux1 ↑n e.to_string
onote.zero.to_string = "0"

def onote.repr' :

onote → string

Print an ordinal notation

Equations

(e.oadd n a).repr' = "(oadd " ++ e.repr' ++ " " ++ to_string ↑n ++ " " ++ a.repr' ++ ")"
onote.zero.repr' = "0"

@[protected, instance]

def onote.has_to_string :

has_to_string onote

Equations

onote.has_to_string = {to_string := onote.to_string}

@[protected, instance]

def onote.has_repr :

Equations

onote.has_repr = {repr := onote.repr'}

@[protected, instance]

def onote.preorder :

Equations

onote.preorder = {le := λ (x y : onote), x.repr ≤ y.repr, lt := λ (x y : onote), x.repr < y.repr, le_refl := onote.preorder._proof_1, le_trans := onote.preorder._proof_2, lt_iff_le_not_le := onote.preorder._proof_3}

theorem onote.lt_def {x y : onote} :

x < y ↔ x.repr < y.repr

theorem onote.le_def {x y : onote} :

x ≤ y ↔ x.repr ≤ y.repr

@[simp]

def onote.of_nat :

Convert a nat into an ordinal

Equations

onote.of_nat n.succ = 0.oadd n.succ_pnat 0
onote.of_nat 0 = 0

Instances for onote.of_nat

onote.NF_of_nat

@[simp]

theorem onote.of_nat_one :

onote.of_nat 1 = 1

@[simp]

theorem onote.repr_of_nat (n : ℕ) :

(onote.of_nat n).repr = ↑n

@[simp]

theorem onote.repr_one :

1.repr = 1

theorem onote.omega_le_oadd (e : onote) (n : ℕ+) (a : onote) :

ordinal.omega ^ e.repr ≤ (e.oadd n a).repr

theorem onote.oadd_pos (e : onote) (n : ℕ+) (a : onote) :

0 < e.oadd n a

def onote.cmp :

onote → onote → ordering

Compare ordinal notations

Equations

(e₁.oadd n₁ a₁).cmp (e₂.oadd n₂ a₂) = (e₁.cmp e₂).or_else ((cmp ↑n₁ ↑n₂).or_else (a₁.cmp a₂))
(ᾰ.oadd ᾰ_1 ᾰ_2).cmp 0 = ordering.gt
0.cmp (ᾰ.oadd ᾰ_1 ᾰ_2) = ordering.lt
0.cmp 0 = ordering.eq

theorem onote.eq_of_cmp_eq {o₁ o₂ : onote} :

o₁.cmp o₂ = ordering.eq → o₁ = o₂

@[protected]

theorem onote.zero_lt_one :

0 < 1

inductive onote.NF_below :

onote → ordinal → Prop

zero : ∀ {b : ordinal}, 0.NF_below b
oadd' : ∀ {e : onote} {n : ℕ+} {a : onote} {eb b : ordinal}, e.NF_below eb → a.NF_below e.repr → e.repr < b → (e.oadd n a).NF_below b

NF_below o b says that o is a normal form ordinal notation satisfying repr o < ω ^ b.

@[class]

structure onote.NF (o : onote) :

Prop

out : Exists o.NF_below

A normal form ordinal notation has the form

ω ^ a₁ * n₁ + ω ^ a₂ * n₂ + ... ω ^ aₖ * nₖ

where a₁ > a₂ > ... > aₖ and all the aᵢ are also in normal form.

We will essentially only be interested in normal form ordinal notations, but to avoid complicating the algorithms we define everything over general ordinal notations and only prove correctness with normal form as an invariant.

Instances of this typeclass

Instances of other typeclasses for onote.NF

onote.decidable_NF

@[protected, instance]

def onote.NF.zero :

theorem onote.NF_below.oadd {e : onote} {n : ℕ+} {a : onote} {b : ordinal} :

onote.NF e → a.NF_below e.repr → e.repr < b → (e.oadd n a).NF_below b

theorem onote.NF_below.fst {e : onote} {n : ℕ+} {a : onote} {b : ordinal} (h : (e.oadd n a).NF_below b) :

theorem onote.NF.fst {e : onote} {n : ℕ+} {a : onote} :

onote.NF (e.oadd n a) → onote.NF e

theorem onote.NF_below.snd {e : onote} {n : ℕ+} {a : onote} {b : ordinal} (h : (e.oadd n a).NF_below b) :

a.NF_below e.repr

theorem onote.NF.snd' {e : onote} {n : ℕ+} {a : onote} :

onote.NF (e.oadd n a) → a.NF_below e.repr

theorem onote.NF.snd {e : onote} {n : ℕ+} {a : onote} (h : onote.NF (e.oadd n a)) :

theorem onote.NF.oadd {e a : onote} (h₁ : onote.NF e) (n : ℕ+) (h₂ : a.NF_below e.repr) :

onote.NF (e.oadd n a)

@[protected, instance]

def onote.NF.oadd_zero (e : onote) (n : ℕ+) [h : onote.NF e] :

onote.NF (e.oadd n 0)

theorem onote.NF_below.lt {e : onote} {n : ℕ+} {a : onote} {b : ordinal} (h : (e.oadd n a).NF_below b) :

e.repr < b

theorem onote.NF_below_zero {o : onote} :

o.NF_below 0 ↔ o = 0

theorem onote.NF.zero_of_zero {e : onote} {n : ℕ+} {a : onote} (h : onote.NF (e.oadd n a)) (e0 : e = 0) :

a = 0

theorem onote.NF_below.repr_lt {o : onote} {b : ordinal} (h : o.NF_below b) :

o.repr < ordinal.omega ^ b

theorem onote.NF_below.mono {o : onote} {b₁ b₂ : ordinal} (bb : b₁ ≤ b₂) (h : o.NF_below b₁) :

o.NF_below b₂

theorem onote.NF.below_of_lt {e : onote} {n : ℕ+} {a : onote} {b : ordinal} (H : e.repr < b) :

onote.NF (e.oadd n a) → (e.oadd n a).NF_below b

theorem onote.NF.below_of_lt' {o : onote} {b : ordinal} :

o.repr < ordinal.omega ^ b → onote.NF o → o.NF_below b

theorem onote.NF_below_of_nat (n : ℕ) :

(onote.of_nat n).NF_below 1

@[protected, instance]

def onote.NF_of_nat (n : ℕ) :

onote.NF (onote.of_nat n)

@[protected, instance]

def onote.NF_one :

theorem onote.oadd_lt_oadd_1 {e₁ : onote} {n₁ : ℕ+} {o₁ e₂ : onote} {n₂ : ℕ+} {o₂ : onote} (h₁ : onote.NF (e₁.oadd n₁ o₁)) (h : e₁ < e₂) :

e₁.oadd n₁ o₁ < e₂.oadd n₂ o₂

theorem onote.oadd_lt_oadd_2 {e o₁ o₂ : onote} {n₁ n₂ : ℕ+} (h₁ : onote.NF (e.oadd n₁ o₁)) (h : ↑n₁ < ↑n₂) :

e.oadd n₁ o₁ < e.oadd n₂ o₂

theorem onote.oadd_lt_oadd_3 {e : onote} {n : ℕ+} {a₁ a₂ : onote} (h : a₁ < a₂) :

e.oadd n a₁ < e.oadd n a₂

theorem onote.cmp_compares (a b : onote) [onote.NF a] [onote.NF b] :

(a.cmp b).compares a b

theorem onote.repr_inj {a b : onote} [onote.NF a] [onote.NF b] :

a.repr = b.repr ↔ a = b

theorem onote.NF.of_dvd_omega_opow {b : ordinal} {e : onote} {n : ℕ+} {a : onote} (h : onote.NF (e.oadd n a)) (d : ordinal.omega ^ b ∣ (e.oadd n a).repr) :

b ≤ e.repr ∧ ordinal.omega ^ b ∣ a.repr

theorem onote.NF.of_dvd_omega {e : onote} {n : ℕ+} {a : onote} (h : onote.NF (e.oadd n a)) :

ordinal.omega ∣ (e.oadd n a).repr → e.repr ≠ 0 ∧ ordinal.omega ∣ a.repr

def onote.top_below (b : onote) :

top_below b o asserts that the largest exponent in o, if it exists, is less than b. This is an auxiliary definition for decidability of NF.

Equations

b.top_below (e.oadd n a) = (e.cmp b = ordering.lt)
b.top_below 0 = true

Instances for onote.top_below

onote.decidable_top_below

@[protected, instance]

def onote.decidable_top_below :

decidable_rel onote.top_below

Equations

onote.decidable_top_below = id (λ (b o : onote), o.cases_on (id decidable.true) (λ (o_ᾰ : onote) (o_ᾰ_1 : ℕ+) (o_ᾰ_2 : onote), id (ordering.decidable_eq (o_ᾰ.cmp b) ordering.lt)))

theorem onote.NF_below_iff_top_below {b : onote} [onote.NF b] {o : onote} :

o.NF_below b.repr ↔ onote.NF o ∧ b.top_below o

@[protected, instance]

def onote.decidable_NF :

decidable_pred onote.NF

Equations

onote.decidable_NF (e.oadd n a) = decidable_of_iff (onote.NF e ∧ onote.NF a ∧ e.top_below a) _
onote.decidable_NF 0 = decidable.is_true onote.NF.zero

def onote.add :

onote → onote → onote

Addition of ordinal notations (correct only for normal input)

Equations

(e.oadd n a).add o = onote.add._match_1 e n (a.add o)
0.add o = o
onote.add._match_1 e n (e'.oadd n' a') = onote.add._match_2 e n e' n' a' (e.cmp e')
onote.add._match_1 e n 0 = e.oadd n 0
onote.add._match_2 e n e' n' a' ordering.gt = e.oadd n (e'.oadd n' a')
onote.add._match_2 e n e' n' a' ordering.eq = e.oadd (n + n') a'
onote.add._match_2 e n e' n' a' ordering.lt = e'.oadd n' a'

@[protected, instance]

def onote.has_add :

Equations

onote.has_add = {add := onote.add}

@[simp]

theorem onote.zero_add (o : onote) :

0 + o = o

theorem onote.oadd_add (e : onote) (n : ℕ+) (a o : onote) :

e.oadd n a + o = onote.add._match_1 e n (a + o)

def onote.sub :

onote → onote → onote

Subtraction of ordinal notations (correct only for normal input)

Equations

(e₁.oadd n₁ a₁).sub (e₂.oadd n₂ a₂) = onote.sub._match_1 e₁ n₁ a₁ n₂ (a₁.sub a₂) (e₁.cmp e₂)
(ᾰ.oadd ᾰ_1 ᾰ_2).sub 0 = ᾰ.oadd ᾰ_1 ᾰ_2
0.sub (ᾰ.oadd ᾰ_1 ᾰ_2) = 0
0.sub onote.zero = 0
onote.sub._match_1 e₁ n₁ a₁ n₂ _f_1 ordering.gt = e₁.oadd n₁ a₁
onote.sub._match_1 e₁ n₁ a₁ n₂ _f_1 ordering.eq = onote.sub._match_2 e₁ n₁ a₁ n₂ _f_1 (↑n₁ - ↑n₂)
onote.sub._match_1 e₁ n₁ a₁ n₂ _f_1 ordering.lt = 0
onote.sub._match_2 e₁ n₁ a₁ n₂ _f_1 k.succ = e₁.oadd k.succ_pnat a₁
onote.sub._match_2 e₁ n₁ a₁ n₂ _f_1 0 = ite (n₁ = n₂) _f_1 0

@[protected, instance]

def onote.has_sub :

Equations

onote.has_sub = {sub := onote.sub}

theorem onote.add_NF_below {b : ordinal} {o₁ o₂ : onote} :

o₁.NF_below b → o₂.NF_below b → (o₁ + o₂).NF_below b

@[protected, instance]

def onote.add_NF (o₁ o₂ : onote) [onote.NF o₁] [onote.NF o₂] :

onote.NF (o₁ + o₂)

@[simp]

theorem onote.repr_add (o₁ o₂ : onote) [onote.NF o₁] [onote.NF o₂] :

(o₁ + o₂).repr = o₁.repr + o₂.repr

theorem onote.sub_NF_below {o₁ o₂ : onote} {b : ordinal} :

o₁.NF_below b → onote.NF o₂ → (o₁ - o₂).NF_below b

@[protected, instance]

def onote.sub_NF (o₁ o₂ : onote) [onote.NF o₁] [onote.NF o₂] :

onote.NF (o₁ - o₂)

@[simp]

theorem onote.repr_sub (o₁ o₂ : onote) [onote.NF o₁] [onote.NF o₂] :

(o₁ - o₂).repr = o₁.repr - o₂.repr

def onote.mul :

onote → onote → onote

Multiplication of ordinal notations (correct only for normal input)

Equations

(e₁.oadd n₁ a₁).mul (e₂.oadd n₂ a₂) = ite (e₂ = 0) (e₁.oadd (n₁ * n₂) a₁) ((e₁ + e₂).oadd n₂ ((e₁.oadd n₁ a₁).mul a₂))
(ᾰ.oadd ᾰ_1 ᾰ_2).mul 0 = 0
0.mul (ᾰ.oadd ᾰ_1 ᾰ_2) = 0
0.mul onote.zero = 0

@[protected, instance]

def onote.has_mul :

Equations

onote.has_mul = {mul := onote.mul}

@[protected, instance]

def onote.mul_zero_class :

mul_zero_class onote

Equations

onote.mul_zero_class = {mul := has_mul.mul onote.has_mul, zero := 0, zero_mul := onote.mul_zero_class._proof_1, mul_zero := onote.mul_zero_class._proof_2}

theorem onote.oadd_mul (e₁ : onote) (n₁ : ℕ+) (a₁ e₂ : onote) (n₂ : ℕ+) (a₂ : onote) :

e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂ = ite (e₂ = 0) (e₁.oadd (n₁ * n₂) a₁) ((e₁ + e₂).oadd n₂ (e₁.oadd n₁ a₁ * a₂))

theorem onote.oadd_mul_NF_below {e₁ : onote} {n₁ : ℕ+} {a₁ : onote} {b₁ : ordinal} (h₁ : (e₁.oadd n₁ a₁).NF_below b₁) {o₂ : onote} {b₂ : ordinal} :

o₂.NF_below b₂ → (e₁.oadd n₁ a₁ * o₂).NF_below (e₁.repr + b₂)

@[protected, instance]

def onote.mul_NF (o₁ o₂ : onote) [onote.NF o₁] [onote.NF o₂] :

onote.NF (o₁ * o₂)

@[simp]

theorem onote.repr_mul (o₁ o₂ : onote) [onote.NF o₁] [onote.NF o₂] :

(o₁ * o₂).repr = o₁.repr * o₂.repr

def onote.split' :

onote → onote × ℕ

Calculate division and remainder of o mod ω. split' o = (a, n) means o = ω * a + n.

Equations

(e.oadd n a).split' = ite (e = 0) (0, ↑n) (onote.split'._match_1 e n a.split')
0.split' = (0, 0)
onote.split'._match_1 e n (a', m) = ((e - 1).oadd n a', m)

def onote.split :

onote → onote × ℕ

Calculate division and remainder of o mod ω. split o = (a, n) means o = a + n, where ω ∣ a.

Equations

(e.oadd n a).split = ite (e = 0) (0, ↑n) (onote.split._match_1 e n a.split)
0.split = (0, 0)
onote.split._match_1 e n (a', m) = (e.oadd n a', m)

def onote.scale (x : onote) :

onote → onote

scale x o is the ordinal notation for ω ^ x * o.

Equations

x.scale (e.oadd n a) = (x + e).oadd n (x.scale a)
x.scale 0 = 0

Instances for onote.scale

onote.NF_scale

def onote.mul_nat :

onote → ℕ → onote

mul_nat o n is the ordinal notation for o * n.

Equations

(e.oadd n a).mul_nat (m + 1) = e.oadd (n * m.succ_pnat) a
(ᾰ.oadd ᾰ_1 ᾰ_2).mul_nat 0 = 0
0.mul_nat m = 0

Instances for onote.mul_nat

onote.NF_mul_nat

def onote.opow_aux (e a0 a : onote) :

ℕ → ℕ → onote

Auxiliary definition to compute the ordinal notation for the ordinal exponentiation in opow

Equations

e.opow_aux a0 a (k + 1) m = (e + a0.mul_nat k).scale a + e.opow_aux a0 a k m
e.opow_aux a0 a n.succ 0 = 0
e.opow_aux a0 a 0 (m + 1) = e.oadd m.succ_pnat 0
e.opow_aux a0 a 0 0 = 0

Instances for onote.opow_aux

onote.NF_opow_aux

def onote.opow (o₁ o₂ : onote) :

opow o₁ o₂ calculates the ordinal notation for the ordinal exponential o₁ ^ o₂.

Equations

o₁.opow o₂ = onote.opow._match_1 o₂ o₁.split
onote.opow._match_1 o₂ (a0.oadd _x _x_1, m) = onote.opow._match_3 a0 _x _x_1 m o₂.split
onote.opow._match_1 o₂ (0, m + 1) = onote.opow._match_2 m o₂.split'
onote.opow._match_1 o₂ (0, 1) = 1
onote.opow._match_1 o₂ (0, 0) = ite (o₂ = 0) 1 0
onote.opow._match_3 a0 _x _x_1 m (b, k + 1) = let eb : onote := a0 * b in (eb + a0.mul_nat k).scale (a0.oadd _x _x_1) + eb.opow_aux a0 ((a0.oadd _x _x_1).mul_nat m) k m
onote.opow._match_3 a0 _x _x_1 m (b, 0) = (a0 * b).oadd 1 0
onote.opow._match_2 m (b', k) = b'.oadd (m.succ_pnat ^ k) 0

@[protected, instance]

def onote.has_pow :

has_pow onote onote

Equations

onote.has_pow = {pow := onote.opow}

theorem onote.opow_def (o₁ o₂ : onote) :

o₁ ^ o₂ = onote.opow._match_1 o₂ o₁.split

theorem onote.split_eq_scale_split' {o o' : onote} {m : ℕ} [onote.NF o] :

o.split' = (o', m) → o.split = (1.scale o', m)

theorem onote.NF_repr_split' {o o' : onote} {m : ℕ} [onote.NF o] :

o.split' = (o', m) → onote.NF o' ∧ o.repr = ordinal.omega * o'.repr + ↑m

theorem onote.scale_eq_mul (x : onote) [onote.NF x] (o : onote) [onote.NF o] :

x.scale o = x.oadd 1 0 * o

@[protected, instance]

def onote.NF_scale (x : onote) [onote.NF x] (o : onote) [onote.NF o] :

onote.NF (x.scale o)

@[simp]

theorem onote.repr_scale (x : onote) [onote.NF x] (o : onote) [onote.NF o] :

(x.scale o).repr = ordinal.omega ^ x.repr * o.repr

theorem onote.NF_repr_split {o o' : onote} {m : ℕ} [onote.NF o] (h : o.split = (o', m)) :

onote.NF o' ∧ o.repr = o'.repr + ↑m

theorem onote.split_dvd {o o' : onote} {m : ℕ} [onote.NF o] (h : o.split = (o', m)) :

ordinal.omega ∣ o'.repr

theorem onote.split_add_lt {o e : onote} {n : ℕ+} {a : onote} {m : ℕ} [onote.NF o] (h : o.split = (e.oadd n a, m)) :

a.repr + ↑m < ordinal.omega ^ e.repr

@[simp]

theorem onote.mul_nat_eq_mul (n : ℕ) (o : onote) :

o.mul_nat n = o * onote.of_nat n

@[protected, instance]

def onote.NF_mul_nat (o : onote) [onote.NF o] (n : ℕ) :

onote.NF (o.mul_nat n)

@[protected, instance]

def onote.NF_opow_aux (e a0 a : onote) [onote.NF e] [onote.NF a0] [onote.NF a] (k m : ℕ) :

onote.NF (e.opow_aux a0 a k m)

@[protected, instance]

def onote.NF_opow (o₁ o₂ : onote) [onote.NF o₁] [onote.NF o₂] :

onote.NF (o₁ ^ o₂)

theorem onote.scale_opow_aux (e a0 a : onote) [onote.NF e] [onote.NF a0] [onote.NF a] (k m : ℕ) :

(e.opow_aux a0 a k m).repr = ordinal.omega ^ e.repr * (0.opow_aux a0 a k m).repr

theorem onote.repr_opow_aux₁ {e a : onote} [Ne : onote.NF e] [Na : onote.NF a] {a' : ordinal} (e0 : e.repr ≠ 0) (h : a' < ordinal.omega ^ e.repr) (aa : a.repr = a') (n : ℕ+) :

(ordinal.omega ^ e.repr * ↑↑n + a') ^ ordinal.omega = (ordinal.omega ^ e.repr) ^ ordinal.omega

theorem onote.repr_opow_aux₂ {a0 a' : onote} [N0 : onote.NF a0] [Na' : onote.NF a'] (m : ℕ) (d : ordinal.omega ∣ a'.repr) (e0 : a0.repr ≠ 0) (h : a'.repr + ↑m < ordinal.omega ^ a0.repr) (n : ℕ+) (k : ℕ) :

let R : ordinal := (0.opow_aux a0 (a0.oadd n a' * onote.of_nat m) k m).repr in (k ≠ 0 → R < (ordinal.omega ^ a0.repr) ^ order.succ ↑k) ∧ (ordinal.omega ^ a0.repr) ^ ↑k * (ordinal.omega ^ a0.repr * ↑↑n + a'.repr) + R = (ordinal.omega ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ order.succ ↑k

theorem onote.repr_opow (o₁ o₂ : onote) [onote.NF o₁] [onote.NF o₂] :

(o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

def onote.fundamental_sequence :

onote → option onote ⊕ (ℕ → onote)

Given an ordinal, returns inl none for 0, inl (some a) for a+1, and inr f for a limit ordinal a, where f i is a sequence converging to a.

Equations

(a.oadd m b).fundamental_sequence = onote.fundamental_sequence._match_1 a m a.fundamental_sequence b.fundamental_sequence
onote.zero.fundamental_sequence = sum.inl option.none
onote.fundamental_sequence._match_1 a m _f_1 (sum.inr f) = sum.inr (λ (i : ℕ), a.oadd m (f i))
onote.fundamental_sequence._match_1 a m _f_1 (sum.inl (option.some b')) = sum.inl (option.some (a.oadd m b'))
onote.fundamental_sequence._match_1 a m _f_1 (sum.inl option.none) = onote.fundamental_sequence._match_2 a _f_1 m.nat_pred
onote.fundamental_sequence._match_2 a (sum.inr f) (m + 1) = sum.inr (λ (i : ℕ), a.oadd m.succ_pnat ((f i).oadd 1 onote.zero))
onote.fundamental_sequence._match_2 a (sum.inr f) 0 = sum.inr (λ (i : ℕ), (f i).oadd 1 onote.zero)
onote.fundamental_sequence._match_2 a (sum.inl (option.some a')) (m + 1) = sum.inr (λ (i : ℕ), a.oadd m.succ_pnat (a'.oadd i.succ_pnat onote.zero))
onote.fundamental_sequence._match_2 a (sum.inl (option.some a')) 0 = sum.inr (λ (i : ℕ), a'.oadd i.succ_pnat onote.zero)
onote.fundamental_sequence._match_2 a (sum.inl option.none) (m + 1) = sum.inl (option.some (onote.zero.oadd m.succ_pnat onote.zero))
onote.fundamental_sequence._match_2 a (sum.inl option.none) 0 = sum.inl (option.some onote.zero)

def onote.fundamental_sequence_prop (o : onote) :

option onote ⊕ (ℕ → onote) → Prop

The property satisfied by fundamental_sequence o:

inl none means o = 0
inl (some a) means o = succ a
inr f means o is a limit ordinal and f is a strictly increasing sequence which converges to o

Equations

o.fundamental_sequence_prop (sum.inr f) = (o.repr.is_limit ∧ (∀ (i : ℕ), f i < f (i + 1) ∧ f i < o ∧ (onote.NF o → onote.NF (f i))) ∧ ∀ (a : ordinal), a < o.repr → (∃ (i : ℕ), a < (f i).repr))
o.fundamental_sequence_prop (sum.inl (option.some a)) = (o.repr = order.succ a.repr ∧ (onote.NF o → onote.NF a))
o.fundamental_sequence_prop (sum.inl option.none) = (o = 0)

theorem onote.fundamental_sequence_has_prop (o : onote) :

o.fundamental_sequence_prop o.fundamental_sequence

def onote.fast_growing :

onote → ℕ → ℕ

The fast growing hierarchy for ordinal notations < ε₀. This is a sequence of functions ℕ → ℕ indexed by ordinals, with the definition:

f_0(n) = n + 1
f_(α+1)(n) = f_α^[n](n)
f_α(n) = f_(α[n])(n) where α is a limit ordinal and α[i] is the fundamental sequence converging to α

Equations

o.fast_growing = onote.fast_growing._match_1 o (λ (a : onote) (h : o.fundamental_sequence_prop (sum.inl (option.some a))) (this : a < o), a.fast_growing) (λ (f : ℕ → onote) (h : o.fundamental_sequence_prop (sum.inr f)) (i : ℕ) (this : f i < o), (f i).fast_growing i) o.fundamental_sequence _
onote.fast_growing._match_1 o _f_1 _f_2 (sum.inr f) h = λ (i : ℕ), have this : f i < o, from _, _f_2 f h i this
onote.fast_growing._match_1 o _f_1 _f_2 (sum.inl (option.some a)) h = have this : a < o, from _, λ (i : ℕ), _f_1 a h this^[i] i
onote.fast_growing._match_1 o _f_1 _f_2 (sum.inl option.none) _x = nat.succ

theorem onote.fast_growing_def {o : onote} {x : option onote ⊕ (ℕ → onote)} (e : o.fundamental_sequence = x) :

o.fast_growing = onote.fast_growing._match_1 o (λ (a : onote) (_x : o.fundamental_sequence_prop (sum.inl (option.some a))) (_x : a < o), a.fast_growing) (λ (f : ℕ → onote) (_x : o.fundamental_sequence_prop (sum.inr f)) (i : ℕ) (_x : f i < o), (f i).fast_growing i) x _

theorem onote.fast_growing_zero' (o : onote) (h : o.fundamental_sequence = sum.inl option.none) :

o.fast_growing = nat.succ

theorem onote.fast_growing_succ (o : onote) {a : onote} (h : o.fundamental_sequence = sum.inl (option.some a)) :

o.fast_growing = λ (i : ℕ), a.fast_growing ^[i] i

theorem onote.fast_growing_limit (o : onote) {f : ℕ → onote} (h : o.fundamental_sequence = sum.inr f) :

o.fast_growing = λ (i : ℕ), (f i).fast_growing i

@[simp]

theorem onote.fast_growing_zero :

0.fast_growing = nat.succ

@[simp]

theorem onote.fast_growing_one :

1.fast_growing = λ (n : ℕ), 2 * n

@[simp]

theorem onote.fast_growing_two :

2.fast_growing = λ (n : ℕ), 2 ^ n * n

def onote.fast_growing_ε₀ (i : ℕ) :

We can extend the fast growing hierarchy one more step to ε₀ itself, using ω^(ω^...^ω^0) as the fundamental sequence converging to ε₀ (which is not an onote). Extending the fast growing hierarchy beyond this requires a definition of fundamental sequence for larger ordinals.

Equations

onote.fast_growing_ε₀ i = ((λ (a : onote), a.oadd 1 0)^[i] 0).fast_growing i

theorem onote.fast_growing_ε₀_zero :

onote.fast_growing_ε₀ 0 = 1

theorem onote.fast_growing_ε₀_one :

onote.fast_growing_ε₀ 1 = 2

theorem onote.fast_growing_ε₀_two :

onote.fast_growing_ε₀ 2 = 2048

def nonote :

The type of normal ordinal notations. (It would have been nicer to define this right in the inductive type, but NF o requires repr which requires onote, so all these things would have to be defined at once, which messes up the VM representation.)

Equations

nonote = {o // onote.NF o}

Instances for nonote

@[protected, instance]

def nonote.decidable_eq :

decidable_eq nonote

Equations

nonote.decidable_eq = nonote.decidable_eq._proof_1.mpr (λ (a b : {o // onote.NF o}), subtype.decidable_eq a b)

@[protected, instance]

def nonote.NF (o : nonote) :

def nonote.mk (o : onote) [h : onote.NF o] :

Construct a nonote from an ordinal notation (and infer normality)

Equations

nonote.mk o = ⟨o, h⟩

noncomputable def nonote.repr (o : nonote) :

The ordinal represented by an ordinal notation. (This function is noncomputable because ordinal arithmetic is noncomputable. In computational applications nonote can be used exclusively without reference to ordinal, but this function allows for correctness results to be stated.)

Equations

o.repr = o.val.repr

@[protected, instance]

def nonote.has_to_string :

has_to_string nonote

Equations

nonote.has_to_string = {to_string := λ (x : nonote), x.val.to_string}

@[protected, instance]

def nonote.has_repr :

has_repr nonote

Equations

nonote.has_repr = {repr := λ (x : nonote), x.val.repr'}

@[protected, instance]

def nonote.preorder :

preorder nonote

Equations

nonote.preorder = {le := λ (x y : nonote), x.repr ≤ y.repr, lt := λ (x y : nonote), x.repr < y.repr, le_refl := nonote.preorder._proof_1, le_trans := nonote.preorder._proof_2, lt_iff_le_not_le := nonote.preorder._proof_3}

@[protected, instance]

def nonote.has_zero :

has_zero nonote

Equations

nonote.has_zero = {zero := ⟨0, onote.NF.zero⟩}

@[protected, instance]

def nonote.inhabited :

inhabited nonote

Equations

nonote.inhabited = {default := 0}

theorem nonote.lt_wf :

well_founded has_lt.lt

@[protected, instance]

def nonote.well_founded_lt :

well_founded_lt nonote

@[protected, instance]

def nonote.has_well_founded :

has_well_founded nonote

Equations

nonote.has_well_founded = {r := has_lt.lt (preorder.to_has_lt nonote), wf := nonote.lt_wf}

def nonote.of_nat (n : ℕ) :

Convert a natural number to an ordinal notation

Equations

nonote.of_nat n = ⟨onote.of_nat n, _⟩

def nonote.cmp (a b : nonote) :

Compare ordinal notations

Equations

a.cmp b = a.val.cmp b.val

theorem nonote.cmp_compares (a b : nonote) :

(a.cmp b).compares a b

@[protected, instance]

def nonote.linear_order :

linear_order nonote

Equations

nonote.linear_order = linear_order_of_compares nonote.cmp nonote.cmp_compares

@[protected, instance]

def nonote.has_lt.lt.is_well_order :

is_well_order nonote has_lt.lt

def nonote.below (a b : nonote) :

Prop

Asserts that repr a < ω ^ repr b. Used in nonote.rec_on

Equations

a.below b = a.val.NF_below b.repr

def nonote.oadd (e : nonote) (n : ℕ+) (a : nonote) (h : a.below e) :

The oadd pseudo-constructor for nonote

Equations

e.oadd n a h = ⟨e.val.oadd n a.val, _⟩

def nonote.rec_on {C : nonote → Sort u_1} (o : nonote) (H0 : C 0) (H1 : Π (e : nonote) (n : ℕ+) (a : nonote) (h : a.below e), C e → C a → C (e.oadd n a h)) :

C o

This is a recursor-like theorem for nonote suggesting an inductive definition, which can't actually be defined this way due to conflicting dependencies.

Equations

o.rec_on H0 H1 = subtype.cases_on o (λ (o : onote) (h : onote.NF o), onote.rec (λ (h : onote.NF onote.zero), H0) (λ (e : onote) (n : ℕ+) (a : onote) (IHe : Π (h : onote.NF e), C ⟨e, h⟩) (IHa : Π (h : onote.NF a), C ⟨a, h⟩) (h : onote.NF (e.oadd n a)), H1 ⟨e, _⟩ n ⟨a, _⟩ _ (IHe _) (IHa _)) o h)

@[protected, instance]

def nonote.has_add :

Addition of ordinal notations

Equations

nonote.has_add = {add := λ (x y : nonote), nonote.mk (x.val + y.val)}

theorem nonote.repr_add (a b : nonote) :

(a + b).repr = a.repr + b.repr

@[protected, instance]

def nonote.has_sub :

Subtraction of ordinal notations

Equations

nonote.has_sub = {sub := λ (x y : nonote), nonote.mk (x.val - y.val)}

theorem nonote.repr_sub (a b : nonote) :

(a - b).repr = a.repr - b.repr

@[protected, instance]

def nonote.has_mul :

Multiplication of ordinal notations

Equations

nonote.has_mul = {mul := λ (x y : nonote), nonote.mk (x.val * y.val)}

theorem nonote.repr_mul (a b : nonote) :

(a * b).repr = a.repr * b.repr

def nonote.opow (x y : nonote) :

Exponentiation of ordinal notations

Equations

x.opow y = nonote.mk (x.val.opow y.val)

theorem nonote.repr_opow (a b : nonote) :

(a.opow b).repr = a.repr ^ b.repr