Misere combinatorial games.

Hackenbush

Hackenbush is played on a connected graph with a designated "ground" vertex. All edges are coloured either Left (bLue) or Right (Red). On their turn, a player removes one of their coloured edges. The resulting position is the connected component containing the ground vertex.

structure MisereGames.Hackenbush (V : Type) : Type

A Hackenbush position on a finite supported graph with a ground vertex.

• graph : SimpleGraph V

  The underlying graph.

• ground : V

  The ground vertex.

• coloring : Sym2 V → Player

  Edge colouring: assigns a colour/player (Left or Right) to each pair of vertices.

• connected (v : V) : v ∈ self.graph.support → self.graph.Reachable v self.ground

  Every vertex incident to an edge is reachable from the ground vertex.

• supportFinset : Finset V

  A finset witnessing the finiteness of the graph's support.

• supportFinset_coe : ↑self.supportFinset = self.graph.support

  The supportFinset coerces to exactly the graph's support.

theorem MisereGames.Hackenbush.edgeSetFinite {V : Type} (hack : Hackenbush V) : hack.graph.edgeSet.Finite

The edge set of a Hackenbush position is finite.

noncomputable def MisereGames.Hackenbush.edgeFinset {V : Type} (hack : Hackenbush V) : Finset (Sym2 V)

The edge finset of a Hackenbush position's graph, derived from support finiteness.

Equations

• hack.edgeFinset = ⋯.toFinset

@[simp]

theorem MisereGames.Hackenbush.mem_edgeFinset {V : Type} {hack : Hackenbush V} {e : Sym2 V} : e ∈ hack.edgeFinset ↔ e ∈ hack.graph.edgeSet

noncomputable def MisereGames.Hackenbush.edgeCard {V : Type} (hack : Hackenbush V) : ℕ

The number of edges in a Hackenbush position.

Equations

• hack.edgeCard = hack.edgeFinset.card

Ground component

def MisereGames.Hackenbush.groundComp {V : Type} (graph : SimpleGraph V) (ground : V) (e : Sym2 V) : SimpleGraph V

The ground component after removing an edge: the subgraph of G.deleteEdges {e} restricted to vertices reachable from the ground vertex. An edge {u, v} is kept iff it was in G, it is not the removed edge, and both u and v are still reachable from ground.

Equations

• One or more equations did not get rendered due to their size.

theorem MisereGames.Hackenbush.groundComp_adj_iff {V : Type} {graph : SimpleGraph V} {ground : V} {e : Sym2 V} {u v : V} : (groundComp graph ground e).Adj u v ↔ (graph.deleteEdges {e}).Adj u v ∧ (graph.deleteEdges {e}).Reachable u ground ∧ (graph.deleteEdges {e}).Reachable v ground

theorem MisereGames.Hackenbush.groundComp_le {V : Type} (graph : SimpleGraph V) (ground : V) (e : Sym2 V) : groundComp graph ground e ≤ graph

theorem MisereGames.Hackenbush.groundComp_edgeSet_subset {V : Type} (graph : SimpleGraph V) (ground : V) (e : Sym2 V) : (groundComp graph ground e).edgeSet ⊆ graph.edgeSet

theorem MisereGames.Hackenbush.groundComp_edgeSet_ssubset {V : Type} {graph : SimpleGraph V} {ground : V} {e : Sym2 V} (he : e ∈ graph.edgeSet) : (groundComp graph ground e).edgeSet ⊂ graph.edgeSet

theorem MisereGames.Hackenbush.groundComp_support_subset {V : Type} (graph : SimpleGraph V) (ground : V) (e : Sym2 V) : (groundComp graph ground e).support ⊆ graph.support

The support of a ground component is a subset of the original graph's support.

theorem MisereGames.Hackenbush.reach_deleteEdges_imp_reach_groundComp {V : Type} {graph : SimpleGraph V} {ground : V} {e : Sym2 V} {v : V} (hv : (graph.deleteEdges {e}).Reachable v ground) : (groundComp graph ground e).Reachable v ground

