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 (grundyValue 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} → SetTheory.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} → SetTheory.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.

noncomputable def SetTheory.PGame.nim : Ordinal.{u} → SetTheory.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

• One or more equations did not get rendered due to their size.

theorem SetTheory.PGame.nim_def (o : Ordinal.{u_1}) : let_fun this := (_ : IsWellOrder (Quotient.out o).α fun (x x_1 : (Quotient.out o).α) => x < x_1); SetTheory.PGame.nim o = SetTheory.PGame.mk (Quotient.out o).α (Quotient.out o).α (fun (o₂ : (Quotient.out o).α) => SetTheory.PGame.nim (Ordinal.typein (fun (x x_1 : (Quotient.out o).α) => x < x_1) o₂)) fun (o₂ : (Quotient.out o).α) => SetTheory.PGame.nim (Ordinal.typein (fun (x x_1 : (Quotient.out o).α) => x < x_1) o₂)

theorem SetTheory.PGame.leftMoves_nim (o : Ordinal.{u_1}) : SetTheory.PGame.LeftMoves (SetTheory.PGame.nim o) = (Quotient.out o).α

theorem SetTheory.PGame.rightMoves_nim (o : Ordinal.{u_1}) : SetTheory.PGame.RightMoves (SetTheory.PGame.nim o) = (Quotient.out o).α

theorem SetTheory.PGame.moveLeft_nim_hEq (o : Ordinal.{u_1}) : let_fun this := (_ : IsWellOrder (Quotient.out o).α fun (x x_1 : (Quotient.out o).α) => x < x_1); HEq (SetTheory.PGame.moveLeft (SetTheory.PGame.nim o)) fun (i : (Quotient.out o).α) => SetTheory.PGame.nim (Ordinal.typein (fun (x x_1 : (Quotient.out o).α) => x < x_1) i)

theorem SetTheory.PGame.moveRight_nim_hEq (o : Ordinal.{u_1}) : let_fun this := (_ : IsWellOrder (Quotient.out o).α fun (x x_1 : (Quotient.out o).α) => x < x_1); HEq (SetTheory.PGame.moveRight (SetTheory.PGame.nim o)) fun (i : (Quotient.out o).α) => SetTheory.PGame.nim (Ordinal.typein (fun (x x_1 : (Quotient.out o).α) => x < x_1) i)

noncomputable def SetTheory.PGame.toLeftMovesNim {o : Ordinal.{u_1}} : ↑(Set.Iio o) ≃ SetTheory.PGame.LeftMoves (SetTheory.PGame.nim o)

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

Equations

• SetTheory.PGame.toLeftMovesNim = (Ordinal.enumIsoOut o).trans (Equiv.cast (_ : (Quotient.out o).α = SetTheory.PGame.LeftMoves (SetTheory.PGame.nim o)))

noncomputable def SetTheory.PGame.toRightMovesNim {o : Ordinal.{u_1}} : ↑(Set.Iio o) ≃ SetTheory.PGame.RightMoves (SetTheory.PGame.nim o)

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

Equations

• SetTheory.PGame.toRightMovesNim = (Ordinal.enumIsoOut o).trans (Equiv.cast (_ : (Quotient.out o).α = SetTheory.PGame.RightMoves (SetTheory.PGame.nim o)))

@[simp]

theorem SetTheory.PGame.toLeftMovesNim_symm_lt {o : Ordinal.{u_1}} (i : SetTheory.PGame.LeftMoves (SetTheory.PGame.nim o)) : ↑(SetTheory.PGame.toLeftMovesNim.symm i) < o

@[simp]

theorem SetTheory.PGame.toRightMovesNim_symm_lt {o : Ordinal.{u_1}} (i : SetTheory.PGame.RightMoves (SetTheory.PGame.nim o)) : ↑(SetTheory.PGame.toRightMovesNim.symm i) < o

@[simp]

theorem SetTheory.PGame.moveLeft_nim' {o : Ordinal.{u}} (i : SetTheory.PGame.LeftMoves (SetTheory.PGame.nim o)) : SetTheory.PGame.moveLeft (SetTheory.PGame.nim o) i = SetTheory.PGame.nim ↑(SetTheory.PGame.toLeftMovesNim.symm i)

theorem SetTheory.PGame.moveLeft_nim {o : Ordinal.{u_1}} (i : ↑(Set.Iio o)) : SetTheory.PGame.moveLeft (SetTheory.PGame.nim o) (SetTheory.PGame.toLeftMovesNim i) = SetTheory.PGame.nim ↑i

@[simp]

theorem SetTheory.PGame.moveRight_nim' {o : Ordinal.{u_1}} (i : SetTheory.PGame.RightMoves (SetTheory.PGame.nim o)) : SetTheory.PGame.moveRight (SetTheory.PGame.nim o) i = SetTheory.PGame.nim ↑(SetTheory.PGame.toRightMovesNim.symm i)

theorem SetTheory.PGame.moveRight_nim {o : Ordinal.{u_1}} (i : ↑(Set.Iio o)) : SetTheory.PGame.moveRight (SetTheory.PGame.nim o) (SetTheory.PGame.toRightMovesNim i) = SetTheory.PGame.nim ↑i

