Library gaia_hydras.GPaths
Gaia-compatible accessibility in epsilon0
(imported from hydras.Epsilon0.Paths)
From mathcomp Require Import all_ssreflect zify.
From hydras Require Import Canon Paths.
From gaia_hydras Require Import T1Bridge GCanon.
From hydras Require Import T1.
From gaia Require Import ssete9.
Import CantorOrdinal.
Importation of Ketonen-Solovay's machinery into gaia's world
(work in progress)
small transition step associated with canonical sequences
#[global] Notation htransition := Epsilon0.Paths.transition.
#[global] Notation hbounded_transitionS := Paths.bounded_transitionS.
Definition transition i (a b: T1) :=
[/\ i != 0 , a!= zero & b == canon a i].
Definition bounded_transitionS n (a b: T1) :=
∃ i, (i ≤ n)%N ∧ transition (S i) a b.
Definition transitionb i (a b: T1) :=
[&& i != 0 , a!= zero & b == canon a i].
Lemma transitionP i a b : reflect (transition i a b )
(transitionb i a b).
TODO : define path_to as a boolean function
#[global] Notation hpath_to := path_to.
#[global] Notation hpath := path.
#[global] Notation hpathS from s to := (path_toS to s from).
#[global] Notation hconst_pathS := const_pathS.
#[global] Notation hconst_path := const_path.
#[global] Notation hgnawS := gnawS.
#[global] Notation hgnaw := gnaw.
#[global] Notation hstandard_gnaw := standard_gnaw.
#[global] Notation hpath := path.
#[global] Notation hpathS from s to := (path_toS to s from).
#[global] Notation hconst_pathS := const_pathS.
#[global] Notation hconst_path := const_path.
#[global] Notation hgnawS := gnawS.
#[global] Notation hgnaw := gnaw.
#[global] Notation hstandard_gnaw := standard_gnaw.
path_to b s alpha : b is accessible from alpha with trace s
Definition path_to (to: T1)(s: seq nat) (from:T1) : Prop :=
hpath_to (g2h to) s (g2h from).
Notation path from s to := (path_to to s from).
Definition acc_from a b := ∃ s, path a s b.
Definition const_path i a b := hconst_path i (g2h a) (g2h b).
Definition standard_path i a j b :=
Paths.standard_path i (g2h a) j (g2h b).
Definition standard_gnaw i a l := h2g (hstandard_gnaw i (g2h a) l).
Definition gnaw a s := h2g (hgnaw (g2h a) s).
Definition gnawS a s := h2g (hgnawS (g2h a) s).
Definition pathS (from: T1)(s: seq nat) (to: T1) : Prop :=
hpathS (g2h from) s (g2h to).
Fixpoint path_tob (b: T1) (s: seq nat) (a:T1): bool :=
match s with
| [::] ⇒ false
| [:: i] ⇒ (i != 0) && transitionb i a b
| i :: s ⇒ (i != 0) && path_tob b s (canon a i)
end.
SSreflect's iota was already defined in Prelude
To simplify
Lemma path_to_inv1 to i from : path_to to [:: i] from →
i ≠ 0 ∧ transition i from to.
Lemma path_to_iff1 to i from :
T1nf from → i ≠ 0 → from ≠ zero →
path_to to [:: i] from ↔ to = canon from i ∧ T1nf from.
Lemma iota_adapt i l: iota i l = MoreLists.iota_from i l.
Lemma standard_gnaw_iota_from i a l :
i ≠ 0 → standard_gnaw i a l = gnaw a (iota i l).
Lemma interval_def i j: MoreLists.interval i j = index_iota i (S j).
Lemma path_to_LT b s a:
path_to b s a → T1nf a → T1nf b → b < a.
Lemma LT_path_to (a b : T1) :
T1nf a → T1nf b → b < a → {s : list nat | path_to b s a}.
Theorem KS_thm_2_4 (lambda : T1) :
T1nf lambda → T1limit lambda →
∀ i j, (i < j)%N →
const_path 1 (canon lambda (S j))
(canon lambda (S i)).
Lemma Cor12 (a: T1) : T1nf a →
∀ b i n, T1nf b → b < a → (i < n)%N →
const_path i.+1 a b → const_path n.+1 a b.
Lemma Lemma2_6_1 (a:T1) :
T1nf a → ∀ b, T1nf b → b < a → {n:nat | const_path n.+1 a b}.
Lemma constant_to_standard_path (a b : T1) (i : nat):
T1nf a → const_path i.+1 a b → zero < a →
{j:nat | standard_path i.+1 a j b}.
Theorem LT_to_standard_path (a b : T1) :
T1nf a → T1nf b → b < a →
{n : nat & {j:nat | standard_path n.+1 a j b}}.
Notation hCanon_plus := Canon_plus.
Definition Canon_plus i a b :=
hCanon_plus i (E0_g2h a) (E0_g2h b).