Ordinal notations
constructive ordinal arithmetic for ordinals < ε₀.
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.
Notation for 0
Equations
Equations
- onote.inhabited = {default := 0}
Equations
Equations
Convert a nat into an ordinal
Equations
- onote.of_nat n.succ = 0.oadd n.succ_pnat 0
- onote.of_nat 0 = 0
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.
Equations
- onote.decidable_top_below = id (λ (b o : onote), o.cases_on (id decidable.true) (λ (o_a : onote) (o_a_1 : ℕ+) (o_a_2 : onote), id (ordering.decidable_eq (o_a.cmp b) ordering.lt)))
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
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'
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₂)
- (a.oadd a_1 a_2).sub 0 = a.oadd a_1 a_2
- 0.sub (a.oadd a_1 a_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
Multiplication of ordinal notations (correct only for normal input)
Auxiliary definition to compute the ordinal notation for the ordinal
exponentiation in power
power o₁ o₂ calculates the ordinal notation for
the ordinal exponential o₁ ^ o₂.
Equations
- o₁.power o₂ = onote.power._match_1 o₂ o₁.split
- onote.power._match_1 o₂ (a0.oadd _x _x_1, m) = onote.power._match_3 a0 _x _x_1 m o₂.split
- onote.power._match_1 o₂ (0, m + 1) = onote.power._match_2 m o₂.split'
- onote.power._match_1 o₂ (0, 1) = 1
- onote.power._match_1 o₂ (0, 0) = ite (o₂ = 0) 1 0
- onote.power._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.power_aux a0 ((a0.oadd _x _x_1).mul_nat m) k m
- onote.power._match_3 a0 _x _x_1 m (b, 0) = (a0 * b).oadd 1 0
- onote.power._match_2 m (b', k) = b'.oadd (m.succ_pnat ^ k) 0
Equations
Equations
- nonote.decidable_eq = nonote.decidable_eq._proof_1.mpr (λ (a b : {o // onote.NF o}), subtype.decidable_eq a b)
Equations
- nonote.has_zero = {zero := ⟨0, onote.NF.zero⟩}
Equations
- nonote.inhabited = {default := 0}
Convert a natural number to an ordinal notation
Equations
- nonote.of_nat n = ⟨onote.of_nat n, _⟩
Equations
- nonote.linear_order = {le := preorder.le nonote.preorder, lt := preorder.lt nonote.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := nonote.linear_order._proof_1, le_total := nonote.linear_order._proof_2}
Equations
- nonote.decidable_lt a b = decidable_of_iff (a.cmp b = ordering.lt) _
Equations
- nonote.decidable_linear_order = {le := linear_order.le nonote.linear_order, lt := linear_order.lt nonote.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := λ (a b : nonote), decidable_of_iff (¬b < a) not_lt, decidable_eq := decidable_eq_of_decidable_le (λ (a b : nonote), decidable_of_iff (¬b < a) not_lt), decidable_lt := nonote.decidable_lt}
This is a recursor-like theorem for nonote suggesting an
inductive definition, which can't actually be defined this
way due to conflicting dependencies.