Alice Laroche, the 18th of September 2023,
using ideas and notations from Ayberk Tosun.

This file is a formalisation of Kirby-Paris Hydra game.  We show that
every battle eventually ends, and use this fact to compute the first
terms of Hydra(n).

[1] https://en.wikipedia.org/wiki/Hydra_game

[2] Kirby, Laurie; Paris, Jeff. Bull. Accessible independence results
for Peano arithmetic.  London Math. Soc, 14 (1982), 285-293.
http://logic.amu.edu.pl/images/3/3c/Kirbyparis.pdf

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Various.Hydra where

open import MLTT.Spartan
open import MLTT.List
open import Ordinals.Notions

\end{code}

The type of Hydra is defined inductively: It is a list of subhydras

\begin{code}

data Hydra : 𝓤₀ ̇ where
Node : List Hydra → Hydra

example₁ : Hydra
example₁ = Node (Node [] ∷ [])

example₂ : Hydra
example₂ = Node (Node [] ∷ Node [] ∷ [])

defeated : Hydra
defeated = Node []

\end{code}

We define the type of head's locations using two inductive type.  This
is to know if the head is a child or a grandchild, to help
implementing hydra regeneration mechanism.

\begin{code}

data HeadLocation₀ : List Hydra → 𝓤₀ ̇ where
here : {hs : List Hydra}
next : {h : Hydra} {hs : List Hydra}

