Sprague–Grundy theorem

TheoremUniqueness of the P-positions of a terminating impartial game#✓fully proved

Write \(x \to y\) when there is a move from position \(x\) to position \(y\), and assume there is no infinite sequence of moves \(x_0 \to x_1 \to x_2 \to \cdots\). Call a set \(P\) of positions stable if no move leads from a position in \(P\) to a position in \(P\), and absorbing if from every position outside \(P\) some move leads to a position in \(P\). Then any two stable and absorbing sets of positions are equal.

In particular the P-positions are determined by stability and absorption, and the N-positions are their complement.

theorem pPositions_unique
    {Position : Type*}
    (move : Position → Position → Prop)
    (hmove : WellFounded (fun next current => move current next))
    (P Q : Set Position)
    (hP_stable : ∀ x y : Position, x ∈ P → move x y → y ∉ P)
    (hP_absorbing : ∀ x : Position, x ∉ P → ∃ y : Position, move x y ∧ y ∈ P)
    (hQ_stable : ∀ x y : Position, x ∈ Q → move x y → y ∉ Q)
    (hQ_absorbing : ∀ x : Position, x ∉ Q → ∃ y : Position, move x y ∧ y ∈ Q) :
    P = Q

Sources

• Antoine Renard and Michel Rigo, "Variants of Wythoff Game with Terminal Positions or Blocking Maneuvers," Journal of Integer Sequences 29 (2026), Article 26.1.6, Proposition (Folklore), lines 438–448, https://cs.uwaterloo.ca/journals/JIS/VOL29/Rigo/rigo5.tex; stability and absorption are defined in lines 430–436. Termination is encoded by the well-foundedness of the move relation on the acyclic game graph.

Used by 1

Used byUniqueness of the set of P-positions

StructureImpartial game#✓fully proved

An impartial game consists of a type of positions, a starting position, for each position \(p\) a finite set of positions reachable from \(p\) in one move, and a rank function assigning a natural number to each position such that every move strictly decreases the rank: if \(q\) is reachable from \(p\) in one move, then \(\mathrm{rank}(q) < \mathrm{rank}(p)\).

Because the move sets are finite and the rank strictly decreases along moves, every play terminates and only finitely many positions are reachable from any position, even if the type of positions is infinite or contains unreachable positions.

structure ImpartialGame where
  Pos : Type
  eqDec : DecidableEq Pos
  moves : Pos → Finset Pos
  rank : Pos → ℕ
  rank_lt : ∀ p q, q ∈ moves p → rank q < rank p
  start : Pos

Used by 34

Used byContinued fractions with maximal optimal play in Euclid · Positions of a Calkin–Wilf row with maximal optimal play in Euclid · The game Euclid · Correctness of the fuel-bounded Euclid classifier · Golden-ratio bounds for N-positions of maximal remoteness above 1 · Golden-ratio bounds for N-positions of maximal remoteness below 1 · Golden-ratio bounds for P-positions of maximal remoteness · Maximal-remoteness paths alternate in pairs · The \((k+1:k)\)-pebbling game · Positions with at most \(k\) pebbles on every vertex are P-positions · Moves of a placement game · Normal-play recursion for placement games · The placement game · The Maximum Nim game · P-positions of Maximum Nim · Equivalence of impartial games via their sum · P-positions are the games of Sprague–Grundy value zero · The Princess and the Roses game · Lim's theorem on five-pile P&R · The P&R Helper game · Simplified Princess and the Roses · Mex rule for Sprague–Grundy values · In two-pile Princess and the Roses, \((1, 1)\) moves to \((0, 0)\) · Slow\(A\)-Nim · The empty position is a P-position · Smith's remoteness function · Recursion for Smith's remoteness · Smith's remoteness vanishes at terminal positions · Equivalence of impartial games · Sum of impartial games · P-positions · Recursive characterization of P-positions · Nim heap · Sprague–Grundy theorem

DefinitionP-positions#✓fully proved

In an impartial game \(G\), the P-positions are defined by well-founded recursion along moves: a position \(p\) is a P-position if and only if no position reachable from \(p\) in one move is a P-position. Positions that are not P-positions are called N-positions.

Under normal play, where the player unable to move loses, the P-positions are exactly the positions from which the player to move loses.

noncomputable def IsP (G : ImpartialGame) : G.Pos → Prop :=
  (wfRel G).fix fun p ih => ∀ q (h : q ∈ G.moves p), ¬ ih q h

Uses 1 · Used by 38

Statement usesImpartial game

