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.

source
@[simp]
theorem SetTheory.PGame.Domineering.shiftUp_symm_apply :
∀ (a : ℤ × ℤ), ↑SetTheory.PGame.Domineering.shiftUp.symm a = (a.fst, a.snd + -1)
source
@[simp]
theorem SetTheory.PGame.Domineering.shiftUp_apply :
∀ (a : ℤ × ℤ), ↑SetTheory.PGame.Domineering.shiftUp a = (a.fst, a.snd + 1)
source
def SetTheory.PGame.Domineering.shiftUp :
ℤ × ℤ ≃ ℤ × ℤ

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

Instances For
    source
    @[simp]
    theorem SetTheory.PGame.Domineering.shiftRight_symm_apply :
    ∀ (a : ℤ × ℤ), ↑SetTheory.PGame.Domineering.shiftRight.symm a = (a.fst + -1, a.snd)
    source
    @[simp]
    theorem SetTheory.PGame.Domineering.shiftRight_apply :
    ∀ (a : ℤ × ℤ), ↑SetTheory.PGame.Domineering.shiftRight a = (a.fst + 1, a.snd)
    source
    def SetTheory.PGame.Domineering.shiftRight :
    ℤ × ℤ ≃ ℤ × ℤ

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

    Instances For
      source
      @[reducible]
      def SetTheory.PGame.Domineering.Board :
      Type

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

      Instances For
        source
        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.

        Instances For
          source
          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.

          Instances For
            source
            theorem SetTheory.PGame.Domineering.mem_left {b : SetTheory.PGame.Domineering.Board} (x : ℤ × ℤ) :
            x ∈ SetTheory.PGame.Domineering.left b ↔ x ∈ b ∧ (x.fst, x.snd - 1) ∈ b
            source
            theorem SetTheory.PGame.Domineering.mem_right {b : SetTheory.PGame.Domineering.Board} (x : ℤ × ℤ) :
            x ∈ SetTheory.PGame.Domineering.right b ↔ x ∈ b ∧ (x.fst - 1, x.snd) ∈ b
            source
            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.

            Instances For
              source
              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.

              Instances For
                source
                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.fst - 1, m.snd) ∈ Finset.erase b m
                source
                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.fst, m.snd - 1) ∈ Finset.erase b m
                source
                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
                source
                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
                source
                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
                source
                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
                source
                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
                source
                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
                source
                instance SetTheory.PGame.Domineering.state :
                SetTheory.PGame.State SetTheory.PGame.Domineering.Board

                The instance describing allowed moves on a Domineering board.

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

                Construct a pre-game from a Domineering board.

                Instances For
                  source
                  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.

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

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

                  Instances For
                    source
                    def SetTheory.PGame.domineering.L :
                    SetTheory.PGame

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

                    Instances For
                      source
                      instance SetTheory.PGame.shortOne :
                      SetTheory.PGame.Short SetTheory.PGame.domineering.one
                      source
                      instance SetTheory.PGame.shortL :
                      SetTheory.PGame.Short SetTheory.PGame.domineering.L