Library hydras.Schutte.CNF

Cantor normal form

Pierre Casteran, Labri and Univ Bordeaux.

From Coq Require Import Arith List Sorting.Sorted
Logic.Epsilon Ensembles.
From hydras Require Export Schutte_basics Ordering_Functions
PartialFun Countable Schutte.Addition AP.
From Coq Require Export Classical.
Import ListNotations.

Set Implicit Arguments.

A Cantor normal form for a countable ordinal alpha is just a sorted list l (in decreasing order) such that alpha is equal to the sum of the terms phi0 beta, for every term beta in l.

Note that, if alpha is greater or equal than epsilon0, the members of l are less or equal than alpha.

For instance, the Cantor Normal Form of epsilon0 is just epsilon0 :: nil.

Definition cnf_t := list Ord.

Fixpoint eval (l : cnf_t) : Ord :=
  match l with
  | nil ⇒ zero
  | beta :: l' ⇒ phi0 beta + eval l'
  end.

Definition sorted (l: cnf_t) :=
  LocallySorted (fun alpha beta ⇒ beta ≤ alpha) l.

Definition is_cnf_of (alpha : Ord)(l : cnf_t) : Prop :=
  sorted l ∧ alpha = eval l.

Definition exponents_lt (alpha: Ord) :=
  Forall (fun beta ⇒ beta < alpha).

Definition exponents_le (alpha : Ord) :=
  Forall (fun beta ⇒ beta ≤ alpha).

Lemma exponents_lt_eval alpha l: exponents_lt alpha l →
                                 eval l < phi0 alpha.

Lemma sorted_tail alpha l: sorted (cons alpha l) → sorted l.

Lemma nf_bounded beta l alpha :
  alpha ≤ phi0 beta → is_cnf_of alpha l →
  exponents_le beta l.

Lemma cnf_of_ap (alpha : Ord) :
  In AP alpha → ∃ l , is_cnf_of alpha l.

Lemma sorted_lt_lt (beta: Ord) : ∀ l alpha,
    sorted (cons alpha l) → alpha < beta →
    eval (cons alpha l) < phi0 beta.

Lemma sorted_lt_lt_2 l alpha :
  sorted (cons alpha l) →
  eval (cons alpha l) < phi0 (succ alpha).

Lemma cnf_head_eq alpha beta ol ol':
  sorted (cons alpha ol) →
  sorted (cons beta ol') →
  eval (cons alpha ol) = eval (cons beta ol') →
  alpha = beta.

Lemma cnf_eq alpha beta ol ol':
  sorted (cons alpha ol) →
  sorted (cons beta ol') →
  eval (cons alpha ol) = eval (cons beta ol') →
  alpha = beta ∧ eval ol = eval ol'.

Lemma cnf_plus1 (ol : cnf_t) :
  sorted ol → ∀ alpha,
    ∃ ol', is_cnf_of (phi0 alpha + eval ol) ol'.

Lemma cnf_plus2 : ∀ ol, sorted ol →
                             ∀ ol', sorted ol' →
                                         ∃ ol'', is_cnf_of (eval ol + eval ol') ol''.

Lemma cnf_plus : ∀ ol alpha,
    is_cnf_of alpha ol → ∀ ol' beta, is_cnf_of beta ol' →
                                           ∃ ol'', is_cnf_of (alpha + beta) ol''.

Every countable ordinal has (at least) a Cantor normal form

(Proof by transfinite induction)

Theorem cnf_exists (alpha : Ord) :
∃ l: cnf_t , is_cnf_of alpha l.
Lemma sorted_lt l alpha: sorted (alpha ::l) →
eval l < phi0 alpha + eval l.

Unicity of cnf

(Proof by induction on lists)

Lemma cnf_unicity l alpha:
is_cnf_of alpha l →
∀ l', is_cnf_of alpha l' → l = l'.

The main result

Theorem cnf_exists_unique (alpha:Ord) :
∃! l: cnf_t , is_cnf_of alpha l.

Cantor Normal Form and the ordinal epsilon0

Lemma cnf_lt_epsilon0 : ∀ l alpha,
    is_cnf_of alpha l →
    alpha < epsilon0 →
    Forall (fun beta ⇒ beta < alpha) l.

The normal form of epsilon0 is just phi0 epsilon0

Lemma cnf_of_epsilon0 : is_cnf_of epsilon0 [epsilon0 ].