data HeadLocation₁ : List Hydra → 𝓤₀ ̇ where
here₀ : {hs hs' : List Hydra}
here₁ : {hs hs' : List Hydra}
next  : {h : Hydra} {hs : List Hydra}

HeadLocation : Hydra → 𝓤₀ ̇

\end{code}

Similarly, we define two cutting functions, one for cutting child head

\begin{code}

cons-mult : {X : 𝓤 ̇ } → X → ℕ → List X → List X
cons-mult x 0 xs = xs
cons-mult x (succ n) xs = x ∷ (cons-mult x n xs)

cut₀ : (hs : List Hydra) → HeadLocation₀ hs → List Hydra
cut₀ (h ∷ hs) (here)    = hs
cut₀ (h ∷ hs) (next l)  = h ∷ (cut₀ hs l)

cut₁ : ℕ → (hs : List Hydra) → HeadLocation₁ hs → List Hydra
cut₁ n (h ∷ hs')         (next  l) = h ∷ (cut₁ n hs' l)
cut₁ n ((Node hs) ∷ hs') (here₀ l) = cons-mult (Node (cut₀ hs l)) (succ n) hs'
cut₁ n ((Node hs) ∷ hs') (here₁ l) = Node (cut₁ n hs l) ∷ hs'

cut : ℕ → (h : Hydra) → HeadLocation h → Hydra
cut n (Node hs) (inl l) = Node (cut₀ hs l)
cut n (Node hs) (inr l) = Node (cut₁ n hs l)

\end{code}

To prove that the process of cutting hydra's heads always end, we
define a relation between hydras and prove it's well founded.

\begin{code}

_⊲_ : Hydra → Hydra → 𝓤₀ ̇
h ⊲ h' = Σ n ꞉ ℕ , Σ l ꞉ HeadLocation h' , h ＝ cut n h' l

pattern step n l eq = (n , l , eq)

_⊲'_ : List Hydra → List Hydra → 𝓤₀ ̇
hs ⊲' hs' = Σ n ꞉ ℕ , ( ( Σ l ꞉ HeadLocation₀ hs' , hs ＝ cut₀ hs' l)
+ ( Σ l ꞉ HeadLocation₁ hs' , hs ＝ cut₁ n hs' l))

pattern step₀ n l eq = (n , inl (l , eq))
pattern step₁ n l eq = (n , inr (l , eq))

⊲⇒⊲' : {hs hs' : List Hydra} → Node hs ⊲ Node hs' → hs ⊲' hs'
⊲⇒⊲' (step n (inl l) refl) = step₀ n l refl
⊲⇒⊲' (step n (inr l) refl) = step₁ n l refl

[]-is-minimum : (hs : List Hydra) → ¬(hs ⊲' [])
[]-is-minimum h (step₀ _ () _)
[]-is-minimum h (step₁ _ () _)

⊲-is-well-founded : is-well-founded _⊲_
⊲'-is-well-founded : is-well-founded _⊲'_

⊲-is-well-founded (Node hs) = acc (recurs (⊲'-is-well-founded hs))
where
recurs : {hs : List Hydra}
→ is-accessible (_⊲'_) hs
→ (h' : Hydra) → h' ⊲ Node hs
→ is-accessible (_⊲_) h'
recurs (acc rec₁) (Node hs') r = acc (recurs (rec₁ hs' (⊲⇒⊲' r)))

⊲'-is-well-founded [] = acc (λ h r → 𝟘-elim ([]-is-minimum h r))
⊲'-is-well-founded (h ∷ hs) =
acc (recurs (⊲-is-well-founded h) (⊲'-is-well-founded hs))
where
recurs : {h : Hydra} {hs : List Hydra}
→ is-accessible _⊲_ h
→ is-accessible _⊲'_ hs
→ (hs' : List Hydra) → hs' ⊲' (h ∷ hs)
→ is-accessible _⊲'_ hs'
recurs (acc rec₁) (acc rec₂) hs' (step₀ n here refl)      = acc rec₂
recurs (acc rec₁) (acc rec₂) hs' (step₀ n (next l) refl)  =
acc (recurs (acc rec₁) (rec₂ _ (step₀ n l refl)))
recurs (acc rec₁) (acc rec₂) hs' (step₁ n (next l) refl)  =
acc (recurs (acc rec₁) (rec₂ _ (step₁ n l refl)))
recurs (acc rec₁) (acc rec₂) hs' (step₁ n (here₁ l) refl) =
acc (recurs (rec₁ _ (step n (inr l) refl)) (acc rec₂))
recurs (acc rec₁) (acc rec₂) hs' (step₁ n (here₀ l) refl) = recurs' n
where
recurs' : (n : ℕ) → is-accessible _⊲'_ (cons-mult _ (succ n) _)
recurs' 0        = acc (recurs (rec₁ _ (step 0 (inl l) refl)) (acc rec₂))
recurs' (succ n) = acc (recurs (rec₁ _ (step 0 (inl l) refl)) (recurs' n))

\end{code}

We can now define Hydra(n) and compute its four first terms.

\begin{code}

leftmost-head₀ : (hs : List Hydra) → hs ≠ []
leftmost-head₀ []                    neq = 𝟘-elim (neq refl)
leftmost-head₀ ((Node (h ∷ hs)) ∷ _) neq =
where
leftmost-head₀' (inl l) = inr (here₀ l)
leftmost-head₀' (inr l) = inr (here₁ l)

leftmost-head (Node (h ∷ hs)) neq = leftmost-head₀ (h ∷ hs) (λ ())

f-Hydra : (n : ℕ) → ℕ
f-Hydra n = battle 1 (tall-hydra n) (⊲-is-well-founded _)
where
tall-hydra : (n : ℕ) → Hydra
tall-hydra 0 = Node []
tall-hydra (succ n) = Node (tall-hydra n ∷ [])

battle : ℕ → (h : Hydra) → is-accessible _⊲_ h → ℕ
battle turn Head            (acc rec₁ ) = 0
battle turn (Node (h ∷ hs)) (acc rec₁ ) =
succ (battle (succ turn) cut-hydra (rec₁ cut-hydra (turn , cut-head , refl)))
where

cut-hydra : Hydra
cut-hydra = cut turn (Node (h ∷ hs)) cut-head

f-Hydra0 : f-Hydra 0 ＝ 0
f-Hydra0 = refl

f-Hydra1 : f-Hydra 1 ＝ 1
f-Hydra1 = refl

f-Hydra2 : f-Hydra 2 ＝ 3
f-Hydra2 = refl

f-Hydra3 : f-Hydra 3 ＝ 37
f-Hydra3 = refl

\end{code}