# mathlib3documentation

set_theory.game.nim

# Nim and the Sprague-Grundy theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

def 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
Instances for pgame.nim
theorem pgame.nim_def (o : ordinal) :
= (quotient.out o).α (λ (o₂ : (quotient.out o).α), (λ (o₂ : (quotient.out o).α),
noncomputable def pgame.to_left_moves_nim {o : ordinal} :

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

Equations

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

Equations
@[simp]
@[simp]
@[simp]
theorem pgame.move_left_nim {o : ordinal} (i : (set.Iio o)) :
@[simp]
theorem pgame.move_right_nim {o : ordinal} (i : (set.Iio o)) :
def pgame.left_moves_nim_rec_on {o : ordinal} {P : (pgame.nim o).left_moves Sort u_2} (i : (pgame.nim o).left_moves) (H : Π (a : ordinal) (H : a < o), P (pgame.to_left_moves_nim a, H⟩)) :
P i

A recursion principle for left moves of a nim game.

Equations
def pgame.right_moves_nim_rec_on {o : ordinal} {P : (pgame.nim o).right_moves Sort u_2} (i : (pgame.nim o).right_moves) (H : Π (a : ordinal) (H : a < o), P (pgame.to_right_moves_nim a, H⟩)) :
P i

A recursion principle for right moves of a nim game.

Equations
@[protected, instance]
@[protected, instance]
noncomputable def pgame.nim_zero_relabelling  :

nim 0 has exactly the same moves as 0.

Equations
@[protected, instance]
noncomputable def pgame.unique_nim_one_left_moves  :
Equations
@[protected, instance]
noncomputable def pgame.unique_nim_one_right_moves  :
Equations
@[simp]
@[simp]
@[simp]
@[simp]
noncomputable def pgame.nim_one_relabelling  :

nim 1 has exactly the same moves as star.

Equations
@[simp]
theorem pgame.nim_birthday (o : ordinal) :
@[simp]
theorem pgame.neg_nim (o : ordinal) :
@[protected, instance]
theorem pgame.nim_fuzzy_zero_of_ne_zero {o : ordinal} (ho : o 0) :
@[simp]
theorem pgame.nim_add_equiv_zero_iff (o₁ o₂ : ordinal) :
(pgame.nim o₁ + pgame.nim o₂).equiv 0 o₁ = o₂
@[simp]
theorem pgame.nim_add_fuzzy_zero_iff {o₁ o₂ : ordinal} :
(pgame.nim o₁ + pgame.nim o₂).fuzzy 0 o₁ o₂
@[simp]
theorem pgame.nim_equiv_iff_eq {o₁ o₂ : ordinal} :
(pgame.nim o₁).equiv (pgame.nim o₂) o₁ = o₂
noncomputable def pgame.grundy_value (G : pgame) :

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

Equations

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

@[simp]
theorem pgame.nim_grundy_value (o : ordinal) :
= o
@[simp]
@[simp]
@[simp]
theorem pgame.grundy_value_neg (G : pgame) [G.impartial] :
@[simp]

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

theorem pgame.nim_add_nim_equiv {n m : } :
theorem pgame.grundy_value_add (G H : pgame) [G.impartial] [H.impartial] {n m : } (hG : G.grundy_value = n) (hH : H.grundy_value = m) :
(G + H).grundy_value = (n.lxor m)