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.

source
@[class]
structure pgame.state (S : Type u) :
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
source
theorem pgame.turn_bound_ne_zero_of_left_move {S : Type u} [pgame.state S] {s t : S} (m : t ∈ pgame.state.L s) :
pgame.state.turn_bound s ≠ 0
source
theorem pgame.turn_bound_ne_zero_of_right_move {S : Type u} [pgame.state S] {s t : S} (m : t ∈ pgame.state.R s) :
pgame.state.turn_bound s ≠ 0
source
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) :
pgame.state.turn_bound t ≤ n
source
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) :
pgame.state.turn_bound t ≤ n
source
def pgame.of_state_aux {S : Type u} [pgame.state S] (n : ℕ) (s : S) (h : pgame.state.turn_bound s ≤ n) :
pgame

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
source
def pgame.of_state_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) :
(pgame.of_state_aux n s hn).relabelling (pgame.of_state_aux m s hm)

Two different (valid) turn bounds give equivalent games.

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

Construct a combinatorial pgame from a state.

Equations
Instances for pgame.of_state
source
def pgame.left_moves_of_state_aux {S : Type u} [pgame.state S] (n : ℕ) {s : S} (h : pgame.state.turn_bound s ≤ n) :
(pgame.of_state_aux n s h).left_moves ≃ {t // t ∈ pgame.state.L s}

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

Equations
source
def pgame.left_moves_of_state {S : Type u} [pgame.state S] (s : S) :
(pgame.of_state s).left_moves ≃ {t // t ∈ pgame.state.L s}

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

Equations
source
def pgame.right_moves_of_state_aux {S : Type u} [pgame.state S] (n : ℕ) {s : S} (h : pgame.state.turn_bound s ≤ n) :
(pgame.of_state_aux n s h).right_moves ≃ {t // t ∈ pgame.state.R s}

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

Equations
source
def pgame.right_moves_of_state {S : Type u} [pgame.state S] (s : S) :
(pgame.of_state s).right_moves ≃ {t // t ∈ pgame.state.R s}

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

Equations
source
def pgame.relabelling_move_left_aux {S : Type u} [pgame.state S] (n : ℕ) {s : S} (h : pgame.state.turn_bound s ≤ n) (t : (pgame.of_state_aux n s h).left_moves) :
((pgame.of_state_aux n s h).move_left t).relabelling (pgame.of_state_aux (n - 1) ↑(⇑(pgame.left_moves_of_state_aux n h) t) _)

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

Equations
source
def pgame.relabelling_move_left {S : Type u} [pgame.state S] (s : S) (t : (pgame.of_state s).left_moves) :
((pgame.of_state s).move_left t).relabelling (pgame.of_state ↑((pgame.left_moves_of_state s).to_fun t))

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

Equations
source
def pgame.relabelling_move_right_aux {S : Type u} [pgame.state S] (n : ℕ) {s : S} (h : pgame.state.turn_bound s ≤ n) (t : (pgame.of_state_aux n s h).right_moves) :
((pgame.of_state_aux n s h).move_right t).relabelling (pgame.of_state_aux (n - 1) ↑(⇑(pgame.right_moves_of_state_aux n h) t) _)

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

Equations
source
def pgame.relabelling_move_right {S : Type u} [pgame.state S] (s : S) (t : (pgame.of_state s).right_moves) :
((pgame.of_state s).move_right t).relabelling (pgame.of_state ↑((pgame.right_moves_of_state s).to_fun t))

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

Equations
source
@[protected, instance]
def pgame.fintype_left_moves_of_state_aux {S : Type u} [pgame.state S] (n : ℕ) (s : S) (h : pgame.state.turn_bound s ≤ n) :
fintype (pgame.of_state_aux n s h).left_moves
Equations
source
@[protected, instance]
def pgame.fintype_right_moves_of_state_aux {S : Type u} [pgame.state S] (n : ℕ) (s : S) (h : pgame.state.turn_bound s ≤ n) :
fintype (pgame.of_state_aux n s h).right_moves
Equations
source
@[protected, instance]
def pgame.short_of_state_aux {S : Type u} [pgame.state S] (n : ℕ) {s : S} (h : pgame.state.turn_bound s ≤ n) :
(pgame.of_state_aux n s h).short
Equations
source
@[protected, instance]
def pgame.short_of_state {S : Type u} [pgame.state S] (s : S) :
(pgame.of_state s).short
Equations
source
def game.of_state {S : Type u} [pgame.state S] (s : S) :
game

Construct a combinatorial game from a state.

Equations