# Games described via "the state of the board". #

We provide a simple mechanism for constructing combinatorial (pre-)games, by describing "the state of the board", and providing an upper bound on the number of turns remaining.

## Implementation notes #

We're very careful to produce a computable definition, so small games can be evaluated using decide. To achieve this, I've had to rely solely on induction on natural numbers: relying on general well-foundedness seems to be poisonous to computation?

See SetTheory/Game/Domineering for an example using this construction.

SetTheory.PGame.State S describes how to interpret s : S as a state of a combinatorial game. Use SetTheory.PGame.ofState s or SetTheory.Game.ofState s to construct the game.

SetTheory.PGame.State.l : S → Finset S and SetTheory.PGame.State.r : S → Finset S describe the states reachable by a move by Left or Right. SetTheory.PGame.State.turnBound : S → ℕ gives an upper bound on the number of possible turns remaining from this state.

• turnBound : S
• l : S
• r : S
• left_bound : ∀ {s t : S},
• right_bound : ∀ {s t : S},
Instances
theorem SetTheory.PGame.State.left_bound {S : Type u} [self : ] {s : S} {t : S} :
theorem SetTheory.PGame.State.right_bound {S : Type u} [self : ] {s : S} {t : S} :
theorem SetTheory.PGame.turnBound_ne_zero_of_left_move {S : Type u} {s : S} {t : S} (m : ) :
theorem SetTheory.PGame.turnBound_ne_zero_of_right_move {S : Type u} {s : S} {t : S} (m : ) :
theorem SetTheory.PGame.turnBound_of_left {S : Type u} {s : S} {t : S} (m : ) (n : ) (h : ) :
theorem SetTheory.PGame.turnBound_of_right {S : Type u} {s : S} {t : S} (m : ) (n : ) (h : ) :
def SetTheory.PGame.ofStateAux {S : Type u} (n : ) (s : S) :

Construct a PGame from a state and a (not necessarily optimal) bound on the number of turns remaining.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def SetTheory.PGame.ofStateAuxRelabelling {S : Type u} (s : S) (n : ) (m : ) (hn : ) (hm : ) :
().Relabelling ()

Two different (valid) turn bounds give equivalent games.

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

Construct a combinatorial PGame from a state.

Equations
Instances For
def SetTheory.PGame.leftMovesOfStateAux {S : Type u} (n : ) {s : S} (h : ) :
().LeftMoves { t : S // }

The equivalence between leftMoves for a PGame constructed using ofStateAux _ s _, and L s.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def SetTheory.PGame.leftMovesOfState {S : Type u} (s : S) :
.LeftMoves { t : S // }

The equivalence between leftMoves for a PGame constructed using ofState s, and l s.

Equations
Instances For
def SetTheory.PGame.rightMovesOfStateAux {S : Type u} (n : ) {s : S} (h : ) :
().RightMoves { t : S // }

The equivalence between rightMoves for a PGame constructed using ofStateAux _ s _, and R s.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def SetTheory.PGame.rightMovesOfState {S : Type u} (s : S) :
.RightMoves { t : S // }

The equivalence between rightMoves for a PGame constructed using ofState s, and R s.

Equations
Instances For
def SetTheory.PGame.relabellingMoveLeftAux {S : Type u} (n : ) {s : S} (h : ) (t : ().LeftMoves) :
(().moveLeft t).Relabelling (SetTheory.PGame.ofStateAux (n - 1) () )

The relabelling showing moveLeft applied to a game constructed using ofStateAux has itself been constructed using ofStateAux.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def SetTheory.PGame.relabellingMoveLeft {S : Type u} (s : S) (t : .LeftMoves) :
(.moveLeft t).Relabelling (SetTheory.PGame.ofState (.toFun t))

The relabelling showing moveLeft applied to a game constructed using of has itself been constructed using of.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def SetTheory.PGame.relabellingMoveRightAux {S : Type u} (n : ) {s : S} (h : ) (t : ().RightMoves) :
(().moveRight t).Relabelling (SetTheory.PGame.ofStateAux (n - 1) () )

The relabelling showing moveRight applied to a game constructed using ofStateAux has itself been constructed using ofStateAux.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def SetTheory.PGame.relabellingMoveRight {S : Type u} (s : S) (t : .RightMoves) :
(.moveRight t).Relabelling (SetTheory.PGame.ofState (.toFun t))

The relabelling showing moveRight applied to a game constructed using of has itself been constructed using of.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance SetTheory.PGame.fintypeLeftMovesOfStateAux {S : Type u} (n : ) (s : S) (h : ) :
Fintype ().LeftMoves
Equations
instance SetTheory.PGame.fintypeRightMovesOfStateAux {S : Type u} (n : ) (s : S) (h : ) :
Fintype ().RightMoves
Equations
instance SetTheory.PGame.shortOfStateAux {S : Type u} (n : ) {s : S} (h : ) :
().Short
Equations
• One or more equations did not get rendered due to their size.
instance SetTheory.PGame.shortOfState {S : Type u} (s : S) :
.Short
Equations
• = id inferInstance

Construct a combinatorial Game from a state.

Equations
Instances For