Documentation

Mathlib.SetTheory.Game.Short

Short games #

A combinatorial game is Short [Conway, ch.9][conway2001] if it has only finitely many positions. In particular, this means there is a finite set of moves at every point.

We prove that the order relations and <, and the equivalence relation , are decidable on short games, although unfortunately in practice decide doesn't seem to be able to prove anything using these instances.

class inductive SetTheory.PGame.Short :
SetTheory.PGameType (u + 1)

A short game is a game with a finite set of moves at every turn.

Instances
    def SetTheory.PGame.fintypeLeft {α : Type u} {β : Type u} {L : αSetTheory.PGame} {R : βSetTheory.PGame} [S : SetTheory.PGame.Short (SetTheory.PGame.mk α β L R)] :

    Extracting the Fintype instance for the indexing type for Left's moves in a short game. This is an unindexed typeclass, so it can't be made a global instance.

    Instances For
      def SetTheory.PGame.fintypeRight {α : Type u} {β : Type u} {L : αSetTheory.PGame} {R : βSetTheory.PGame} [S : SetTheory.PGame.Short (SetTheory.PGame.mk α β L R)] :

      Extracting the Fintype instance for the indexing type for Right's moves in a short game. This is an unindexed typeclass, so it can't be made a global instance.

      Instances For
        def SetTheory.PGame.moveLeftShort' {xl : Type u_1} {xr : Type u_1} (xL : xlSetTheory.PGame) (xR : xrSetTheory.PGame) [S : SetTheory.PGame.Short (SetTheory.PGame.mk xl xr xL xR)] (i : xl) :

        Extracting the Short instance for a move by Left. This would be a dangerous instance potentially introducing new metavariables in typeclass search, so we only make it an instance locally.

        Instances For
          def SetTheory.PGame.moveRightShort' {xl : Type u_1} {xr : Type u_1} (xL : xlSetTheory.PGame) (xR : xrSetTheory.PGame) [S : SetTheory.PGame.Short (SetTheory.PGame.mk xl xr xL xR)] (j : xr) :

          Extracting the Short instance for a move by Right. This would be a dangerous instance potentially introducing new metavariables in typeclass search, so we only make it an instance locally.

          Instances For

            This leads to infinite loops if made into an instance.

            Instances For
              class inductive SetTheory.PGame.ListShort :

              Evidence that every PGame in a list is Short.

              Instances
                @[deprecated SetTheory.PGame.listShortGet]

                If x is a short game, and y is a relabelling of x, then y is also short.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.

                  Auxiliary construction of decidability instances. We build Decidable (x ≤ y) and Decidable (x ⧏ y) in a simultaneous induction. Instances for the two projections separately are provided below.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For