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 prove that the grundy value of a sum G + H corresponds to the nimber sum of the individual grundy values.

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

@[irreducible]

noncomputable def SetTheory.PGame.nim (o : 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}) : SetTheory.PGame.nim o = SetTheory.PGame.mk o.toType o.toType (fun (x : o.toType) => SetTheory.PGame.nim ↑(o.enumIsoToType.symm x)) fun (x : o.toType) => SetTheory.PGame.nim ↑(o.enumIsoToType.symm x)

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

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

theorem SetTheory.PGame.moveLeft_nim_hEq (o : Ordinal.{u_1}) : HEq (SetTheory.PGame.nim o).moveLeft fun (i : o.toType) => SetTheory.PGame.nim ↑(o.enumIsoToType.symm i)

theorem SetTheory.PGame.moveRight_nim_hEq (o : Ordinal.{u_1}) : HEq (SetTheory.PGame.nim o).moveRight fun (i : o.toType) => SetTheory.PGame.nim ↑(o.enumIsoToType.symm i)

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

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

Equations

• SetTheory.PGame.toLeftMovesNim = o.enumIsoToType.trans (Equiv.cast ⋯)

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

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

Equations

• SetTheory.PGame.toRightMovesNim = o.enumIsoToType.trans (Equiv.cast ⋯)

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

A recursion principle for left moves of a nim game.

Equations

• SetTheory.PGame.leftMovesNimRecOn i H = ⋯.mpr (H ((Ordinal.typein fun (x1 x2 : o.toType) => x1 < x2).toRelEmbedding ((Equiv.cast ⋯).symm i)) ⋯)

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

A recursion principle for right moves of a nim game.

Equations

• SetTheory.PGame.rightMovesNimRecOn i H = ⋯.mpr (H ((Ordinal.typein fun (x1 x2 : o.toType) => x1 < x2).toRelEmbedding ((Equiv.cast ⋯).symm i)) ⋯)

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

Equations

• SetTheory.PGame.isEmpty_nim_zero_leftMoves = ⋯

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

Equations

• SetTheory.PGame.isEmpty_nim_zero_rightMoves = ⋯

def SetTheory.PGame.nimZeroRelabelling : (SetTheory.PGame.nim 0).Relabelling 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.nim 1).LeftMoves

Equations

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

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

Equations

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

@[simp]

theorem SetTheory.PGame.default_nim_one_leftMoves_eq : default = SetTheory.PGame.toLeftMovesNim ⟨0, ⋯⟩

@[simp]

theorem SetTheory.PGame.default_nim_one_rightMoves_eq : default = SetTheory.PGame.toRightMovesNim ⟨0, ⋯⟩

@[simp]

theorem SetTheory.PGame.toLeftMovesNim_one_symm (i : (SetTheory.PGame.nim 1).LeftMoves) : SetTheory.PGame.toLeftMovesNim.symm i = ⟨0, ⋯⟩

@[simp]

theorem SetTheory.PGame.toRightMovesNim_one_symm (i : (SetTheory.PGame.nim 1).RightMoves) : SetTheory.PGame.toRightMovesNim.symm i = ⟨0, ⋯⟩

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

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

def SetTheory.PGame.nimOneRelabelling : (SetTheory.PGame.nim 1).Relabelling 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.nim o).birthday = 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.nim o).Impartial

Equations

• ⋯ = ⋯

theorem SetTheory.PGame.nim_fuzzy_zero_of_ne_zero {o : Ordinal.{u_1}} (ho : o ≠ 0) : (SetTheory.PGame.nim o).Fuzzy 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.nim o₁ + SetTheory.PGame.nim o₂).Fuzzy 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₂

@[irreducible]

noncomputable def SetTheory.PGame.grundyValue (G : SetTheory.PGame) : Nimber

The Grundy value of an impartial game is recursively defined as the minimum excluded value (the infimum of the complement) of the Grundy values of either its left or right options.

This is the ordinal which corresponds to the game of nim that the game is equivalent to.

This function takes a value in Nimber. This is a type synonym for the ordinals which has the same ordering, but addition in Nimber is such that it corresponds to the grundy value of the addition of games. See that file for more information on nimbers and their arithmetic.

Equations

