mathlib documentation

set_theory.game.state

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 dec_trivial. 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 set_theory/game/domineering for an example using this construction.

@[class]
structure pgame.state  :
Type uType u

pgame_state S describes how to interpret s : S as a state of a combinatorial game. Use pgame.of s or game.of s to construct the game.

pgame_state.L : S → finset S and pgame_state.R : S → finset S describe the states reachable by a move by Left or Right. pgame_state.turn_bound : S → ℕ gives an upper bound on the number of possible turns remaining from this state.

Instances
theorem pgame.turn_bound_of_left {S : Type u} [pgame.state S] {s t : S} (m : t pgame.state.L s) (n : ) :

theorem pgame.turn_bound_of_right {S : Type u} [pgame.state S] {s t : S} (m : t pgame.state.R s) (n : ) :

def pgame.of_aux {S : Type u} [pgame.state S] (n : ) (s : S) :

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

Equations
def pgame.of_aux_relabelling {S : Type u} [pgame.state S] (s : S) (n m : ) (hn : pgame.state.turn_bound s n) (hm : pgame.state.turn_bound s m) :

Two different (valid) turn bounds give equivalent games.

Equations
def pgame.of {S : Type u} [pgame.state S] :
S → pgame

Construct a combinatorial pgame from a state.

Equations
def pgame.left_moves_of_aux {S : Type u} [pgame.state S] (n : ) {s : S} (h : pgame.state.turn_bound s n) :

The equivalence between left_moves for a pgame constructed using of_aux _ s _, and L s.

Equations
def pgame.left_moves_of {S : Type u} [pgame.state S] (s : S) :

The equivalence between left_moves for a pgame constructed using of s, and L s.

Equations
def pgame.right_moves_of_aux {S : Type u} [pgame.state S] (n : ) {s : S} (h : pgame.state.turn_bound s n) :

The equivalence between right_moves for a pgame constructed using of_aux _ s _, and R s.

Equations
def pgame.right_moves_of {S : Type u} [pgame.state S] (s : S) :

The equivalence between right_moves for a pgame constructed using of s, and R s.

Equations

The relabelling showing move_left applied to a game constructed using of_aux has itself been constructed using of_aux.

Equations

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

Equations

The relabelling showing move_right applied to a game constructed using of_aux has itself been constructed using of_aux.

Equations

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

Equations
@[instance]
def pgame.short_of_aux {S : Type u} [pgame.state S] (n : ) {s : S} (h : pgame.state.turn_bound s n) :

Equations
@[instance]
def pgame.short_of {S : Type u} [pgame.state S] (s : S) :

Equations
def game.of {S : Type u} [pgame.state S] :
S → game

Construct a combinatorial game from a state.

Equations