Documentation

Mathlib.SetTheory.Game.Domineering

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.

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

Instances For

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

    Instances For
      @[reducible]

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

      Instances For

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

        Instances For

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

          Instances For

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

            Instances For

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

              Instances For

                The instance describing allowed moves on a Domineering board.

                Construct a pre-game from a Domineering board.

                Instances For

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

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

                  Instances For

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

                    Instances For