Domineering as a combinatorial game.

We define the game of Domineering, played on a chessboard of arbitrary shape (possibly even disconnected). Left moves by placing a domino vertically, while Right moves by placing a domino horizontally.

This is only a fragment of a full development; in order to successfully analyse positions we would need some more theorems. Most importantly, we need a general statement that allows us to discard irrelevant moves. Specifically to domineering, we need the fact that disjoint parts of the chessboard give sums of games.

def IGame.Domineering : Type

A Domineering board is an arbitrary finite subset of ℤ × ℤ.

Equations

• IGame.Domineering = Finset (ℤ × ℤ)

instance IGame.instDomineeringDecidableEq : DecidableEq Domineering

Equations

• IGame.instDomineeringDecidableEq a b = a.decidableEq b

@[match_pattern]

def IGame.toDomineering : Finset (ℤ × ℤ) ≃ Domineering

Equations

• IGame.toDomineering = Equiv.refl (Finset (ℤ × ℤ))

@[match_pattern]

def IGame.ofDomineering : Domineering ≃ Finset (ℤ × ℤ)

Equations

• IGame.ofDomineering = Equiv.refl IGame.Domineering

@[simp]

theorem IGame.toDomineering_ofDomineering (a : Domineering) : toDomineering (ofDomineering a) = a

@[simp]

theorem IGame.ofDomineering_toDomineering (s : Finset (ℤ × ℤ)) : ofDomineering (toDomineering s) = s

unsafe instance IGame.Domineering.instRepr : Repr Domineering

Equations

• IGame.Domineering.instRepr = Finset.instRepr

def IGame.Domineering.left (b : Domineering) : Finset (ℤ × ℤ)

Left can play anywhere that a square and the square below it are open.

Equations

• b.left = IGame.ofDomineering b ∩ Finset.map ((Equiv.refl ℤ).prodCongr (Equiv.addRight 1)).toEmbedding (IGame.ofDomineering b)

def IGame.Domineering.right (b : Domineering) : Finset (ℤ × ℤ)

Right can play anywhere that a square and the square to the left are open.

Equations

• b.right = IGame.ofDomineering b ∩ Finset.map (Equiv.prodCongr (Equiv.addRight 1) (Equiv.refl ℤ)).toEmbedding (IGame.ofDomineering b)

theorem IGame.Domineering.mem_left {b : Domineering} {m : ℤ × ℤ} : m ∈ b.left ↔ m ∈ ofDomineering b ∧ (m.1, m.2 - 1) ∈ ofDomineering b

theorem IGame.Domineering.mem_right {b : Domineering} {m : ℤ × ℤ} : m ∈ b.right ↔ m ∈ ofDomineering b ∧ (m.1 - 1, m.2) ∈ ofDomineering b

theorem IGame.Domineering.subset_of_mem_left {b : Domineering} {m : ℤ × ℤ} (h : m ∈ b.left) : {m, (m.1, m.2 - 1)} ⊆ ofDomineering b

theorem IGame.Domineering.subset_of_mem_right {b : Domineering} {m : ℤ × ℤ} (h : m ∈ b.right) : {m, (m.1 - 1, m.2)} ⊆ ofDomineering b

def IGame.Domineering.moveLeft (b : Domineering) (m : ℤ × ℤ) : Domineering

After Left moves, two vertically adjacent squares are removed from the Domineering.

Equations

• b.moveLeft m = IGame.toDomineering (((IGame.ofDomineering b).erase m).erase (m.1, m.2 - 1))

def IGame.Domineering.moveRight (b : Domineering) (m : ℤ × ℤ) : Domineering

After Left moves, two horizontally adjacent squares are removed from the Domineering.

Equations

• b.moveRight m = IGame.toDomineering (((IGame.ofDomineering b).erase m).erase (m.1 - 1, m.2))

theorem IGame.Domineering.moveLeft_subset (b : Domineering) (m : ℤ × ℤ) : ofDomineering (b.moveLeft m) ⊆ ofDomineering b

theorem IGame.Domineering.moveRight_subset (b : Domineering) (m : ℤ × ℤ) : ofDomineering (b.moveRight m) ⊆ ofDomineering b

def IGame.Domineering.relLeft (a b : Domineering) : Prop

Left can move from b to a when there exists some m ∈ left b with a = b.moveLeft m.

Equations

• a.relLeft b = ∃ m ∈ b.left, a = b.moveLeft m

def IGame.Domineering.relRight (a b : Domineering) : Prop

Right can move from b to a when there exists some m ∈ right b with a = b.moveRight m.

Equations

• a.relRight b = ∃ m ∈ b.right, a = b.moveRight m

instance IGame.Domineering.instDecidableRelRelLeft : DecidableRel relLeft

Equations

• x✝¹.instDecidableRelRelLeft x✝ = inferInstanceAs (Decidable (∃ x ∈ x✝.left, x✝¹ = x✝.moveLeft x))

instance IGame.Domineering.instDecidableRelRelRight : DecidableRel relRight

Equations

• x✝¹.instDecidableRelRelRight x✝ = inferInstanceAs (Decidable (∃ x ∈ x✝.right, x✝¹ = x✝.moveRight x))

theorem IGame.Domineering.card_of_mem_left {b : Domineering} {m : ℤ × ℤ} (h : m ∈ b.left) : 2 ≤ (ofDomineering b).card

theorem IGame.Domineering.card_of_mem_right {b : Domineering} {m : ℤ × ℤ} (h : m ∈ b.right) : 2 ≤ (ofDomineering b).card

theorem IGame.Domineering.moveLeft_card {b : Domineering} {m : ℤ × ℤ} (h : m ∈ b.left) : (ofDomineering (b.moveLeft m)).card + 2 = (ofDomineering b).card

theorem IGame.Domineering.moveRight_card {b : Domineering} {m : ℤ × ℤ} (h : m ∈ b.right) : (ofDomineering (b.moveRight m)).card + 2 = (ofDomineering b).card

theorem IGame.Domineering.card_of_relLeft {a b : Domineering} (h : a.relLeft b) : (ofDomineering a).card + 2 = (ofDomineering b).card

theorem IGame.Domineering.card_of_relRight {a b : Domineering} (h : a.relRight b) : (ofDomineering a).card + 2 = (ofDomineering b).card

theorem IGame.Domineering.subrelation_relLeft : Subrelation relLeft (InvImage (fun (x1 x2 : ℕ) => x1 < x2) fun (b : Domineering) => (ofDomineering b).card)

theorem IGame.Domineering.subrelation_relRight : Subrelation relRight (InvImage (fun (x1 x2 : ℕ) => x1 < x2) fun (b : Domineering) => (ofDomineering b).card)

instance IGame.Domineering.instIsWellFoundedRelLeft : IsWellFounded Domineering relLeft

instance IGame.Domineering.instIsWellFoundedRelRight : IsWellFounded Domineering relRight

instance IGame.Domineering.instConcreteGame : ConcreteGame Domineering

Equations

• IGame.Domineering.instConcreteGame = { relLeft := IGame.Domineering.relLeft, relRight := IGame.Domineering.relRight, isWellFounded_rel := IGame.Domineering.instConcreteGame._proof_1 }