Misere combinatorial games.

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 MisereGames.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 MisereGames.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][siegel:CombinatorialGameTheory:2013]).

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

theorem MisereGames.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 MisereGames.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 MisereGames.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 MisereGames.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

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

theorem MisereGames.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 MisereGames.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 MisereGames.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 MisereGames.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)