Combinatorial games from a type of states

In the literature, games are often described in terms of their game graphs, which can be thought of as (not necessarily properly) 2-edge-coloured rooted arborescences. Or more informally as a set of states with move relations for Left and Right (the two players).

We define a structure GameGraph that facilitates this viewpoint, bundling the Left and Right option set functions along with the type, as well as GameGraph.toForm, which turns the graph into the relevant type of game form.

Design notes

When working with any "specific" game (Nim, Domineering, Hackenbush, et cetera), one can use GameGraph to set up the basic theorems and definitions, but the intent is that one need not work with GameGraph directly most of the time.

structure GameGraph (α : Type v) : Type v

A game graph is a type of states endowed with option sets for Left and Right.

Use GameGraph.toForm to turn this structure into the appropriate game type.

• moves : Player → α → Set α

  The sets of options for the players.

Well-founded games

class GameGraph.IsWellFounded {α : Type v} (c : GameGraph α) : Prop

A game graph is well-founded if from every position there is no infinite sequence of (not necessarily alternating) Left and Right moves. In the literature, such a game is called loopfree (see Siegel, Definition 4.1 on p. 34).

• wf : IsWellFounded α fun (a b : α) => ∃ (p : Player), a ∈ c.moves p b

theorem GameGraph.IsWellFounded.of_subrelation {α : Type v} {g : GameGraph α} (r : α → α → Prop) [IsWellFounded α r] (hr : ∀ (a b : α) (p : Player), a ∈ g.moves p b → r a b) : g.IsWellFounded

def GameGraph.moveRecOn {α : Type v} {g : GameGraph α} [g.IsWellFounded] {motive : α → Sort u_1} (x : α) (ind : (x : α) → ((p : Player) → (y : α) → y ∈ g.moves p x → motive y) → motive x) : motive x

Conway induction: build data for a game by recursively building it on its Left and Right sets.

Equations

• One or more equations did not get rendered due to their size.

theorem GameGraph.moveRecOn_eq {α : Type v} {g : GameGraph α} [g.IsWellFounded] {motive : α → Sort u_1} (x : α) (ind : (x : α) → ((p : Player) → (y : α) → y ∈ g.moves p x → motive y) → motive x) : moveRecOn x ind = ind x fun (x_1 : Player) (y : α) (x : y ∈ g.moves x_1 x) => moveRecOn y ind

def GameGraph.toForm {α : Type v} {g : GameGraph α} [Hl : ∀ (a : α), Small.{u, v} ↑(g.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(g.moves Player.right a)] [g.IsWellFounded] {G : Type (u + 1)} [Form G] (a : α) : G

Turns a state of a GameGraph into a Form.

Equations

• GameGraph.toForm a = GameGraph.moveRecOn a fun (x : α) (IH : (p : Player) → (y : α) → y ∈ g.moves p x → G) => !{fun (p : Player) => Set.range fun (b : ↑(g.moves p x)) => IH p ↑b ⋯}

theorem GameGraph.toForm_def' {α : Type v} {g : GameGraph α} [Hl : ∀ (a : α), Small.{u, v} ↑(g.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(g.moves Player.right a)] [g.IsWellFounded] {G : Type (u + 1)} [Form G] (a : α) : toForm a = !{fun (p : Player) => toForm '' g.moves p a}

theorem GameGraph.toForm_def {α : Type v} {g : GameGraph α} [Hl : ∀ (a : α), Small.{u, v} ↑(g.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(g.moves Player.right a)] [g.IsWellFounded] {G : Type (u + 1)} [Form G] (a : α) : toForm a = !{toForm '' g.moves Player.left a | toForm '' g.moves Player.right a}

@[simp]

theorem GameGraph.moves_toForm {α : Type v} {g : GameGraph α} [Hl : ∀ (a : α), Small.{u, v} ↑(g.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(g.moves Player.right a)] [g.IsWellFounded] {G : Type (u + 1)} [Form G] (p : Player) (a : α) : Moves.moves p (toForm a) = toForm '' g.moves p a

theorem GameGraph.mem_moves_toForm_of_mem {α : Type v} {g : GameGraph α} [Hl : ∀ (a : α), Small.{u, v} ↑(g.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(g.moves Player.right a)] [g.IsWellFounded] {G : Type (u + 1)} [Form G] (p : Player) {a b : α} (hab : b ∈ g.moves p a) : toForm b ∈ Moves.moves p (toForm a)