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.

@[simp]

theorem SetTheory.PGame.Domineering.shiftUp_symm_apply : ∀ (a : ℤ × ℤ), SetTheory.PGame.Domineering.shiftUp.symm a = (a.1, a.2 + -1)

@[simp]

theorem SetTheory.PGame.Domineering.shiftUp_apply : ∀ (a : ℤ × ℤ), SetTheory.PGame.Domineering.shiftUp a = (a.1, a.2 + 1)

def SetTheory.PGame.Domineering.shiftUp : ℤ × ℤ ≃ ℤ × ℤ

The equivalence (x, y) ↦ (x, y+1).

Equations

• SetTheory.PGame.Domineering.shiftUp = Equiv.prodCongr (Equiv.refl ℤ) (Equiv.addRight 1)

@[simp]

theorem SetTheory.PGame.Domineering.shiftRight_symm_apply : ∀ (a : ℤ × ℤ), SetTheory.PGame.Domineering.shiftRight.symm a = (a.1 + -1, a.2)

@[simp]

theorem SetTheory.PGame.Domineering.shiftRight_apply : ∀ (a : ℤ × ℤ), SetTheory.PGame.Domineering.shiftRight a = (a.1 + 1, a.2)

def SetTheory.PGame.Domineering.shiftRight : ℤ × ℤ ≃ ℤ × ℤ

The equivalence (x, y) ↦ (x+1, y).

Equations

• SetTheory.PGame.Domineering.shiftRight = Equiv.prodCongr (Equiv.addRight 1) (Equiv.refl ℤ)

@[reducible]

def SetTheory.PGame.Domineering.Board : Type

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

Equations

• SetTheory.PGame.Domineering.Board = Finset (ℤ × ℤ)

def SetTheory.PGame.Domineering.left (b : SetTheory.PGame.Domineering.Board) : Finset (ℤ × ℤ)

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

Equations

• SetTheory.PGame.Domineering.left b = b ∩ Finset.map (Equiv.toEmbedding SetTheory.PGame.Domineering.shiftUp) b

def SetTheory.PGame.Domineering.right (b : SetTheory.PGame.Domineering.Board) : Finset (ℤ × ℤ)

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

Equations

• SetTheory.PGame.Domineering.right b = b ∩ Finset.map (Equiv.toEmbedding SetTheory.PGame.Domineering.shiftRight) b

theorem SetTheory.PGame.Domineering.mem_left {b : SetTheory.PGame.Domineering.Board} (x : ℤ × ℤ) : x ∈ SetTheory.PGame.Domineering.left b ↔ x ∈ b ∧ (x.1, x.2 - 1) ∈ b

theorem SetTheory.PGame.Domineering.mem_right {b : SetTheory.PGame.Domineering.Board} (x : ℤ × ℤ) : x ∈ SetTheory.PGame.Domineering.right b ↔ x ∈ b ∧ (x.1 - 1, x.2) ∈ b

def SetTheory.PGame.Domineering.moveLeft (b : SetTheory.PGame.Domineering.Board) (m : ℤ × ℤ) : SetTheory.PGame.Domineering.Board

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

Equations

• SetTheory.PGame.Domineering.moveLeft b m = Finset.erase (Finset.erase b m) (m.1, m.2 - 1)

def SetTheory.PGame.Domineering.moveRight (b : SetTheory.PGame.Domineering.Board) (m : ℤ × ℤ) : SetTheory.PGame.Domineering.Board

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

Equations

• SetTheory.PGame.Domineering.moveRight b m = Finset.erase (Finset.erase b m) (m.1 - 1, m.2)

theorem SetTheory.PGame.Domineering.fst_pred_mem_erase_of_mem_right {b : SetTheory.PGame.Domineering.Board} {m : ℤ × ℤ} (h : m ∈ SetTheory.PGame.Domineering.right b) : (m.1 - 1, m.2) ∈ Finset.erase b m

theorem SetTheory.PGame.Domineering.snd_pred_mem_erase_of_mem_left {b : SetTheory.PGame.Domineering.Board} {m : ℤ × ℤ} (h : m ∈ SetTheory.PGame.Domineering.left b) : (m.1, m.2 - 1) ∈ Finset.erase b m

theorem SetTheory.PGame.Domineering.card_of_mem_left {b : SetTheory.PGame.Domineering.Board} {m : ℤ × ℤ} (h : m ∈ SetTheory.PGame.Domineering.left b) : 2 ≤ b.card

theorem SetTheory.PGame.Domineering.card_of_mem_right {b : SetTheory.PGame.Domineering.Board} {m : ℤ × ℤ} (h : m ∈ SetTheory.PGame.Domineering.right b) : 2 ≤ b.card

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

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

theorem SetTheory.PGame.Domineering.moveLeft_smaller {b : SetTheory.PGame.Domineering.Board} {m : ℤ × ℤ} (h : m ∈ SetTheory.PGame.Domineering.left b) : (SetTheory.PGame.Domineering.moveLeft b m).card / 2 < b.card / 2

theorem SetTheory.PGame.Domineering.moveRight_smaller {b : SetTheory.PGame.Domineering.Board} {m : ℤ × ℤ} (h : m ∈ SetTheory.PGame.Domineering.right b) : (SetTheory.PGame.Domineering.moveRight b m).card / 2 < b.card / 2

instance SetTheory.PGame.Domineering.state : SetTheory.PGame.State SetTheory.PGame.Domineering.Board

The instance describing allowed moves on a Domineering board.

Equations

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

def SetTheory.PGame.domineering (b : SetTheory.PGame.Domineering.Board) : SetTheory.PGame

Construct a pre-game from a Domineering board.

Equations

• SetTheory.PGame.domineering b = SetTheory.PGame.ofState b

instance SetTheory.PGame.shortDomineering (b : SetTheory.PGame.Domineering.Board) : SetTheory.PGame.Short (SetTheory.PGame.domineering b)

All games of Domineering are short, because each move removes two squares.

Equations

• SetTheory.PGame.shortDomineering b = id inferInstance

def SetTheory.PGame.domineering.one : SetTheory.PGame

The Domineering board with two squares arranged vertically, in which Left has the only move.

Equations

• SetTheory.PGame.domineering.one = SetTheory.PGame.domineering (List.toFinset [(0, 0), (0, 1)])

def SetTheory.PGame.domineering.L : SetTheory.PGame

The L shaped Domineering board, in which Left is exactly half a move ahead.

Equations

• SetTheory.PGame.domineering.L = SetTheory.PGame.domineering (List.toFinset [(0, 2), (0, 1), (0, 0), (1, 0)])

instance SetTheory.PGame.shortOne : SetTheory.PGame.Short SetTheory.PGame.domineering.one

Equations

• SetTheory.PGame.shortOne = id inferInstance

instance SetTheory.PGame.shortL : SetTheory.PGame.Short SetTheory.PGame.domineering.L

Equations

• SetTheory.PGame.shortL = id inferInstance