Reachability in G.deleteEdges {e} from ground implies reachability in the ground component.

theorem MisereGames.Hackenbush.groundComp_connected {V : Type} (graph : SimpleGraph V) (ground : V) (e : Sym2 V) (v : V) : v ∈ (groundComp graph ground e).support → (groundComp graph ground e).Reachable v ground

The ground component is connected.

noncomputable def MisereGames.Hackenbush.remove {V : Type} (hack : Hackenbush V) (e : Sym2 V) : Hackenbush V

Remove an edge from a Hackenbush position and take the ground component.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MisereGames.Hackenbush.remove_graph {V : Type} (hack : Hackenbush V) (e : Sym2 V) : (hack.remove e).graph = groundComp hack.graph hack.ground e

@[simp]

theorem MisereGames.Hackenbush.remove_ground {V : Type} (hack : Hackenbush V) (e : Sym2 V) : (hack.remove e).ground = hack.ground

@[simp]

theorem MisereGames.Hackenbush.remove_coloring {V : Type} (hack : Hackenbush V) (e : Sym2 V) : (hack.remove e).coloring = hack.coloring

theorem MisereGames.Hackenbush.edgeCard_remove_lt {V : Type} (hack : Hackenbush V) (e : Sym2 V) (he : e ∈ hack.graph.edgeSet) : (hack.remove e).edgeCard < hack.edgeCard

Removing an edge strictly decreases the edge count.

Ground edges

noncomputable def MisereGames.Hackenbush.groundEdges {V : Type} (hack : Hackenbush V) (p : Player) : Finset (Sym2 V)

The set of p-coloured ground edges (edges incident with the ground vertex).

Equations

• hack.groundEdges p = {e ∈ hack.edgeFinset | hack.ground ∈ e ∧ hack.coloring e = p}

noncomputable def MisereGames.Hackenbush.groundCount {V : Type} (hack : Hackenbush V) (p : Player) : ℕ

The number of p-coloured edges incident with ground vertex.

Equations

• hack.groundCount p = (hack.groundEdges p).card

