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.

Nim game

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

theorem IGame.nim_def (o : Nimber) : nim o = {nim '' Set.Iio o | nim '' Set.Iio o}ᴵ

@[simp]

theorem IGame.leftMoves_nim (o : Nimber) : (nim o).leftMoves = nim '' Set.Iio o

@[simp]

theorem IGame.rightMoves_nim (o : Nimber) : (nim o).rightMoves = nim '' Set.Iio o

theorem IGame.forall_leftMoves_nim {P : IGame → Prop} {o : Nimber} : (∀ x ∈ (nim o).leftMoves, P x) ↔ ∀ a < o, P (nim a)

theorem IGame.forall_rightMoves_nim {P : IGame → Prop} {o : Nimber} : (∀ x ∈ (nim o).rightMoves, P x) ↔ ∀ a < o, P (nim a)

theorem IGame.exists_leftMoves_nim {P : IGame → Prop} {o : Nimber} : (∃ x ∈ (nim o).leftMoves, P x) ↔ ∃ a < o, P (nim a)

theorem IGame.exists_rightMoves_nim {P : IGame → Prop} {o : Nimber} : (∃ x ∈ (nim o).rightMoves, P x) ↔ ∃ a < o, P (nim a)

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

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

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

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

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

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

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

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

theorem IGame.mem_leftMoves_nim_of_lt {a b : Nimber} (h : a < b) : nim a ∈ (nim b).leftMoves

theorem IGame.mem_rightMoves_nim_of_lt {a b : Nimber} (h : a < b) : nim a ∈ (nim b).rightMoves

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 = o

@[simp, irreducible]

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

@[irreducible]

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