Library hydras.Epsilon0.Hprime

A hierarchy of rapidly growing functions

After Hardy, Wainer, Ketonen, Solovay, etc .

Pierre Casteran, LaBRI, University of Bordeaux

Remark

Some notations (mainly names of fast-growing functions) of our development may differ slightly from the litterature. Although this fact does not affect our proofs, we are preparing a future version where the names F_ alpha, f_alpha, H _alpha, etc., are fully consistent with the cited articles. This change will be provisionally made in a branch called Hardy (in reference to the Hardy hierarchy).

From Coq Require Import ArithRing Lia.
From hydras Require Import E0 Canon Paths.
From hydras Require Import Exp2 Iterates Simple_LexProd.
Import RelationClasses Relations.
From hydras Require Import Compat815.
From Equations Require Import Equations.

Open Scope E0_scope.

A variant of the Hardy Wainer hierarchy

#[ global ] Instance Olt : WellFounded E0lt := E0lt_wf.

Equations H'_ (alpha: E0) (i:nat) : nat by wf alpha E0lt :=
  H'_ alpha i with E0_eq_dec alpha E0zero :=
    { | left _zero ⇒ i ;
      | right _nonzero
          with Utils.dec (E0limit alpha) :=
          { | left _limit ⇒ H'_ (Canon alpha (S i)) i ;
            | right _successor ⇒ H'_ (E0_pred alpha) (S i)}}.

Solve All Obligations with auto with E0.

Paraphrases of the equations for H'

Lemma H'_eq1 : ∀ i, H'_ E0zero i = i.

Lemma H'_eq2_0 alpha i :
  E0is_succ alpha →
  H'_ alpha i = H'_ (E0_pred alpha) (S i).

Lemma H'_eq3 alpha i :
  E0limit alpha → H'_ alpha i = H'_ (Canon alpha (S i)) i.

Lemma H'_eq2 alpha i :
  H'_ (E0_succ alpha) i = H'_ alpha (S i).

#[local] Hint Rewrite H'_eq1 H'_eq2 : H'_rw.

Ltac lim_rw alpha := (assert (E0limit alpha) by auto with E0);
                     rewrite (H'_eq3 alpha); auto with E0.

Examples : First steps of the hierarchy

Lemma H'_Fin : ∀ i k : nat, H'_ (E0fin i) k = (i +k)%nat.

Lemma H'_omega : ∀ k, H'_ E0_omega k = S (2 × k)%nat.

Lemma H'_Plus_Fin alpha : ∀ i k : nat,
    H'_ (alpha + i)%e0 k = H'_ alpha (i + k)%nat.

Lemma H'_omega_double k :
  H'_ (E0_omega × 2)%e0 k = (4 × k + 3)%nat.

Lemma H'_omega_3 k : H'_ (E0_omega × 3)%e0 k = (8 × k + 7)%nat.

Lemma H'_omega_4 k : H'_ (E0_omega × 4)%e0 k = (16 × k + 15)%nat.

Lemma H'_omega_i (i:nat) : ∀ k,
    H'_ (E0_omega × i)%e0 k = (exp2 i × k + Nat.pred (exp2 i))%nat.

Let us note that the square of omega can be expressed through the Phi0 function

Remark Phi0_def : E0_phi0 2 = ltac:(mko (T1omega × T1omega)%t1).

Lemma H'_omega_sqr : ∀ k,
H'_ (E0_phi0 2)%e0 k = (exp2 (S k ) × (S k ) - 1)%nat.

Composition lemma

Section H'_cons.
Variable alpha : E0.
Variable i : nat.

Lemma H'_cons : ∀ beta, (beta o < E0_phi0 alpha)%e0 →
                             ∀ k, H'_ (Cons alpha i beta) k =
                                        H'_ (Omega_term alpha i) (H'_ beta k).

Lemma H'_Omega_term_1 : alpha ≠ E0zero → ∀ k,
    H'_ (Omega_term alpha (S i)) k =
    H'_ (Omega_term alpha i) (H'_ (E0_phi0 alpha) k).
End H'_cons.

Lemma H'_Omega_term_0 (alpha : E0) :
alpha ≠ E0zero → ∀ i k,
  H'_ (Omega_term alpha i) k = iterate (H'_ (E0_phi0 alpha)) (S i) k.

Lemma H'_Fin_iterate : ∀ i k,
    H'_ (E0fin (S i)) k = iterate (H'_ (E0fin 1)) (S i) k.

