Arc Kayles
Lax783278.ArcKayles · concepts/Lax783278/ArcKayles.lean · lax-783278
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural 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
Lean source view on GitHub
| 1 | import Mathlib.Combinatorics.SimpleGraph.Basic |
| 2 | import Mathlib.Data.Finset.Card |
| 3 | import Mathlib.Data.Finset.Prod |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Arc Kayles |
| 8 | type: definition |
| 9 | --- |
| 10 | A position consists of a finite set of surviving vertices of a simple graph. |
| 11 | A move removes the two endpoints of a surviving edge. Under normal play, |
| 12 | the player with no legal move loses. A position is winning for the player |
| 13 | to move if some legal move leaves a position losing for the opponent. |
| 14 | Isolated vertices may be retained: they permit no moves. |
| 15 | -/ |
| 16 | |
| 17 | namespace Lax783278.ArcKayles |
| 18 | |
| 19 | open scoped Classical |
| 20 | |
| 21 | variable {V : Type} [DecidableEq V] |
| 22 | |
| 23 | /-- The position after playing an edge with endpoints `u` and `v`. -/ |
| 24 | def remove (S : Finset V) (u v : V) : Finset V := (S.erase u).erase v |
| 25 | |
| 26 | /-- Legal moves, represented by ordered pairs of endpoints. -/ |
| 27 | noncomputable def moves (G : SimpleGraph V) (S : Finset V) : Finset (V × V) := |
| 28 | (S ×ˢ S).filter fun e => G.Adj e.1 e.2 |
| 29 | |
| 30 | /-- Backward induction through `rounds` moves. With no rounds left the |
| 31 | player to move loses; otherwise a winning move leaves a losing position. -/ |
| 32 | def WinningAfter (G : SimpleGraph V) : ℕ → Finset V → Prop |
| 33 | | 0, _ => False |
| 34 | | rounds + 1, S => |
| 35 | ∃ e ∈ moves G S, ¬ WinningAfter G rounds (remove S e.1 e.2) |
| 36 | |
| 37 | /-- A winning strategy for the next player. There are at most `S.card` moves, |
| 38 | since every move removes vertices, so this many rounds evaluates the whole game. -/ |
| 39 | def Winning (G : SimpleGraph V) (S : Finset V) : Prop := |
| 40 | WinningAfter G S.card S |
| 41 | |
| 42 | end Lax783278.ArcKayles |
| 43 |
Builds on
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments