Lax Lean Archive

Sprague–Grundy values

Lax689614.Grundy · concepts/Lax689614/Grundy.lean · lax-689614

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 Lax689614.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 Lax689614.Grundy
    17
    18open ArcKayles
    19
    20noncomputable def mex (S : Finset ℕ) : ℕ := sInf {n : ℕ | n ∉ S}
    21
    22noncomputable def value {V : Type} [DecidableEq V]
    23 (G : SimpleGraph V) (S : Finset V) : ℕ :=
    24 mex ((moves G S).attach.image fun e => value G (remove S e.val.1 e.val.2))
    25termination_by S.card
    26decreasing_by
    27 have h := e.property
    28 simp only [moves, Finset.mem_filter, Finset.mem_product] at h
    29 exact lt_of_le_of_lt Finset.card_erase_le (Finset.card_erase_lt_of_mem h.1.1)
    30
    31end Lax689614.Grundy
    32
    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…