Library hydras.Hydra.Epsilon0_Needed_Free

Pierre Castéran, LaBRI and University of Bordeaux

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

We generalize the results of libraries Omega_Small and Omega2_Small: We prove that no ordinal strictly less than epsilon0 can be used as a variant for proving the termination of all hydra battles. We use the so-called "Ketonen-Solovay machinery" for building a proof that shares the same structure as for the libraries above, but is much longer

Bounded variants

Open Scope t1_scope.

Section Impossibility_Proof.

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

  Let big_h := big_h mu.
  Let small_h := small_h mu m.

  #[local] Hint Resolve nf_m : hydra.

  Lemma m_ge : m big_h t1 ≤ m small_h.

Proof of the inequality m small_h t1< m big_h

  Lemma m_variant_LT : ∀ h h', h -+-> h' → m h' t1 < m h.

  Lemma big_to_small : big_h -+-> small_h.

  Lemma m_lt : m small_h t1 < m big_h.

  Fact self_lt_free : m big_h t1 < m big_h .

  Theorem Impossibility_free : False.

End Impossibility_Proof.

Check Impossibility_free.