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 ConcreteGame which facilitates this construction, bundling the left and right set functions along with the type, as well as functions ConcreteGame.toLGame and ConcreteGame.toIGame which turn them into the appropriate type of game.

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

Design notes

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

structure ConcreteGame (α : Type v) : Type v

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

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

• leftMoves : α → Set α

  The set of options for the left player.

• rightMoves : α → Set α

  The set of options for the right player.

def ConcreteGame.IsOption {α : Type v} (c : ConcreteGame α) (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 ∈ c.leftMoves b ∪ c.rightMoves b)

theorem ConcreteGame.IsOption.of_mem_leftMoves {α : Type v} {c : ConcreteGame α} {a b : α} : a ∈ c.leftMoves b → c.IsOption a b

theorem ConcreteGame.IsOption.of_mem_rightMoves {α : Type v} {c : ConcreteGame α} {a b : α} : a ∈ c.rightMoves b → c.IsOption a b

instance ConcreteGame.instSmallSubtypeIsOption {α : Type v} {c : ConcreteGame α} [∀ (a : α), Small.{u, v} ↑(c.leftMoves a)] [∀ (a : α), Small.{u, v} ↑(c.rightMoves a)] (a : α) : Small.{u, v} { b : α // c.IsOption b a }

Loopy games

def ConcreteGame.toLGame {α : Type v} (c : ConcreteGame α) [∀ (a : α), Small.{u, v} ↑(c.leftMoves a)] [∀ (a : α), Small.{u, v} ↑(c.rightMoves a)] (a : α) : LGame

Turns a state of a ConcreteLGame into an LGame.

Equations

• c.toLGame a = LGame.corec c.leftMoves c.rightMoves a

@[simp]

theorem ConcreteGame.leftMoves_toLGame {α : Type v} (c : ConcreteGame α) [∀ (a : α), Small.{u, v} ↑(c.leftMoves a)] [∀ (a : α), Small.{u, v} ↑(c.rightMoves a)] (a : α) : (c.toLGame a).leftMoves = c.toLGame '' c.leftMoves a

@[simp]

theorem ConcreteGame.rightMoves_toLGame {α : Type v} (c : ConcreteGame α) [∀ (a : α), Small.{u, v} ↑(c.leftMoves a)] [∀ (a : α), Small.{u, v} ↑(c.rightMoves a)] (a : α) : (c.toLGame a).rightMoves = c.toLGame '' c.rightMoves a

theorem ConcreteGame.mem_leftMoves_toLGame_of_mem {α : Type v} {c : ConcreteGame α} [∀ (a : α), Small.{u, v} ↑(c.leftMoves a)] [∀ (a : α), Small.{u, v} ↑(c.rightMoves a)] {a b : α} (hab : b ∈ c.leftMoves a) : c.toLGame b ∈ (c.toLGame a).leftMoves

theorem ConcreteGame.mem_rightMoves_toLGame_of_mem {α : Type v} {c : ConcreteGame α} [∀ (a : α), Small.{u, v} ↑(c.leftMoves a)] [∀ (a : α), Small.{u, v} ↑(c.rightMoves a)] {a b : α} (hab : b ∈ c.rightMoves a) : c.toLGame b ∈ (c.toLGame a).rightMoves

theorem ConcreteGame.neg_toLGame {α : Type v} {c : ConcreteGame α} [∀ (a : α), Small.{u, v} ↑(c.leftMoves a)] [∀ (a : α), Small.{u, v} ↑(c.rightMoves a)] (h : c.leftMoves = c.rightMoves) (a : α) : -c.toLGame a = c.toLGame a

Well-founded games

def ConcreteGame.moveRecOn {α : Type v} (c : ConcreteGame α) [H : IsWellFounded α c.IsOption] {motive : α → Sort u_1} (x : α) (mk : (x : α) → ((y : α) → y ∈ c.leftMoves x → motive y) → ((y : α) → y ∈ c.rightMoves 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

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

@[irreducible]

def ConcreteGame.toIGame {α : Type v} (c : ConcreteGame α) [∀ (a : α), Small.{u, v} ↑(c.leftMoves a)] [∀ (a : α), Small.{u, v} ↑(c.rightMoves a)] [H : IsWellFounded α c.IsOption] (a : α) : IGame

Turns a state of a ConcreteIGame into an IGame.

Equations

• c.toIGame a = {Set.range fun (b : ↑(c.leftMoves a)) => c.toIGame ↑b | Set.range fun (b : ↑(c.rightMoves a)) => c.toIGame ↑b}ᴵ

@[simp]

theorem ConcreteGame.leftMoves_toIGame {α : Type v} (c : ConcreteGame α) [∀ (a : α), Small.{u, v} ↑(c.leftMoves a)] [∀ (a : α), Small.{u, v} ↑(c.rightMoves a)] [H : IsWellFounded α c.IsOption] (a : α) : (c.toIGame a).leftMoves = c.toIGame '' c.leftMoves a

@[simp]

theorem ConcreteGame.rightMoves_toIGame {α : Type v} (c : ConcreteGame α) [∀ (a : α), Small.{u, v} ↑(c.leftMoves a)] [∀ (a : α), Small.{u, v} ↑(c.rightMoves a)] [H : IsWellFounded α c.IsOption] (a : α) : (c.toIGame a).rightMoves = c.toIGame '' c.rightMoves a

theorem ConcreteGame.mem_leftMoves_toIGame_of_mem {α : Type v} {c : ConcreteGame α} [∀ (a : α), Small.{u, v} ↑(c.leftMoves a)] [∀ (a : α), Small.{u, v} ↑(c.rightMoves a)] [H : IsWellFounded α c.IsOption] {a b : α} (hab : b ∈ c.leftMoves a) : c.toIGame b ∈ (c.toIGame a).leftMoves

theorem ConcreteGame.mem_rightMoves_toIGame_of_mem {α : Type v} {c : ConcreteGame α} [∀ (a : α), Small.{u, v} ↑(c.leftMoves a)] [∀ (a : α), Small.{u, v} ↑(c.rightMoves a)] [H : IsWellFounded α c.IsOption] {a b : α} (hab : b ∈ c.rightMoves a) : c.toIGame b ∈ (c.toIGame a).rightMoves

@[simp]

theorem ConcreteGame.toLGame_toIGame {α : Type v} (c : ConcreteGame α) [∀ (a : α), Small.{u, v} ↑(c.leftMoves a)] [∀ (a : α), Small.{u, v} ↑(c.rightMoves a)] [H : IsWellFounded α c.IsOption] (a : α) : IGame.toLGame (c.toIGame a) = c.toLGame a

theorem ConcreteGame.neg_toIGame {α : Type v} {c : ConcreteGame α} [∀ (a : α), Small.{u, v} ↑(c.leftMoves a)] [∀ (a : α), Small.{u, v} ↑(c.rightMoves a)] [H : IsWellFounded α c.IsOption] (h : c.leftMoves = c.rightMoves) (a : α) : -c.toIGame a = c.toIGame a

theorem ConcreteGame.impartial_toIGame {α : Type v} {c : ConcreteGame α} [∀ (a : α), Small.{u, v} ↑(c.leftMoves a)] [∀ (a : α), Small.{u, v} ↑(c.rightMoves a)] [H : IsWellFounded α c.IsOption] (h : c.leftMoves = c.rightMoves) (a : α) : (c.toIGame a).Impartial

Convenience constructors

def ConcreteGame.ofImpartial {α : Type v} (moves : α → Set α) : ConcreteGame α

Create a ConcreteGame from a single function used for the left and right moves.

Equations

• ConcreteGame.ofImpartial moves = { leftMoves := moves, rightMoves := moves }

@[simp]

theorem ConcreteGame.ofImpartial_leftMoves {α : Type v} (moves : α → Set α) : (ofImpartial moves).leftMoves = moves

@[simp]

theorem ConcreteGame.ofImpartial_rightMoves {α : Type v} (moves : α → Set α) : (ofImpartial moves).rightMoves = moves

theorem ConcreteGame.isOption_ofImpartial_iff {α : Type v} {moves : α → Set α} {a b : α} : (ofImpartial moves).IsOption a b ↔ a ∈ moves b

@[simp]

theorem ConcreteGame.isOption_ofImpartial {α : Type v} (moves : α → Set α) : (ofImpartial moves).IsOption = fun (a b : α) => a ∈ moves b

instance ConcreteGame.instSmallElemLeftMovesOfImpartial {α : Type v} (moves : α → Set α) [Hm : ∀ (a : α), Small.{u, v} ↑(moves a)] (a : α) : Small.{u, v} ↑((ofImpartial moves).leftMoves a)

instance ConcreteGame.instSmallElemRightMovesOfImpartial {α : Type v} (moves : α → Set α) [Hm : ∀ (a : α), Small.{u, v} ↑(moves a)] (a : α) : Small.{u, v} ↑((ofImpartial moves).rightMoves a)

@[simp]

theorem ConcreteGame.neg_toLGame_ofImpartial {α : Type v} (moves : α → Set α) [Hm : ∀ (a : α), Small.{u, v} ↑(moves a)] (a : α) : -(ofImpartial moves).toLGame a = (ofImpartial moves).toLGame a

instance ConcreteGame.impartial_toIGame_ofImpartial {α : Type v} (moves : α → Set α) [Hm : ∀ (a : α), Small.{u, v} ↑(moves a)] [IsWellFounded α (ofImpartial moves).IsOption] (a : α) : ((ofImpartial moves).toIGame a).Impartial

@[simp]

theorem ConcreteGame.neg_toIGame_ofImpartial {α : Type v} (moves : α → Set α) [Hm : ∀ (a : α), Small.{u, v} ↑(moves a)] [IsWellFounded α (ofImpartial moves).IsOption] (a : α) : -(ofImpartial moves).toIGame a = (ofImpartial moves).toIGame a