Nim and the Sprague-Grundy theorem #
This file contains the definition for nim for any ordinal O
. In the game of nim O₁
both players
may move to nim O₂
for any O₂ < O₁
.
We also define a Grundy value for an impartial game G
and prove the Sprague-Grundy theorem, that
G
is equivalent to nim (grundy_value G)
.
Finally, we compute the sum of finite Grundy numbers: if G
and H
have Grundy values n
and m
,
where n
and m
are natural numbers, then G + H
has the Grundy value n xor m
.
Implementation details #
The pen-and-paper definition of nim defines the possible moves of nim O
to be {O' | O' < O}
.
However, this definition does not work for us because it would make the type of nim
ordinal.{u} → pgame.{u + 1}
, which would make it impossible for us to state the Sprague-Grundy
theorem, since that requires the type of nim
to be ordinal.{u} → pgame.{u}
. For this reason, we
instead use O.out.α
for the possible moves, which makes proofs significantly more messy and
tedious, but avoids the universe bump.
The lemma nim_def
is somewhat prone to produce "motive is not type correct" errors. If you run
into this problem, you may find the lemmas exists_ordinal_move_left_eq
and exists_move_left_eq
useful.
ordinal.out'
has the sole purpose of making nim
computable. It performs the same job as
quotient.out
but is specific to ordinals.
Equations
- o.out' = {α := (quotient.out o).α, r := has_lt.lt (preorder.to_has_lt (quotient.out o).α), wo := _}
The definition of single-heap nim, which can be viewed as a pile of stones where each player can take a positive number of stones from it on their turn.
Equations
Instances for nim
Equations
- pgame.nim.left_moves.unique = pgame.nim.left_moves.unique._proof_2.mpr ordinal.unique_out_one
Equations
- pgame.nim.right_moves.unique = pgame.nim.right_moves.unique._proof_2.mpr ordinal.unique_out_one
nim 0
has exactly the same moves as 0
.
Equations
nim 1
has exactly the same moves as star
.
Equations
- pgame.nim.nim_one_relabelling = pgame.nim.nim_one_relabelling._proof_2.mpr (pgame.relabelling.mk (id (equiv.equiv_of_unique (quotient.out 1).α punit)) (id (equiv.equiv_of_unique (quotient.out 1).α punit)) (λ (i : (pgame.mk (quotient.out 1).α (quotient.out 1).α (λ (O₂ : (quotient.out 1).α), nim (ordinal.typein has_lt.lt O₂)) (λ (O₂ : (quotient.out 1).α), nim (ordinal.typein has_lt.lt O₂))).left_moves), _.mpr pgame.nim.nim_zero_relabelling) (λ (j : pgame.star.right_moves), _.mpr pgame.nim.nim_zero_relabelling))
Turns an ordinal less than O
into a left move for nim O
and viceversa.
Equations
- pgame.nim.to_left_moves_nim = O.enum_iso_out.to_equiv.trans (equiv.cast pgame.nim.to_left_moves_nim._proof_1)
Turns an ordinal less than O
into a right move for nim O
and viceversa.
Equations
- pgame.nim.to_right_moves_nim = O.enum_iso_out.to_equiv.trans (equiv.cast pgame.nim.to_right_moves_nim._proof_1)
The Grundy value of an impartial game, the ordinal which corresponds to the game of nim that the game is equivalent to
Equations
- G.grundy_value = ordinal.mex (λ (i : G.left_moves), (G.move_left i).grundy_value)
The Sprague-Grundy theorem which states that every impartial game is equivalent to a game of nim, namely the game of nim corresponding to the games Grundy value