# 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.

@[irreducible]
noncomputable def SetTheory.PGame.nim :

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
theorem SetTheory.PGame.nim_def (o : Ordinal.{u_1}) :
let_fun this := ; = SetTheory.PGame.mk () () (fun (o₂ : ()) => SetTheory.PGame.nim (Ordinal.typein (fun (x x_1 : ()) => x < x_1) o₂)) fun (o₂ : ()) => SetTheory.PGame.nim (Ordinal.typein (fun (x x_1 : ()) => x < x_1) o₂)
theorem SetTheory.PGame.leftMoves_nim (o : Ordinal.{u_1}) :
.LeftMoves = ()
theorem SetTheory.PGame.rightMoves_nim (o : Ordinal.{u_1}) :
.RightMoves = ()
theorem SetTheory.PGame.moveLeft_nim_hEq (o : Ordinal.{u_1}) :
let_fun this := ; HEq .moveLeft fun (i : ()) => SetTheory.PGame.nim (Ordinal.typein (fun (x x_1 : ()) => x < x_1) i)
theorem SetTheory.PGame.moveRight_nim_hEq (o : Ordinal.{u_1}) :
let_fun this := ; HEq .moveRight fun (i : ()) => SetTheory.PGame.nim (Ordinal.typein (fun (x x_1 : ()) => x < x_1) i)
noncomputable def SetTheory.PGame.toLeftMovesNim {o : Ordinal.{u_1}} :
() .LeftMoves

Turns an ordinal less than o into a left move for nim o and viceversa.

Equations
• SetTheory.PGame.toLeftMovesNim = o.enumIsoOut.trans ()
Instances For
noncomputable def SetTheory.PGame.toRightMovesNim {o : Ordinal.{u_1}} :
() .RightMoves

Turns an ordinal less than o into a right move for nim o and viceversa.

Equations
• SetTheory.PGame.toRightMovesNim = o.enumIsoOut.trans ()
Instances For
@[simp]
theorem SetTheory.PGame.toLeftMovesNim_symm_lt {o : Ordinal.{u_1}} (i : .LeftMoves) :
(SetTheory.PGame.toLeftMovesNim.symm i) < o
@[simp]
theorem SetTheory.PGame.toRightMovesNim_symm_lt {o : Ordinal.{u_1}} (i : .RightMoves) :
(SetTheory.PGame.toRightMovesNim.symm i) < o
@[simp]
theorem SetTheory.PGame.moveLeft_nim' {o : Ordinal.{u}} (i : .LeftMoves) :
.moveLeft i = SetTheory.PGame.nim (SetTheory.PGame.toLeftMovesNim.symm i)
theorem SetTheory.PGame.moveLeft_nim {o : Ordinal.{u_1}} (i : ()) :
.moveLeft (SetTheory.PGame.toLeftMovesNim i) =
@[simp]
theorem SetTheory.PGame.moveRight_nim' {o : Ordinal.{u_1}} (i : .RightMoves) :
.moveRight i = SetTheory.PGame.nim (SetTheory.PGame.toRightMovesNim.symm i)
theorem SetTheory.PGame.moveRight_nim {o : Ordinal.{u_1}} (i : ()) :
.moveRight (SetTheory.PGame.toRightMovesNim i) =
def SetTheory.PGame.leftMovesNimRecOn {o : Ordinal.{u_2}} {P : .LeftMovesSort u_1} (i : .LeftMoves) (H : (a : Ordinal.{u_2}) → (H : a < o) → P (SetTheory.PGame.toLeftMovesNim a, H)) :
P i

A recursion principle for left moves of a nim game.

Equations
• = .mpr (H (Ordinal.typein (fun (x x_1 : ()) => x < x_1) (().symm i)) )
Instances For
def SetTheory.PGame.rightMovesNimRecOn {o : Ordinal.{u_2}} {P : .RightMovesSort u_1} (i : .RightMoves) (H : (a : Ordinal.{u_2}) → (H : a < o) → P (SetTheory.PGame.toRightMovesNim a, H)) :
P i

A recursion principle for right moves of a nim game.

