Library hydras.Epsilon0.Canon
Canonical Sequences of ordinals below epsilon0
Pierre Casteran,
LaBRI and University of Bordeaux.
After J. Ketonen and R. Solovay's paper
" Rapidly Growing Ramsey Functions" in
Annals of mathematics, Mar. 1981
From Coq Require Export Arith Lia.
Import Relations Relation_Operators.
From hydras.Prelude Require Import DecPreOrder.
From hydras.Epsilon0 Require Export T1 E0.
Set Implicit Arguments.
Open Scope t1_scope.
Fixpoint canon alpha (i:nat) : T1 :=
match alpha with
| zero ⇒ zero
| cons zero 0 zero ⇒ zero
| cons zero (S k) zero ⇒ FS k
| cons gamma 0 zero ⇒ (match T1.pred gamma with
Some gamma' ⇒
match i with
| 0 ⇒ zero
| S j ⇒ cons gamma' j zero
end
| None ⇒ cons (canon gamma i) 0 zero
end)
| cons gamma (S n) zero ⇒
(match T1.pred gamma with
Some gamma' ⇒
(match i with
0 ⇒ cons gamma n zero
| S j ⇒ cons gamma n (cons gamma' j zero)
end)
| None ⇒ cons gamma n (cons (canon gamma i) 0 zero)
end)
| cons alpha n beta ⇒ cons alpha n (canon beta i)
end.
Section Canon_examples.
#[local] Open Scope ppT1_scope.
Close Scope ppT1_scope.
Goal canon (T1omega ^ T1omega) 10 = phi0 10.
End Canon_examples.
Lemma canon_zero i : canon zero i = zero.
Lemma canon_tail :
∀ alpha n beta i, nf (cons alpha n beta) →
beta ≠ 0 →
canon (cons alpha n beta) i =
cons alpha n (canon beta i).
Lemma canonS_lim1 : ∀ i lambda,
nf lambda → T1limit lambda
→ canon (cons lambda 0 zero) (S i) =
T1.phi0 (canon lambda (S i)).
Lemma canon_lim1 : ∀ i lambda, nf lambda → T1limit lambda
→ canon (cons lambda 0 zero) i =
T1.phi0 (canon lambda i).
Here
Lemma canonS_lim2 i n lambda:
nf lambda → T1limit lambda
→ canon (cons lambda (S n) zero) (S i) =
cons lambda n (T1.phi0 (canon lambda (S i))).
Lemma canon0_lim2 n lambda:
nf lambda → T1limit lambda
→ canon (cons lambda (S n) zero) 0 =
cons lambda n (T1.phi0 (canon lambda 0)).
Lemma canon_lim2 i n lambda :
nf lambda → T1limit lambda
→ canon (cons lambda (S n) zero) i =
cons lambda n (T1.phi0 (canon lambda i)).
Lemma canon_lim3 i n alpha lambda :
nf alpha → nf lambda → T1limit lambda →
canon (cons alpha n lambda) i = cons alpha n (canon lambda i).
Lemma canon_succ i alpha :
nf alpha → canon (succ alpha) i = alpha. Lemma canonS_succ i alpha : nf alpha →
canon (succ alpha) (S i) = alpha.
Lemma canon0_succ alpha : nf alpha → canon (succ alpha) 0 = alpha.
Lemma canonS_phi0_succ_eqn i gamma:
nf gamma →
canon (T1.phi0 (succ gamma)) (S i) = cons gamma i zero.
Lemma canon0_phi0_succ_eqn gamma:
nf gamma →
canon (T1.phi0 (succ gamma)) 0 = zero.
Lemma canonS_cons_succ_eqn2 i n gamma :
nf gamma →
canon (cons (T1.succ gamma) (S n) zero) (S i) =
cons (T1.succ gamma) n (cons gamma i zero).
Lemma canon0_cons_succ_eqn2 n gamma :
nf gamma →
canon (cons (T1.succ gamma) (S n) zero) 0=
cons (T1.succ gamma) n zero.
Lemma canon_SSn_zero (i:nat) :
∀ alpha n ,
nf alpha →
canon (cons alpha (S n) zero) i =
cons alpha n (canon (cons alpha 0 zero) i).
#[deprecated(note="use canon_SSn_zero")]
Notation canonSSn := canon_SSn_zero (only parsing).
Lemma canonS_zero_inv (alpha:T1) (i:nat) :
canon alpha (S i) = zero → alpha = zero ∨ alpha = one.
Lemma canonS_LT i alpha :
nf alpha → alpha ≠ zero →
canon alpha (S i) t1< alpha.
Lemma canon0_LT alpha :
nf alpha → alpha ≠ zero →
canon alpha 0 t1< alpha.
Lemma nf_canon i alpha: nf alpha → nf (canon alpha i).
Lemma canon_LT i alpha : nf alpha → alpha ≠ zero →
canon alpha i t1< alpha.
Lemma canon_lt : ∀ i alpha, nf alpha → alpha ≠ zero →
T1.lt (canon alpha i) alpha.
Lemma canonS_cons_not_zero : ∀ i alpha n beta,
alpha ≠ zero → canon (cons alpha n beta) (S i) ≠ zero.
Lemma canonS_limit_strong lambda :
nf lambda → T1limit lambda →
∀ beta, beta t1< lambda → {i:nat | beta t1< canon lambda (S i)}.
Lemma canon_limit_strong lambda :
nf lambda →
T1limit lambda →
∀ beta, beta t1< lambda →
{i:nat | beta t1< canon lambda i}.
Lemma canonS_limit_lub (lambda : T1) :
nf lambda → T1limit lambda → strict_lub (fun i ⇒ canon lambda( S i)) lambda.
Lemma canon_limit_mono alpha i j : nf alpha → T1limit alpha →
i < j →
canon alpha i t1< canon alpha j.
Lemma canonS_limit_mono alpha i j : nf alpha → T1limit alpha →
i < j →
canon alpha (S i) t1< canon alpha (S j).
Lemma canonS_LE alpha n :
nf alpha → canon alpha (S n) t1≤ canon alpha (S (S n)).
exercise after Guillaume Melquiond
From hydras Require Import Fuel.
Fixpoint approx alpha beta fuel i :=
match fuel with
FO ⇒ None
| Fuel.FS f ⇒
let gamma := canon alpha (S i) in
if decide (lt beta gamma)
then Some (i,gamma)
else approx alpha beta (f tt) (S i)
end.
Lemma approx_ok alpha beta :
∀ fuel i j gamma, approx alpha beta fuel i = Some (j,gamma) →
gamma = canon alpha (S j) ∧ lt beta gamma.
Open Scope E0_scope.
#[program] Definition Canon (alpha:E0)(i:nat): E0 :=
@mkord (@canon (cnf alpha) i) _.
Lemma Canon_Succ beta n: Canon (E0_succ beta) (S n) = beta.
Lemma Canon_Omega k : Canon E0_omega k = E0fin k.
#[global] Hint Rewrite Canon_Omega : E0_rw.
Lemma CanonSSn (i:nat) :
∀ alpha n , alpha ≠ E0zero →
Canon (Cons alpha (S n) E0zero) (S i) =
Cons alpha n (Canon (E0_phi0 alpha) (S i)).
Lemma CanonS_phi0_lim alpha k : E0limit alpha →
Canon (E0_phi0 alpha) (S k) =
E0_phi0 (Canon alpha (S k)).
Lemma CanonS_lt : ∀ i alpha, alpha ≠ E0zero →
Canon alpha (S i) o< alpha.
Lemma Canon_lt : ∀ i alpha, alpha ≠ E0zero → Canon alpha i o< alpha.
Lemma Canon_of_limit_not_null : ∀ i alpha, E0limit alpha →
Canon alpha (S i) ≠ E0zero.
#[global]
Hint Resolve CanonS_lt Canon_lt Canon_of_limit_not_null : E0.
Lemma CanonS_phi0_Succ alpha i : Canon (E0_phi0 (E0_succ alpha)) (S i) =
Omega_term alpha i.