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 (grundyValue 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} → SetTheory.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} → SetTheory.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
- One or more equations did not get rendered due to their size.
Instances For
Turns an ordinal less than o into a left move for nim o and viceversa.
Equations
- SetTheory.PGame.toLeftMovesNim = (Ordinal.enumIsoOut o).trans (Equiv.cast ⋯)
Instances For
Turns an ordinal less than o into a right move for nim o and viceversa.
Equations
- SetTheory.PGame.toRightMovesNim = (Ordinal.enumIsoOut o).trans (Equiv.cast ⋯)
Instances For
A recursion principle for left moves of a nim game.
Equations
- SetTheory.PGame.leftMovesNimRecOn i H = Eq.mpr ⋯ (H (Ordinal.typein (fun (x x_1 : (Quotient.out o).α) => x < x_1) ((Equiv.cast ⋯).symm i)) ⋯)
Instances For
A recursion principle for right moves of a nim game.
Equations
- SetTheory.PGame.rightMovesNimRecOn i H = Eq.mpr ⋯ (H (Ordinal.typein (fun (x x_1 : (Quotient.out o).α) => x < x_1) ((Equiv.cast ⋯).symm i)) ⋯)
Instances For
nim 1 has exactly the same moves as star.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
The Grundy value of an impartial game, the ordinal which corresponds to the game of nim that the game is equivalent to
Equations
Instances For
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
The Grundy value of the sum of two nim games with natural numbers of piles equals their bitwise xor.