Library gaia_hydras.GCanon
Gaia-compatible canonical sequences
(imported from hydras.Epsilon0.Canon)
From mathcomp Require Import all_ssreflect zify.
From hydras Require Import Canon.
Require Import T1Bridge.
From hydras Require Import T1.
From gaia Require Import ssete9.
Import CantorOrdinal.
Set Implicit Arguments.
Importation of Ketonen-Solovay's machinery into gaia's world
(work in progress)
Note that a lemma Foo may mask Canon.Foo
#[global] Notation hcanon := Epsilon0.Canon.canon.
Definition canon (a: T1) (i:nat) : T1 := h2g (hcanon (g2h a) i).
Notation canonS a := (fun i ⇒ canon a (S i)).
Example ex0: canon (phi0 T1omega) 6 == phi0 (\F 6).
Example ex1: canonS (phi0 T1omega) 6 == phi0 (\F 7).
rewriting lemmas
Lemma gcanon_zero i: canon zero i = zero.
Lemma g2h_canon a i: g2h (canon a i) = hcanon (g2h a) i.
Lemma canon_succ i a (Ha: T1nf a):
canon (T1succ a) i = a.
Lemma canonS_LE a n: T1nf a → canon a n.+1 ≤ canon a n.+2.
Lemma canon0_phi0_succE a:
T1nf a → canon (phi0 (T1succ a)) 0 = zero.
Lemma canon0_lt a:
T1nf a → a ≠ zero → T1lt (canon a 0) a.
Lemma canonS_lt (i : nat) [a : T1]:
T1nf a → a ≠ zero → T1lt (canon a i.+1) a.
Lemma canon_lt (i : nat) [a : T1]: T1nf a → a ≠ zero → canon a i < a.
Lemma canonS_cons_not_zero (i : nat) (a : T1) (n : nat) (b : T1):
a ≠ zero → canon (cons a n b) i.+1 ≠ zero.
Lemma limit_canonS_not_zero i lambda:
T1nf lambda → T1limit lambda → canon lambda i.+1 ≠ zero.
Lemma canonS_phi0_succE (i : nat) (gamma : T1):
T1nf gamma → canon (phi0 (T1succ gamma)) i.+1 = cons gamma i zero.
Lemma canon_SSn_zero (i : nat) (a : T1) (n : nat):
T1nf a →
canon (cons a n.+1 zero) i = cons a n (canon (phi0 a) i).
Lemma canonS_zero_inv (a : T1) (i : nat):
canon a i.+1 = zero → a = zero ∨ a = one.
Lemma canon_lim1 i (lambda: T1) :
T1nf lambda →
T1limit lambda → canon (phi0 lambda) i = phi0 (canon lambda i).
Lemma canon_tail a (n : nat) b (i : nat):
T1nf (cons a n b) →
b ≠ zero → canon (cons a n b) i = cons a n (canon b i).
Lemma canonS_ocons_succE i n (gamma: T1)(Hnf : T1nf gamma) :
canon (cons (T1succ gamma) n.+1 zero) i.+1 =
cons (T1succ gamma) n (cons gamma i zero).
Lemma canon_lim2 i n (lambda : T1) (Hnf: T1nf lambda) (Hlim: T1limit lambda):
canon (cons lambda n.+1 zero) i = cons lambda n (phi0 (canon lambda i)).
Lemma canon_lim3 i n a lambda (Ha: T1nf a)
(Hlambda: T1nf lambda) (Hlim :T1limit lambda) :
canon (cons a n lambda) i = cons a n (canon lambda i).
Lemma canon_limit_strong lambda :
T1nf lambda → T1limit lambda →
∀ b, T1nf b →
T1lt b lambda → {i : nat | b < canon lambda i}.
Lemma T1nf_canon a i : T1nf a → T1nf (canon a i).
Lemma gcanon_limit_v2 (lambda: T1):
T1nf lambda → T1limit lambda → limit_v2 (canon lambda) lambda.
Lemma canon_limit_mono lambda i j (Hnf : T1nf lambda)
(Hlim : T1limit lambda) (Hij : (i < j)%N) :
canon lambda i < canon lambda j.
Lemma canon_limit_of lambda (Hnf : T1nf lambda) (Hlim : T1limit lambda) :
limit_of (canon lambda) lambda.