Library hydras.Hydra.Omega_Small
Pierre Castéran, University of Bordeaux and LaBRI
From Coq Require Import Arith Lia.
From hydras Require Import Hydra_Lemmas ON_Generic ON_Omega.
Open Scope nat_scope.
#[global] Instance height_var : Hvariant Omega free height.
Abort.
Lemma height_bad : ¬ Hvariant Omega free height.
There is no measure into omega for proving termination
of all hydra battles
Let us assume there exists a variant from Hydra into nat
for proving the termination of all hydra battles
Omega is an ordinal notation for the least infinite ordinal
omega, whose members are the natural numbers.
Variable m : Hydra → nat.
Context (Hvar : Hvariant Omega free m).
Let iota (i: nat) := hyd_mult head (S i).
Let big_h := hyd1 (hyd1 head).
Let small_h := iota (m big_h).
Fact big_to_small: ∀ i, battle_rel free i big_h small_h.
#[local] Hint Resolve big_to_small : hydra.
Lemma m_lt : m small_h < m big_h.
In order to find a contradiction, we prove the inequality
m big_h <= m small_h, i.e. m big_h <= m (iota (m h))
For that purpose, we prove the inequality i <= m (iota i) for any i