Documentation

Mathlib.SetTheory.Game.State

Games described via "the state of the board". #

We provide a simple mechanism for constructing combinatorial (pre-)games, by describing "the state of the board", and providing an upper bound on the number of turns remaining.

Implementation notes #

We're very careful to produce a computable definition, so small games can be evaluated using decide. To achieve this, I've had to rely solely on induction on natural numbers: relying on general well-foundedness seems to be poisonous to computation?

See SetTheory/Game/Domineering for an example using this construction.

source
class SetTheory.PGame.State (S : Type u) :
Type u

SetTheory.PGame.State S describes how to interpret s : S as a state of a combinatorial game. Use SetTheory.PGame.ofState s or SetTheory.Game.ofState s to construct the game.

SetTheory.PGame.State.l : S → Finset S and SetTheory.PGame.State.r : S → Finset S describe the states reachable by a move by Left or Right. SetTheory.PGame.State.turnBound : S → ℕ gives an upper bound on the number of possible turns remaining from this state.

Instances
    source
    theorem SetTheory.PGame.turnBound_ne_zero_of_left_move {S : Type u} [SetTheory.PGame.State S] {s : S} {t : S} (m : t ∈ SetTheory.PGame.State.l s) :
    SetTheory.PGame.State.turnBound s ≠ 0
    source
    theorem SetTheory.PGame.turnBound_ne_zero_of_right_move {S : Type u} [SetTheory.PGame.State S] {s : S} {t : S} (m : t ∈ SetTheory.PGame.State.r s) :
    SetTheory.PGame.State.turnBound s ≠ 0
    source
    theorem SetTheory.PGame.turnBound_of_left {S : Type u} [SetTheory.PGame.State S] {s : S} {t : S} (m : t ∈ SetTheory.PGame.State.l s) (n : ℕ) (h : SetTheory.PGame.State.turnBound s ≤ n + 1) :
    SetTheory.PGame.State.turnBound t ≤ n
    source
    theorem SetTheory.PGame.turnBound_of_right {S : Type u} [SetTheory.PGame.State S] {s : S} {t : S} (m : t ∈ SetTheory.PGame.State.r s) (n : ℕ) (h : SetTheory.PGame.State.turnBound s ≤ n + 1) :
    SetTheory.PGame.State.turnBound t ≤ n
    source
    def SetTheory.PGame.ofStateAux {S : Type u} [SetTheory.PGame.State S] (n : ℕ) (s : S) :
    SetTheory.PGame.State.turnBound s ≤ n → SetTheory.PGame

    Construct a PGame from a state and a (not necessarily optimal) bound on the number of turns remaining.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def SetTheory.PGame.ofStateAuxRelabelling {S : Type u} [SetTheory.PGame.State S] (s : S) (n : ℕ) (m : ℕ) (hn : SetTheory.PGame.State.turnBound s ≤ n) (hm : SetTheory.PGame.State.turnBound s ≤ m) :
      SetTheory.PGame.Relabelling (SetTheory.PGame.ofStateAux n s hn) (SetTheory.PGame.ofStateAux m s hm)

      Two different (valid) turn bounds give equivalent games.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def SetTheory.PGame.ofState {S : Type u} [SetTheory.PGame.State S] (s : S) :
        SetTheory.PGame

        Construct a combinatorial PGame from a state.

        Equations
        Instances For
          source
          def SetTheory.PGame.leftMovesOfStateAux {S : Type u} [SetTheory.PGame.State S] (n : ℕ) {s : S} (h : SetTheory.PGame.State.turnBound s ≤ n) :
          SetTheory.PGame.LeftMoves (SetTheory.PGame.ofStateAux n s h) ≃ { t : S // t ∈ SetTheory.PGame.State.l s }

          The equivalence between leftMoves for a PGame constructed using ofStateAux _ s _, and L s.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def SetTheory.PGame.leftMovesOfState {S : Type u} [SetTheory.PGame.State S] (s : S) :
            SetTheory.PGame.LeftMoves (SetTheory.PGame.ofState s) ≃ { t : S // t ∈ SetTheory.PGame.State.l s }

            The equivalence between leftMoves for a PGame constructed using ofState s, and l s.

            Equations
            Instances For
              source
              def SetTheory.PGame.rightMovesOfStateAux {S : Type u} [SetTheory.PGame.State S] (n : ℕ) {s : S} (h : SetTheory.PGame.State.turnBound s ≤ n) :
              SetTheory.PGame.RightMoves (SetTheory.PGame.ofStateAux n s h) ≃ { t : S // t ∈ SetTheory.PGame.State.r s }

              The equivalence between rightMoves for a PGame constructed using ofStateAux _ s _, and R s.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def SetTheory.PGame.rightMovesOfState {S : Type u} [SetTheory.PGame.State S] (s : S) :
                SetTheory.PGame.RightMoves (SetTheory.PGame.ofState s) ≃ { t : S // t ∈ SetTheory.PGame.State.r s }

                The equivalence between rightMoves for a PGame constructed using ofState s, and R s.

                Equations
                Instances For
                  source
                  def SetTheory.PGame.relabellingMoveLeftAux {S : Type u} [SetTheory.PGame.State S] (n : ℕ) {s : S} (h : SetTheory.PGame.State.turnBound s ≤ n) (t : SetTheory.PGame.LeftMoves (SetTheory.PGame.ofStateAux n s h)) :
                  SetTheory.PGame.Relabelling (SetTheory.PGame.moveLeft (SetTheory.PGame.ofStateAux n s h) t) (SetTheory.PGame.ofStateAux (n - 1) ↑((SetTheory.PGame.leftMovesOfStateAux n h) t) (_ : SetTheory.PGame.State.turnBound ↑((SetTheory.PGame.leftMovesOfStateAux n h) t) ≤ n - 1))

                  The relabelling showing moveLeft applied to a game constructed using ofStateAux has itself been constructed using ofStateAux.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def SetTheory.PGame.relabellingMoveLeft {S : Type u} [SetTheory.PGame.State S] (s : S) (t : SetTheory.PGame.LeftMoves (SetTheory.PGame.ofState s)) :
                    SetTheory.PGame.Relabelling (SetTheory.PGame.moveLeft (SetTheory.PGame.ofState s) t) (SetTheory.PGame.ofState ↑((SetTheory.PGame.leftMovesOfState s).toFun t))

                    The relabelling showing moveLeft applied to a game constructed using of has itself been constructed using of.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def SetTheory.PGame.relabellingMoveRightAux {S : Type u} [SetTheory.PGame.State S] (n : ℕ) {s : S} (h : SetTheory.PGame.State.turnBound s ≤ n) (t : SetTheory.PGame.RightMoves (SetTheory.PGame.ofStateAux n s h)) :
                      SetTheory.PGame.Relabelling (SetTheory.PGame.moveRight (SetTheory.PGame.ofStateAux n s h) t) (SetTheory.PGame.ofStateAux (n - 1) ↑((SetTheory.PGame.rightMovesOfStateAux n h) t) (_ : SetTheory.PGame.State.turnBound ↑((SetTheory.PGame.rightMovesOfStateAux n h) t) ≤ n - 1))

                      The relabelling showing moveRight applied to a game constructed using ofStateAux has itself been constructed using ofStateAux.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def SetTheory.PGame.relabellingMoveRight {S : Type u} [SetTheory.PGame.State S] (s : S) (t : SetTheory.PGame.RightMoves (SetTheory.PGame.ofState s)) :
                        SetTheory.PGame.Relabelling (SetTheory.PGame.moveRight (SetTheory.PGame.ofState s) t) (SetTheory.PGame.ofState ↑((SetTheory.PGame.rightMovesOfState s).toFun t))

                        The relabelling showing moveRight applied to a game constructed using of has itself been constructed using of.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          instance SetTheory.PGame.fintypeLeftMovesOfStateAux {S : Type u} [SetTheory.PGame.State S] (n : ℕ) (s : S) (h : SetTheory.PGame.State.turnBound s ≤ n) :
                          Fintype (SetTheory.PGame.LeftMoves (SetTheory.PGame.ofStateAux n s h))
                          Equations
                          source
                          instance SetTheory.PGame.fintypeRightMovesOfStateAux {S : Type u} [SetTheory.PGame.State S] (n : ℕ) (s : S) (h : SetTheory.PGame.State.turnBound s ≤ n) :
                          Fintype (SetTheory.PGame.RightMoves (SetTheory.PGame.ofStateAux n s h))
                          Equations
                          source
                          instance SetTheory.PGame.shortOfStateAux {S : Type u} [SetTheory.PGame.State S] (n : ℕ) {s : S} (h : SetTheory.PGame.State.turnBound s ≤ n) :
                          SetTheory.PGame.Short (SetTheory.PGame.ofStateAux n s h)
                          Equations
                          • One or more equations did not get rendered due to their size.
                          source
                          instance SetTheory.PGame.shortOfState {S : Type u} [SetTheory.PGame.State S] (s : S) :
                          SetTheory.PGame.Short (SetTheory.PGame.ofState s)
                          Equations
                          source
                          def SetTheory.Game.ofState {S : Type u} [SetTheory.PGame.State S] (s : S) :
                          SetTheory.Game

                          Construct a combinatorial Game from a state.

                          Equations
                          Instances For