# mathlib3documentation

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.

@[simp]
theorem pgame.domineering.shift_up_apply (x : × ) :
= (x.fst, x.snd + 1)

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

Equations
@[simp]
@[simp]
theorem pgame.domineering.shift_right_apply (x : × ) :
= (x.fst + 1, x.snd)
@[simp]

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

Equations
@[protected, instance]

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

Equations
Instances for pgame.domineering.board

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

Equations

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

Equations
theorem pgame.domineering.mem_left (x : × ) :
x b (x.fst, x.snd - 1) b
theorem pgame.domineering.mem_right (x : × ) :
x b (x.fst - 1, x.snd) b

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

Equations

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

Equations
theorem pgame.domineering.card_of_mem_left {m : × } (h : m ) :
2
theorem pgame.domineering.move_left_card {m : × } (h : m ) :
theorem pgame.domineering.move_left_smaller {m : × } (h : m ) :
< / 2
theorem pgame.domineering.move_right_smaller {m : × } (h : m ) :
< / 2
@[protected, instance]

The instance describing allowed moves on a Domineering board.

Equations

Construct a pre-game from a Domineering board.

Equations
Instances for pgame.domineering
@[protected, instance]

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

Equations

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

Equations
Instances for pgame.domineering.one

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

Equations
Instances for pgame.domineering.L
@[protected, instance]
Equations
@[protected, instance]
Equations