Hackenbush

Hackenbush is played on a connected graph with a designated "ground" vertex. Edges are coloured Left (bLue), Right (Red) or green, which either player may remove. On their turn, a player removes an edge of their colour or a green edge. The resulting position is the connected component containing the ground vertex.

Green edges touching the ground are excluded: a single one is ⋆, which has no stride, and Stewart shows that with green ground edges the misère outcome problem is NP-hard. This is a hereditary condition, since edges never change colour, so it is part of the structure.

structure Hackenbush (V : Type) : Type

• graph : SimpleGraph V

  The underlying graph.

• ground : V

  The ground vertex.

• coloring : Sym2 V → Color

  Edge colouring.

• 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.

• ground_colored (e : Sym2 V) : e ∈ self.graph.edgeSet → self.ground ∈ e → self.coloring e ≠ Color.green

  No edge touching the ground is green.

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

The edge set of a Hackenbush position is finite.

def 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 Hackenbush.mem_edgeFinset {V : Type} {hack : Hackenbush V} {e : Sym2 V} : e ∈ hack.edgeFinset ↔ e ∈ hack.graph.edgeSet

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

The number of edges in a Hackenbush position.

Equations

• hack.edgeCard = hack.edgeFinset.card

Ground component

def 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 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 Hackenbush.groundComp_le {V : Type} (graph : SimpleGraph V) (ground : V) (e : Sym2 V) : groundComp graph ground e ≤ graph

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

theorem 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 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 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 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.

def 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 Hackenbush.remove_graph {V : Type} (hack : Hackenbush V) (e : Sym2 V) : (hack.remove e).graph = groundComp hack.graph hack.ground e

@[simp]

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

@[simp]

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

theorem 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

def 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 = Hackenbush.Color.ofPlayer p}

theorem Hackenbush.mem_groundEdges_iff {V : Type} {hack : Hackenbush V} {e : Sym2 V} {p : Player} : e ∈ hack.groundEdges p ↔ e ∈ hack.graph.edgeSet ∧ hack.ground ∈ e ∧ hack.coloring e = Color.ofPlayer p

def 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 Hackenbush.groundCount_eq_card {V : Type} (hack : Hackenbush V) (p : Player) : hack.groundCount p = (hack.groundEdges p).card

theorem 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 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 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 = Color.ofPlayer p) : (hack.remove e).groundCount p = hack.groundCount p - 1

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

theorem Hackenbush.groundCount_remove_of_ne {V : Type} {hack : Hackenbush V} {e : Sym2 V} {p : Player} (hc : hack.coloring e ≠ Color.ofPlayer p) : (hack.remove e).groundCount p = hack.groundCount p

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

theorem 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 Hackenbush.groundCount_remove_ge {V : Type} (hack : Hackenbush V) (e : Sym2 V) (p : Player) : (hack.remove e).groundCount p ≥ hack.groundCount p - 1

Removing any edge lowers the ground count by at most one.

theorem Hackenbush.groundCount_remove_le {V : Type} (hack : Hackenbush V) (e : Sym2 V) (p : Player) : (hack.remove e).groundCount p ≤ hack.groundCount p

Removing an edge never raises a ground count.

theorem Hackenbush.remove_graph_ne_bot_of_ground_edge {V : Type} {hack : Hackenbush V} {e e' : Sym2 V} (he' : e' ∈ hack.graph.edgeSet) (hgnd : hack.ground ∈ e') (hne : e' ≠ e) : (hack.remove e).graph ≠ ⊥

If some ground edge other than the removed one exists, the position stays nonempty.

Hackenbush game structure

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

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

Equations

• Hackenbush.moves p hack = {hack' : Hackenbush V | ∃ e ∈ hack.graph.edgeSet, hack.coloring e ≠ Hackenbush.Color.ofPlayer (-p) ∧ hack' = hack.remove e}

theorem Hackenbush.mem_moves_iff {V : Type} {p : Player} {hack hack' : Hackenbush V} : hack' ∈ Hackenbush.moves p hack ↔ ∃ e ∈ hack.graph.edgeSet, hack.coloring e ≠ Color.ofPlayer (-p) ∧ hack' = hack.remove e

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

Equations

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

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

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

Convert a Hackenbush position to a GameForm.

Equations

• hack.toGameForm = GameGraph.toForm hack

@[simp]

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

theorem 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 ≠ Color.ofPlayer (-p) ∧ g = (hack.remove e).toGameForm

theorem Hackenbush.toGameForm_remove_mem_moves {V : Type} {hack : Hackenbush V} {e : Sym2 V} {p : Player} (he : e ∈ hack.graph.edgeSet) (hc : hack.coloring e ≠ Color.ofPlayer (-p)) : (hack.remove e).toGameForm ∈ Moves.moves p hack.toGameForm

theorem Hackenbush.toGameForm_remove_mem_moves_of_eq {V : Type} {hack : Hackenbush V} {e : Sym2 V} {p : Player} (he : e ∈ hack.graph.edgeSet) (hc : hack.coloring e = Color.ofPlayer p) : (hack.remove e).toGameForm ∈ Moves.moves p hack.toGameForm

theorem 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 Hackenbush.exists_ground_edge {V : Type} {hack : Hackenbush V} (h_ne : hack.graph ≠ ⊥) : ∃ e ∈ hack.graph.edgeSet, hack.ground ∈ e

theorem 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 = Color.ofPlayer (-p)

theorem 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 ≠ Color.ofPlayer (-p)) (hgc : hack.groundCount p = 0) : (hack.remove e).graph ≠ ⊥

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

theorem 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 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 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 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.

@[instance_reducible]

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

Equations

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

def 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 Hackenbush.starPos_groundCount_left (l r : ℕ) : (starPos l r).groundCount Player.left = l

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

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

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

Equations

• Hackenbush.equivInt = GameForm.MisereQuotient.stridedEquivInt

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

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

Equations

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

theorem 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