Library hydras.Schutte.Correctness_E0
Injection from the set of ordinal terms in Cantor normal form
into the set of Schutte's countable ordinal numbers stricly less than
epsilon0.
Pierre Castéran, Univ. Bordeaux and LaBRI
This is intented to be a validation of main constructions and functions
designed for the type T1.
From hydras Require Import Epsilon0.Epsilon0 ON_Generic.
From hydras Require Import Schutte_basics Schutte.Addition AP CNF.
Import List PartialFun Ensembles.
Fixpoint inject (t:T1) : Ord :=
match t with
| T1.zero ⇒ zero
| T1.cons a n b ⇒ AP._phi0 (inject a) × S n + inject b
end.
Lemma inject_of_finite_pos : ∀ n, inject (\F (S n)) = F (S n).
Theorem inject_of_zero : inject T1.zero = zero.
Theorem inject_of_finite (n : nat):
inject (\F n) = n.
Theorem inject_of_omega :
inject T1omega = Schutte_basics._omega.
Theorem inject_of_phi0 (alpha : T1):
inject (T1.phi0 alpha) = AP._phi0 (inject alpha).
Theorem inject_mono (beta gamma : T1) :
T1.lt beta gamma →
T1.nf beta → T1.nf gamma →
inject beta < inject gamma.
Theorem inject_injective (beta gamma : T1) : nf beta → nf gamma →
inject beta = inject gamma → beta = gamma.
Theorem inject_monoR (beta gamma : T1) :
T1.nf beta → T1.nf gamma →
inject beta < inject gamma →
(beta t1< gamma)%t1.
Theorem inject_lt_epsilon0 (alpha : T1):
inject alpha < epsilon0.
Lemma inject_rw (a b: T1) n : inject (T1.cons a n b) =
mult_Sn (AP._phi0 (inject a)) n + inject b.
Theorem inject_plus (alpha beta : T1):
nf alpha → nf beta →
inject (alpha + beta)%t1 = inject alpha + inject beta.
Theorem inject_mult_fin_r (alpha : T1) :
nf alpha →
∀ n:nat,
inject (alpha × n)%t1 = inject alpha × n.
Lemma inject_lt_epsilon0_ex_cnf (alpha : Ord) :
∀ (H : alpha < epsilon0)
(l: list Ord), is_cnf_of alpha l →
∃ t: T1, nf t ∧ inject t = eval l.
Theorem inject_lt_epsilon0_ex (alpha : Ord) (H : alpha < epsilon0) :
∃ t: T1, nf t ∧ inject t = alpha.
Theorem inject_lt_epsilon0_ex_unique (alpha : Ord) (H : alpha < epsilon0) :
∃! t: T1, nf t ∧ inject t = alpha.
Theorem embedding : fun_bijection (nf: Ensemble T1)
(members epsilon0)
inject.
#[ global ] Instance Epsilon0_correct :
ON_correct epsilon0 Epsilon0 (fun alpha ⇒ inject (cnf alpha)).
Correctness of E0.plus