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]
- turn_bound : S → ℕ
- L : S → finset S
- R : S → finset S
- left_bound : ∀ {s t : S}, t ∈ pgame.state.L s → pgame.state.turn_bound t < pgame.state.turn_bound s
- right_bound : ∀ {s t : S}, t ∈ pgame.state.R s → pgame.state.turn_bound t < pgame.state.turn_bound s
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_ne_zero_of_left_move
{S : Type u}
[pgame.state S]
{s t : S} :
t ∈ pgame.state.L s → pgame.state.turn_bound s ≠ 0
theorem
pgame.turn_bound_ne_zero_of_right_move
{S : Type u}
[pgame.state S]
{s t : S} :
t ∈ pgame.state.R s → pgame.state.turn_bound s ≠ 0
theorem
pgame.turn_bound_of_left
{S : Type u}
[pgame.state S]
{s t : S}
(m : t ∈ pgame.state.L s)
(n : ℕ) :
pgame.state.turn_bound s ≤ n + 1 → pgame.state.turn_bound t ≤ n
theorem
pgame.turn_bound_of_right
{S : Type u}
[pgame.state S]
{s t : S}
(m : t ∈ pgame.state.R s)
(n : ℕ) :
pgame.state.turn_bound s ≤ n + 1 → pgame.state.turn_bound t ≤ n
def
pgame.of_aux
{S : Type u}
[pgame.state S]
(n : ℕ)
(s : S) :
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
- pgame.of_aux (n + 1) s h = pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), pgame.of_aux n ↑t _) (λ (t : {t // t ∈ pgame.state.R s}), pgame.of_aux n ↑t _)
- pgame.of_aux 0 s h = pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)
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) :
(pgame.of_aux n s hn).relabelling (pgame.of_aux m s hm)
Two different (valid) turn bounds give equivalent games.
Equations
- pgame.of_aux_relabelling s (n + 1) (m + 1) hn hm = id (pgame.relabelling.mk (equiv.refl (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), pgame.of_aux n ↑t _) (λ (t : {t // t ∈ pgame.state.R s}), pgame.of_aux n ↑t _)).left_moves) (equiv.refl (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), pgame.of_aux n ↑t _) (λ (t : {t // t ∈ pgame.state.R s}), pgame.of_aux n ↑t _)).right_moves) (λ (i : (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), pgame.of_aux n ↑t _) (λ (t : {t // t ∈ pgame.state.R s}), pgame.of_aux n ↑t _)).left_moves), pgame.of_aux_relabelling ↑i n m _ _) (λ (j : (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), pgame.of_aux m ↑t _) (λ (t : {t // t ∈ pgame.state.R s}), pgame.of_aux m ↑t _)).right_moves), pgame.of_aux_relabelling ↑(⇑((equiv.refl (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), pgame.of_aux n ↑t _) (λ (t : {t // t ∈ pgame.state.R s}), pgame.of_aux n ↑t _)).right_moves).symm) j) n m _ _))
- pgame.of_aux_relabelling s (n + 1) 0 hn hm = id (pgame.relabelling.mk (equiv.refl (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), pgame.of_aux n ↑t _) (λ (t : {t // t ∈ pgame.state.R s}), pgame.of_aux n ↑t _)).left_moves) (equiv.refl (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), pgame.of_aux n ↑t _) (λ (t : {t // t ∈ pgame.state.R s}), pgame.of_aux n ↑t _)).right_moves) (λ (i : (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), pgame.of_aux n ↑t _) (λ (t : {t // t ∈ pgame.state.R s}), pgame.of_aux n ↑t _)).left_moves), id (λ (i : {t // t ∈ pgame.state.L s}), false.rec (((pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), pgame.of_aux n ↑t _) (λ (t : {t // t ∈ pgame.state.R s}), pgame.of_aux n ↑t _)).move_left i).relabelling ((pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).move_left (⇑(equiv.refl (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), pgame.of_aux n ↑t _) (λ (t : {t // t ∈ pgame.state.R s}), pgame.of_aux n ↑t _)).left_moves) i))) _) i) (λ (j : (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).right_moves), id (λ (j : {t // t ∈ pgame.state.R s}), false.rec (((pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), pgame.of_aux n ↑t _) (λ (t : {t // t ∈ pgame.state.R s}), pgame.of_aux n ↑t _)).move_right (⇑((equiv.refl (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), pgame.of_aux n ↑t _) (λ (t : {t // t ∈ pgame.state.R s}), pgame.of_aux n ↑t _)).right_moves).symm) j)).relabelling ((pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).move_right j)) _) j))
- pgame.of_aux_relabelling s 0 (m + 1) hn hm = id (pgame.relabelling.mk (equiv.refl (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).left_moves) (equiv.refl (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).right_moves) (λ (i : (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).left_moves), id (λ (i : {t // t ∈ pgame.state.L s}), false.rec (((pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).move_left i).relabelling ((pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), pgame.of_aux m ↑t _) (λ (t : {t // t ∈ pgame.state.R s}), pgame.of_aux m ↑t _)).move_left (⇑(equiv.refl (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).left_moves) i))) _) i) (λ (j : (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), pgame.of_aux m ↑t _) (λ (t : {t // t ∈ pgame.state.R s}), pgame.of_aux m ↑t _)).right_moves), id (λ (j : {t // t ∈ pgame.state.R s}), false.rec (((pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).move_right (⇑((equiv.refl (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).right_moves).symm) j)).relabelling ((pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), pgame.of_aux m ↑t _) (λ (t : {t // t ∈ pgame.state.R s}), pgame.of_aux m ↑t _)).move_right j)) _) j))
- pgame.of_aux_relabelling s 0 0 hn hm = id (pgame.relabelling.mk (equiv.refl (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).left_moves) (equiv.refl (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).right_moves) (λ (i : (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).left_moves), id (λ (i : {t // t ∈ pgame.state.L s}), false.rec (((pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).move_left i).relabelling ((pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).move_left (⇑(equiv.refl (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).left_moves) i))) _) i) (λ (j : (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).right_moves), id (λ (j : {t // t ∈ pgame.state.R s}), false.rec (((pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).move_right (⇑((equiv.refl (pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).right_moves).symm) j)).relabelling ((pgame.mk {t // t ∈ pgame.state.L s} {t // t ∈ pgame.state.R s} (λ (t : {t // t ∈ pgame.state.L s}), false.rec pgame _) (λ (t : {t // t ∈ pgame.state.R s}), false.rec pgame _)).move_right j)) _) j))
Construct a combinatorial pgame from a state.
Equations
- pgame.of s = pgame.of_aux (pgame.state.turn_bound s) s _
def
pgame.left_moves_of_aux
{S : Type u}
[pgame.state S]
(n : ℕ)
{s : S}
(h : pgame.state.turn_bound s ≤ n) :
(pgame.of_aux n s h).left_moves ≃ {t // t ∈ pgame.state.L s}
The equivalence between left_moves for a pgame constructed using of_aux _ s _, and L s.
Equations
- pgame.left_moves_of_aux n h = nat.rec (λ (h : pgame.state.turn_bound s ≤ 0), equiv.refl (pgame.of_aux 0 s h).left_moves) (λ (n_n : ℕ) (n_ih : Π (h : pgame.state.turn_bound s ≤ n_n), (pgame.of_aux n_n s h).left_moves ≃ {t // t ∈ pgame.state.L s}) (h : pgame.state.turn_bound s ≤ n_n.succ), equiv.refl (pgame.of_aux n_n.succ s h).left_moves) n h
def
pgame.left_moves_of
{S : Type u}
[pgame.state S]
(s : S) :
(pgame.of s).left_moves ≃ {t // t ∈ pgame.state.L 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) :
(pgame.of_aux n s h).right_moves ≃ {t // t ∈ pgame.state.R s}
The equivalence between right_moves for a pgame constructed using of_aux _ s _, and R s.
Equations
- pgame.right_moves_of_aux n h = nat.rec (λ (h : pgame.state.turn_bound s ≤ 0), equiv.refl (pgame.of_aux 0 s h).right_moves) (λ (n_n : ℕ) (n_ih : Π (h : pgame.state.turn_bound s ≤ n_n), (pgame.of_aux n_n s h).right_moves ≃ {t // t ∈ pgame.state.R s}) (h : pgame.state.turn_bound s ≤ n_n.succ), equiv.refl (pgame.of_aux n_n.succ s h).right_moves) n h
def
pgame.right_moves_of
{S : Type u}
[pgame.state S]
(s : S) :
(pgame.of s).right_moves ≃ {t // t ∈ pgame.state.R s}
The equivalence between right_moves for a pgame constructed using of s, and R s.
Equations
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_aux n s h).left_moves) :
((pgame.of_aux n s h).move_left t).relabelling (pgame.of_aux (n - 1) ↑(⇑(pgame.left_moves_of_aux n h) t) _)
The relabelling showing move_left applied to a game constructed using of_aux
has itself been constructed using of_aux.
Equations
- pgame.relabelling_move_left_aux n h t = nat.rec (λ (h : pgame.state.turn_bound s ≤ 0) (t : (pgame.of_aux 0 s h).left_moves), false.rec (((pgame.of_aux 0 s h).move_left t).relabelling (pgame.of_aux (0 - 1) ↑(⇑(pgame.left_moves_of_aux 0 h) t) _)) _) (λ (n_n : ℕ) (n_ih : Π (h : pgame.state.turn_bound s ≤ n_n) (t : (pgame.of_aux n_n s h).left_moves), ((pgame.of_aux n_n s h).move_left t).relabelling (pgame.of_aux (n_n - 1) ↑(⇑(pgame.left_moves_of_aux n_n h) t) _)) (h : pgame.state.turn_bound s ≤ n_n.succ) (t : (pgame.of_aux n_n.succ s h).left_moves), pgame.relabelling.refl ((pgame.of_aux n_n.succ s h).move_left t)) n h t
def
pgame.relabelling_move_left
{S : Type u}
[pgame.state S]
(s : S)
(t : (pgame.of s).left_moves) :
((pgame.of s).move_left t).relabelling (pgame.of ↑((pgame.left_moves_of s).to_fun t))
The relabelling showing move_left applied to a game constructed using of
has itself been constructed using of.
Equations
- pgame.relabelling_move_left s t = (pgame.relabelling_move_left_aux (pgame.state.turn_bound s) _ t).trans (pgame.of_aux_relabelling ↑(⇑(pgame.left_moves_of_aux (pgame.state.turn_bound s) _) t) (pgame.state.turn_bound s - 1) (pgame.state.turn_bound ↑((pgame.left_moves_of s).to_fun t)) _ _)
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_aux n s h).right_moves) :
((pgame.of_aux n s h).move_right t).relabelling (pgame.of_aux (n - 1) ↑(⇑(pgame.right_moves_of_aux n h) t) _)
The relabelling showing move_right applied to a game constructed using of_aux
has itself been constructed using of_aux.
Equations
- pgame.relabelling_move_right_aux n h t = nat.rec (λ (h : pgame.state.turn_bound s ≤ 0) (t : (pgame.of_aux 0 s h).right_moves), false.rec (((pgame.of_aux 0 s h).move_right t).relabelling (pgame.of_aux (0 - 1) ↑(⇑(pgame.right_moves_of_aux 0 h) t) _)) _) (λ (n_n : ℕ) (n_ih : Π (h : pgame.state.turn_bound s ≤ n_n) (t : (pgame.of_aux n_n s h).right_moves), ((pgame.of_aux n_n s h).move_right t).relabelling (pgame.of_aux (n_n - 1) ↑(⇑(pgame.right_moves_of_aux n_n h) t) _)) (h : pgame.state.turn_bound s ≤ n_n.succ) (t : (pgame.of_aux n_n.succ s h).right_moves), pgame.relabelling.refl ((pgame.of_aux n_n.succ s h).move_right t)) n h t
def
pgame.relabelling_move_right
{S : Type u}
[pgame.state S]
(s : S)
(t : (pgame.of s).right_moves) :
((pgame.of s).move_right t).relabelling (pgame.of ↑((pgame.right_moves_of s).to_fun t))
The relabelling showing move_right applied to a game constructed using of
has itself been constructed using of.
Equations
- pgame.relabelling_move_right s t = (pgame.relabelling_move_right_aux (pgame.state.turn_bound s) _ t).trans (pgame.of_aux_relabelling ↑(⇑(pgame.right_moves_of_aux (pgame.state.turn_bound s) _) t) (pgame.state.turn_bound s - 1) (pgame.state.turn_bound ↑((pgame.right_moves_of s).to_fun t)) _ _)
@[instance]
def
pgame.fintype_left_moves_of_aux
{S : Type u}
[pgame.state S]
(n : ℕ)
(s : S)
(h : pgame.state.turn_bound s ≤ n) :
fintype (pgame.of_aux n s h).left_moves
Equations
- pgame.fintype_left_moves_of_aux n s h = fintype.of_equiv {t // t ∈ pgame.state.L s} (pgame.left_moves_of_aux n h).symm
@[instance]
def
pgame.fintype_right_moves_of_aux
{S : Type u}
[pgame.state S]
(n : ℕ)
(s : S)
(h : pgame.state.turn_bound s ≤ n) :
fintype (pgame.of_aux n s h).right_moves
Equations
- pgame.fintype_right_moves_of_aux n s h = fintype.of_equiv {t // t ∈ pgame.state.R s} (pgame.right_moves_of_aux n h).symm
@[instance]
def
pgame.short_of_aux
{S : Type u}
[pgame.state S]
(n : ℕ)
{s : S}
(h : pgame.state.turn_bound s ≤ n) :
(pgame.of_aux n s h).short
Equations
- pgame.short_of_aux (n + 1) h = pgame.short.mk' (λ (i : (pgame.of_aux (n + 1) s h).left_moves), pgame.short_of_relabelling (pgame.relabelling_move_left_aux (n + 1) h i).symm (pgame.short_of_aux n _)) (λ (j : (pgame.of_aux (n + 1) s h).right_moves), pgame.short_of_relabelling (pgame.relabelling_move_right_aux (n + 1) h j).symm (pgame.short_of_aux n _))
- pgame.short_of_aux 0 h = pgame.short.mk' (λ (i : (pgame.of_aux 0 s h).left_moves), false.rec ((pgame.of_aux 0 s h).move_left i).short _) (λ (j : (pgame.of_aux 0 s h).right_moves), false.rec ((pgame.of_aux 0 s h).move_right j).short _)
@[instance]