Documentation

CombinatorialGames.Game.Specific.Nim

Nim and the Sprague-Grundy theorem #

In the game of nim o, for o an ordinal number, both players may move to nim a for any a < o.

We also define a Grundy value for an impartial game x and prove the Sprague-Grundy theorem, that x is equivalent to nim (grundy x). Finally, we prove that the grundy value of a sum x + y corresponds to the nimber sum of the individual grundy values.

source
theorem Nimber.Iio_toNimber (n : ℕ) :
Set.Iio (Ordinal.toNimber ↑n) = ⇑Ordinal.toNimber '' Set.Iio ↑n

Nim game #

source
@[irreducible]
noncomputable def IGame.nim (o : Nimber) :
IGame

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
    source
    theorem IGame.nim_def (o : Nimber) :
    nim o = {nim '' Set.Iio o | nim '' Set.Iio o}ᴵ
    source
    @[simp]
    theorem IGame.leftMoves_nim (o : Nimber) :
    (nim o).leftMoves = nim '' Set.Iio o
    source
    @[simp]
    theorem IGame.rightMoves_nim (o : Nimber) :
    (nim o).rightMoves = nim '' Set.Iio o
    source
    theorem IGame.forall_leftMoves_nim {P : IGame → Prop} {o : Nimber} :
    (∀ x ∈ (nim o).leftMoves, P x) ↔ ∀ a < o, P (nim a)
    source
    theorem IGame.forall_rightMoves_nim {P : IGame → Prop} {o : Nimber} :
    (∀ x ∈ (nim o).rightMoves, P x) ↔ ∀ a < o, P (nim a)
    source
    theorem IGame.exists_leftMoves_nim {P : IGame → Prop} {o : Nimber} :
    (∃ x ∈ (nim o).leftMoves, P x) ↔ ∃ a < o, P (nim a)
    source
    theorem IGame.exists_rightMoves_nim {P : IGame → Prop} {o : Nimber} :
    (∃ x ∈ (nim o).rightMoves, P x) ↔ ∃ a < o, P (nim a)
    source
    theorem IGame.forall_leftMoves_nim_natCast {P : IGame → Prop} {n : ℕ} :
    (∀ x ∈ (nim (Ordinal.toNimber ↑n)).leftMoves, P x) ↔ ∀ m < n, P (nim (Ordinal.toNimber ↑m))
    source
    theorem IGame.forall_rightMoves_nim_natCast {P : IGame → Prop} {n : ℕ} :
    (∀ x ∈ (nim (Ordinal.toNimber ↑n)).rightMoves, P x) ↔ ∀ m < n, P (nim (Ordinal.toNimber ↑m))
    source
    theorem IGame.exists_leftMoves_nim_natCast {P : IGame → Prop} {n : ℕ} :
    (∃ x ∈ (nim (Ordinal.toNimber ↑n)).leftMoves, P x) ↔ ∃ m < n, P (nim (Ordinal.toNimber ↑m))
    source
    theorem IGame.exists_rightMoves_nim_natCast {P : IGame → Prop} {n : ℕ} :
    (∃ x ∈ (nim (Ordinal.toNimber ↑n)).rightMoves, P x) ↔ ∃ m < n, P (nim (Ordinal.toNimber ↑m))
    source
    theorem IGame.forall_leftMoves_nim_ofNat {P : IGame → Prop} {n : ℕ} [n.AtLeastTwo] :
    (∀ x ∈ (nim (Ordinal.toNimber (OfNat.ofNat n))).leftMoves, P x) ↔ ∀ m < n, P (nim (Ordinal.toNimber ↑m))
    source
    theorem IGame.forall_rightMoves_nim_ofNat {P : IGame → Prop} {n : ℕ} [n.AtLeastTwo] :
    (∀ x ∈ (nim (Ordinal.toNimber (OfNat.ofNat n))).rightMoves, P x) ↔ ∀ m < n, P (nim (Ordinal.toNimber ↑m))
    source
    theorem IGame.exists_leftMoves_nim_ofNat {P : IGame → Prop} {n : ℕ} [n.AtLeastTwo] :
    (∃ x ∈ (nim (Ordinal.toNimber (OfNat.ofNat n))).leftMoves, P x) ↔ ∃ m < n, P (nim (Ordinal.toNimber ↑m))
    source
    theorem IGame.exists_rightMoves_nim_ofNat {P : IGame → Prop} {n : ℕ} [n.AtLeastTwo] :
    (∃ x ∈ (nim (Ordinal.toNimber (OfNat.ofNat n))).rightMoves, P x) ↔ ∃ m < n, P (nim (Ordinal.toNimber ↑m))
    source
    theorem IGame.mem_leftMoves_nim_of_lt {a b : Nimber} (h : a < b) :
    nim a ∈ (nim b).leftMoves
    source
    theorem IGame.mem_rightMoves_nim_of_lt {a b : Nimber} (h : a < b) :
    nim a ∈ (nim b).rightMoves
    source
    theorem IGame.nim_injective :
    Function.Injective nim
    source
    @[simp]
    theorem IGame.nim_inj {a b : Nimber} :
    nim a = nim b ↔ a = b
    source
    @[simp]
    theorem IGame.nim_zero :
    nim 0 = 0
    source
    @[simp]
    theorem IGame.nim_one :
    nim 1 = ⋆
    source
    @[simp, irreducible]
    theorem IGame.birthday_nim (o : Nimber) :
    (nim o).birthday = o
    source
    @[simp, irreducible]
    theorem IGame.neg_nim (o : Nimber) :
    -nim o = nim o
    source
    @[irreducible]
    instance IGame.impartial_nim (o : Nimber) :
    (nim o).Impartial
    source
    @[simp]
    theorem IGame.nim_equiv_iff {a b : Nimber} :
    nim a ≈ nim b ↔ a = b
    source
    @[simp]
    theorem IGame.nim_fuzzy_iff {a b : Nimber} :
    nim a ‖ nim b ↔ a ≠ b
    source
    @[irreducible]
    theorem IGame.nim_add_equiv (a b : Nimber) :
    nim a + nim b ≈ nim (a + b)

    Grundy value #

    source
    @[irreducible]
    noncomputable def IGame.Impartial.grundy (x : IGame) :
    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 nimber which corresponds to the game of nim that the game is equivalent to.

    Equations
    Instances For
      source
      theorem IGame.Impartial.grundy_def (x : IGame) :
      grundy x = sInf (grundy '' x.leftMoves)ᶜ

      This version is stated in terms of left moves of x.

      source
      theorem IGame.Impartial.le_grundy_iff {x : IGame} {o : Nimber} :
      o ≤ grundy x ↔ Set.Iio o ⊆ grundy '' x.leftMoves

      This version is stated in terms of left moves of x.

      source
      theorem IGame.Impartial.lt_grundy_iff {x : IGame} {o : Nimber} :
      o < grundy x ↔ Set.Iic o ⊆ grundy '' x.leftMoves

      This version is stated in terms of left moves of x.

      source
      theorem IGame.Impartial.mem_grundy_image_of_lt {x : IGame} {o : Nimber} (h : o < grundy x) :
      o ∈ grundy '' x.leftMoves

      This version is stated in terms of left moves of x.

      source
      theorem IGame.Impartial.grundy_ne {x y : IGame} (hy : y ∈ x.leftMoves) :
      grundy y ≠ grundy x

      This version is stated in terms of left moves of x.

      source
      @[irreducible]
      theorem IGame.Impartial.equiv_nim_grundy (x : IGame) [x.Impartial] :
      x ≈ nim (grundy 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_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.grundy_add (x y : IGame) [x.Impartial] [y.Impartial] :
      grundy (x + y) = grundy x + grundy y
      source
      theorem IGame.Impartial.grundy_def' (x : IGame) [x.Impartial] :
      grundy x = sInf (grundy '' x.rightMoves)ᶜ

      This version is stated in terms of right moves of x.

      source
      theorem IGame.Impartial.le_grundy_iff' {x : IGame} [x.Impartial] {o : Nimber} :
      o ≤ grundy x ↔ Set.Iio o ⊆ grundy '' x.rightMoves

      This version is stated in terms of right moves of x.

      source
      theorem IGame.Impartial.lt_grundy_iff' {x : IGame} [x.Impartial] {o : Nimber} :
      o < grundy x ↔ Set.Iic o ⊆ grundy '' x.rightMoves

      This version is stated in terms of right moves of x.

      source
      theorem IGame.Impartial.mem_grundy_image_of_lt' {x : IGame} [x.Impartial] {o : Nimber} (h : o < grundy x) :
      o ∈ grundy '' x.rightMoves

      This version is stated in terms of right moves of x.

      source
      theorem IGame.Impartial.grundy_ne' {x y : IGame} [x.Impartial] (hy : y ∈ x.rightMoves) :
      grundy y ≠ grundy x

      This version is stated in terms of right moves of x.