Library hydras.Hydra.Hydra_Termination

Proof of termination of all hydra battles

Pierre Casteran, Univ. Bordeaux, LaBRI, UMR 5800

From hydras Require Export Hydra_Lemmas.
From hydras Require Import E0 Hessenberg.
Import ON_Generic.

epsilon0

Fixpoint m (h:Hydra) : T1 :=
  match h with head ⇒ T1.zero
             | node hs ⇒ ms hs
end
with ms (s:Hydrae) : T1 :=
  match s with hnil ⇒ T1.zero
              | hcons h s' ⇒ T1.phi0 (m h) o + ms s'
end.

Lemma ms_eqn2 : ∀ h s, ms (hcons h s) = T1.phi0 (m h) o + ms s.

Lemma o_finite_mult_S_rw :
  ∀ n a, o_finite_mult (S n) a = a o + o_finite_mult n a.

The functions m and ms return well formed ordinals (less than epsilon0)

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

Lemma ms_nf : ∀ s, nf (ms s).

#[global] Hint Resolve m_nf nf_phi0 ms_nf : T1.

Lemma ms_eqn3 : ∀ h n s, ms (hcons_mult h n s) =
o_finite_mult n (T1.phi0 (m h)) o + ms s.

Open Scope t1_scope.

Lemma S0_decr_0 :
  ∀ s s', S0 s s' → T1.lt (ms s') (ms s).

Lemma S0_decr:
  ∀ s s', S0 s s' → ms s' t1 < ms s.

Lemma R1_decr_0 : ∀ h h',
                  R1 h h' → T1.lt (m h') (m h).

Lemma R1_decr :
  ∀ h h', R1 h h' → m h' t1 < m h.
Lemma S1_decr_0 n:
  ∀ s s', S1 n s s' → T1.lt (ms s') (ms s).

Lemma S1_decr n:
  ∀ s s', S1 n s s' → ms s' t1 < ms s.

Lemma m_ms : ∀ s, m (node s) = ms s.

Lemma R2_decr_0 n : ∀ h h', R2 n h h' → T1.lt (m h') (m h).

Lemma R2_decr n : ∀ h h', R2 n h h' → m h' t1 < m h.

Lemma round_decr : ∀ h h', h -1-> h' → m h' t1 < m h.

#[ global, program ] Instance var (h:Hydra) : E0:= @mkord (m h) _.

#[global] Instance HVariant_0 : Hvariant T1_wf free m.

#[global] Instance HVariant : Hvariant Epsilon0 free var.

Theorem every_battle_terminates : Termination.