Uproot Hackenbush

Uproot Hackenbush is played on the same positions as Hackenbush (a graph with a ground vertex, blue/red/green edges, no green edge touching the ground). Besides the usual move of cutting an edge of your own colour or a green edge, a player may uproot: delete a ground edge of the opponent's colour, provided the position has at least two ground edges. Everything disconnected from the ground falls away as usual.

Uproot is a sacrifice: it spends a move to remove one of the opponent's obligations. The proviso guarantees an uproot never empties the position; without it a single red ground edge would force Left to move to 0 and lose. Since the proviso reads the whole position, a disjunctive sum of two positions is not a position, so the class of positions is not closed under addition and the stride result is proved by GameForm.hasStride_of_options rather than via ordinal sums.

Under misère play the strides of a position are its ground counts, exactly as in Hackenbush (hasStride_groundCount), so uprooting never changes an outcome (misereOutcome_eq_hackenbush) and the misère quotient is ℤ. Two bare blue ground edges form {1 | 1}: the player with no obligations is forced to uproot, lowering the opponent's stride, which is why the stride definition compares the best move against the opponent's stride candidate.

def Hackenbush.groundEdgeFinset {V : Type} (hack : Hackenbush V) : Finset (Sym2 V)

The ground edges of a position, of either colour.

Equations

• hack.groundEdgeFinset = {e ∈ hack.edgeFinset | hack.ground ∈ e}

theorem Hackenbush.mem_groundEdgeFinset_iff {V : Type} {hack : Hackenbush V} {e : Sym2 V} : e ∈ hack.groundEdgeFinset ↔ e ∈ hack.graph.edgeSet ∧ hack.ground ∈ e

def Hackenbush.Uproot.CanRemove {V : Type} (hack : Hackenbush V) (p : Player) (e : Sym2 V) : Prop

Player p may delete e: it is not of the opponent's colour, or it is a ground edge and at least two ground edges exist.

Equations

• Hackenbush.Uproot.CanRemove hack p e = (hack.coloring e ≠ Hackenbush.Color.ofPlayer (-p) ∨ hack.ground ∈ e ∧ 2 ≤ hack.groundEdgeFinset.card)

theorem Hackenbush.Uproot.canRemove_of_ne {V : Type} {hack : Hackenbush V} {p : Player} {e : Sym2 V} (hc : hack.coloring e ≠ Color.ofPlayer (-p)) : CanRemove hack p e

theorem Hackenbush.Uproot.canRemove_of_eq {V : Type} {hack : Hackenbush V} {p : Player} {e : Sym2 V} (hc : hack.coloring e = Color.ofPlayer p) : CanRemove hack p e

theorem Hackenbush.Uproot.canRemove_of_ground {V : Type} {hack : Hackenbush V} (p : Player) {e : Sym2 V} (hg : hack.ground ∈ e) (h2 : 2 ≤ hack.groundEdgeFinset.card) : CanRemove hack p e

theorem Hackenbush.Uproot.exists_canRemove {V : Type} (hack : Hackenbush V) (e : Sym2 V) : ∃ (p : Player), CanRemove hack p e

Some player may delete any edge.

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

Moves in Uproot Hackenbush.

Equations

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

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

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

Equations

• GameGraph.uprootHackenbush = { moves := Hackenbush.Uproot.moves }

instance Hackenbush.Uproot.instIsWellFoundedUprootHackenbush {V : Type} : GameGraph.uprootHackenbush.IsWellFounded

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

Convert an Uproot Hackenbush position to a GameForm.

Equations

• Hackenbush.Uproot.toGameForm hack = GameGraph.toForm hack

@[simp]

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

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

theorem Hackenbush.Uproot.toGameForm_remove_mem_moves {V : Type} {hack : Hackenbush V} {e : Sym2 V} {p : Player} (he : e ∈ hack.graph.edgeSet) (hc : CanRemove hack p e) : toGameForm (hack.remove e) ∈ Moves.moves p (toGameForm hack)

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

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

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

A move by a player with no ground edges never empties the position.

Stride theory

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

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

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

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

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

The p-stride of an Uproot Hackenbush position equals the number of p-coloured ground edges, exactly as in Hackenbush.

theorem Hackenbush.Uproot.misereOutcome_eq_hackenbush {V : Type} (hack : Hackenbush V) : Form.Misere.Outcome.MisereOutcome (toGameForm hack) = Form.Misere.Outcome.MisereOutcome hack.toGameForm

Uprooting never changes an outcome.

def Hackenbush.Uproot.ruleset {V : Type} : Ruleset (Hackenbush V)

Uproot Hackenbush as a ruleset. This is a different Ruleset structure on the same position type as Hackenbush, so it is not an instance.

Equations

• Hackenbush.Uproot.ruleset = { toGameForm := Hackenbush.Uproot.toGameForm, moves_toGameForm := ⋯ }

def Hackenbush.Uproot.Forms (V : Type) (g : GameForm) : Prop

The game forms of Uproot Hackenbush positions.

Equations

• Hackenbush.Uproot.Forms V g = ∃ (hack : Hackenbush V), g = Hackenbush.Uproot.toGameForm hack

instance Hackenbush.Uproot.instHereditaryGameFormForms {V : Type} : Form.Hereditary (Forms V)

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

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

Equations

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

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

Equations

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