mathlib3 documentation

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) :

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_of_left {S : Type u} [pgame.state S] {s t : S} (m : t pgame.state.L s) (n : ) (h : pgame.state.turn_bound s n + 1) :
theorem pgame.turn_bound_of_right {S : Type u} [pgame.state S] {s t : S} (m : t pgame.state.R s) (n : ) (h : pgame.state.turn_bound s n + 1) :
def pgame.of_state_aux {S : Type u} [pgame.state S] (n : ) (s : S) (h : pgame.state.turn_bound s 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

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

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

Equations

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

Equations

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

Equations

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

Equations

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_right applied to a game constructed using of_state_aux has itself been constructed using of_state_aux.

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