Library hydras.Hydra.Epsilon0_Needed_Generic

Pierre Castéran, LaBRI and University of Bordeaux

Technical definitions and lemmas about variants bounded by some ordinal les than epsilon0

From hydras Require Import Hydra_Lemmas Epsilon0 Canon Paths O2H.
From Coq Require Import Relation_Operators.

Open Scope t1_scope.

Section Bounded.

  Context (B: Battle)
          (mu: T1)
          (Hmu: nf mu)
          (m : Hydra → T1)
          (Var : Hvariant T1_wf B m)
          (Hy : BoundedVariant Var mu).

  Hypothesis m_decrease : ∀ i h h', round_n i h h'→ m h' t1 < m h.

  Lemma nf_m : ∀ h, nf (m h).

  #[local] Hint Resolve Rem0 : hydra.

  Lemma mu_positive : mu ≠ T1.zero.

  Lemma m_ge_0 alpha: nf alpha → alpha t1 ≤ m (iota alpha).

Definition big_h := iota mu.
Definition beta_h := m big_h.
Definition small_h := iota beta_h.

Lemma mu_beta_h : acc_from mu beta_h.

Corollary m_ge_generic : m big_h t1 ≤ m small_h.

End Bounded.