mathlib documentation

set_theory.game.nim

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 {O' | O' < 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, which makes proofs significantly more messy and tedious, but avoids the universe bump.

The lemma nim_def is somewhat prone to produce "motive is not type correct" errors. If you run into this problem, you may find the lemmas exists_ordinal_move_left_eq and exists_move_left_eq useful.

ordinal.out' has the sole purpose of making nim computable. It performs the same job as quotient.out but is specific to ordinals.

Equations
def 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 nim
theorem pgame.nim.nim_def (O : ordinal) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable def pgame.nim.left_moves.unique  :
Equations
@[protected, instance]
Equations
@[simp]
theorem pgame.nim.nim_zero_equiv  :
(nim 0).equiv 0
@[simp]
theorem pgame.nim.nim_birthday (O : ordinal) :
(nim O).birthday = O
noncomputable def pgame.nim.to_left_moves_nim {O : ordinal} :

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

Equations
noncomputable def pgame.nim.to_right_moves_nim {O : ordinal} :

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

Equations
@[simp]
theorem pgame.nim.neg_nim (O : ordinal) :
-nim O = nim O
@[protected, instance]
theorem pgame.nim.exists_ordinal_move_left_eq {O : ordinal} (i : (nim O).left_moves) :
∃ (O' : ordinal) (H : O' < O), (nim O).move_left i = nim O'
theorem pgame.nim.exists_move_left_eq {O O' : ordinal} (h : O' < O) :
∃ (i : (nim O).left_moves), (nim O).move_left i = nim O'
theorem pgame.nim.non_zero_first_wins {O : ordinal} (hO : O 0) :
(nim O).fuzzy 0
@[simp]
theorem pgame.nim.add_equiv_zero_iff_eq (O₁ O₂ : ordinal) :
(nim O₁ + nim O₂).equiv 0 O₁ = O₂
@[simp]
theorem pgame.nim.add_fuzzy_zero_iff_ne (O₁ O₂ : ordinal) :
(nim O₁ + nim O₂).fuzzy 0 O₁ O₂
@[simp]
theorem pgame.nim.equiv_iff_eq (O₁ O₂ : ordinal) :
(nim O₁).equiv (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]
@[simp]
theorem pgame.nim_add_nim_equiv {n m : } :
(nim n + nim m).equiv (nim (n.lxor 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)