mathlib3documentation

set_theory.game.state

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 (S : Type u) :
• turn_bound : S
• L : S
• R : S
• left_bound : {s t : S},
• right_bound : {s t : S},

pgame_state S describes how to interpret s : S as a state of a combinatorial game. Use pgame.of_state s or game.of_state 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 of this typeclass
Instances of other typeclasses for pgame.state
• pgame.state.has_sizeof_inst
theorem pgame.turn_bound_ne_zero_of_left_move {S : Type u} [pgame.state S] {s t : S} (m : t ) :
theorem pgame.turn_bound_ne_zero_of_right_move {S : Type u} [pgame.state S] {s t : S} (m : t ) :
theorem pgame.turn_bound_of_left {S : Type u} [pgame.state S] {s t : S} (m : t ) (n : ) (h : n + 1) :
theorem pgame.turn_bound_of_right {S : Type u} [pgame.state S] {s t : S} (m : t ) (n : ) (h : n + 1) :
def pgame.of_state_aux {S : Type u} [pgame.state S] (n : ) (s : S) (h : n) :

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

Equations
Instances for pgame.of_state_aux
def pgame.of_state_aux_relabelling {S : Type u} [pgame.state S] (s : S) (n m : ) (hn : n) (hm : m) :
hn).relabelling hm)

Two different (valid) turn bounds give equivalent games.

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

Construct a combinatorial pgame from a state.

Equations
Instances for pgame.of_state
def pgame.left_moves_of_state_aux {S : Type u} [pgame.state S] (n : ) {s : S} (h : n) :
h).left_moves {t // t

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

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

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

Equations
def pgame.right_moves_of_state_aux {S : Type u} [pgame.state S] (n : ) {s : S} (h : n) :
h).right_moves {t // t

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

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

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

Equations
def pgame.relabelling_move_left_aux {S : Type u} [pgame.state S] (n : ) {s : S} (h : n) (t : h).left_moves) :

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

Equations

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

Equations
def pgame.relabelling_move_right_aux {S : Type u} [pgame.state S] (n : ) {s : S} (h : n) (t : h).right_moves) :

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

Equations

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

Equations
@[protected, instance]
def pgame.fintype_left_moves_of_state_aux {S : Type u} [pgame.state S] (n : ) (s : S) (h : n) :
Equations
@[protected, instance]
def pgame.fintype_right_moves_of_state_aux {S : Type u} [pgame.state S] (n : ) (s : S) (h : n) :
Equations
@[protected, instance]
def pgame.short_of_state_aux {S : Type u} [pgame.state S] (n : ) {s : S} (h : n) :
h).short
Equations
@[protected, instance]
def pgame.short_of_state {S : Type u} [pgame.state S] (s : S) :
Equations
def game.of_state {S : Type u} [pgame.state S] (s : S) :

Construct a combinatorial game from a state.

Equations