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 CutExpand 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 CutExpand r on Multiset α: CutExpand 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.

def Relation.CutExpand {α : Type u_1} (r : α → α → Prop) (s' : Multiset α) (s : Multiset α) : Prop

The relation that specifies valid moves in our hydra game. CutExpand 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 DecidableEq α, 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.cutExpand_iff below converts between this convenient definition and the direct translation when r is irreflexive.

Equations

• Relation.CutExpand r s' s = ∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ s' + {a} = s + t

theorem Relation.cutExpand_le_invImage_lex {α : Type u_1} {r : α → α → Prop} [DecidableEq α] [IsIrrefl α r] : Relation.CutExpand r ≤ InvImage (Finsupp.Lex (rᶜ ⊓ fun (x x_1 : α) => x ≠ x_1) fun (x x_1 : ℕ) => x < x_1) ⇑Multiset.toFinsupp

theorem Relation.cutExpand_singleton {α : Type u_1} {r : α → α → Prop} {s : Multiset α} {x : α} (h : ∀ x' ∈ s, r x' x) : Relation.CutExpand r s {x}

theorem Relation.cutExpand_singleton_singleton {α : Type u_1} {r : α → α → Prop} {x' : α} {x : α} (h : r x' x) : Relation.CutExpand r {x'} {x}

theorem Relation.cutExpand_add_left {α : Type u_1} {r : α → α → Prop} {t : Multiset α} {u : Multiset α} (s : Multiset α) : Relation.CutExpand r (s + t) (s + u) ↔ Relation.CutExpand r t u

theorem Relation.cutExpand_iff {α : Type u_1} {r : α → α → Prop} [DecidableEq α] [IsIrrefl α r] {s' : Multiset α} {s : Multiset α} : Relation.CutExpand r s' s ↔ ∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = Multiset.erase s a + t

theorem Relation.not_cutExpand_zero {α : Type u_1} {r : α → α → Prop} [IsIrrefl α r] (s : Multiset α) : ¬Relation.CutExpand r s 0

theorem Relation.cutExpand_fibration {α : Type u_1} (r : α → α → Prop) : Relation.Fibration (Prod.GameAdd (Relation.CutExpand r) (Relation.CutExpand r)) (Relation.CutExpand r) fun (s : Multiset α × Multiset α) => s.1 + s.2

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

theorem Relation.acc_of_singleton {α : Type u_1} {r : α → α → Prop} [IsIrrefl α r] {s : Multiset α} (hs : ∀ a ∈ s, Acc (Relation.CutExpand r) {a}) : Acc (Relation.CutExpand r) s

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

theorem Acc.cutExpand {α : Type u_1} {r : α → α → Prop} [IsIrrefl α r] {a : α} (hacc : Acc r a) : Acc (Relation.CutExpand r) {a}

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

theorem WellFounded.cutExpand {α : Type u_1} {r : α → α → Prop} (hr : WellFounded r) : WellFounded (Relation.CutExpand r)

CutExpand r is well-founded when r is.