Library hydras.Hydra.Hydra_Lemmas
Pierre Casteran
LaBRI, Université de Bordeaux
From Coq Require Import Arith Lia List Relation_Operators
Operators_Properties Peano_dec Wellfounded.Inverse_Image
Wellfounded.Inclusion.
From hydras Require Import More_Arith Epsilon0 Hessenberg
Simple_LexProd MoreLibHyps.
From hydras Require Export Hydra_Definitions.
Import Relations.
Open Scope nat_scope.
Lemma add_r_0 : ∀ h: Hydra, add_r h 0 = h.
Lemma hy_app_assoc :
∀ (s1 s2 s3 : Hydrae) ,
hy_app s1 (hy_app s2 s3) = hy_app (hy_app s1 s2) s3.
Lemma hcons_mult_app : ∀ (h: Hydra) (n :nat) (s s': Hydrae),
hcons_mult h n (hy_app s s') =
hy_app (hcons_mult h n s) s'.
Lemma hcons_mult_comm :
∀ i h s,
hcons_mult h i (hcons h s) = hcons h (hcons_mult h i s).
Lemma R1_iff s s' : R1 (node s) (node s') ↔ S0 s s'.
Lemma R2_iff i s s' : R2 i (node s) (node s') ↔
S1 i s s' ∨ S2 i s s'.
Lemma S2_iff : ∀ n h h' s s',
S2 n (hcons h s) (hcons h' s') ↔
R2 n h h' ∧ s = s' ∨
h = h' ∧ S2 n s s'.
Lemma S0_app : ∀ s1 s2 s3, S0 s2 s3 →
S0 (hy_app s1 s2)
(hy_app s1 s3).
Lemma R1_app : ∀ s1 s2 s3,
R1 (node s2) (node s3) →
R1 (node (hy_app s1 s2)) (node (hy_app s1 s3)).
Lemma S1_app n : ∀ s1 s2 s3,
S1 n s2 s3 → S1 n (hy_app s1 s2) (hy_app s1 s3).
Induction Schemes for R2
Scheme R2_ind2 := Induction for R2 Sort Prop
with
S2_ind2 := Induction for S2 Sort Prop.
Arguments R2_ind2 n P P0 : rename.
Arguments S2_ind2 n P P0 : rename.
Lemma S2_app : ∀ n s1 s2 ,
S2 n s1 s2 →
∀ l, S2 n (hy_app l s1) (hy_app l s2).
Lemma R2_app n : ∀ s1 s2 ,
R2 n (node s1) (node s2) →
∀ l, R2 n (node (hy_app l s1))
(node (hy_app l s2)).
Lemma hcons_mult_S0 : ∀ h i s s' ,
S0 s s' →
S0 (hcons_mult h i s)
(hcons_mult h i s').
Lemma hcons_mult_S1 n : ∀ h i s s' , S1 n s s' →
S1 n (hcons_mult h i s)
(hcons_mult h i s').
Lemma hcons_mult_S2 n : ∀ h i s s' , S2 n s s' →
S2 n (hcons_mult h i s)
(hcons_mult h i s').
Lemma rounds_trans {B:Battle} :
∀ i h j h', rounds B i h j h' →
∀ k h0, rounds B k h0 i h →
rounds B k h0 j h'.
Lemma standard_incl_free : ∀ i h h',
battle_rel standard i h h'→ battle_rel free i h h' .
Lemma standard_battle_head :
∀ i h j h',
@rounds standard i h j h' → h ≠ head.
Lemma round_plus_trans : ∀ h h' h'', h -+-> h' →
h' -+-> h'' →
h -+-> h''.
Lemma S0_remove_r : ∀ l , S0 (add_head_r l) l.
Lemma S0_remove_r_i : ∀ i l, S0 (add_head_r_plus l (S i))
(add_head_r_plus l i).
Lemma R1_remove_r_i : ∀ i h,
R1 (add_r h (S i)) (add_r h i).
Lemma round_n_remove_h : ∀ i j h,
round_n j (add_r h (S i)) (add_r h i).
Lemma remove_heads_r : ∀ i h j, rounds standard
j
(add_r h (S i))
(S i+j)%nat
h.
Lemma remove_heads_r_free: ∀ i h j, rounds free
j
(add_r h (S i))
(S i+j)%nat
h.
Lemma variant_mono_free {A:Type} {Lt: relation A}{Tr : Transitive Lt}
{Wf: well_founded Lt} m {V: Hvariant Wf free m}:
∀ i h j h', rounds free i h j h' → Lt (m h') (m h).
Lemma m_strict_mono {A:Type} {Lt: relation A}{St: StrictOrder Lt}
{Wf: well_founded Lt} m (V: @Hvariant _ _ Wf free m){h h':Hydra}:
h -+-> h' → Lt (m h') (m h).
companion lemmas for R1 and R2
Lemma round_n_inv i h h' : round_n i h h' → R1 h h' ∨ R2 i h h'.
Lemma rounds_free_equiv1 : ∀ i j h h',
rounds free i h j h' →
h -+-> h'.
Lemma rounds_free_equiv2 : ∀ h h',
h -+-> h' →
∀ i, ∃ j, rounds free i h j h'.
Lemma Termination_strong (B:Battle) :
Termination → B_termination B.
Lemma Hvariant_Termination {A : Type} {lt : relation A}
(Hwf : well_founded lt) (m : Hydra → A) :
@Hvariant _ _ Hwf free m → Termination.
If the hydra is not reduced to a head, there exists at
least one head that Hercules can chop off
chose a lowest head
Definition next_round n :
∀ h , round_spec h n.
Definition next_step (f : ∀ n h, round_spec h n) n h :=
match f n h with
inright _ ⇒ head
| inleft (exist _ h' _) ⇒ h'
end.
Definition classic_battle f t h :=
let fix go n t h :=
match h, t with head, _ ⇒ h
| _, 0 ⇒ h
| _, S t' ⇒ go (S n) t' (next_step f n h)
end
in go 1 t h.