Library gaia_hydras.GL_alpha

From mathcomp Require Import all_ssreflect zify.
From gaia Require Export ssete9.
From Coq Require Import Logic.Eqdep_dec.
From hydras Require Import DecPreOrder.
From hydras Require Import T1 E0.
From hydras Require Paths L_alpha.
From hydras Require Import L_alpha.
From gaia_hydras Require Import T1Bridge GCanon GPaths GHprime.

Set Implicit Arguments.

Definition L_ (alpha:E0) (i:nat): nat :=
 L_alpha.L_ (E0_g2h alpha) i.

Lemma L_zeroE i : L_ E0zero i = i.

Lemma L_eq2 alpha i :
  E0is_succ alpha → L_ alpha i = L_ (E0_pred alpha) (S i).

Lemma L_succE alpha i : L_ (E0_succ alpha) i = L_ alpha i.+1.

Lemma L_limE alpha i :
  E0limit alpha → L_ alpha i = L_ (E0Canon alpha i) (S i).

Lemma L_finite : ∀ i k :nat, L_ (E0fin i) k = (i+k)%nat.

Lemma L_omega : ∀ k, L_ E0_omega k = S (2 × k)%nat.

Lemma L_ge_id alpha : ∀ i, (i ≤ L_ alpha i)%N.

Lemma L_ge_S alpha i:
  alpha ≠ E0zero → (i < L_ alpha i)%N.

Definition L_spec (alpha:T1) (f: nat → nat):=
  Large_Sets.L_spec (g2h alpha) f.

Lemma L_spec0 (f:nat → nat) : L_spec zero f ↔ ∀ k, f k.+1 = k.+1.

Lemma L_spec1 (a:T1) (f:nat → nat) :
  a != zero →
  L_spec a f ↔
    (∀ k,
        Large_Sets.mlarge (g2h a)
                          ( MoreLists.interval (S k)
                                               (Nat.pred (f (S k))))) .

Lemma L_pos_inv a f :
 a != zero → L_spec a f →
                        ∀ k, (S k < f (S k))%N.

Theorem L_correct a : L_spec (cnf a) (L_ a).

Theorem H'_L_ a i: (H'_ a i ≤ L_ a i.+1)%N.