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 three definitions for the Grundy value. leftGrundy and rightGrundy are computed using the left/right options of the game respectively, and are 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 leftGrundy or rightGrundy.

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

Grundy value

@[irreducible]

def IGame.leftGrundy (x : IGame) : Nimber

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

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

Equations

• x.leftGrundy = sInf (Set.range fun (y : ↑x.leftMoves) => (↑y).leftGrundy)ᶜ

theorem IGame.leftGrundy_def (x : IGame) : x.leftGrundy = sInf (leftGrundy '' x.leftMoves)ᶜ

theorem IGame.le_leftGrundy_iff {x : IGame} {o : Nimber} : o ≤ x.leftGrundy ↔ Set.Iio o ⊆ leftGrundy '' x.leftMoves

theorem IGame.lt_leftGrundy_iff {x : IGame} {o : Nimber} : o < x.leftGrundy ↔ Set.Iic o ⊆ leftGrundy '' x.leftMoves

theorem IGame.mem_leftGrundy_image_of_lt {x : IGame} {o : Nimber} (h : o < x.leftGrundy) : o ∈ leftGrundy '' x.leftMoves

theorem IGame.leftGrundy_le_of_notMem {x : IGame} {o : Nimber} (h : o ∉ leftGrundy '' x.leftMoves) : x.leftGrundy ≤ o

theorem IGame.leftGrundy_ne {x y : IGame} (hy : y ∈ x.leftMoves) : y.leftGrundy ≠ x.leftGrundy

@[simp, irreducible]

theorem IGame.leftGrundy_add (x y : IGame) : (x + y).leftGrundy = x.leftGrundy + y.leftGrundy

@[irreducible]

def IGame.rightGrundy (x : IGame) : Nimber

The right Grundy value of a game is recursively defined as the minimum excluded value (the infimum of the complement) of the right Grundy values of its 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

• x.rightGrundy = sInf (Set.range fun (y : ↑x.rightMoves) => (↑y).rightGrundy)ᶜ

theorem IGame.rightGrundy_def (x : IGame) : x.rightGrundy = sInf (rightGrundy '' x.rightMoves)ᶜ

@[simp, irreducible]

theorem IGame.leftGrundy_neg (x : IGame) : (-x).leftGrundy = x.rightGrundy

@[simp]

theorem IGame.rightGrundy_neg (x : IGame) : (-x).rightGrundy = x.leftGrundy

@[simp]

theorem IGame.leftGrundy_image_neg (s : Set IGame) : leftGrundy '' (-s) = rightGrundy '' s

@[simp]

theorem IGame.rightGrundy_image_neg (s : Set IGame) : rightGrundy '' (-s) = leftGrundy '' s

theorem IGame.le_rightGrundy_iff {x : IGame} {o : Nimber} : o ≤ x.rightGrundy ↔ Set.Iio o ⊆ rightGrundy '' x.rightMoves

theorem IGame.lt_rightGrundy_iff {x : IGame} {o : Nimber} : o < x.rightGrundy ↔ Set.Iic o ⊆ rightGrundy '' x.rightMoves

theorem IGame.mem_rightGrundy_image_of_lt {x : IGame} {o : Nimber} (h : o < x.rightGrundy) : o ∈ rightGrundy '' x.rightMoves

theorem IGame.rightGrundy_le_of_notMem {x : IGame} {o : Nimber} (h : o ∉ rightGrundy '' x.rightMoves) : x.rightGrundy ≤ o

theorem IGame.rightGrundy_ne {x y : IGame} : y ∈ x.rightMoves → y.rightGrundy ≠ x.rightGrundy

@[simp]

theorem IGame.rightGrundy_add (x y : IGame) : (x + y).rightGrundy = x.rightGrundy + y.rightGrundy

@[simp]

theorem IGame.leftGrundy_sub (x y : IGame) : (x - y).leftGrundy = x.leftGrundy + y.rightGrundy

@[simp]

