mathlib3 documentation

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.

source
def pgame.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
Instances for pgame.nim
source
theorem pgame.nim_def (o : ordinal) :
pgame.nim o = pgame.mk (quotient.out o).α (quotient.out o).α (λ (o₂ : (quotient.out o).α), pgame.nim (ordinal.typein has_lt.lt o₂)) (λ (o₂ : (quotient.out o).α), pgame.nim (ordinal.typein has_lt.lt o₂))
source
theorem pgame.left_moves_nim (o : ordinal) :
(pgame.nim o).left_moves = (quotient.out o).α
source
theorem pgame.right_moves_nim (o : ordinal) :
(pgame.nim o).right_moves = (quotient.out o).α
source
theorem pgame.move_left_nim_heq (o : ordinal) :
(pgame.nim o).move_left == λ (i : (quotient.out o).α), pgame.nim (ordinal.typein has_lt.lt i)
source
theorem pgame.move_right_nim_heq (o : ordinal) :
(pgame.nim o).move_right == λ (i : (quotient.out o).α), pgame.nim (ordinal.typein has_lt.lt i)
source
noncomputable def pgame.to_left_moves_nim {o : ordinal} :
↥(set.Iio o) ≃ (pgame.nim o).left_moves

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

Equations
source
noncomputable def pgame.to_right_moves_nim {o : ordinal} :
↥(set.Iio o) ≃ (pgame.nim o).right_moves

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

Equations
source
@[simp]
theorem pgame.to_left_moves_nim_symm_lt {o : ordinal} (i : (pgame.nim o).left_moves) :
↑(⇑(pgame.to_left_moves_nim.symm) i) < o
source
@[simp]
theorem pgame.to_right_moves_nim_symm_lt {o : ordinal} (i : (pgame.nim o).right_moves) :
↑(⇑(pgame.to_right_moves_nim.symm) i) < o
source
@[simp]
theorem pgame.move_left_nim' {o : ordinal} (i : (pgame.nim o).left_moves) :
(pgame.nim o).move_left i = pgame.nim (⇑(pgame.to_left_moves_nim.symm) i).val
source
theorem pgame.move_left_nim {o : ordinal} (i : ↥(set.Iio o)) :
(pgame.nim o).move_left (⇑pgame.to_left_moves_nim i) = pgame.nim ↑i
source
@[simp]
theorem pgame.move_right_nim' {o : ordinal} (i : (pgame.nim o).right_moves) :
(pgame.nim o).move_right i = pgame.nim (⇑(pgame.to_right_moves_nim.symm) i).val
source
theorem pgame.move_right_nim {o : ordinal} (i : ↥(set.Iio o)) :
(pgame.nim o).move_right (⇑pgame.to_right_moves_nim i) = pgame.nim ↑i
source
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
source
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
source
@[protected, instance]
def pgame.is_empty_nim_zero_left_moves  :
is_empty (pgame.nim 0).left_moves
source
@[protected, instance]
def pgame.is_empty_nim_zero_right_moves  :
is_empty (pgame.nim 0).right_moves
source
noncomputable def pgame.nim_zero_relabelling  :
(pgame.nim 0).relabelling 0

nim 0 has exactly the same moves as 0.

Equations
source
theorem pgame.nim_zero_equiv  :
(pgame.nim 0).equiv 0
source
@[protected, instance]
noncomputable def pgame.unique_nim_one_left_moves  :
unique (pgame.nim 1).left_moves
Equations
source
@[protected, instance]
noncomputable def pgame.unique_nim_one_right_moves  :
unique (pgame.nim 1).right_moves
Equations
source
@[simp]
theorem pgame.default_nim_one_left_moves_eq  :
inhabited.default = ⇑pgame.to_left_moves_nim ⟨0, _⟩
source
@[simp]
theorem pgame.default_nim_one_right_moves_eq  :
inhabited.default = ⇑pgame.to_right_moves_nim ⟨0, _⟩
source
@[simp]
theorem pgame.to_left_moves_nim_one_symm (i : (pgame.nim 1).left_moves) :
⇑(pgame.to_left_moves_nim.symm) i = ⟨0, _⟩
source
@[simp]
theorem pgame.to_right_moves_nim_one_symm (i : (pgame.nim 1).right_moves) :
⇑(pgame.to_right_moves_nim.symm) i = ⟨0, _⟩
source
theorem pgame.nim_one_move_left (x : (pgame.nim 1).left_moves) :
(pgame.nim 1).move_left x = pgame.nim 0
source
theorem pgame.nim_one_move_right (x : (pgame.nim 1).right_moves) :
(pgame.nim 1).move_right x = pgame.nim 0
source
noncomputable def pgame.nim_one_relabelling  :
(pgame.nim 1).relabelling pgame.star

