Library hydras.Hydra.Hydra_Theorems

Pierre Castéran, Univ. Bordeaux and LaBRI

From hydras Require Import Hydra_Lemmas Epsilon0_Needed_Free
     Epsilon0_Needed_Std Hydra_Termination L_alpha Battle_length Ack.
Import E0 Large_Sets Hprime Paths MoreLists O2H Hydra_Definitions Iterates.
Export Hydra_Definitions.

Liveness

If the hydra is not reduced to one head, then Hercules can chop off some head

Corollary Alive_free : Alive free.
Corollary Alive_standard : Alive standard.

Termination of free battles


Theorem Variant_LT_free_0 : @Hvariant _ _ T1_wf free Hydra_Termination.m.

Theorem Variant_lt_free: @Hvariant _ _ E0lt_wf free Hydra_Termination.var.

Theorem Variant_LT_standard : @Hvariant _ _ T1_wf standard Hydra_Termination.m.

Theorem Variant_lt_standard : @Hvariant _ _ E0lt_wf standard Hydra_Termination.var.


Impossibility theorems

Termination of free battles cannot be proven with a variant from hydras into a segment with
Impossiblity to define a variant bounded by some ordinal less than epsilon0

Check Impossibility_free.

About battle_length_std.

Open Scope nat_scope.


Theorem battle_length_std_Hardy (alpha : E0) :
  alpha ≠ E0zero →
  ∀ k , 1 ≤ k →
             ∃ l: nat,
               H'_ alpha k - k ≤ l ∧
               battle_length standard k (iota (cnf alpha)) l.


Battle length is not PR


From hydras Require Import primRec F_alpha AckNotPR
  PrimRecExamples F_omega.
Import E0.


Section battle_length_notPR.

  Context (H: ∀ alpha, isPR 1 (l_std alpha)).


A counter example


  Let alpha := E0_phi0 E0_omega.
  Let h := iota (cnf alpha).


let us get rid of the substraction ...


  Let m k := L_ alpha (S k).

  Remark m_eqn : ∀ k, m k = (l_std alpha k + k)%nat.

  #[local] Instance mIsPR : isPR 1 m.


  Remark m_ge_F_omega k: F_ E0_omega (S k) ≤ m (S k).
We compare m with the Ackermann function

  Remark m_ge_Ack: ∀ n, 2 ≤ n → Ack (S n) (S n) ≤ m (S n).

  Remark m_dominates_Ack_from_3 : ∀ n, 3 ≤ n → Ack n n ≤ m n.


  Remark m_dominates_Ack :
    dominates (fun n ⇒ S (m n)) (fun n ⇒ Ack.Ack n n).

 Lemma SmNotPR : isPR 1 (fun n ⇒ S (m n)) → False.


  Theorem LNotPR : False.

End battle_length_notPR.

Check l_std_ok.

Check LNotPR.

Search L_ F_.