• G.grundyValue = sInf (Set.range fun (i : G.LeftMoves) => (G.moveLeft i).grundyValue)ᶜ

theorem SetTheory.PGame.grundyValue_eq_sInf_moveLeft (G : SetTheory.PGame) : G.grundyValue = sInf (Set.range (SetTheory.PGame.grundyValue ∘ G.moveLeft))ᶜ

@[deprecated SetTheory.PGame.grundyValue_eq_sInf_moveLeft]

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

theorem SetTheory.PGame.grundyValue_ne_moveLeft {G : SetTheory.PGame} (i : G.LeftMoves) : (G.moveLeft i).grundyValue ≠ G.grundyValue

theorem SetTheory.PGame.le_grundyValue_of_Iio_subset_moveLeft {G : SetTheory.PGame} {o : Nimber} (h : Set.Iio o ⊆ Set.range (SetTheory.PGame.grundyValue ∘ G.moveLeft)) : o ≤ G.grundyValue

theorem SetTheory.PGame.exists_grundyValue_moveLeft_of_lt {G : SetTheory.PGame} {o : Nimber} (h : o < G.grundyValue) : ∃ (i : G.LeftMoves), (G.moveLeft i).grundyValue = o

theorem SetTheory.PGame.grundyValue_le_of_forall_moveLeft {G : SetTheory.PGame} {o : Nimber} (h : ∀ (i : G.LeftMoves), (G.moveLeft i).grundyValue ≠ o) : G.grundyValue ≤ o

@[irreducible]

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

The Sprague-Grundy theorem states that every impartial game is equivalent to a game of nim, namely the game of nim corresponding to the game's Grundy value.

theorem SetTheory.PGame.grundyValue_eq_iff_equiv_nim {G : SetTheory.PGame} [G.Impartial] {o : Nimber} : G.grundyValue = o ↔ G ≈ SetTheory.PGame.nim (Nimber.toOrdinal o)

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

theorem SetTheory.PGame.grundyValue_eq_sInf_moveRight (G : SetTheory.PGame) [G.Impartial] : G.grundyValue = sInf (Set.range (SetTheory.PGame.grundyValue ∘ G.moveRight))ᶜ

@[deprecated SetTheory.PGame.grundyValue_eq_sInf_moveRight]

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

theorem SetTheory.PGame.grundyValue_ne_moveRight {G : SetTheory.PGame} [G.Impartial] (i : G.RightMoves) : (G.moveRight i).grundyValue ≠ G.grundyValue

theorem SetTheory.PGame.le_grundyValue_of_Iio_subset_moveRight {G : SetTheory.PGame} [G.Impartial] {o : Nimber} (h : Set.Iio o ⊆ Set.range (SetTheory.PGame.grundyValue ∘ G.moveRight)) : o ≤ G.grundyValue

theorem SetTheory.PGame.exists_grundyValue_moveRight_of_lt {G : SetTheory.PGame} [G.Impartial] {o : Nimber} (h : o < G.grundyValue) : ∃ (i : G.RightMoves), (G.moveRight i).grundyValue = o

theorem SetTheory.PGame.grundyValue_le_of_forall_moveRight {G : SetTheory.PGame} [G.Impartial] {o : Nimber} (h : ∀ (i : G.RightMoves), (G.moveRight i).grundyValue ≠ o) : G.grundyValue ≤ o

@[irreducible]

theorem SetTheory.PGame.grundyValue_nim_add_nim (x : Ordinal.{u_1}) (y : Ordinal.{u_1}) : (SetTheory.PGame.nim x + SetTheory.PGame.nim y).grundyValue = Ordinal.toNimber x + Ordinal.toNimber y

The Grundy value of the sum of two nim games equals their nimber addition.

theorem SetTheory.PGame.nim_add_nim_equiv (x : Ordinal.{u_1}) (y : Ordinal.{u_1}) : SetTheory.PGame.nim x + SetTheory.PGame.nim y ≈ SetTheory.PGame.nim (Nimber.toOrdinal (Ordinal.toNimber x + Ordinal.toNimber y))

@[simp]

theorem SetTheory.PGame.grundyValue_add (G : SetTheory.PGame) (H : SetTheory.PGame) [G.Impartial] [H.Impartial] : (G + H).grundyValue = G.grundyValue + H.grundyValue