Used byCorrectness of the fuel-bounded Euclid classifier · The Euclid P-position test is correct · Totals at which every pebbling game is an N-game · Pebbling on the triangle: total 6k-1 with a pile of at least 4k+1 · Pebbling on the triangle: N-positions with total 6k-2ℓ+1 and a small pile · Pebbling on the triangle: total 6k-1 with every pile at most 4k · Pebbling on the triangle: N-positions with an empty vertex · Pebbling on the triangle: piles 4k+1, k-1, k-1 form a P-position · Pebbling on the triangle: total 6k-2ℓ with no pile above half is a P-position · Pebbling on the triangle: a single pile of 2k+3 pebbles is a P-position · Pebbling on the triangle: a two-parameter family of P-positions · Winning positions of \((2:1)\)-pebbling on \(K_2\) · Positions in \(Y_{aabc}\) are N-positions of \((2:1)\)-pebbling on \(C_4\) · Positions in \((X_{abab} \cup X_{aabc} \cup X_{aaab}) \cap (\hat Y_{abab})^c\) are N-positions of \((2:1)\)-pebbling on \(C_4\) · Parity decides \((2:1)\)-pebbling on \(C_4\) in \(\hat X_{aabb} \cup X_{abac}\) · Positions in \(\hat Y_{abab}\) are P-positions of \((2:1)\)-pebbling on \(C_4\) · Positions in \((X_{abab} \cup X_{aabc} \cup X_{aaab}) \cap \hat Y_{abac}\) are P-positions of \((2:1)\)-pebbling on \(C_4\) · Positions with at most \(k\) pebbles on every vertex are P-positions · First-player win in a placement game · Normal-play recursion for placement games · P-positions of Maximum Nim · Grundy value zero characterizes P-positions in Maximum Nim · Equivalence of impartial games via their sum · P-positions are the games of Sprague–Grundy value zero · Lim's theorem on five-pile P&R · Proposition 1 (odd P-positions of exact slow k-NIM) · Positions with the same reduction have the same outcome · P-positions of Slow \(A\)-Nim via the playable game graph · The empty position is a P-position · P-positions of Slow A-Nim with A = {1, n}, n even · P-positions of Slow A-Nim with A = {1, k}, k odd · P-positions of Slow A-Nim with A = {1, 2} on five stacks · P-positions of Slow \(\{1,2\}\)-Nim on four stacks · P-positions of Slow \(\{1,2\}\)-Nim on three stacks · Partial structure of the P-positions of Slow \(A\)-Nim · Equivalence of impartial games · Recursive characterization of P-positions · Sprague–Grundy theorem

DefinitionSum of impartial games#✓fully proved

