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 set.Iio 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. You can use to_left_moves_nim
and
to_right_moves_nim
to convert an ordinal less than o
into a left or right move of nim o
, and
vice versa.
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
- pgame.nim o₁ = let f : (quotient.out o₁).α → pgame := λ (o₂ : (quotient.out o₁).α), pgame.nim (ordinal.typein (quotient.out o₁).r o₂) in pgame.mk (quotient.out o₁).α (quotient.out o₁).α f f
Instances for pgame.nim
Turns an ordinal less than o
into a left move for nim o
and viceversa.
Equations
- pgame.to_left_moves_nim = o.enum_iso_out.to_equiv.trans (equiv.cast pgame.to_left_moves_nim._proof_1)
Turns an ordinal less than o
into a right move for nim o
and viceversa.
Equations
- pgame.to_right_moves_nim = o.enum_iso_out.to_equiv.trans (equiv.cast pgame.to_right_moves_nim._proof_1)
nim 0
has exactly the same moves as 0
.
Equations
Equations
- pgame.unique_nim_one_left_moves = (equiv.cast pgame.unique_nim_one_left_moves._proof_1).unique
Equations
- pgame.unique_nim_one_right_moves = (equiv.cast pgame.unique_nim_one_right_moves._proof_1).unique
nim 1
has exactly the same moves as star
.
Equations
- pgame.nim_one_relabelling = pgame.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).α), pgame.nim (ordinal.typein has_lt.lt o₂)) (λ (o₂ : (quotient.out 1).α), pgame.nim (ordinal.typein has_lt.lt o₂))).left_moves), _.mpr pgame.nim_zero_relabelling) (λ (j : (pgame.mk (quotient.out 1).α (quotient.out 1).α (λ (o₂ : (quotient.out 1).α), pgame.nim (ordinal.typein has_lt.lt o₂)) (λ (o₂ : (quotient.out 1).α), pgame.nim (ordinal.typein has_lt.lt o₂))).right_moves), _.mpr pgame.nim_zero_relabelling))
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