Documentation

CombinatorialGames.Game.Impartial.Grundy

Grundy value #

The Grundy value of an impartial game is recursively defined as the least nimber not among the Grundy values of either its left or right options. This map respects addition and multiplication.

We provide two definitions for the Grundy value. grundyAux is computed using either the left or right options of the game, and is defined for all games. To make the API symmetric, we also provide Impartial.grundy, which enforces that the game is impartial, and is thus equal to either of grundyAux left or grundyAux right.

The Sprague-Grundy theorem Impartial.nim_grundy_equiv shows that any impartial game is equivalent to a game of Nim, namely that corresponding to its Grundy value.

Grundy value #

source
@[irreducible]
def IGame.grundyAux (p : Player) (x : IGame) :
Nimber

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

This is an auxiliary definition for reasoning about games not yet known to be impartial. Use Impartial.grundy for an impartial game.

Equations
Instances For
    source
    theorem IGame.grundyAux_def (p : Player) (x : IGame) :
    grundyAux p x = sInf (grundyAux p '' moves p x)ᶜ
    source
    theorem IGame.le_grundyAux_iff {p : Player} {x : IGame} {o : Nimber} :
    o ≤ grundyAux p x ↔ Set.Iio o ⊆ grundyAux p '' moves p x
    source
    theorem IGame.lt_grundyAux_iff {p : Player} {x : IGame} {o : Nimber} :
    o < grundyAux p x ↔ Set.Iic o ⊆ grundyAux p '' moves p x
    source
    theorem IGame.mem_grundyAux_image_of_lt {p : Player} {x : IGame} {o : Nimber} (h : o < grundyAux p x) :
    o ∈ grundyAux p '' moves p x
    source
    theorem IGame.grundyAux_le_of_notMem {p : Player} {x : IGame} {o : Nimber} (h : o ∉ grundyAux p '' moves p x) :
    grundyAux p x ≤ o
    source
    theorem IGame.grundyAux_ne {p : Player} {x y : IGame} (hy : y ∈ moves p x) :
    grundyAux p y ≠ grundyAux p x
    source
    @[simp, irreducible]
    theorem IGame.grundyAux_add (p : Player) (x y : IGame) :
    grundyAux p (x + y) = grundyAux p x + grundyAux p y
    source
    @[simp, irreducible]
    theorem IGame.grundyAux_neg (p : Player) (x : IGame) :
    grundyAux p (-x) = grundyAux (-p) x
    source
    @[simp]
    theorem IGame.grundyAux_image_neg (p : Player) (s : Set IGame) :
    grundyAux p '' (-s) = grundyAux (-p) '' s
    source
    @[simp]
    theorem IGame.grundyAux_sub (p : Player) (x y : IGame) :
    grundyAux p (x - y) = grundyAux p x + grundyAux (-p) y
    source
    def IGame.Impartial.grundy (x : IGame) [x.Impartial] :
    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 its options.

    This definition enforces that x is impartial. If you want to talk about the left or right Grundy values of a game (e.g. if you don't yet know it to be impartial), use grundyAux. The lemma grundyAux_eq_grundy shows that both definitions match in the case of an impartial game.

    Equations
    Instances For
      source
      @[irreducible]
      theorem IGame.Impartial.nim_grundy_equiv (x : IGame) [x.Impartial] :
      nim (grundy x) ≈ x

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

      source
      theorem IGame.Impartial.grundy_eq_iff_equiv_nim {x : IGame} [x.Impartial] {o : Nimber} :
      grundy x = o ↔ x ≈ nim o
      source
      theorem IGame.Impartial.grundy_eq {x : IGame} [x.Impartial] {o : Nimber} :
      x ≈ nim o → grundy x = o

      Alias of the reverse direction of IGame.Impartial.grundy_eq_iff_equiv_nim.

      source
      theorem IGame.Impartial.grundy_eq_zero_iff {x : IGame} [x.Impartial] :
      grundy x = 0 ↔ x ≈ 0
      source
      @[simp]
      theorem IGame.Impartial.grundy_eq_iff_equiv {x y : IGame} [x.Impartial] [y.Impartial] :
      grundy x = grundy y ↔ x ≈ y
      source
      @[simp]
      theorem IGame.Impartial.grundy_nim (o : Nimber) :
      grundy (nim o) = o
      source
      @[simp]
      theorem IGame.Impartial.grundy_zero :
      grundy 0 = 0
      source
      @[simp]
      theorem IGame.Impartial.grundy_star :
      grundy ⋆ = 1
      source
      @[simp]
      theorem IGame.Impartial.grundy_neg (x : IGame) [x.Impartial] :
      grundy (-x) = grundy x
      source
      @[simp]
      theorem IGame.Impartial.grundyAux_eq_grundy (p : Player) (x : IGame) [x.Impartial] :
      grundyAux p x = grundy x
      source
      @[simp]
      theorem IGame.Impartial.grundy_add (x y : IGame) [x.Impartial] [y.Impartial] :
      grundy (x + y) = grundy x + grundy y
      source
      theorem IGame.nim_add_equiv (a b : Nimber) :
      nim a + nim b ≈ nim (a + b)
      source
      theorem IGame.Impartial.grundy_moves_ne {p : Player} {x y : IGame} [x.Impartial] (hy : y ∈ moves p x) :
      have this := ⋯; grundy y ≠ grundy x
      source
      theorem IGame.Impartial.lt_of_numeric_of_pos (x : IGame) [x.Impartial] {y : IGame} [y.Numeric] (hy : 0 < y) :
      x < y

      One half of the lawnmower theorem for impartial games.

      source
      theorem IGame.Impartial.lt_of_numeric_of_neg (x : IGame) [x.Impartial] {y : IGame} [y.Numeric] (hy : y < 0) :
      y < x

      One half of the lawnmower theorem for impartial games.

      source
      theorem IGame.Impartial.of_grundyAux_left_eq_grundyAux_right {x : IGame} (h : ∀ (p : Player), ∀ y ∈ moves p x, y.Impartial) (H : grundyAux left x = grundyAux right x) :
      x.Impartial

      If a game x has only impartial options, and its left Grundy value equals its right Grundy value, then it's impartial.