Documentation

Mathlib.SetTheory.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 (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.

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.
Instances For
    theorem SetTheory.PGame.nim_def (o : Ordinal.{u_1}) :
    let_fun this := (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1); SetTheory.PGame.nim o = SetTheory.PGame.mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => SetTheory.PGame.nim (Ordinal.typein (fun x x_1 => x < x_1) o₂)) fun o₂ => SetTheory.PGame.nim (Ordinal.typein (fun x x_1 => x < x_1) o₂)
    theorem SetTheory.PGame.moveLeft_nim_hEq (o : Ordinal.{u_1}) :
    let_fun this := (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1); HEq (SetTheory.PGame.moveLeft (SetTheory.PGame.nim o)) fun i => SetTheory.PGame.nim (Ordinal.typein (fun x x_1 => 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 => x < x_1); HEq (SetTheory.PGame.moveRight (SetTheory.PGame.nim o)) fun i => SetTheory.PGame.nim (Ordinal.typein (fun x x_1 => x < x_1) i)

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

    Instances For

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

      Instances For
        @[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
        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
        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.

        Instances For
          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.

          Instances For

            nim 0 has exactly the same moves as 0.

            Instances For
              @[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) }

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

              Equations
              Instances For

                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]

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