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' has the sole purpose of making nim computable. It performs the same job as quotient.out but is specific to ordinals.

Equations

o.out' = {α := (quotient.out o).α, r := has_lt.lt (preorder.to_has_lt (quotient.out o).α), wo := _}

def nim :

ordinal → pgame

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₁ = let f : O₁.out'.α → pgame := λ (O₂ : O₁.out'.α), nim (ordinal.typein O₁.out'.r O₂) in pgame.mk O₁.out'.α O₁.out'.α f f

Instances for nim

pgame.nim.nim_impartial

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

nim O = pgame.mk (quotient.out O).α (quotient.out O).α (λ (O₂ : (quotient.out O).α), nim (ordinal.typein has_lt.lt O₂)) (λ (O₂ : (quotient.out O).α), nim (ordinal.typein has_lt.lt O₂))

@[protected, instance]

def pgame.nim.left_moves.is_empty :

is_empty (nim 0).left_moves

@[protected, instance]

def pgame.nim.right_moves.is_empty :

is_empty (nim 0).right_moves

@[protected, instance]

noncomputable def pgame.nim.left_moves.unique :

unique (nim 1).left_moves

Equations

pgame.nim.left_moves.unique = pgame.nim.left_moves.unique._proof_2.mpr ordinal.unique_out_one

@[protected, instance]

noncomputable def pgame.nim.right_moves.unique :

unique (nim 1).right_moves

Equations

pgame.nim.right_moves.unique = pgame.nim.right_moves.unique._proof_2.mpr ordinal.unique_out_one

def pgame.nim.nim_zero_relabelling :

(nim 0).relabelling 0

nim 0 has exactly the same moves as 0.

Equations

pgame.nim.nim_zero_relabelling = pgame.relabelling.is_empty (nim 0)

@[simp]

theorem pgame.nim.nim_zero_equiv :

(nim 0).equiv 0

noncomputable def pgame.nim.nim_one_relabelling :

(nim 1).relabelling pgame.star

nim 1 has exactly the same moves as star.

Equations

pgame.nim.nim_one_relabelling = pgame.nim.nim_one_relabelling._proof_2.mpr (pgame.relabelling.mk (id (equiv.equiv_of_unique (quotient.out 1).α punit)) (id (equiv.equiv_of_unique (quotient.out 1).α punit)) (λ (i : (pgame.mk (quotient.out 1).α (quotient.out 1).α (λ (O₂ : (quotient.out 1).α), nim (ordinal.typein has_lt.lt O₂)) (λ (O₂ : (quotient.out 1).α), nim (ordinal.typein has_lt.lt O₂))).left_moves), _.mpr pgame.nim.nim_zero_relabelling) (λ (j : pgame.star.right_moves), _.mpr pgame.nim.nim_zero_relabelling))

@[simp]

theorem pgame.nim.nim_one_equiv :

(nim 1).equiv pgame.star

@[simp]

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

(nim O).birthday = O

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

(nim O).left_moves = (quotient.out O).α

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

(nim O).right_moves = (quotient.out O).α

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

(nim O).move_left == λ (i : (quotient.out O).α), nim (ordinal.typein has_lt.lt i)

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

(nim O).move_right == λ (i : (quotient.out O).α), nim (ordinal.typein has_lt.lt i)

noncomputable def pgame.nim.to_left_moves_nim {O : ordinal} :

↥(set.Iio O) ≃ (nim O).left_moves

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

Equations

pgame.nim.to_left_moves_nim = O.enum_iso_out.to_equiv.trans (equiv.cast pgame.nim.to_left_moves_nim._proof_1)

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

↥(set.Iio O) ≃ (nim O).right_moves

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

Equations

pgame.nim.to_right_moves_nim = O.enum_iso_out.to_equiv.trans (equiv.cast pgame.nim.to_right_moves_nim._proof_1)

@[simp]

theorem pgame.nim.to_left_moves_nim_symm_lt {O : ordinal} (i : (nim O).left_moves) :

↑(⇑(pgame.nim.to_left_moves_nim.symm) i) < O

@[simp]

theorem pgame.nim.to_right_moves_nim_symm_lt {O : ordinal} (i : (nim O).right_moves) :

↑(⇑(pgame.nim.to_right_moves_nim.symm) i) < O

@[simp]

theorem pgame.nim.move_left_nim' {O : ordinal} (i : (nim O).left_moves) :

(nim O).move_left i = nim (⇑(pgame.nim.to_left_moves_nim.symm) i).val

theorem pgame.nim.move_left_nim {O : ordinal} (i : ↥(set.Iio O)) :

(nim O).move_left (⇑pgame.nim.to_left_moves_nim i) = nim ↑i

@[simp]

theorem pgame.nim.move_right_nim' {O : ordinal} (i : (nim O).right_moves) :

(nim O).move_right i = nim (⇑(pgame.nim.to_right_moves_nim.symm) i).val

theorem pgame.nim.move_right_nim {O : ordinal} (i : ↥(set.Iio O)) :

(nim O).move_right (⇑pgame.nim.to_right_moves_nim i) = nim ↑i

@[simp]

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

@[protected, 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.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

G.grundy_value = ordinal.mex (λ (i : G.left_moves), (G.move_left i).grundy_value)

theorem pgame.grundy_value_def (G : pgame) :

G.grundy_value = ordinal.mex (λ (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

@[simp]

theorem pgame.grundy_value_eq_iff_equiv_nim (G : pgame) [G.impartial] (O : ordinal) :

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

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

(nim O).grundy_value = O

@[simp]

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

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

@[simp]

theorem pgame.grundy_value_zero :

0.grundy_value = 0

@[simp]

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

G.grundy_value = 0 ↔ G.equiv 0

theorem pgame.grundy_value_star :

pgame.star.grundy_value = 1

@[simp]

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)