Lemma H'_Omega_term (alpha : E0) :
  ∀ i k,
    H'_ (Omega_term alpha i) k =
    iterate (H'_ (E0_phi0 alpha)) (S i) k.

Definition H'_succ_fun f k := iterate f (S k) k.

Lemma H'_Phi0_succ_1 alpha : alpha ≠ E0zero → ∀ k,
      H'_ (E0_phi0 (E0_succ alpha)) k = H'_succ_fun (H'_ (E0_phi0 alpha)) k.

Lemma H'_Phi0_succ_0 : ∀ k,
    H'_ (E0_phi0 (E0_succ E0zero)) k = H'_succ_fun (H'_ (E0_phi0 E0zero)) k.

Lemma H'_Phi0_succ alpha : ∀ k,
    H'_ (E0_phi0 (E0_succ alpha)) k = H'_succ_fun (H'_ (E0_phi0 alpha)) k.

Lemma H'_Phi0_Si : ∀ i k,
    H'_ (E0_phi0 (S i)) k = iterate H'_succ_fun i (H'_ E0_omega) k.

Lemma H'_omega_cube : ∀ k,
    H'_ (E0_phi0 3)%e0 k = iterate (H'_ (E0_phi0 2)) (S k) k.

Section H'_omega_cube_3.

  Let f k := (exp2 (S k) × (S k ) - 1)%nat.

  Remark R0 k : H'_ (E0_phi0 3)%e0 k = iterate f (S k) k.

   Fact F0 : H'_ (E0_phi0 3) 3 = f (f (f (f 3))).

f (f 3))

  Let N := (exp2 64 × 64 - 1)%nat.

  Remark N_simpl: N = exp2 70 - 1.

  Fact F1 : H'_ (E0_phi0 3) 3 = f (f N).

  Fact F1_simpl :
    H'_ (E0_phi0 3) 3 =
    (exp2 (exp2 (S N) × S N) × (exp2 (S N) × S N ) - 1)%nat.
  Fact F2 : H'_ (E0_phi0 3 + 3) 0 = f (f N).

  Remark f_minoration n p : 0 < n → n ≤ p → exp2 n ≤ f p.

  Fact F3 : (exp2 (exp2 N) ≤ H'_ (E0_phi0 3 + 3) 0).

End H'_omega_cube_3.

Lemma H'_Phi0_omega :
  ∀ k, H'_ (E0_phi0 E0_omega) k =
            iterate H'_succ_fun k (H'_ E0_omega) k.

Lemma H'_Phi0_omega_exact_formula k :
  H'_ (E0_phi0 E0_omega) k =
    let F f i := iterate f (S i) i
    in let g k := S (2 × k)%nat
       in iterate F k g k.

Lemma H'_omega_sqr_min : ∀ k, 0 ≠ k →
                                    (exp2 (S k) ≤ H'_ (E0_phi0 2) k)%nat.

Lemma H'_omega_cube_min k :
  0 ≠ k → (hyper_exp2 (1 + k) ≤ H'_ (E0_phi0 3) k)%nat.

Remark H'_non_mono1 :
  ¬ (∀ alpha beta k,
        (alpha o ≤ beta)%e0 →
        (H'_ alpha k ≤ H'_ beta k)%nat).

Section Proof_of_Abstract_Properties.

  Record P (alpha:E0) : Prop :=
    mkP {
        PA : strict_mono (H'_ alpha);
        PB : alpha ≠ E0zero → ∀ n, (n < H'_ alpha n)%nat;
        PC : H'_ alpha <<= H'_ (E0_succ alpha);
        PD : dominates_from 1 (H'_ (E0_succ alpha)) (H'_ alpha);
        PE : ∀ beta n, Canon_plus n alpha beta →
                            (H'_ beta n ≤ H'_ alpha n)%nat}.

  Section The_induction.

    Lemma PA_Zero : strict_mono (H'_ E0zero).

    Lemma PD_Zero : dominates_from 1 (H'_ (E0_succ E0zero)) (H'_ E0zero).

    #[local] Hint Resolve PD_Zero PA_Zero : E0.

    Lemma PC_Zero : H'_ E0zero <<= H'_ (E0_succ E0zero).

    #[local] Hint Resolve PC_Zero : core.

    Lemma PZero : P E0zero.

    Variable alpha : E0.
    Hypothesis Halpha : ∀ beta, E0lt beta alpha → P beta.

    Section alpha_Succ.
      Variable beta: E0.
      Hypothesis alpha_def : alpha = E0_succ beta.

      Remark PA_Succ : strict_mono (H'_ alpha).

      Remark RB : alpha ≠ E0zero →∀ n, (n < H'_ alpha n)%nat.

      Remark RD : dominates_from 1 (H'_ (E0_succ alpha)) (H'_ alpha).

      Remark RE : ∀ beta n, Canon_plus n alpha beta →
                                 (H'_ beta n ≤ H'_ alpha n)%nat.

      Remark RC : H'_ alpha <<= H'_ (E0_succ alpha).

      Remark RP : P alpha.

    End alpha_Succ.

    Section alpha_limit.
      Hypothesis Hlim : E0limit alpha.

      Remark RBlim : ∀ n, (n < H'_ alpha n)%nat.

      Remark RAlim : strict_mono (H'_ alpha).

      Remark RClim : H'_ alpha <<= H'_ (E0_succ alpha).

      Remark RDlim : dominates_from 1 (H'_ (E0_succ alpha)) (H'_ alpha).

      Remark RElim : ∀ beta n, Canon_plus n alpha beta →
                                    (H'_ beta n ≤ H'_ alpha n)%nat.

    End alpha_limit.

    Lemma P_alpha_0 : P alpha.

  End The_induction.

  Theorem P_alpha : ∀ alpha, P alpha.
End Proof_of_Abstract_Properties.

Section Abstract_Properties.

  Variable alpha : E0.

  Theorem H'_alpha_mono : strict_mono (H'_ alpha).

  Theorem H'_alpha_gt : alpha ≠ E0zero → ∀ n, (n < H'_ alpha n)%nat.

  Theorem H'_alpha_Succ_le : H'_ alpha <<= H'_ (E0_succ alpha).

  Theorem H'_alpha_dom : dominates_from 1 (H'_ (E0_succ alpha)) (H'_ alpha).

H'_ is not mononotonous in alpha in general. Nevertheless, this lemma may help (from KS)

  Theorem H'_restricted_mono_l : ∀ beta n, Canon_plus n alpha beta →
                                                H'_ beta n ≤ H'_ alpha n.

  Lemma H'_alpha_ge_id : id <<= H'_ alpha.

  Lemma H'_alpha_mono_weak : ∀ k l, k ≤ l →
                                         H'_ alpha k ≤ H'_ alpha l.

End Abstract_Properties.

Monotony of H' w.r.t. its first argument

Although Lemma H'_non_mono1 tells us that H' is not monotonous with respect to its argument alpha, we prove that, if alpha<beta, then H'_ alpha k < H'_ beta k for large enough k. For that purpose, we apply a few lemmas from the Ketonen-Solovay article.

Lemma H'_mono_l_0 alpha beta :
  alpha o < beta →
  {n : nat | ∀ p, n ≤ p → H'_ alpha (S p) ≤ H'_ beta (S p)}.

Lemma H'_mono_l_1 alpha beta :
  alpha o ≤ beta →
  {n : nat | ∀ p, n ≤ p → H'_ alpha (S p) ≤ H'_ beta (S p)}.

Section Proof_of_H'_mono_l.

  Variables alpha beta: E0.
  Hypothesis H_alpha_beta: alpha o < beta.

  Section Succ_case.
    Variable gamma: E0.
    Hypothesis Hgamma : beta = E0_succ gamma.

    Remark R1 : alpha o ≤ gamma.

    Remark R2 : {n : nat | ∀ p, n ≤ p → H'_ alpha (S p) ≤ H'_ gamma (S p)}.

    Remark R3 : {n : nat | ∀ p, n ≤ p →
                                    H'_ alpha (S p) < H'_ beta (S p)}.

  End Succ_case.

  Section Limit_case.
    Hypothesis Hbeta: E0limit beta.

    Remark R4 : E0_succ alpha o < beta.

    Remark R5 : {n : nat | ∀ p, n ≤ p →
                                     H'_ alpha (S p) < H'_ beta (S p)}.

  End Limit_case.

  Lemma H'_mono_l : {n : nat | ∀ p, n ≤ p →
                                        H'_ alpha (S p) < H'_ beta (S p)}.

  Theorem H'_dom : dominates_strong (H'_ beta) (H'_ alpha).
End Proof_of_H'_mono_l.

About H'_dom.

Goal
  (0 < H'_ (ltac :(mko (T1omega × T1omega × T1omega )%t1 )) 12)%nat.