mathlib documentation

set_theory.​game.​nim

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

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

This is the same as ordinal.type_out but defined to use ordinal.out.

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
theorem nim.​nim_def (O : ordinal) :
nim O = pgame.mk O.out.α O.out.α (λ (O₂ : O.out.α), nim (ordinal.typein O.out.r O₂)) (λ (O₂ : O.out.α), nim (ordinal.typein O.out.r O₂))

theorem nim.​nim_wf_lemma {O₁ : ordinal} (O₂ : O₁.out.α) :
ordinal.typein O₁.out.r O₂ < O₁

theorem nim.​nim_sum_first_loses_iff_eq (O₁ O₂ : ordinal) :
(nim O₁ + nim O₂).first_loses O₁ = O₂

theorem nim.​nim_sum_first_wins_iff_neq (O₁ O₂ : ordinal) :
(nim O₁ + nim O₂).first_wins O₁ O₂

theorem nim.​nim_equiv_iff_eq (O₁ O₂ : ordinal) :
(nim O₁).equiv (nim O₂) O₁ = O₂

def nim.​nonmoves {α : Type u} :
(α → ordinal)set ordinal

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
theorem nim.​nonmoves_nonempty {α : Type u} (M : α → ordinal) :
∃ (O : ordinal), O nim.nonmoves M

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

Equations
theorem nim.​Sprague_Grundy {G : pgame} (hG : G.impartial) :

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