Library hydras.Hydra.Hydra_Examples
From Coq Require Import Arith Lia.
From hydras Require Import Hydra_Lemmas More_Arith.
Open Scope nat_scope.
Check Hydra_rect2.
Module Examples.
Example ex1 : ∀ h h', R1 (hyd3 h head h') (hyd2 h h').
Example Hy := hyd3 head
(hyd2
(hyd1
(hyd2 head head))
head)
head.
Example Hy' := hyd2 head
(hyd2
(hyd1
(hyd2 head head))
head).
Example ex4: round Hy Hy'.
Example Hy'' :=
hyd2 head
(hyd2
(hyd_mult (hyd1 head) 5)
head).
Example Hy'H'' : round Hy' Hy''.
Example R2_example: R2 4 Hy' Hy''.
move to 2nd sub-hydra (0-based indices)
move to first sub-hydra
we're at distance 2 from the to-be-chopped-off head
let's go to the first daughter,
then chop-off the leftmost head
Example Exx : {h' | round Hy' h'}.
Example Ex5 : {h' | Hy -*-> h'}.
Example Hy''' :=
node (hcons head
(hcons_mult (hyd1 (hyd_mult (hyd1 head) 5)) 3 hnil)).
Example hsize_bigger : (hsize Hy'' < hsize Hy''')%nat.
Example height_not_strictly_decreasing : height Hy'' = height Hy'''.
Example Hy_1 : R1 Hy Hy'.
Example Hy_2 : R2 4 Hy' Hy''.
Example ex_2 :{Hy'' | R2 4 Hy' Hy''}.
Example Hy_3 : R2 2 Hy'' Hy'''.
Example Hy''_Hy''' : Hy'' -1-> Hy'''.
Example Hy_Hy''' : Hy -+-> Hy'''.
End Examples.
Check Hydra_ind.
Module Bad.
Lemma height_lt_size (h:Hydra) : height h < hsize h. End Bad.
Lemma height_lt_size (h:Hydra) : height h < hsize h.