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.

def ordinal.out (o : ordinal) :

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

o.out = {α := (quotient.out o).α, r := λ (x y : (quotient.out o).α), (quotient.out o).r x y, wo := _}

theorem ordinal.type_out' (o : ordinal) :

ordinal.type o.out.r = o

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

def nim (a : ordinal) :

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

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 pgame.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 pgame.nim.nim_wf_lemma {O₁ : ordinal} (O₂ : O₁.out.α) :

ordinal.typein O₁.out.r O₂ < O₁

@[instance]

def pgame.nim.nim_impartial (O : ordinal) :

(nim O).impartial

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.zero_first_loses :

(nim 0).first_loses

theorem pgame.nim.non_zero_first_wins (O : ordinal) (hO : O ≠ 0) :

(nim O).first_wins

theorem pgame.nim.sum_first_loses_iff_eq (O₁ O₂ : ordinal) :

(nim O₁ + nim O₂).first_loses ↔ O₁ = O₂

theorem pgame.nim.sum_first_wins_iff_neq (O₁ O₂ : ordinal) :

(nim O₁ + nim O₂).first_wins ↔ O₁ ≠ O₂

theorem pgame.nim.equiv_iff_eq (O₁ O₂ : ordinal) :

(nim O₁).equiv (nim O₂) ↔ O₁ = O₂

def pgame.nonmoves {α : Type u} (M : α → 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

pgame.nonmoves M = {O : ordinal | ¬∃ (a : α), M a = O}

theorem pgame.nonmoves_nonempty {α : Type u} (M : α → ordinal) :

∃ (O : ordinal), O ∈ pgame.nonmoves M

def pgame.grundy_value (G : pgame) [G.impartial] :

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

Equations

G.grundy_value = λ (hG : G.impartial), ordinal.omin (pgame.nonmoves (λ (i : G.left_moves), (G.move_left i).grundy_value)) _

theorem pgame.grundy_value_def (G : pgame) [G.impartial] :

G.grundy_value = ordinal.omin (pgame.nonmoves (λ (i : G.left_moves), (G.move_left i).grundy_value)) _

theorem pgame.equiv_nim_grundy_value (G : pgame) [G.impartial] :

G.equiv (nim G.grundy_value)

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 pgame.equiv_nim_iff_grundy_value_eq (G : pgame) [G.impartial] (O : ordinal) :

G.equiv (nim O) ↔ G.grundy_value = O

theorem pgame.nim.grundy_value (O : ordinal) :

(nim O).grundy_value = O

theorem pgame.equiv_iff_grundy_value_eq (G H : pgame) [G.impartial] [H.impartial] :

G.equiv H ↔ G.grundy_value = H.grundy_value

theorem pgame.grundy_value_zero :

0.grundy_value = 0

theorem pgame.equiv_zero_iff_grundy_value (G : pgame) [G.impartial] :

G.equiv 0 ↔ G.grundy_value = 0

theorem pgame.grundy_value_nim_add_nim (n m : ℕ) :

(nim ↑n + nim ↑m).grundy_value = ↑(n.lxor m)

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)