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 = Prod.map id (fun (x : ℤ) => x + -1) a

@[simp]

theorem SetTheory.PGame.Domineering.shiftUp_apply : ∀ (a : ℤ × ℤ), SetTheory.PGame.Domineering.shiftUp a = Prod.map id (fun (x : ℤ) => x + 1) a

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

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

Equations

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

@[simp]

theorem SetTheory.PGame.Domineering.shiftRight_symm_apply : ∀ (a : ℤ × ℤ), SetTheory.PGame.Domineering.shiftRight.symm a = Prod.map (fun (x : ℤ) => x + -1) id a

@[simp]

theorem SetTheory.PGame.Domineering.shiftRight_apply : ∀ (a : ℤ × ℤ), SetTheory.PGame.Domineering.shiftRight a = Prod.map (fun (x : ℤ) => x + 1) id a

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, inline]

abbrev 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 SetTheory.PGame.Domineering.shiftUp.toEmbedding 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 SetTheory.PGame.Domineering.shiftRight.toEmbedding 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 b m).erase (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 b m).erase (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 ≤ Finset.card b

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

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

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

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

theorem SetTheory.PGame.Domineering.moveRight_smaller {b : SetTheory.PGame.Domineering.Board} {m : ℤ × ℤ} (h : m ∈ SetTheory.PGame.Domineering.right b) : Finset.card (SetTheory.PGame.Domineering.moveRight b m) / 2 < Finset.card b / 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.domineering b).Short

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 [(0, 0), (0, 1)].toFinset

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 [(0, 2), (0, 1), (0, 0), (1, 0)].toFinset

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

Equations

• SetTheory.PGame.shortOne = id inferInstance

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

Equations

• SetTheory.PGame.shortL = id inferInstance