Nim

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

This is an impartial game; in fact, in a strong sense, it's the simplest impartial game, as by the Sprague-Grundy theorem, any other impartial game is equivalent to some game of nim. As such, many results on Nim are proven in Game.Impartial.Grundy.

We define nim in terms of a Nimber rather than an Ordinal, as this makes the results nim (a + b) ≈ nim a + nim b and nim (a * b) ≈ nim a * nim b much easier to state.

@[reducible, inline]

abbrev GameGraph.nim : GameGraph Nimber

The game of nim as a GameGraph.

Equations

• GameGraph.nim = { moves := fun (x : Player) => Set.Iio }

instance GameGraph.instIsWellFoundedNimberIsOptionNim : IsWellFounded Nimber nim.IsOption

Nim game

noncomputable def IGame.nim : 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

• IGame.nim = GameGraph.nim.toIGame

theorem IGame.nim_def (o : Nimber) : nim o = !{fun (x : Player) => nim '' Set.Iio o}

@[simp]

theorem IGame.moves_nim (p : Player) (o : Nimber) : moves p (nim o) = nim '' Set.Iio o

theorem IGame.forall_moves_nim {p : Player} {P : IGame → Prop} {o : Nimber} : (∀ x ∈ moves p (nim o), P x) ↔ ∀ a < o, P (nim a)

theorem IGame.exists_moves_nim {p : Player} {P : IGame → Prop} {o : Nimber} : (∃ x ∈ moves p (nim o), P x) ↔ ∃ a < o, P (nim a)

theorem IGame.forall_moves_nim_natCast {p : Player} {P : IGame → Prop} {n : ℕ} : (∀ x ∈ moves p (nim (Nimber.of ↑n)), P x) ↔ ∀ m < n, P (nim (Nimber.of ↑m))

theorem IGame.exists_moves_nim_natCast {p : Player} {P : IGame → Prop} {n : ℕ} : (∃ x ∈ moves p (nim (Nimber.of ↑n)), P x) ↔ ∃ m < n, P (nim (Nimber.of ↑m))

theorem IGame.forall_moves_nim_ofNat {p : Player} {P : IGame → Prop} {n : ℕ} [n.AtLeastTwo] : (∀ x ∈ moves p (nim (Nimber.of (OfNat.ofNat n))), P x) ↔ ∀ m < n, P (nim (Nimber.of ↑m))

theorem IGame.exists_moves_nim_ofNat {p : Player} {P : IGame → Prop} {n : ℕ} [n.AtLeastTwo] : (∃ x ∈ moves p (nim (Nimber.of (OfNat.ofNat n))), P x) ↔ ∃ m < n, P (nim (Nimber.of ↑m))

theorem IGame.mem_moves_nim_of_lt {a b : Nimber} (p : Player) (h : a < b) : nim a ∈ moves p (nim b)

theorem IGame.nim_injective : Function.Injective nim

@[simp]

theorem IGame.nim_inj {a b : Nimber} : nim a = nim b ↔ a = b

@[simp]

theorem IGame.nim_zero : nim 0 = 0

@[simp]

theorem IGame.nim_one : nim 1 = ⋆

@[simp, irreducible]

theorem IGame.birthday_nim (o : Nimber) : (nim o).birthday = NatOrdinal.of (Nimber.val o)

@[simp]

theorem IGame.neg_nim (o : Nimber) : -nim o = nim o

instance IGame.Impartial.nim (o : Nimber) : (nim o).Impartial

@[irreducible]

instance IGame.Dicotic.nim (o : Nimber) : (nim o).Dicotic

@[simp]

theorem IGame.nim_equiv_iff {a b : Nimber} : nim a ≈ nim b ↔ a = b

@[simp]

theorem IGame.nim_fuzzy_iff {a b : Nimber} : nim a ‖ nim b ↔ a ≠ b