The sum \(G + H\) of two impartial games \(G\) and \(H\) is the impartial game whose positions are the pairs \((a, b)\) of a position \(a\) of \(G\) and a position \(b\) of \(H\), and in which a move changes exactly one component: from \((a, b)\) one may move to \((a', b)\) for any move from \(a\) to \(a'\) in \(G\), or to \((a, b')\) for any move from \(b\) to \(b'\) in \(H\). Its starting position is the pair of the starting positions of \(G\) and \(H\), and the rank of \((a, b)\) is the sum of the ranks of \(a\) in \(G\) and of \(b\) in \(H\).

MetaMathlibExt.SpragueGrundy.gameSum · 24 lines

noncomputable def gameSum (G H : ImpartialGame) : ImpartialGame :=
  letI := G.eqDec
  letI := H.eqDec
  { Pos := G.Pos × H.Pos
    eqDec := inferInstance
    moves := fun p =>
      (G.moves p.1).image (fun a => (a, p.2)) ∪
        (H.moves p.2).image (fun b => (p.1, b))
    rank := fun p => G.rank p.1 + H.rank p.2
    rank_lt := by
      intro p q h
      simp only [Finset.mem_union, Finset.mem_image] at h
      cases h with
      | inl h1 =>
        obtain ⟨a', ha', heq⟩ := h1
        change (a', p.2) = q at heq
        subst heq
        exact Nat.add_lt_add_right (G.rank_lt p.1 a' ha') _
      | inr h2 =>
        obtain ⟨b', hb', heq⟩ := h2
        change (p.1, b') = q at heq
        subst heq
        exact Nat.add_lt_add_left (H.rank_lt p.2 b' hb') _
    start := (G.start, H.start) }

Uses 1 · Used by 3

Statement usesImpartial game

Used byEquivalence of impartial games via their sum · Equivalence of impartial games · Sprague–Grundy theorem

DefinitionNim heap#✓fully proved

For a natural number \(n\), the Nim heap of size \(n\) is the impartial game whose positions are \(0, 1, \dots, n\), whose starting position is \(n\), and in which a move from \(k\) goes to any \(j < k\); the rank of a position is its value.

def nimHeap (n : ℕ) : ImpartialGame where
  Pos := Fin (n + 1)
  eqDec := inferInstance
  moves := fun k => Finset.univ.filter (fun j => j.val < k.val)
  rank := fun k => k.val
  rank_lt := by
    intro k j h
    simpa using h
  start := ⟨n, Nat.lt_succ_self n⟩

Uses 1 · Used by 15

Statement usesImpartial game

Used byP-positions are the games of Sprague–Grundy value zero · Sprague–Grundy value \(5\) of P&R Helper on region \(U\) · P&R Helper positions of Sprague–Grundy value 4 on region U · Sprague–Grundy values of P&R Helper on region R · Sprague–Grundy values of P&R Helper on region L · Sprague–Grundy values of P&R Helper on region D · P&R Helper positions of Sprague–Grundy value 1 on regions U and R · P&R Helper positions of Sprague–Grundy value 6 or 7 on region U · P&R Helper positions of Sprague–Grundy value 3 on region U · P&R Helper positions of Sprague–Grundy value 2 on region U · P&R Helper positions of Sprague–Grundy value 0 · Sprague–Grundy values of three-pile Princess and the Roses · Sprague–Grundy values of two-pile Princess and the Roses · Mex rule for Sprague–Grundy values · Sprague–Grundy theorem

DefinitionEquivalence of impartial games#✓fully proved

Two impartial games \(G\) and \(H\) are equivalent when no third game tells them apart as summands: for every impartial game \(K\), the starting position of the sum \(G + K\) is a P-position if and only if the starting position of the sum \(H + K\) is a P-position. The starting position of a sum is the pair of the starting positions of its summands.

noncomputable def Equiv (G H : ImpartialGame) : Prop :=
  ∀ K : ImpartialGame,
    IsP (gameSum G K) (G.start, K.start) ↔
      IsP (gameSum H K) (H.start, K.start)

Uses 3 · Used by 19

Statement usesImpartial game · P-positions · Sum of impartial games

Used byEquivalence of impartial games via their sum · P-positions are the games of Sprague–Grundy value zero · Four-pile P&R reduces to P&R Helper · Four-pile P&R is equivalent to simplified P&R · Adding to the three largest piles of four-pile P&R · Sprague–Grundy value \(5\) of P&R Helper on region \(U\) · P&R Helper positions of Sprague–Grundy value 4 on region U · Sprague–Grundy values of P&R Helper on region R · Sprague–Grundy values of P&R Helper on region L · Sprague–Grundy values of P&R Helper on region D · P&R Helper positions of Sprague–Grundy value 1 on regions U and R · P&R Helper positions of Sprague–Grundy value 6 or 7 on region U · P&R Helper positions of Sprague–Grundy value 3 on region U · P&R Helper positions of Sprague–Grundy value 2 on region U · P&R Helper positions of Sprague–Grundy value 0 · Sprague–Grundy values of three-pile Princess and the Roses · Sprague–Grundy values of two-pile Princess and the Roses · Mex rule for Sprague–Grundy values · Sprague–Grundy theorem

TheoremRecursive characterization of P-positions#✓fully proved

In an impartial game \(G\), a position \(p\) is a P-position if and only if every position reachable from \(p\) in one move is not a P-position.

theorem isP_iff (G : ImpartialGame) (p : G.Pos) :
    IsP G p ↔ ∀ q (_ : q ∈ G.moves p), ¬ IsP G q

Uses 2 · Used by 6

Statement usesImpartial game · P-positions

Used byCorrectness of the fuel-bounded Euclid classifier · Positions with at most \(k\) pebbles on every vertex are P-positions · Normal-play recursion for placement games · P-positions of Maximum Nim · The empty position is a P-position · Sprague–Grundy theorem

TheoremSprague–Grundy theorem#✓fully proved

Every impartial game \(G\) is equivalent to a Nim heap: there is a natural number \(n\) such that \(G\) is equivalent to the Nim heap of size \(n\).

theorem sprague_grundy (G : ImpartialGame) :
    ∃ n : ℕ, Equiv G (nimHeap n)

Sources

• Tanya Khovanova and Joshua Xiong, "Nim Fractals", Journal of Integer Sequences 17 (2014), lines 101–105, https://cs.uwaterloo.ca/journals/JIS/VOL17/Khovanova/khova6.tex. Its cited original references: Grundy, Eureka 2 (1939), 6–8, reprinted 27 (1964), 9–11; Sprague, Tôhoku Math. Journal 41 (1935–1936), 438–444.

Uses 6

Statement usesEquivalence of impartial games · Impartial game · Nim heap

Proof usesP-positions · Sum of impartial games · Recursive characterization of P-positions

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.