Library hydras.Hydra.O2H
Injection from ordinals (less than epsilon0) in CNF into hydras.
Pierre Castéran, LaBRI and Univ. Bordeaux
We define a function iota : T1 → Hydra such that if alpha < beta, then there exists a battle from iota beta to iota alpha.
Note that iota is not a bijection, but is sufficient for proving
impossibility lemmas or minoration of battle lengths (see Hydra_Theorems).
From Coq Require Import Relation_Operators.
From hydras Require Import Hydra_Lemmas Epsilon0 Canon Paths .
Import Hydra_Definitions.
Let us transform any ordinal term into an hydra
Fixpoint iota (a : T1) : Hydra :=
match a with
| zero ⇒ head
| cons c n b ⇒ node (hcons_mult (iota c) (S n) (iotas b))
end
with iotas (a : T1) : Hydrae :=
match a with
| zero ⇒ hnil
| cons a0 n b ⇒ hcons_mult (iota a0) (S n) (iotas b)
end.
We now prove a lot of technical lemmas that relate Hydras and
ordinals.
Lemma iota_iotas : ∀ alpha, nf alpha →
node (iotas alpha) = iota alpha .
Lemma iotas_succ : ∀ alpha, nf alpha →
iotas (T1.succ alpha) =
hy_app (iotas alpha) (hcons head hnil).
Lemma hy_app_l_nil : ∀ l, hy_app l hnil = l.
Lemma iota_succ_R1 : ∀ o, nf o → R1 (iota (T1.succ o)) (iota o).
Lemma iota_succ_round_n : ∀ i alpha,
nf alpha → round_n i (iota (T1.succ alpha)) (iota alpha).
Lemma iota_succ_round : ∀ o, nf o → iota (T1.succ o) -1-> iota o.
Lemma iota_rw1 :
∀ i alpha, nf alpha → T1limit alpha = true →
iota (canon (cons alpha 0 zero) (S i)) =
hyd1 (iota (canon alpha (S i))).
Lemma iota_rw2 :
∀ i n alpha, nf alpha → T1limit alpha = true →
iota (canon (cons alpha (S n) zero) (S i)) =
node (hcons_mult (iota alpha) (S n)
(hcons
(iota (canon alpha (S i))) hnil)).
Lemma iota_rw3 :
∀ i alpha, nf alpha →
iota (canon (cons (T1.succ alpha) 0 zero) (S i)) =
node (hcons_mult (iota alpha) (S i) hnil).
Lemma iota_rw4 :
∀ i n alpha , nf alpha →
iota (canon (cons (T1.succ alpha) (S n) zero) (S i)) =
node (hcons_mult (iota (T1.succ alpha)) (S n)
(hcons_mult (iota alpha) (S i) hnil)).
Lemma iota_tail :
∀ i alpha n beta,
nf (cons alpha n beta) →
beta ≠ zero →
iota (canon (cons alpha n beta) (S i)) =
node (hcons_mult (iota alpha) (S n) (iotas (canon beta (S i)))).
Lemma R1_hcons : ∀ h s1 s2, R1 (node s1) (node s2) →
R1 (node (hcons h s1)) (node (hcons h s2)).
Lemma R1_hcons_mult : ∀ n h s1 s2,
R1 (node s1) (node s2) →
R1 (node (hcons_mult h n s1))
(node (hcons_mult h n s2)).
Lemma R1_R2 : ∀ h h', R1 h h' → R2 0 (hyd1 h) (hyd1 h').
Inductive mem_head : Hydrae → Prop :=
hh_1 : ∀ s, mem_head (hcons head s)
| hh_2 : ∀ h s, mem_head s → mem_head (hcons h s).
Lemma S0_mem_head : ∀ s s', S0 s s' → mem_head s.
Lemma mem_head_mult_inv : ∀ n h s, mem_head (hcons_mult h n s) →
h = head ∨ mem_head s.
Lemma R1_mem_head : ∀ l l', R1 (node l) (node l') → mem_head l.
Lemma limit_no_head : ∀ alpha, nf alpha → T1limit alpha = true →
¬ mem_head (iotas alpha).
Lemma limit_no_R1 : ∀ alpha, nf alpha →
T1limit alpha = true →
∀ h', ¬ R1 (iota alpha) h'.
Lemma iota_of_succ :
∀ beta, nf beta →
iota (T1.succ beta) =
match (iota beta) with
node s ⇒ node (hy_app s (hcons head hnil))
end.
Lemma canonS_iota_i : ∀ i alpha , nf alpha → alpha ≠ zero →
round_n i (iota alpha) (iota (canon alpha (S i))).
Lemma canonS_iota i a :
nf a → a ≠ 0 → iota a -1-> iota (canon a (S i)).
Lemma canonS_rel_rounds : ∀ n alpha beta,
nf alpha → nf beta →
alpha ≠ zero →
beta = canon alpha (S n) →
iota alpha -+-> iota beta.
Lemma trace_to_round_plus h' : ∀ t h, trace_to h' t h → round_plus h h'.
Import MoreLists.
Lemma trace_to_std i h j h': (i ≤ j)%nat →
trace_to h' (interval i j) h →
rounds standard i h (S j) h'.
Lemma path_toS_trace alpha s beta :
path_toS beta s alpha → nf alpha → trace_to (iota beta) s (iota alpha).
Lemma path_toS_round_plus alpha s beta :
path_toS beta s alpha → nf alpha →
iota alpha -+-> iota beta.
Lemma path_to_round_plus a s b :
path_to b s a → nf a → iota a -+-> iota b.
Lemma acc_from_to_round_plus alpha beta :
nf alpha → nf beta → alpha ≠ 0 →
acc_from alpha beta → iota alpha -+-> iota beta.
Any strict inequality on T1 can be converted into a (free) battle