logic.hydra

# Termination of a hydra game #

This file deals with the following version of the hydra game: each head of the hydra is labelled by an element in a type α, and when you cut off one head with label a, it grows back an arbitrary but finite number of heads, all labelled by elements smaller than a with respect to a well-founded relation r on α. We show that no matter how (in what order) you choose cut off the heads, the game always terminates, i.e. all heads will eventually be cut off (but of course it can last arbitrarily long, i.e. takes an arbitrary finite number of steps).

This result is stated as the well-foundedness of the cut_expand relation defined in this file: we model the heads of the hydra as a multiset of elements of α, and the valid "moves" of the game are modelled by the relation cut_expand r on multiset α: cut_expand r s' s is true iff s' is obtained by removing one head a ∈ s and adding back an arbitrary multiset t of heads such that all a' ∈ t satisfy r a' a.

To prove this theorem, we follow the proof by Peter LeFanu Lumsdaine at https://mathoverflow.net/a/229084/3332, and along the way we introduce the notion of fibration of relations.

TODO: formalize the relations corresponding to more powerful (e.g. Kirby–Paris and Buchholz) hydras, and prove their well-foundedness.

def relation.fibration {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop) (f : α → β) :
Prop

A function f : α → β is a fibration between the relation rα and rβ if for all a : α and b : β, whenever b : β and f a are related by rβ, b is the image of some a' : α under f, and a' and a are related by rα.

Equations
• f = ∀ ⦃a : α⦄ ⦃b : β⦄, rβ b (f a)(∃ (a' : α), rα a' a f a' = b)
theorem acc.of_fibration {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} (f : α → β) (fib : f) {a : α} (ha : acc a) :
acc (f a)

If f : α → β is a fibration between relations rα and rβ, and a : α is accessible under rα, then f a is accessible under rβ.

theorem acc.of_downward_closed {α : Type u_1} {β : Type u_2} {rβ : β → β → Prop} (f : α → β) (dc : ∀ {a : α} {b : β}, rβ b (f a)b ) (a : α) (ha : acc (inv_image f) a) :
acc (f a)
def relation.cut_expand {α : Type u_1} (r : α → α → Prop) (s' s : multiset α) :
Prop

The relation that specifies valid moves in our hydra game. cut_expand r s' s means that s' is obtained by removing one head a ∈ s and adding back an arbitrary multiset t of heads such that all a' ∈ t satisfy r a' a.

This is most directly translated into s' = s.erase a + t, but multiset.erase requires decidable_eq α, so we use the equivalent condition s' + {a} = s + t instead, which is also easier to verify for explicit multisets s', s and t.

We also don't include the condition a ∈ s because s' + {a} = s + t already guarantees a ∈ s + t, and if r is irreflexive then a ∉ t, which is the case when r is well-founded, the case we are primarily interested in.

The lemma relation.cut_expand_iff below converts between this convenient definition and the direct translation when r is irreflexive.

Equations
• s = ∃ (t : multiset α) (a : α), (∀ (a' : α), a' tr a' a) s' + {a} = s + t
theorem relation.cut_expand_singleton {α : Type u_1} {r : α → α → Prop} {s : multiset α} {x : α} (h : ∀ (x' : α), x' sr x' x) :
{x}
theorem relation.cut_expand_singleton_singleton {α : Type u_1} {r : α → α → Prop} {x' x : α} (h : r x' x) :
{x'} {x}
theorem relation.cut_expand_add_left {α : Type u_1} {r : α → α → Prop} {t u : multiset α} (s : multiset α) :
(s + t) (s + u) u
theorem relation.cut_expand_iff {α : Type u_1} {r : α → α → Prop} [decidable_eq α] [ r] {s' s : multiset α} :
s ∃ (t : multiset α) (a : α), (∀ (a' : α), a' tr a' a) a s s' = s.erase a + t
theorem relation.not_cut_expand_zero {α : Type u_1} {r : α → α → Prop} [ r] (s : multiset α) :
¬ 0
theorem relation.cut_expand_fibration {α : Type u_1} (r : α → α → Prop) :
(λ (s : × multiset α), s.fst + s.snd)

For any relation r on α, multiset addition multiset α × multiset α → multiset α is a fibration between the game sum of cut_expand r with itself and cut_expand r itself.

theorem relation.acc_of_singleton {α : Type u_1} {r : α → α → Prop} [ r] {s : multiset α} :
(∀ (a : α), a s {a}) s

A multiset is accessible under cut_expand if all its singleton subsets are, assuming r is irreflexive.

theorem acc.cut_expand {α : Type u_1} {r : α → α → Prop} [ r] {a : α} (hacc : acc r a) :
{a}

A singleton {a} is accessible under cut_expand r if a is accessible under r, assuming r is irreflexive.

theorem well_founded.cut_expand {α : Type u_1} {r : α → α → Prop} (hr : well_founded r) :

cut_expand r is well-founded when r is.