theorem MisereGames.Hackenbush.groundEdge_mem_groundComp {V : Type} {graph : SimpleGraph V} {ground : V} {e e' : Sym2 V} (he' : e' ∈ graph.edgeSet) (hne : e' ≠ e) (hgnd : ground ∈ e') (hconn : ∀ v ∈ graph.support, graph.Reachable v ground) : e' ∈ (groundComp graph ground e).edgeSet

A ground edge (other than the removed one) survives in the ground component.

theorem MisereGames.Hackenbush.groundEdges_remove_eq {V : Type} (hack : Hackenbush V) (e : Sym2 V) (p : Player) : (hack.groundEdges p).erase e = (hack.remove e).groundEdges p

Ground edges of the removed position = ground edges of original minus the removed edge.

Ground count properties under edge removal

theorem MisereGames.Hackenbush.groundCount_remove_ground {V : Type} {hack : Hackenbush V} {e : Sym2 V} {p : Player} (he : e ∈ hack.graph.edgeSet) (hg : hack.ground ∈ e) (hc : hack.coloring e = p) : (hack.remove e).groundCount p = hack.groundCount p - 1

Ground count after removing a ground p-edge decreases by 1.

theorem MisereGames.Hackenbush.groundCount_remove_neg {V : Type} {hack : Hackenbush V} {e : Sym2 V} {p : Player} (hc : hack.coloring e = -p) : (hack.remove e).groundCount p = hack.groundCount p

Ground count is preserved when removing an edge of different colour.

theorem MisereGames.Hackenbush.groundCount_remove_non_ground {V : Type} {hack : Hackenbush V} {e : Sym2 V} {p : Player} (hng : hack.ground ∉ e) : (hack.remove e).groundCount p = hack.groundCount p

Ground count is preserved when removing a non-ground edge.

theorem MisereGames.Hackenbush.groundCount_neg_remove {V : Type} {hack : Hackenbush V} {e : Sym2 V} {p : Player} (hc : hack.coloring e = p) : (hack.remove e).groundCount (-p) = hack.groundCount (-p)

Removing a p-coloured edge preserves (-p)-coloured ground count.

theorem MisereGames.Hackenbush.groundCount_move {V : Type} {hack : Hackenbush V} {e : Sym2 V} {p : Player} (he : e ∈ hack.graph.edgeSet) (hc : hack.coloring e = p) : (hack.remove e).groundCount p ≥ hack.groundCount p - 1

For any p-move, the groundCount p of the result is ≥ groundCount p - 1.

Hackenbush game structure

def MisereGames.Hackenbush.moves {V : Type} (p : Player) (hack : Hackenbush V) : Set (Hackenbush V)

Moves in Hackenbush: remove an edge of your colour and take the ground component.

Equations

• MisereGames.Hackenbush.moves p hack = {hack' : MisereGames.Hackenbush V | ∃ e ∈ hack.graph.edgeSet, hack.coloring e = p ∧ hack' = hack.remove e}

theorem MisereGames.Hackenbush.mem_moves_iff {V : Type} {p : Player} {hack hack' : Hackenbush V} : hack' ∈ Hackenbush.moves p hack ↔ ∃ e ∈ hack.graph.edgeSet, hack.coloring e = p ∧ hack' = hack.remove e

def GameGraph.hackenbush {V : Type} : MisereGames.GameGraph (MisereGames.Hackenbush V)

The game graph whose moves are Hackenbush edge removals.

Equations

• GameGraph.hackenbush = { moves := MisereGames.Hackenbush.moves }

instance MisereGames.Hackenbush.instIsWellFoundedHackenbush {V : Type} : GameGraph.hackenbush.IsWellFounded

noncomputable def MisereGames.Hackenbush.toGameForm {V : Type} (hack : Hackenbush V) : GameForm

Convert a Hackenbush position to a GameForm.

Equations

• hack.toGameForm = MisereGames.GameGraph.toForm hack

@[simp]

theorem MisereGames.Hackenbush.moves_toGameForm {V : Type} (p : Player) (hack : Hackenbush V) : Moves.moves p hack.toGameForm = toGameForm '' Hackenbush.moves p hack

theorem MisereGames.Hackenbush.mem_moves_toGameForm_iff {V : Type} {p : Player} {hack : Hackenbush V} {g : GameForm} : g ∈ Moves.moves p hack.toGameForm ↔ ∃ (e : Sym2 V) (_ : e ∈ hack.graph.edgeSet), hack.coloring e = p ∧ g = (hack.remove e).toGameForm

theorem MisereGames.Hackenbush.toGameForm_remove_mem_moves {V : Type} {hack : Hackenbush V} {e : Sym2 V} (he : e ∈ hack.graph.edgeSet) : (hack.remove e).toGameForm ∈ Moves.moves (hack.coloring e) hack.toGameForm

theorem MisereGames.Hackenbush.toGameForm_eq_zero_iff {V : Type} {hack : Hackenbush V} : hack.toGameForm = 0 ↔ hack.graph = ⊥

The game form is zero iff the graph has no edges.

Existence of ground edges

theorem MisereGames.Hackenbush.exists_ground_edge {V : Type} {hack : Hackenbush V} (h_ne : hack.graph ≠ ⊥) : ∃ e ∈ hack.graph.edgeSet, hack.ground ∈ e

theorem MisereGames.Hackenbush.exists_neg_ground_edge {V : Type} {hack : Hackenbush V} {p : Player} (h_ne : hack.graph ≠ ⊥) (hgc : hack.groundCount p = 0) : ∃ e ∈ hack.graph.edgeSet, hack.ground ∈ e ∧ hack.coloring e = -p

theorem MisereGames.Hackenbush.move_not_zero_of_groundCount_zero {V : Type} {hack : Hackenbush V} {p : Player} {e : Sym2 V} (he : e ∈ hack.graph.edgeSet) (hc : hack.coloring e = p) (hgc : hack.groundCount p = 0) : (hack.remove e).graph ≠ ⊥

A p-move cannot lead to the zero game when groundCount p = 0.

theorem MisereGames.Hackenbush.groundCount_zero_of_option {V : Type} {hack : Hackenbush V} {p : Player} {e : Sym2 V} (hgc : hack.groundCount p = 0) : (hack.remove e).groundCount p = 0

Removing any edge preserves the zero-ness of groundCount p.

Stride theory

theorem MisereGames.Hackenbush.isSolved_of_groundCount_zero {V : Type} {hack : Hackenbush V} {p : Player} (hgc : hack.groundCount p = 0) : GameForm.IsSolved p hack.toGameForm

When p has no ground edges, the position is solved for p.

theorem MisereGames.Hackenbush.not_isSolved_of_groundCount_pos {V : Type} {hack : Hackenbush V} {p : Player} (hgc : 1 ≤ hack.groundCount p) : ¬GameForm.IsSolved p hack.toGameForm

When groundCount p ≥ 1, the position is not solved for p.

theorem MisereGames.Hackenbush.hasStride_groundCount {V : Type} (hack : Hackenbush V) (p : Player) : GameForm.HasStride p hack.toGameForm (hack.groundCount p)

The p-stride of a Hackenbush position equals the number of p-coloured ground edges.

@[implicit_reducible]

noncomputable instance MisereGames.Hackenbush.instRuleset {V : Type} : Ruleset (Hackenbush V)

Equations

• MisereGames.Hackenbush.instRuleset = { toGameForm := MisereGames.Hackenbush.toGameForm, moves_toGameForm := ⋯ }

noncomputable def MisereGames.Hackenbush.starPos (l r : ℕ) : Hackenbush ℕ

A star Hackenbush position over ℕ with l left ground edges and r right ground edges. Ground vertex is 0. Left edges connect 0 to 1, ..., l. Right edges connect 0 to l+1, ..., l+r. The colouring uses max u v (the non-zero endpoint of each star edge) to determine colour.

Equations

• One or more equations did not get rendered due to their size.

theorem MisereGames.Hackenbush.starPos_groundCount_left (l r : ℕ) : (starPos l r).groundCount Player.left = l

theorem MisereGames.Hackenbush.starPos_groundCount_right (l r : ℕ) : (starPos l r).groundCount Player.right = r

instance MisereGames.Hackenbush.instStridedFormsNat : GameForm.Strided (Ruleset.Forms (Hackenbush ℕ))

noncomputable def MisereGames.Hackenbush.equivInt : MisereQuotient (Ruleset.Forms (Hackenbush ℕ)) ≃ ℤ

The misère quotient of finite-star Hackenbush positions is equivalent to ℤ.

Equations

• MisereGames.Hackenbush.equivInt = MisereGames.GameForm.MisereQuotient.stridedEquivInt

theorem MisereGames.Hackenbush.le_iff_equiv_ge (a b : MisereQuotient (Ruleset.Forms (Hackenbush ℕ))) : a ≤ b ↔ GameForm.MisereQuotient.stridedEquivInt a ≥ GameForm.MisereQuotient.stridedEquivInt b

noncomputable def MisereGames.Hackenbush.closure.equivInt : MisereQuotient (Form.ClosedUnderAdd.closure (Ruleset.Forms (Hackenbush ℕ))) ≃ ℤ

The additive closure of Hackenbush positions has quotient equivalent to ℤ.

Equations

• MisereGames.Hackenbush.closure.equivInt = MisereGames.GameForm.MisereQuotient.stridedEquivInt

theorem MisereGames.Hackenbush.closure.le_iff_equiv_ge (a b : MisereQuotient (Form.ClosedUnderAdd.closure (Ruleset.Forms (Hackenbush ℕ)))) : a ≤ b ↔ GameForm.MisereQuotient.stridedEquivInt a ≥ GameForm.MisereQuotient.stridedEquivInt b