def SetTheory.PGame.leftMovesNimRecOn {o : Ordinal.{u_2}} {P : SetTheory.PGame.LeftMoves (SetTheory.PGame.nim o) → Sort u_1} (i : SetTheory.PGame.LeftMoves (SetTheory.PGame.nim o)) (H : (a : Ordinal.{u_2}) → (H : a < o) → P (SetTheory.PGame.toLeftMovesNim { val := a, property := H })) : P i

A recursion principle for left moves of a nim game.

Equations

• One or more equations did not get rendered due to their size.

def SetTheory.PGame.rightMovesNimRecOn {o : Ordinal.{u_2}} {P : SetTheory.PGame.RightMoves (SetTheory.PGame.nim o) → Sort u_1} (i : SetTheory.PGame.RightMoves (SetTheory.PGame.nim o)) (H : (a : Ordinal.{u_2}) → (H : a < o) → P (SetTheory.PGame.toRightMovesNim { val := a, property := H })) : P i

A recursion principle for right moves of a nim game.

Equations

• One or more equations did not get rendered due to their size.

instance SetTheory.PGame.isEmpty_nim_zero_leftMoves : IsEmpty (SetTheory.PGame.LeftMoves (SetTheory.PGame.nim 0))

Equations

• SetTheory.PGame.isEmpty_nim_zero_leftMoves = (_ : IsEmpty (SetTheory.PGame.LeftMoves (SetTheory.PGame.nim 0)))

instance SetTheory.PGame.isEmpty_nim_zero_rightMoves : IsEmpty (SetTheory.PGame.RightMoves (SetTheory.PGame.nim 0))

Equations

• SetTheory.PGame.isEmpty_nim_zero_rightMoves = (_ : IsEmpty (SetTheory.PGame.RightMoves (SetTheory.PGame.nim 0)))

def SetTheory.PGame.nimZeroRelabelling : SetTheory.PGame.Relabelling (SetTheory.PGame.nim 0) 0

nim 0 has exactly the same moves as 0.

Equations

• SetTheory.PGame.nimZeroRelabelling = SetTheory.PGame.Relabelling.isEmpty (SetTheory.PGame.nim 0)

theorem SetTheory.PGame.nim_zero_equiv : SetTheory.PGame.nim 0 ≈ 0

noncomputable instance SetTheory.PGame.uniqueNimOneLeftMoves : Unique (SetTheory.PGame.LeftMoves (SetTheory.PGame.nim 1))

Equations

• SetTheory.PGame.uniqueNimOneLeftMoves = Equiv.unique (Equiv.cast SetTheory.PGame.uniqueNimOneLeftMoves.proof_1)

noncomputable instance SetTheory.PGame.uniqueNimOneRightMoves : Unique (SetTheory.PGame.RightMoves (SetTheory.PGame.nim 1))

Equations

• SetTheory.PGame.uniqueNimOneRightMoves = Equiv.unique (Equiv.cast SetTheory.PGame.uniqueNimOneRightMoves.proof_1)

@[simp]

theorem SetTheory.PGame.default_nim_one_leftMoves_eq : default = SetTheory.PGame.toLeftMovesNim { val := 0, property := (_ : 0 ∈ Set.Iio 1) }

@[simp]

theorem SetTheory.PGame.default_nim_one_rightMoves_eq : default = SetTheory.PGame.toRightMovesNim { val := 0, property := (_ : 0 ∈ Set.Iio 1) }

@[simp]

theorem SetTheory.PGame.toLeftMovesNim_one_symm (i : SetTheory.PGame.LeftMoves (SetTheory.PGame.nim 1)) : SetTheory.PGame.toLeftMovesNim.symm i = { val := 0, property := (_ : 0 ∈ Set.Iio 1) }

@[simp]

theorem SetTheory.PGame.toRightMovesNim_one_symm (i : SetTheory.PGame.RightMoves (SetTheory.PGame.nim 1)) : SetTheory.PGame.toRightMovesNim.symm i = { val := 0, property := (_ : 0 ∈ Set.Iio 1) }

theorem SetTheory.PGame.nim_one_moveLeft (x : SetTheory.PGame.LeftMoves (SetTheory.PGame.nim 1)) : SetTheory.PGame.moveLeft (SetTheory.PGame.nim 1) x = SetTheory.PGame.nim 0

theorem SetTheory.PGame.nim_one_moveRight (x : SetTheory.PGame.RightMoves (SetTheory.PGame.nim 1)) : SetTheory.PGame.moveRight (SetTheory.PGame.nim 1) x = SetTheory.PGame.nim 0

def SetTheory.PGame.nimOneRelabelling : SetTheory.PGame.Relabelling (SetTheory.PGame.nim 1) SetTheory.PGame.star

nim 1 has exactly the same moves as star.

Equations

• One or more equations did not get rendered due to their size.

theorem SetTheory.PGame.nim_one_equiv : SetTheory.PGame.nim 1 ≈ SetTheory.PGame.star

@[simp]

theorem SetTheory.PGame.nim_birthday (o : Ordinal.{u_1}) : SetTheory.PGame.birthday (SetTheory.PGame.nim o) = o

@[simp]

theorem SetTheory.PGame.neg_nim (o : Ordinal.{u_1}) : -SetTheory.PGame.nim o = SetTheory.PGame.nim o

instance SetTheory.PGame.nim_impartial (o : Ordinal.{u_1}) : SetTheory.PGame.Impartial (SetTheory.PGame.nim o)

Equations

• (_ : SetTheory.PGame.Impartial (SetTheory.PGame.nim o)) = (_ : SetTheory.PGame.Impartial (SetTheory.PGame.nim o))

theorem SetTheory.PGame.nim_fuzzy_zero_of_ne_zero {o : Ordinal.{u_1}} (ho : o ≠ 0) : SetTheory.PGame.Fuzzy (SetTheory.PGame.nim o) 0

@[simp]

theorem SetTheory.PGame.nim_add_equiv_zero_iff (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_1}) : SetTheory.PGame.nim o₁ + SetTheory.PGame.nim o₂ ≈ 0 ↔ o₁ = o₂

@[simp]

theorem SetTheory.PGame.nim_add_fuzzy_zero_iff {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} : SetTheory.PGame.Fuzzy (SetTheory.PGame.nim o₁ + SetTheory.PGame.nim o₂) 0 ↔ o₁ ≠ o₂

@[simp]

theorem SetTheory.PGame.nim_equiv_iff_eq {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} : SetTheory.PGame.nim o₁ ≈ SetTheory.PGame.nim o₂ ↔ o₁ = o₂

noncomputable def SetTheory.PGame.grundyValue : SetTheory.PGame → Ordinal.{u}

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

Equations

• SetTheory.PGame.grundyValue x = Ordinal.mex fun (i : SetTheory.PGame.LeftMoves x) => SetTheory.PGame.grundyValue (SetTheory.PGame.moveLeft x i)

theorem SetTheory.PGame.grundyValue_eq_mex_left (G : SetTheory.PGame) : SetTheory.PGame.grundyValue G = Ordinal.mex fun (i : SetTheory.PGame.LeftMoves G) => SetTheory.PGame.grundyValue (SetTheory.PGame.moveLeft G i)

theorem SetTheory.PGame.equiv_nim_grundyValue (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : G ≈ SetTheory.PGame.nim (SetTheory.PGame.grundyValue G)

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 SetTheory.PGame.grundyValue_eq_iff_equiv_nim {G : SetTheory.PGame} [SetTheory.PGame.Impartial G] {o : Ordinal.{u_1}} : SetTheory.PGame.grundyValue G = o ↔ G ≈ SetTheory.PGame.nim o

@[simp]

theorem SetTheory.PGame.nim_grundyValue (o : Ordinal.{u}) : SetTheory.PGame.grundyValue (SetTheory.PGame.nim o) = o

theorem SetTheory.PGame.grundyValue_eq_iff_equiv (G : SetTheory.PGame) (H : SetTheory.PGame) [SetTheory.PGame.Impartial G] [SetTheory.PGame.Impartial H] : SetTheory.PGame.grundyValue G = SetTheory.PGame.grundyValue H ↔ G ≈ H

@[simp]

theorem SetTheory.PGame.grundyValue_zero : SetTheory.PGame.grundyValue 0 = 0

theorem SetTheory.PGame.grundyValue_iff_equiv_zero (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : SetTheory.PGame.grundyValue G = 0 ↔ G ≈ 0

@[simp]

theorem SetTheory.PGame.grundyValue_star : SetTheory.PGame.grundyValue SetTheory.PGame.star = 1

@[simp]

theorem SetTheory.PGame.grundyValue_neg (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : SetTheory.PGame.grundyValue (-G) = SetTheory.PGame.grundyValue G

theorem SetTheory.PGame.grundyValue_eq_mex_right (G : SetTheory.PGame) [SetTheory.PGame.Impartial G] : SetTheory.PGame.grundyValue G = Ordinal.mex fun (i : SetTheory.PGame.RightMoves G) => SetTheory.PGame.grundyValue (SetTheory.PGame.moveRight G i)

@[simp]

theorem SetTheory.PGame.grundyValue_nim_add_nim (n : ℕ) (m : ℕ) : SetTheory.PGame.grundyValue (SetTheory.PGame.nim ↑n + SetTheory.PGame.nim ↑m) = ↑(n ^^^ m)

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

theorem SetTheory.PGame.nim_add_nim_equiv {n : ℕ} {m : ℕ} : SetTheory.PGame.nim ↑n + SetTheory.PGame.nim ↑m ≈ SetTheory.PGame.nim ↑(n ^^^ m)

theorem SetTheory.PGame.grundyValue_add (G : SetTheory.PGame) (H : SetTheory.PGame) [SetTheory.PGame.Impartial G] [SetTheory.PGame.Impartial H] {n : ℕ} {m : ℕ} (hG : SetTheory.PGame.grundyValue G = ↑n) (hH : SetTheory.PGame.grundyValue H = ↑m) : SetTheory.PGame.grundyValue (G + H) = ↑(n ^^^ m)