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).
ordinal.out and ordinal.type_out' are required to make the definition of nim computable.
ordinal.out performs the same job as quotient.out but is specific to ordinals.
Equations
- o.out = {α := (quotient.out o).α, r := λ (x y : (quotient.out o).α), (quotient.out o).r x y, wo := _}
This is the same as ordinal.type_out but defined to use ordinal.out.
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.
This definition will be used in the proof of the Sprague-Grundy theorem. It takes a function from some type to ordinals and returns a nonempty set of ordinals with empty intersection with the image of the function. It is guaranteed that the smallest ordinal not in the image will be in the set, i.e. we can use this to find the mex.
Equations
- nim.nonmoves M = {O : ordinal | ¬∃ (a : α), M a = O}
The Grundy value of an impartial game, the ordinal which corresponds to the game of nim that the game is equivalent to
Equations
- nim.Grundy_value = λ (hG : G.impartial), ordinal.omin (nim.nonmoves (λ (i : G.left_moves), nim.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