Termination of a hydra game #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

We follow the proof by Peter LeFanu Lumsdaine at https://mathoverflow.net/a/229084/3332.

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

source

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

relation.cut_expand r s' s = ∃ (t : multiset α) (a : α), (∀ (a' : α), a' ∈ t → r a' a) ∧ s' + {a} = s + t

source

theorem relation.cut_expand_le_inv_image_lex {α : Type u_1} {r : α → α → Prop} [hi : is_irrefl α r] :

relation.cut_expand r ≤ inv_image (finsupp.lex (rᶜ ⊓ ne) has_lt.lt) ⇑multiset.to_finsupp

source

theorem relation.cut_expand_singleton {α : Type u_1} {r : α → α → Prop} {s : multiset α} {x : α} (h : ∀ (x' : α), x' ∈ s → r x' x) :

relation.cut_expand r s {x}

source

theorem relation.cut_expand_singleton_singleton {α : Type u_1} {r : α → α → Prop} {x' x : α} (h : r x' x) :

relation.cut_expand r {x'} {x}

source

theorem relation.cut_expand_add_left {α : Type u_1} {r : α → α → Prop} {t u : multiset α} (s : multiset α) :

relation.cut_expand r (s + t) (s + u) ↔ relation.cut_expand r t u

source

theorem relation.cut_expand_iff {α : Type u_1} {r : α → α → Prop} [decidable_eq α] [is_irrefl α r] {s' s : multiset α} :

relation.cut_expand r s' s ↔ ∃ (t : multiset α) (a : α), (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ s' = s.erase a + t

source

theorem relation.not_cut_expand_zero {α : Type u_1} {r : α → α → Prop} [is_irrefl α r] (s : multiset α) :

¬relation.cut_expand r s 0

source

theorem relation.cut_expand_fibration {α : Type u_1} (r : α → α → Prop) :

relation.fibration (prod.game_add (relation.cut_expand r) (relation.cut_expand r)) (relation.cut_expand r) (λ (s : multiset α × 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.

source

theorem relation.acc_of_singleton {α : Type u_1} {r : α → α → Prop} [is_irrefl α r] {s : multiset α} :

(∀ (a : α), a ∈ s → acc (relation.cut_expand r) {a}) → acc (relation.cut_expand r) s

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

source

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

acc (relation.cut_expand r) {a}

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

source

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

well_founded (relation.cut_expand r)

cut_expand r is well-founded when r is.