mathlib3 documentation

set_theory.game.domineering

Domineering as a combinatorial game. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
@[simp]
theorem pgame.domineering.shift_up_apply (x : ℤ × ℤ) :
⇑pgame.domineering.shift_up x = (x.fst, x.snd + 1)
source
def pgame.domineering.shift_up  :
ℤ × ℤ ≃ ℤ × ℤ

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

Equations
source
@[simp]
theorem pgame.domineering.shift_up_symm_apply (x : ℤ × ℤ) :
⇑(pgame.domineering.shift_up.symm) x = (x.fst, x.snd - 1)
source
@[simp]
theorem pgame.domineering.shift_right_apply (x : ℤ × ℤ) :
⇑pgame.domineering.shift_right x = (x.fst + 1, x.snd)
source
@[simp]
theorem pgame.domineering.shift_right_symm_apply (x : ℤ × ℤ) :
⇑(pgame.domineering.shift_right.symm) x = (x.fst - 1, x.snd)
source
def pgame.domineering.shift_right  :
ℤ × ℤ ≃ ℤ × ℤ

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

Equations
source
@[protected, instance]
def pgame.domineering.board.inhabited  :
inhabited pgame.domineering.board
source
def pgame.domineering.board  :
Type

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

Equations
Instances for pgame.domineering.board
source
def pgame.domineering.left (b : pgame.domineering.board) :
finset (ℤ × ℤ)

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

Equations
source
def pgame.domineering.right (b : pgame.domineering.board) :
finset (ℤ × ℤ)

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

Equations
source
theorem pgame.domineering.mem_left {b : pgame.domineering.board} (x : ℤ × ℤ) :
x ∈ pgame.domineering.left b ↔ x ∈ b ∧ (x.fst, x.snd - 1) ∈ b
source
theorem pgame.domineering.mem_right {b : pgame.domineering.board} (x : ℤ × ℤ) :
x ∈ pgame.domineering.right b ↔ x ∈ b ∧ (x.fst - 1, x.snd) ∈ b
source
def pgame.domineering.move_left (b : pgame.domineering.board) (m : ℤ × ℤ) :
pgame.domineering.board

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

Equations
source
def pgame.domineering.move_right (b : pgame.domineering.board) (m : ℤ × ℤ) :
pgame.domineering.board

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

Equations
source
theorem pgame.domineering.fst_pred_mem_erase_of_mem_right {b : pgame.domineering.board} {m : ℤ × ℤ} (h : m ∈ pgame.domineering.right b) :
(m.fst - 1, m.snd) ∈ finset.erase b m
source
theorem pgame.domineering.snd_pred_mem_erase_of_mem_left {b : pgame.domineering.board} {m : ℤ × ℤ} (h : m ∈ pgame.domineering.left b) :
(m.fst, m.snd - 1) ∈ finset.erase b m
source
theorem pgame.domineering.card_of_mem_left {b : pgame.domineering.board} {m : ℤ × ℤ} (h : m ∈ pgame.domineering.left b) :
2 ≤ finset.card b
source
theorem pgame.domineering.card_of_mem_right {b : pgame.domineering.board} {m : ℤ × ℤ} (h : m ∈ pgame.domineering.right b) :
2 ≤ finset.card b
source
theorem pgame.domineering.move_left_card {b : pgame.domineering.board} {m : ℤ × ℤ} (h : m ∈ pgame.domineering.left b) :
finset.card (pgame.domineering.move_left b m) + 2 = finset.card b
source
theorem pgame.domineering.move_right_card {b : pgame.domineering.board} {m : ℤ × ℤ} (h : m ∈ pgame.domineering.right b) :
finset.card (pgame.domineering.move_right b m) + 2 = finset.card b
source
theorem pgame.domineering.move_left_smaller {b : pgame.domineering.board} {m : ℤ × ℤ} (h : m ∈ pgame.domineering.left b) :
finset.card (pgame.domineering.move_left b m) / 2 < finset.card b / 2
source
theorem pgame.domineering.move_right_smaller {b : pgame.domineering.board} {m : ℤ × ℤ} (h : m ∈ pgame.domineering.right b) :
finset.card (pgame.domineering.move_right b m) / 2 < finset.card b / 2
source
@[protected, instance]
def pgame.domineering.state  :
pgame.state pgame.domineering.board

The instance describing allowed moves on a Domineering board.

Equations
source
def pgame.domineering (b : pgame.domineering.board) :
pgame

Construct a pre-game from a Domineering board.

Equations
Instances for pgame.domineering
source
@[protected, instance]
def pgame.short_domineering (b : pgame.domineering.board) :
(pgame.domineering b).short

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

Equations
source
def pgame.domineering.one  :
pgame

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

Equations
Instances for pgame.domineering.one
source
def pgame.domineering.L  :
pgame

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

Equations
Instances for pgame.domineering.L
source
@[protected, instance]
def pgame.short_one  :
pgame.domineering.one.short
Equations
source
@[protected, instance]
def pgame.short_L  :
pgame.domineering.L.short
Equations