Equations
• = .mpr (H (Ordinal.typein (fun (x x_1 : ()) => x < x_1) (().symm i)) )
Instances For

nim 0 has exactly the same moves as 0.

Equations
Instances For
noncomputable instance SetTheory.PGame.uniqueNimOneLeftMoves :
Unique .LeftMoves
Equations
noncomputable instance SetTheory.PGame.uniqueNimOneRightMoves :
Unique .RightMoves
Equations
@[simp]
theorem SetTheory.PGame.default_nim_one_leftMoves_eq :
default = SetTheory.PGame.toLeftMovesNim 0,
@[simp]
theorem SetTheory.PGame.default_nim_one_rightMoves_eq :
default = SetTheory.PGame.toRightMovesNim 0,
@[simp]
theorem SetTheory.PGame.toLeftMovesNim_one_symm (i : .LeftMoves) :
SetTheory.PGame.toLeftMovesNim.symm i = 0,
@[simp]
theorem SetTheory.PGame.toRightMovesNim_one_symm (i : .RightMoves) :
SetTheory.PGame.toRightMovesNim.symm i = 0,
theorem SetTheory.PGame.nim_one_moveLeft (x : .LeftMoves) :
.moveLeft x =
theorem SetTheory.PGame.nim_one_moveRight (x : .RightMoves) :
.moveRight x =

nim 1 has exactly the same moves as star.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem SetTheory.PGame.nim_birthday (o : Ordinal.{u_1}) :
.birthday = o
instance SetTheory.PGame.nim_impartial (o : Ordinal.{u_1}) :
.Impartial
Equations
• =
@[simp]
@[simp]
theorem SetTheory.PGame.nim_add_fuzzy_zero_iff {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :
().Fuzzy 0 o₁ o₂
@[simp]
theorem SetTheory.PGame.nim_equiv_iff_eq {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :
o₁ = o₂
@[irreducible]
noncomputable def SetTheory.PGame.grundyValue :

The Grundy value of an impartial game, the ordinal which corresponds to the game of nim that the game is equivalent to

Equations
• x.grundyValue = Ordinal.mex fun (i : x.LeftMoves) => (x.moveLeft i).grundyValue
Instances For
theorem SetTheory.PGame.grundyValue_eq_mex_left (G : SetTheory.PGame) :
G.grundyValue = Ordinal.mex fun (i : G.LeftMoves) => (G.moveLeft i).grundyValue
@[irreducible]

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

theorem SetTheory.PGame.grundyValue_eq_iff_equiv_nim {G : SetTheory.PGame} [G.Impartial] {o : Ordinal.{u_1}} :
G.grundyValue = o
@[simp]
theorem SetTheory.PGame.nim_grundyValue (o : Ordinal.{u}) :
.grundyValue = o
theorem SetTheory.PGame.grundyValue_eq_iff_equiv (G : SetTheory.PGame) (H : SetTheory.PGame) [G.Impartial] [H.Impartial] :
G.grundyValue = H.grundyValue G H
@[simp]
theorem SetTheory.PGame.grundyValue_iff_equiv_zero (G : SetTheory.PGame) [G.Impartial] :
G.grundyValue = 0 G 0
@[simp]
theorem SetTheory.PGame.grundyValue_neg (G : SetTheory.PGame) [G.Impartial] :
(-G).grundyValue = G.grundyValue
theorem SetTheory.PGame.grundyValue_eq_mex_right (G : SetTheory.PGame) [G.Impartial] :
G.grundyValue = Ordinal.mex fun (i : G.RightMoves) => (G.moveRight i).grundyValue
@[simp]
theorem SetTheory.PGame.grundyValue_nim_add_nim (n : ) (m : ) :
().grundyValue = (n ^^^ m)

The Grundy value of the sum of two nim games with natural numbers of piles equals their bitwise xor.

theorem SetTheory.PGame.grundyValue_add (G : SetTheory.PGame) (H : SetTheory.PGame) [G.Impartial] [H.Impartial] {n : } {m : } (hG : G.grundyValue = n) (hH : H.grundyValue = m) :
(G + H).grundyValue = (n ^^^ m)