theorem IGame.rightGrundy_sub (x y : IGame) : (x - y).rightGrundy = x.rightGrundy + y.leftGrundy

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 leftGrundy or rightGrundy. The lemmas leftGrundy_eq_grundy and rightGrundy_eq_grundy show that both definitions match in the case of an impartial game.

Equations

• IGame.Impartial.grundy x = x.rightGrundy

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

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

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.

theorem IGame.Impartial.grundy_eq_zero_iff {x : IGame} [x.Impartial] : grundy x = 0 ↔ x ≈ 0

@[simp]

theorem IGame.Impartial.grundy_eq_iff_equiv {x y : IGame} [x.Impartial] [y.Impartial] : grundy x = grundy y ↔ x ≈ y

@[simp]

theorem IGame.Impartial.grundy_nim (o : Nimber) : grundy (nim o) = o

@[simp]

theorem IGame.Impartial.grundy_zero : grundy 0 = 0

@[simp]

theorem IGame.Impartial.grundy_star : grundy ⋆ = 1

@[simp]

theorem IGame.Impartial.grundy_neg (x : IGame) [x.Impartial] : grundy (-x) = grundy x

@[simp]

theorem IGame.Impartial.leftGrundy_eq_grundy (x : IGame) [x.Impartial] : x.leftGrundy = grundy x

@[simp]

theorem IGame.Impartial.rightGrundy_eq_grundy (x : IGame) [x.Impartial] : x.rightGrundy = grundy x

@[simp]

theorem IGame.Impartial.grundy_add (x y : IGame) [x.Impartial] [y.Impartial] : grundy (x + y) = grundy x + grundy y

theorem IGame.nim_add_equiv (a b : Nimber) : nim a + nim b ≈ nim (a + b)

theorem IGame.Impartial.grundy_leftMove_ne {x y : IGame} [x.Impartial] (hy : y ∈ x.leftMoves) : have this := ⋯; grundy y ≠ grundy x

theorem IGame.Impartial.grundy_rightMove_ne {x y : IGame} [x.Impartial] (hy : y ∈ x.rightMoves) : have this := ⋯; grundy y ≠ grundy x

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.

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.

theorem IGame.Impartial.of_leftGrundy_eq_rightGrundy {x : IGame} (hl : ∀ y ∈ x.leftMoves, y.Impartial) (hr : ∀ y ∈ x.rightMoves, y.Impartial) (H : x.leftGrundy = x.rightGrundy) : x.Impartial

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

Multiplication

instance IGame.Impartial.mul (x y : IGame) [x.Impartial] [y.Impartial] : (x * y).Impartial

@[simp]

theorem IGame.Impartial.grundy_mul (x y : IGame) [x.Impartial] [y.Impartial] : grundy (x * y) = grundy x * grundy y

theorem IGame.nim_mul_equiv (a b : Nimber) : nim a * nim b ≈ nim (a * b)

theorem IGame.Impartial.mul_equiv_zero {x y : IGame} [x.Impartial] [y.Impartial] : x * y ≈ 0 ↔ x ≈ 0 ∨ y ≈ 0

instance IGame.Impartial.mulOption (x y a b : IGame) [x.Impartial] [y.Impartial] [a.Impartial] [b.Impartial] : (mulOption x y a b).Impartial

theorem IGame.Impartial.mul_congr_left {x₁ x₂ y : IGame} [x₁.Impartial] [x₂.Impartial] [y.Impartial] (he : x₁ ≈ x₂) : x₁ * y ≈ x₂ * y

theorem IGame.Impartial.mul_congr_right {x y₁ y₂ : IGame} [x.Impartial] [y₁.Impartial] [y₂.Impartial] (he : y₁ ≈ y₂) : x * y₁ ≈ x * y₂

theorem IGame.Impartial.mul_congr {x₁ x₂ y₁ y₂ : IGame} [x₁.Impartial] [x₂.Impartial] [y₁.Impartial] [y₂.Impartial] (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁ * y₁ ≈ x₂ * y₂