# Documentation

Mathlib.SetTheory.Game.Short

# Short games #

A combinatorial game is Short [Conway, ch.9][conway2001] if it has only finitely many positions. In particular, this means there is a finite set of moves at every point.

We prove that the order relations ≤ and <, and the equivalence relation ≈, are decidable on short games, although unfortunately in practice decide doesn't seem to be able to prove anything using these instances.

class inductive SetTheory.PGame.Short :
SetTheory.PGameType (u + 1)
• mk: {α β : Type u} → {L : } → {R : } → ((i : α) → ) → ((j : β) → ) → [inst : ] → [inst : ] → SetTheory.PGame.Short ()

A short game is a game with a finite set of moves at every turn.

Instances
def SetTheory.PGame.Short.mk' {x : SetTheory.PGame} (sL : ) (sR : ) :

A synonym for Short.mk that specifies the pgame in an implicit argument.

Instances For
def SetTheory.PGame.fintypeLeft {α : Type u} {β : Type u} {L : } {R : } [S : SetTheory.PGame.Short ()] :

Extracting the Fintype instance for the indexing type for Left's moves in a short game. This is an unindexed typeclass, so it can't be made a global instance.

Instances For
def SetTheory.PGame.fintypeRight {α : Type u} {β : Type u} {L : } {R : } [S : SetTheory.PGame.Short ()] :

Extracting the Fintype instance for the indexing type for Right's moves in a short game. This is an unindexed typeclass, so it can't be made a global instance.

Instances For
def SetTheory.PGame.moveLeftShort' {xl : Type u_1} {xr : Type u_1} (xL : ) (xR : ) [S : SetTheory.PGame.Short (SetTheory.PGame.mk xl xr xL xR)] (i : xl) :

Extracting the Short instance for a move by Left. This would be a dangerous instance potentially introducing new metavariables in typeclass search, so we only make it an instance locally.

Instances For
def SetTheory.PGame.moveRightShort' {xl : Type u_1} {xr : Type u_1} (xL : ) (xR : ) [S : SetTheory.PGame.Short (SetTheory.PGame.mk xl xr xL xR)] (j : xr) :

Extracting the Short instance for a move by Right. This would be a dangerous instance potentially introducing new metavariables in typeclass search, so we only make it an instance locally.

Instances For
def SetTheory.PGame.Short.ofIsEmpty {l : Type u_1} {r : Type u_1} {xL : } {xR : } [] [] :

Instances For
class inductive SetTheory.PGame.ListShort :
Type (u + 1)

Evidence that every PGame in a list is Short.

Instances
instance SetTheory.PGame.ListShort.cons (hd : SetTheory.PGame) [short_hd : ] (tl : ) [short_tl : ] :
instance SetTheory.PGame.listShortGet (L : ) (i : Fin ()) :
Equations
@[deprecated SetTheory.PGame.listShortGet]
instance SetTheory.PGame.listShortNthLe (L : ) (i : Fin ()) :
SetTheory.PGame.Short (List.nthLe L i (_ : i < ))

If x is a short game, and y is a relabelling of x, then y is also short.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
instance SetTheory.PGame.shortNat (n : ) :
Equations

Auxiliary construction of decidability instances. We build Decidable (x ≤ y) and Decidable (x ⧏ y) in a simultaneous induction. Instances for the two projections separately are provided below.

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