Library hydras.Hydra.Omega2_Small
Pierre Castéran, University of Bordeaux and LaBRI
From Coq Require Import Arith Peano_dec Lia Relations Relation_Operators.
From hydras Require Import Hydra_Lemmas Simple_LexProd ON_Omega2.
Import ON_Generic.
There is no measure into omega^2 for proving termination
of all hydra battles
Let us assume there is a variant from Hydra into omega^2
for proving the termination of all hydra battles
Variable m : Hydra → rep Omega2.
Context
(Hvar: Hvariant Omega2 free m).
Let big_h := hyd1 (hyd2 head head).
To every pair of natural numbers we associate an hydra
with branches of length 2 and branches of length 1
Let iota (p: ON_Omega2.t) :=
node (hcons_mult (hyd1 head) (fst p)
(hcons_mult head (snd p) hnil)).
Let small_h := iota (m big_h).
#[local] Hint Constructors R1 S1 S2 : hydra.
Lemma m_big_h_not_null : m big_h ≠ zero.
Lemma big_to_small : big_h -+-> small_h.
Corollary m_lt : m small_h o< m big_h.
Proof of the inequality m big_h o≤ m small_h
Let us decompose any inequality p o< q into elementary steps
Inductive step : t → t → Prop :=
| succ_step : ∀ i j, step (i, S j) (i, j)
| limit_step : ∀ i j, step (S i, 0) (i, j).
Lemma succ_rounds : ∀ i j, iota (i,S j) -+-> iota (i, j).
Lemma limit_rounds_0 :
∀ i j, round_n j (iota (S i, 0)) (iota (i, S j)).
Lemma limit_rounds : ∀ i j, iota (S i, 0) -+-> iota (i, j).
#[local] Hint Constructors step clos_trans_1n : hydra.
#[local] Hint Resolve lex_1 lex_2: hydra.
#[local] Hint Unfold lt : hydra.
Lemma step_to_battle : ∀ p q, step p q → iota p -+-> iota q.
#[local] Hint Resolve step_to_battle : hydra.
Lemma m_ge : m big_h o≤ m small_h.
Theorem Impossible : False.
End Impossibility_Proof.