Lax Lean Archive

Arc Kayles

Lax689614.ArcKayles · concepts/Lax689614/ArcKayles.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

    A position consists of a finite set of surviving vertices of a simple graph. A move removes the two endpoints of a surviving edge. Under normal play, the player with no legal move loses. A position is winning for the player to move if some legal move leaves a position losing for the opponent. Isolated vertices may be retained: they permit no moves.

    Concept map
    1 concept; 10 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Basic
    2import Mathlib.Data.Finset.Card
    3import Mathlib.Data.Finset.Prod
    4
    5/-!
    6---
    7title: Arc Kayles
    8type: definition
    9---
    10A position consists of a finite set of surviving vertices of a simple graph.
    11A move removes the two endpoints of a surviving edge. Under normal play,
    12the player with no legal move loses. A position is winning for the player
    13to move if some legal move leaves a position losing for the opponent.
    14Isolated vertices may be retained: they permit no moves.
    15-/
    16
    17namespace Lax689614.ArcKayles
    18
    19variable {V : Type} [DecidableEq V]
    20
    21/-- The position after playing an edge with endpoints `u` and `v`. -/
    22def remove (S : Finset V) (u v : V) : Finset V := (S.erase u).erase v
    23
    24/-- Legal moves, represented by ordered pairs of endpoints. -/
    25noncomputable def moves (G : SimpleGraph V) (S : Finset V) : Finset (V × V) := by
    26 classical
    27 exact (S ×ˢ S).filter fun e => G.Adj e.1 e.2
    28
    29/-- Winning for the next player, by backward induction on surviving vertices. -/
    30def Winning (G : SimpleGraph V) (S : Finset V) : Prop :=
    31 ∃ e : {e // e ∈ moves G S}, ¬ Winning G (remove S e.val.1 e.val.2)
    32termination_by S.card
    33decreasing_by
    34 have h := e.property
    35 simp only [moves, Finset.mem_filter, Finset.mem_product] at h
    36 exact lt_of_le_of_lt Finset.card_erase_le (Finset.card_erase_lt_of_mem h.1.1)
    37
    38end Lax689614.ArcKayles
    39
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…