Library hydras.Epsilon0.F_alpha
From hydras Require Import Iterates Simple_LexProd Exp2.
From hydras Require Import E0 Canon Paths primRec Hprime.
Import RelationClasses Relations.
From Coq Require Import ArithRing Lia.
Require Import Compat815.
From Equations Require Import Equations.
From hydras Require Import primRec.
For masking primRec's iterate
Definition call_lt (c c' : E0 × nat) :=
lexico E0lt (Peano.lt) c c'.
Lemma call_lt_wf : well_founded call_lt.
#[ global ] Instance WF : WellFounded call_lt := call_lt_wf.
Equations F_star (c: E0 × nat) (i:nat) : nat by wf c call_lt :=
F_star (alpha, 0) i := i;
F_star (alpha, 1) i
with E0_eq_dec alpha E0zero :=
{ | left _zero ⇒ S i ;
| right _nonzero
with Utils.dec (E0limit alpha) :=
{ | left _limit ⇒ F_star (Canon alpha i,1) i ;
| right _notlimit ⇒
F_star (E0_pred alpha, S i) i}};
F_star (alpha,(S (S n))) i :=
F_star (alpha, 1) (F_star (alpha, (S n)) i).
Definition F_ alpha i := F_star (alpha, 1) i.
Lemma F_star_zero_eqn : ∀ alpha i, F_star (alpha, 0) i = i.
Lemma Fstar_S : ∀ alpha n i, F_star (alpha, S (S n)) i =
F_ alpha (F_star (alpha, S n) i).
Lemma F_eq2 : ∀ alpha i,
E0is_succ alpha →
F_ alpha i = F_star (E0_pred alpha, S i) i.
Lemma F_star_Succ: ∀ alpha n i,
F_star (alpha, S n) i =
F_ alpha (F_star (alpha, n) i).
Lemma F_star_iterate : ∀ alpha n i,
F_star (alpha, n) i = iterate (F_ alpha) n i.
Lemma F_zero_eqn : ∀ i, F_ E0zero i = S i.
Lemma F_lim_eqn : ∀ alpha i,
E0limit alpha →
F_ alpha i = F_ (Canon alpha i) i.
Lemma F_succ_eqn : ∀ alpha i,
F_ (E0_succ alpha) i = iterate (F_ alpha) (S i) i.
Tactic Notation "undiag2" constr(n) integer(occ1) integer(occ2) :=
let n' := fresh "n" in
generalize n at occ1 occ2; intro n'; induction n'.
Lemma LF1 : ∀ i, F_ 1 i = S (2 × i).
Lemma LF2 : ∀ i, exp2 i × i < F_ 2 i.
Corollary LF2' : ∀ i, 1 ≤ i → exp2 i < F_ 2 i.
Lemma F_alpha_0_eq : ∀ alpha: E0, F_ alpha 0 = 1.
Search (Canon ?a _ o< ?a).
Qed.
Properties of F_ alpha
Theorem F_alpha_mono alpha : strict_mono (F_ alpha).
Theorem F_alpha_gt alpha : ∀ n, n < F_ alpha n.
Corollary F_alpha_positive alpha : ∀ n, 0 < F_ alpha n.
Theorem F_alpha_Succ_le alpha : F_ alpha <<= F_ (E0_succ alpha).
Theorem F_alpha_dom alpha :
dominates_from 1 (F_ (E0_succ alpha)) (F_ alpha).
Theorem F_restricted_mono_l alpha :
∀ beta n, Canon_plus n alpha beta →
F_ beta n ≤ F_ alpha n.
#[deprecated(note="use F_alpha_gt")]
Notation F_alpha_ge_S := StrictOrder_Transitive (only parsing).
Lemma LF2_0 : dominates_from 0 (F_ 2) (fun i ⇒ exp2 i × i).
Lemma LF3_2 : dominates_from 2 (F_ 3) (fun n ⇒ iterate exp2 (S n) n).
From Ketonen and Solovay, page 284, op. cit.
Section F_monotony_l.
Variables alpha beta : E0.
Hypothesis H'_beta_alpha : E0lt beta alpha.
Lemma F_mono_l_0 : ∀ n,
Canon_plus (S n) alpha beta →
∀ i, (S n < i → F_ beta i < F_ alpha i)%nat.
Lemma F_mono_l: dominates (F_ alpha) (F_ beta).
End F_monotony_l.
Section H'_F.
Let P (alpha: E0) :=
∀ n, (F_ alpha (S n) ≤ H'_ (E0_phi0 alpha) (S n))%nat.
Variable alpha: E0.
Hypothesis IHalpha : ∀ beta, beta o< alpha → P beta.
Lemma HF0 : P E0zero.
Lemma HFsucc : E0is_succ alpha → P alpha.
The following proof is far from being trivial.
It uses some lemmas from the Ketonen-Solovay machinery
Lemma HFLim : E0limit alpha → P alpha.
End H'_F.
Lemma H'_F alpha : ∀ n, F_ alpha (S n) ≤ H'_ (E0_phi0 alpha) (S n).
Equations f_star (c: E0 × nat) (i:nat) : nat by wf c call_lt :=
f_star (alpha, 0) i := i;
f_star (alpha, 1) i
with E0_eq_dec alpha E0zero :=
{ | left _zero ⇒ S i ;
| right _nonzero
with Utils.dec (E0limit alpha) :=
{ | left _limit ⇒ f_star (Canon alpha i,1) i ;
| right _successor ⇒
f_star (E0_pred alpha, i) i}};
f_star (alpha,(S (S n))) i :=
f_star (alpha, 1) (f_star (alpha, (S n)) i).
Finally, f_ alpha is defined as its first iterate !
Lemma f_star_zero_eqn : ∀ alpha i, f_star (alpha, 0) i = i.
Lemma fstar_S : ∀ alpha n i, f_star (alpha, S (S n)) i =
f_ alpha (f_star (alpha, S n) i).
Lemma f_eq2 : ∀ alpha i,
E0is_succ alpha →
f_ alpha i = f_star (E0_pred alpha, i) i.
Lemma f_star_Succ: ∀ alpha n i,
f_star (alpha, S n) i =
f_ alpha (f_star (alpha, n) i).
Lemma f_star_iterate : ∀ alpha n i,
f_star (alpha, n) i = iterate (f_ alpha) n i.
Lemma f_zero_eqn : ∀ i, f_ E0zero i = S i.
Lemma f_lim_eqn : ∀ alpha i, E0limit alpha →
f_ alpha i = f_ (Canon alpha i) i.
Lemma f_succ_eqn : ∀ alpha i,
f_ (E0_succ alpha) i = iterate (f_ alpha) i i.
Lemma id_le_f_alpha (alpha: E0) : ∀ i, i ≤ f_ alpha i.
Section Properties_of_f_alpha.
Record Q (alpha:E0) : Prop :=
mkQ {
QA : strict_mono (f_ alpha);
QD : dominates_from 2 (f_ (E0_succ alpha)) (f_ alpha);
QE : ∀ beta n, Canon_plus n alpha beta →
f_ beta n ≤ f_ alpha n}.
Section The_induction.
Lemma QA0 : strict_mono (f_ E0zero).
Lemma QD0 : dominates_from 2 (f_ (E0_succ E0zero)) (f_ E0zero).
TODO : Study the equality F alpha i = Nat.pred (f alpha (S i))