Library hydras.Hydra.BigBattle

A long hydra battle

Pierre Castéran, LaBRI, Univ Bordeaux

From Coq Require Import Arith Relations Lia.
From hydras Require Import Hydra_Definitions Hydra_Lemmas Iterates Exp2.

Let us consider a small hydra hinit

#[local] Notation h3 := (hyd_mult head 3).
Definition hinit := hyd3 h3 head head.

the first steps of a standard battle (Hercules chops off the rightmost head)

Lemma L_0_2 : rounds standard 0 hinit 2 (hyd1 h3).

In the next round, there is a replication of h3 into 3 copies of h2
More generally, all the future hydras will be composed of several copies of h2, then several copies of h1, then several heads


Notation h2 := (hyd_mult head 2).
Notation h1 := (hyd1 head).

Notation hyd a b c :=
  (node (hcons_mult h2 a
             (hcons_mult h1 b
                         (hcons_mult head c hnil)))).


Lemma L_2_3 : rounds standard 2 (hyd1 h3) 3 (hyd 3 0 0).

Lemma L_0_3 : rounds standard 0 hinit 3 (hyd 3 0 0).

From now on, we abstract the configurations of the battle as tuples (round number, n2, n1, nh) where n2 (resp. n1, nh) is the number of daughters of type h2 resp. h1, heads


Record state : Type :=
  mks {round : nat ; n2 : nat ; n1 : nat ; nh : nat}.



Definition (s : state) :=
  match s with
  | mks round a b (S c) ⇒ mks (S round) a b c
  | mks round a (S b) 0 ⇒ mks (S round) a b (S round)
  | mks round (S a) 0 0 ⇒ mks (S round) a (S round) 0
  | _ ⇒ s
  end.


returns the state at the n-th round


Definition test n := iterate next (n-3) (mks 3 3 0 0).


















Definition doubleS (n : nat) := 2 × (S n).




OK, instead of tests based on the function next, we consider now relations (which allow us to consider accessibility predicates)
steps i a b c j a' b' c' has almost the same meaning as iterate test (j - i) (mks t a b c) = (mks t' a' b' c')


Inductive one_step (i: nat) :
  nat → nat → nat → nat → nat → nat → Prop :=
| step1: ∀ a b c, one_step i a b (S c) a b c
| step2: ∀ a b , one_step i a (S b) 0 a b (S i)
| step3: ∀ a, one_step i (S a) 0 0 a (S i) 0.



Lemma step_rounds : ∀ i a b c a' b' c',
    one_step i a b c a' b' c' →
    rounds standard i (hyd a b c) (S i) (hyd a' b' c').


Inductive steps : nat → nat → nat → nat →
                  nat → nat → nat → nat → Prop :=
| steps1 : ∀ i a b c a' b' c',
    one_step i a b c a' b' c' → steps i a b c (S i) a' b' c'
| steps_S : ∀ i a b c j a' b' c' k a'' b'' c'',
    steps i a b c j a' b' c' →
    steps j a' b' c' k a'' b'' c'' →
    steps i a b c k a'' b'' c''.

reachability (for i > 0)

Definition reachable (i a b c : nat) : Prop :=
  steps 3 3 0 0 i a b c.



Lemma steps_rounds : ∀ i a b c j a' b' c',
    steps i a b c j a' b' c' →
    rounds standard i (hyd a b c) j (hyd a' b' c').

From now on, we play again the same tests as above, but instead of plain uses of Compute, we prove and register lemmas that we will be used later


Lemma L4 : reachable 4 2 4 0.

Now we prove some laws we observed in our test phase


Lemma LS : ∀ c a b i, steps i a b (S c) (i + S c) a b 0.

The law that relates two consecutive events with (nh = 0)

Lemma doubleS_law : ∀ a b i, steps i a (S b) 0 (doubleS i) a b 0.

Lemma reachable_S : ∀ i a b, reachable i a (S b) 0 →
                                   reachable (doubleS i) a b 0.




Lemma L10 : reachable 10 2 3 0.

Lemma L22 : reachable 22 2 2 0.

Lemma L46 : reachable 46 2 1 0.

Lemma L94 : reachable 94 2 0 0.

Lemma L95 : reachable 95 1 95 0.



Lemma L0_95 : rounds standard 3 (hyd 3 0 0) 95 (hyd 1 95 0).


No more tests ! we are going to build bigger transitions



Lemma Bigstep : ∀ b i a , reachable i a b 0 →
                               reachable (iterate doubleS b i) a 0 0.




From all the lemmas above, we now get a pretty big step


Definition M := iterate doubleS 95 95.

Lemma L2_95 : reachable M 1 0 0.
the next step creates (M+1) copies of h1



Lemma L2_95_S : reachable (S M) 0 (S M) 0.



Definition N := iterate doubleS (S M) (S M).

Theorem SuperbigStep : reachable N 0 0 0.

We can ow apply our study based on abstract states to "real" hydras
transforming our relation one_step into standard battles
We get now statements about hydras and battles



Lemma Almost_done :
  rounds standard 3 (hyd 3 0 0) N (hyd 0 0 0).

Theorem Done :
  rounds standard 0 hinit N head.



The natural number N is expressed in terms of the (iterate doubleS) function. The rest of this file is dedicated to get an intuition of how it is huge . Our idea is to get a minoration by exponentials of base 2

Lemma minoration_0 : ∀ n, 2 × n ≤ doubleS n.
Lemma minoration_1 : ∀ n x, exp2 n × x ≤ iterate doubleS n x.
Lemma minoration_2 : exp2 95 × 95 ≤ M.
Lemma minoration_3 : exp2 (S M) × S M ≤ N.
Lemma exp2_mono1 : ∀ n p, n ≤ p → exp2 n ≤ exp2 p .

Lemma minoration : exp2 (exp2 95 × 95) ≤ N.
Hence, the length of the battle is greater or equal than exp2 (exp2 95 * 95), a number whose representation in base 10 has at least 10 ^ 30 digits !
from OCAML
let exp2 x = 2.0 ** x;;
let _ = exp2 95.0 *. 95.0;;
float = 3.76333771942755604e+30
N >= 2 ** 3.7e+30
log10 N >= 3.7e+30 * log10 2 >= 1.0e+30
N >= 10 ** (10 ** 30)