Library hydras.Epsilon0.L_alpha
Computing the length of paths from alpha to zero
From hydras Require Import Hprime E0 Canon Paths
Large_Sets.
From hydras Require Import Simple_LexProd Iterates .
From Coq Require Import ArithRing Lia.
From Equations Require Import Equations.
Import RelationClasses Relations.
#[global] Instance Olt : WellFounded E0lt := E0lt_wf.
#[global] Hint Resolve Olt : E0.
Using Coq-Equations for building a function which satisfies
Large_sets.L_spec
Equations L_ (alpha: E0) (i:nat) : nat by wf alpha E0lt :=
L_ alpha i with E0_eq_dec alpha E0zero :=
{ | left _zero ⇒ i ;
| right _nonzero
with Utils.dec (E0limit alpha) :=
{ | left _limit ⇒ L_ (Canon alpha i) (S i) ;
| right _successor ⇒ L_ (E0_pred alpha) (S i)}}.
Solve All Obligations with auto with E0.
About L__equation_1.
Paraphrase of equations generated by coq-equations
Lemma L_zero_eqn : ∀ i, L_ E0zero i = i.
Lemma L_eq2 alpha i :
E0is_succ alpha → L_ alpha i = L_ (E0_pred alpha) (S i).
Lemma L_succ_eqn alpha i :
L_ (E0_succ alpha) i = L_ alpha (S i).
#[export] Hint Rewrite L_zero_eqn L_succ_eqn : L_rw.
Lemma L_lim_eqn alpha i :
E0limit alpha →
L_ alpha i = L_ (Canon alpha i) (S i).
Lemma L_finite : ∀ i k :nat, L_ 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.
Lemma L_ge_S alpha :
alpha ≠ E0zero → S <<= L_ alpha.
Lemma L_succ_ok beta f :
nf beta → S <<= f → L_spec beta f →
L_spec (succ beta) (fun k ⇒ f (S k)).
L_ is correct w.r.t. its specification
Section L_correct_proof.
Let P alpha := L_spec (cnf alpha) (L_ alpha).
Lemma L_ok0 : P E0zero.
Lemma L_ok_succ beta : P beta → P (E0_succ beta).
Lemma L_ok_lim alpha :
(∀ beta, (beta o< alpha)%e0 → P beta) →
E0limit alpha → P alpha.
Lemma L_ok (alpha: E0) : P alpha.
End L_correct_proof.
Theorem L_correct alpha : L_spec (cnf alpha) (L_ alpha).
Comparison with Hardy's function H