Library gaia_hydras.GHydra

From mathcomp Require Import all_ssreflect zify.

From Coq Require Import Logic.Eqdep_dec.
From hydras Require Import DecPreOrder ON_Generic.
From hydras Require Import T1 E0 Hessenberg Hydra_Theorems Hydra_Definitions
     Hydra_Termination Battle_length Hydra_Examples
     Epsilon0_Needed_Free Epsilon0_Needed_Std.
From gaia Require Export ssete9.
Require Import T1Bridge GHessenberg GL_alpha GPrelude.
Set Implicit Arguments.

Import Hydra_Definitions.

Fixpoint m (h:Hydra) : T1 :=
  if h is node (hcons _ _ as hs) then ms hs else zero
with ms (s : Hydrae) : T1 :=
  if s is hcons h s' then phi0 (m h) o+ ms s' else zero.


Lemma m_ref h : g2h (m h) = (Hydra_Termination.m h).

Lemma m_nf h : T1nf (m h).

Lemma mVariant: Hvariant nf_Wf free m .

Theorem every_battle_terminates : Termination.

Definition l_std alpha k := (L_ alpha (S k) - k)%nat.

Lemma l_stdE alpha k : l_std alpha k = Battle_length.l_std (E0_g2h alpha) k.

Definition T1toH (a: T1) : Hydra := O2H.iota (g2h a).

Lemma l_std_ok : ∀ alpha : E0,
    alpha != E0zero →
    ∀ k : nat,
      (1 ≤ k)%N → battle_length standard k (T1toH (cnf alpha))
                                  (l_std alpha k).

Section ImpossibilityProof.
  Context (b: Battle).
  Variable mu:T1.
  Hypothesis nfMu: T1nf mu.
  Variable m : Hydra → T1.
  Let mh (h:Hydra) := g2h (m h).

  Context (Var : Hvariant nf_Wf b m)
           (BVar: BoundedVariant Var mu).

  #[local] Instance hVar : Hvariant T1_wf b mh.

  #[local] Instance bVar : BoundedVariant hVar (g2h mu).

  End ImpossibilityProof.


Lemma Impossibility_free mu m (Var: Hvariant nf_Wf free m):
  ¬ BoundedVariant Var mu.

Lemma Impossibility_std mu m (Var: Hvariant nf_Wf standard m):
  ¬ BoundedVariant Var mu.