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, and a new operation game_add that combines to relations to form a relation on the product type, which is used to define addition of games in combinatorial game theory.

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)
inductive relation.game_add {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop) :
α × βα × β → Prop
• fst : ∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {a' a : α} {b : β}, rα a' a (a', b) (a, b)
• snd : ∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {a : α} {b' b : β}, rβ b' b (a, b') (a, b)

The "addition of games" relation in combinatorial game theory, on the product type: if rα a' a means that a ⟶ a' is a valid move in game α, and rβ b' b means that b ⟶ b' is a valid move in game β, then game_add rα rβ specifies the valid moves in the juxtaposition of α and β: the player is free to choose one of the games and make a move in it, while leaving the other game unchanged.

theorem relation.game_add_le_lex {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop) :
prod.lex

game_add is a subrelation of prod.lex.

theorem relation.rprod_le_trans_gen_game_add {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop) :

prod.rprod is a subrelation of the transitive closure of game_add.

theorem acc.game_add {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {a : α} {b : β} (ha : acc a) (hb : acc b) :
acc rβ) (a, b)

If a is accessible under rα and b is accessible under rβ, then (a, b) is accessible under relation.game_add rα rβ. Notice that prod.lex_accessible requires the stronger condition ∀ b, acc rβ b.

theorem well_founded.game_add {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} (hα : well_founded rα) (hβ : well_founded rβ) :

The sum of two well-founded games is well-founded.

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.