Combinatorial games from a type of states

In the literature, mathematicians often describe games as graphs, consisting of a set of states, as well as move relations for the left and right players. We define a structure GameGraph which facilitates this construction, bundling the left and right set functions along with the type, as well as functions GameGraph.toLGame and GameGraph.toIGame which turn them into the appropriate type of game.

Mathematically, GameGraph.toLGame is nothing but the corecursor on loopy games, while GameGraph.toIGame is defined inductively.

Design notes

When working with any "specific" game (nim, domineering, etc.) you can use GameGraph to set up the basic theorems and definitions, but the intent is that you're not working with GameGraph directly most of the time.

structure GameGraph (α : Type v) : Type v

A game graph is a type of states endowed with move sets for the left and right players.

You can use GameGraph.toLGame and GameGraph.toIGame to turn this structure into the appropriate game type.

• moves : Player → α → Set α

  The sets of options for the players.

def GameGraph.IsOption {α : Type v} (c : GameGraph α) (a b : α) : Prop

IsOption a b means that a is either a left or a right move for b.

Equations

• c.IsOption a b = (a ∈ ⋃ (p : Player), c.moves p b)

theorem GameGraph.isOption_iff_mem_union {α : Type v} {c : GameGraph α} {a b : α} : c.IsOption a b ↔ a ∈ c.moves Player.left b ∪ c.moves Player.right b

theorem GameGraph.IsOption.of_mem_moves {α : Type v} {c : GameGraph α} {p : Player} {a b : α} (h : a ∈ c.moves p b) : c.IsOption a b

theorem GameGraph.isWellFounded_isOption_of_eq {α : Type v} {c : GameGraph α} (r : α → α → Prop) [Hr : IsWellFounded α r] (hr : ∀ (p : Player) (x : α), c.moves p x = {y : α | r y x}) : IsWellFounded α c.IsOption

instance GameGraph.instSmallSubtypeIsOption {α : Type v} {c : GameGraph α} [Hl : ∀ (a : α), Small.{u, v} ↑(c.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(c.moves Player.right a)] (b : α) : Small.{u, v} { a : α // c.IsOption a b }

Loopy games

def GameGraph.toLGame {α : Type v} (c : GameGraph α) [Hl : ∀ (a : α), Small.{u, v} ↑(c.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(c.moves Player.right a)] (a : α) : LGame

Turns a state of a GameGraph into an LGame.

Equations

• c.toLGame a = LGame.corec c.moves a

@[simp]

theorem GameGraph.moves_toLGame {α : Type v} (c : GameGraph α) (p : Player) [Hl : ∀ (a : α), Small.{u, v} ↑(c.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(c.moves Player.right a)] (a : α) : LGame.moves p (c.toLGame a) = c.toLGame '' c.moves p a

theorem GameGraph.toLGame_def' {α : Type v} {c : GameGraph α} [Hl : ∀ (a : α), Small.{u, v} ↑(c.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(c.moves Player.right a)] (a : α) : c.toLGame a = !{fun (p : Player) => c.toLGame '' c.moves p a}

theorem GameGraph.toLGame_def {α : Type v} {c : GameGraph α} [Hl : ∀ (a : α), Small.{u, v} ↑(c.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(c.moves Player.right a)] (a : α) : c.toLGame a = !{c.toLGame '' c.moves Player.left a | c.toLGame '' c.moves Player.right a}

theorem GameGraph.mem_moves_toLGame_of_mem {α : Type v} {c : GameGraph α} {p : Player} [Hl : ∀ (a : α), Small.{u, v} ↑(c.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(c.moves Player.right a)] {a b : α} (hab : b ∈ c.moves p a) : c.toLGame b ∈ LGame.moves p (c.toLGame a)

theorem GameGraph.neg_toLGame {α : Type v} {c : GameGraph α} [Hl : ∀ (a : α), Small.{u, v} ↑(c.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(c.moves Player.right a)] (h : c.moves Player.left = c.moves Player.right) (a : α) : -c.toLGame a = c.toLGame a

Well-founded games

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

Conway recursion: build data for a game by recursively building it on its left and right sets.

Equations

• c.moveRecOn x mk = IsWellFounded.fix c.IsOption (fun (x : α) (IH : (y : α) → c.IsOption y x → motive y) => mk x fun (x_1 : Player) (x_2 : α) (h : x_2 ∈ c.moves x_1 x) => IH x_2 ⋯) x

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

def GameGraph.toIGame {α : Type v} (c : GameGraph α) [Hl : ∀ (a : α), Small.{u, v} ↑(c.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(c.moves Player.right a)] [H : IsWellFounded α c.IsOption] (a : α) : IGame

Turns a state of a GameGraph into an IGame.

Equations

• c.toIGame a = c.moveRecOn a fun (x : α) (IH : (p : Player) → (y : α) → y ∈ c.moves p x → IGame) => !{fun (p : Player) => Set.range fun (b : ↑(c.moves p x)) => IH p ↑b ⋯}

theorem GameGraph.toIGame_def' {α : Type v} {c : GameGraph α} [Hl : ∀ (a : α), Small.{u, v} ↑(c.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(c.moves Player.right a)] [H : IsWellFounded α c.IsOption] (a : α) : c.toIGame a = !{fun (p : Player) => c.toIGame '' c.moves p a}

theorem GameGraph.toIGame_def {α : Type v} {c : GameGraph α} [Hl : ∀ (a : α), Small.{u, v} ↑(c.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(c.moves Player.right a)] [H : IsWellFounded α c.IsOption] (a : α) : c.toIGame a = !{c.toIGame '' c.moves Player.left a | c.toIGame '' c.moves Player.right a}

@[simp]

theorem GameGraph.moves_toIGame {α : Type v} (c : GameGraph α) (p : Player) [Hl : ∀ (a : α), Small.{u, v} ↑(c.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(c.moves Player.right a)] [H : IsWellFounded α c.IsOption] (a : α) : IGame.moves p (c.toIGame a) = c.toIGame '' c.moves p a

theorem GameGraph.mem_moves_toIGame_of_mem {α : Type v} {c : GameGraph α} {p : Player} [Hl : ∀ (a : α), Small.{u, v} ↑(c.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(c.moves Player.right a)] [H : IsWellFounded α c.IsOption] {a b : α} (hab : b ∈ c.moves p a) : c.toIGame b ∈ IGame.moves p (c.toIGame a)

@[simp]

theorem GameGraph.toLGame_toIGame {α : Type v} (c : GameGraph α) [Hl : ∀ (a : α), Small.{u, v} ↑(c.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(c.moves Player.right a)] [H : IsWellFounded α c.IsOption] (a : α) : IGame.toLGame (c.toIGame a) = c.toLGame a

theorem GameGraph.neg_toIGame {α : Type v} {c : GameGraph α} [Hl : ∀ (a : α), Small.{u, v} ↑(c.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(c.moves Player.right a)] [H : IsWellFounded α c.IsOption] (h : c.moves Player.left = c.moves Player.right) (a : α) : -c.toIGame a = c.toIGame a

theorem GameGraph.impartial_toIGame {α : Type v} {c : GameGraph α} [Hl : ∀ (a : α), Small.{u, v} ↑(c.moves Player.left a)] [Hr : ∀ (a : α), Small.{u, v} ↑(c.moves Player.right a)] [H : IsWellFounded α c.IsOption] (h : c.moves Player.left = c.moves Player.right) (a : α) : (c.toIGame a).Impartial