Lax Lean Archive

Sprague–Grundy values

Lax783278.Grundy · concepts/Lax783278/Grundy.lean · lax-783278

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    The minimum excluded value of a finite set of natural numbers is the least natural number outside the set. The Sprague–Grundy value of a position is the minimum excluded value of the values reachable in one move. In particular, a terminal position has value zero.

    Concept map
    2 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax783278.ArcKayles
    2import Mathlib.Order.ConditionallyCompleteLattice.Basic
    3import Mathlib.Order.Lattice.Nat
    4
    5/-!
    6---
    7title: Sprague–Grundy values
    8type: definition
    9---
    10The minimum excluded value of a finite set of natural numbers is the least
    11natural number outside the set. The Sprague–Grundy value of a position is
    12the minimum excluded value of the values reachable in one move.
    13In particular, a terminal position has value zero.
    14-/
    15
    16namespace Lax783278.Grundy
    17
    18open ArcKayles
    19
    20/-- The least natural number not in the finite set `S`. -/
    21noncomputable def mex (S : Finset ℕ) : ℕ := sInf {n : ℕ | n ∉ S}
    22
    23/-- The game value obtained from `rounds` rounds of backward induction.
    24A position at depth zero has value zero; each further round takes the
    25minimum excluded value of its immediate successors. -/
    26noncomputable def valueAfter {V : Type} [DecidableEq V]
    27 (G : SimpleGraph V) : ℕ → Finset V → ℕ
    28 | 0, _ => 0
    29 | rounds + 1, S =>
    30 mex ((moves G S).image fun e => valueAfter G rounds (remove S e.1 e.2))
    31
    32/-- The Sprague–Grundy value of the complete game tree. Its depth is at most
    33the number of surviving vertices, because every move removes two vertices. -/
    34noncomputable def value {V : Type} [DecidableEq V]
    35 (G : SimpleGraph V) (S : Finset V) : ℕ :=
    36 valueAfter G S.card S
    37
    38end Lax783278.Grundy
    39
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…