Combinatorial games from a type of states

A "concrete" game is a type of states endowed with well-founded move relations for the left and right players. This is often a more convenient representation for a game, which can then be used to define a IGame.

class ConcreteGame (α : Type u_2) : Type u_2

A "concrete" game is a type of states endowed with well-founded move relations for the left and right players.

• relLeft : α → α → Prop

  The move relation for the left player.

• relRight : α → α → Prop

  The move relation for the right player.

• isWellFounded_rel : IsWellFounded α fun (a b : α) => relLeft a b ∨ relRight a b

  The move relation is well-founded.

def ConcreteGame.«term_≺ₗ_» : Lean.TrailingParserDescr

Equations

• ConcreteGame.«term_≺ₗ_» = Lean.ParserDescr.trailingNode `ConcreteGame.«term_≺ₗ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≺ₗ ") (Lean.ParserDescr.cat `term 51))

def ConcreteGame.«term_≺ᵣ_» : Lean.TrailingParserDescr

Equations

• ConcreteGame.«term_≺ᵣ_» = Lean.ParserDescr.trailingNode `ConcreteGame.«term_≺ᵣ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≺ᵣ ") (Lean.ParserDescr.cat `term 51))

theorem ConcreteGame.subrelation_relLeft {α : Type u_1} [ConcreteGame α] : Subrelation relLeft fun (a b : α) => relLeft a b ∨ relRight a b

theorem ConcreteGame.subrelation_relRight {α : Type u_1} [ConcreteGame α] : Subrelation relRight fun (a b : α) => relLeft a b ∨ relRight a b

instance ConcreteGame.instIsWellFoundedRelLeft {α : Type u_1} [ConcreteGame α] : IsWellFounded α relLeft

instance ConcreteGame.instIsWellFoundedRelRight {α : Type u_1} [ConcreteGame α] : IsWellFounded α relRight

def ConcreteGame.ofImpartial {α : Type u_1} (r : α → α → Prop) [h : IsWellFounded α r] : ConcreteGame α

Defines a concrete game from a single relation, to be used for both players.

Equations

• ConcreteGame.ofImpartial r = { relLeft := r, relRight := r, isWellFounded_rel := ⋯ }

@[irreducible]

def ConcreteGame.toIGame {α : Type u_1} [ConcreteGame α] (a : α) : IGame

Turns a state of a ConcreteGame into an IGame.

Equations

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

theorem ConcreteGame.toIGame_def {α : Type u_1} [ConcreteGame α] (a : α) : toIGame a = {toIGame '' {b : α | relLeft b a} | toIGame '' {b : α | relRight b a}}ᴵ

@[simp]

theorem ConcreteGame.leftMoves_toIGame {α : Type u_1} [ConcreteGame α] (a : α) : (toIGame a).leftMoves = toIGame '' {b : α | relLeft b a}

@[simp]

theorem ConcreteGame.rightMoves_toIGame {α : Type u_1} [ConcreteGame α] (a : α) : (toIGame a).rightMoves = toIGame '' {b : α | relRight b a}

theorem ConcreteGame.mem_leftMoves_toIGame_of_relLeft {α : Type u_1} [ConcreteGame α] {a b : α} (hab : relLeft b a) : toIGame b ∈ (toIGame a).leftMoves

theorem ConcreteGame.mem_rightMoves_toIGame_of_relRight {α : Type u_1} [ConcreteGame α] {a b : α} (hab : relRight b a) : toIGame b ∈ (toIGame a).rightMoves

@[irreducible]

theorem ConcreteGame.neg_toIGame {α : Type u_1} [ConcreteGame α] (h : relLeft = relRight) (a : α) : -toIGame a = toIGame a

@[irreducible]

theorem ConcreteGame.impartial_toIGame {α : Type u_1} [ConcreteGame α] (h : relLeft = relRight) (a : α) : (toIGame a).Impartial

def ToImpartial (α : Type u_2) : Type u_2

A type alias to turn a concrete game impartial, by allowing both players to perform each other's moves.

Equations

• ToImpartial α = α

def toImpartial {α : Type u_1} : α ≃ ToImpartial α

Equations

• toImpartial = Equiv.refl α

def ofImpartial {α : Type u_1} : ToImpartial α ≃ α

Equations

• ofImpartial = Equiv.refl (ToImpartial α)

@[simp]

theorem ofImpartial_toImpartial {α : Type u_1} (x : α) : ofImpartial (toImpartial x) = x

@[simp]

theorem toImpartial_ofImpartial {α : Type u_1} (x : ToImpartial α) : toImpartial (ofImpartial x) = x

instance instConcreteGameToImpartial {α : Type u_1} [ConcreteGame α] : ConcreteGame (ToImpartial α)

Equations

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

instance instImpartialToIGameToImpartialCoeEquivToImpartial {α : Type u_1} [ConcreteGame α] (x : α) : (ConcreteGame.toIGame (toImpartial x)).Impartial

theorem ToImpartial.relLeft_iff {α : Type u_1} {x y : ToImpartial α} [ConcreteGame α] : ConcreteGame.relLeft x y ↔ ConcreteGame.relLeft (ofImpartial x) (ofImpartial y) ∨ ConcreteGame.relRight (ofImpartial x) (ofImpartial y)

theorem ToImpartial.relRight_iff {α : Type u_1} {x y : ToImpartial α} [ConcreteGame α] : ConcreteGame.relRight x y ↔ ConcreteGame.relLeft (ofImpartial x) (ofImpartial y) ∨ ConcreteGame.relRight (ofImpartial x) (ofImpartial y)