nim 1 has exactly the same moves as star.

Equations
source
theorem pgame.nim_one_equiv  :
(pgame.nim 1).equiv pgame.star
source
@[simp]
theorem pgame.nim_birthday (o : ordinal) :
(pgame.nim o).birthday = o
source
@[simp]
theorem pgame.neg_nim (o : ordinal) :
-pgame.nim o = pgame.nim o
source
@[protected, instance]
def pgame.nim_impartial (o : ordinal) :
(pgame.nim o).impartial
source
theorem pgame.nim_fuzzy_zero_of_ne_zero {o : ordinal} (ho : o ≠ 0) :
(pgame.nim o).fuzzy 0
source
@[simp]
theorem pgame.nim_add_equiv_zero_iff (o₁ o₂ : ordinal) :
(pgame.nim o₁ + pgame.nim o₂).equiv 0 ↔ o₁ = o₂
source
@[simp]
theorem pgame.nim_add_fuzzy_zero_iff {o₁ o₂ : ordinal} :
(pgame.nim o₁ + pgame.nim o₂).fuzzy 0 ↔ o₁ ≠ o₂
source
@[simp]
theorem pgame.nim_equiv_iff_eq {o₁ o₂ : ordinal} :
(pgame.nim o₁).equiv (pgame.nim o₂) ↔ o₁ = o₂
source
noncomputable def pgame.grundy_value (G : pgame) :
ordinal

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

Equations
source
theorem pgame.grundy_value_eq_mex_left (G : pgame) :
G.grundy_value = ordinal.mex (λ (i : G.left_moves), (G.move_left i).grundy_value)
source
theorem pgame.equiv_nim_grundy_value (G : pgame) [G.impartial] :
G.equiv (pgame.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

source
theorem pgame.grundy_value_eq_iff_equiv_nim {G : pgame} [G.impartial] {o : ordinal} :
G.grundy_value = o ↔ G.equiv (pgame.nim o)
source
@[simp]
theorem pgame.nim_grundy_value (o : ordinal) :
(pgame.nim o).grundy_value = o
source
theorem pgame.grundy_value_eq_iff_equiv (G H : pgame) [G.impartial] [H.impartial] :
G.grundy_value = H.grundy_value ↔ G.equiv H
source
@[simp]
theorem pgame.grundy_value_zero  :
0.grundy_value = 0
source
theorem pgame.grundy_value_iff_equiv_zero (G : pgame) [G.impartial] :
G.grundy_value = 0 ↔ G.equiv 0
source
@[simp]
theorem pgame.grundy_value_star  :
pgame.star.grundy_value = 1
source
@[simp]
theorem pgame.grundy_value_neg (G : pgame) [G.impartial] :
(-G).grundy_value = G.grundy_value
source
theorem pgame.grundy_value_eq_mex_right (G : pgame) [G.impartial] :
G.grundy_value = ordinal.mex (λ (i : G.right_moves), (G.move_right i).grundy_value)
source
@[simp]
theorem pgame.grundy_value_nim_add_nim (n m : ℕ) :
(pgame.nim ↑n + pgame.nim ↑m).grundy_value = ↑(n.lxor m)

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

source
theorem pgame.nim_add_nim_equiv {n m : ℕ} :
(pgame.nim ↑n + pgame.nim ↑m).equiv (pgame.nim ↑(n.lxor m))
source
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)