Hackenbush colours

Edges in Hackenbush are bLue (Left's), Red (Right's) or green (either player's).

inductive Hackenbush.Color : Type

• blue : Color
• red : Color
• green : Color

@[instance_reducible]

instance Hackenbush.instDecidableEqColor : DecidableEq Color

Equations

• Hackenbush.instDecidableEqColor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hackenbush.Color.ofPlayer : Player → Color

The colour of player p's edges.

Equations

• Hackenbush.Color.ofPlayer Player.left = Hackenbush.Color.blue
• Hackenbush.Color.ofPlayer Player.right = Hackenbush.Color.red

@[simp]

theorem Hackenbush.Color.ofPlayer_left : ofPlayer Player.left = blue

@[simp]

theorem Hackenbush.Color.ofPlayer_right : ofPlayer Player.right = red

@[simp]

theorem Hackenbush.Color.ofPlayer_inj {p q : Player} : ofPlayer p = ofPlayer q ↔ p = q

@[simp]

theorem Hackenbush.Color.ofPlayer_ne_green (p : Player) : ofPlayer p ≠ green

@[simp]

theorem Hackenbush.Color.green_ne_ofPlayer (p : Player) : green ≠ ofPlayer p

theorem Hackenbush.Color.ofPlayer_ne_ofPlayer_neg (p : Player) : ofPlayer p ≠ ofPlayer (-p)

theorem Hackenbush.Color.exists_ne_ofPlayer_neg (c : Color) : ∃ (p : Player), c ≠ ofPlayer (-p)

Every colour may be cut by some player.

theorem Hackenbush.Color.eq_ofPlayer_neg_of_ne {c : Color} {p : Player} (h_green : c ≠ green) (h_ne : c ≠ ofPlayer p) : c = ofPlayer (-p)

theorem Hackenbush.Color.exists_eq_ofPlayer {c : Color} (h_green : c ≠ green) : ∃ (p : Player), c = ofPlayer p