Documentation

CombinatorialGames.Game.Short

Short games #

A combinatorial game is Short if it has only finitely many subpositions. In particular, this means there is a finite set of moves at every point.

We historically defined Short x as data, which we then used to enable some degree of computation on combinatorial games. This functionality is now implemented through the game_cmp tactic instead.

source
@[irreducible]
def IGame.ShortAux (x : IGame) :
Prop
Equations
Instances For
    source
    class IGame.Short (x : IGame) :
    Prop

    A short game is one with finitely many subpositions. That is, the left and right sets are finite, and all of the games in them are short as well.

    Instances
      source
      theorem IGame.short_iff_aux (x : IGame) :
      x.Short ↔ x.ShortAux
      source
      theorem IGame.short_def {x : IGame} :
      x.Short ↔ ∀ (p : Player), (moves p x).Finite ∧ ∀ y ∈ moves p x, y.Short
      source
      theorem IGame.Short.mk {x : IGame} :
      (∀ (p : Player), (moves p x).Finite ∧ ∀ y ∈ moves p x, y.Short) → x.Short

      Alias of the reverse direction of IGame.short_def.

      source
      theorem IGame.Short.finite_moves (p : Player) (x : IGame) [h : x.Short] :
      (moves p x).Finite
      source
      theorem IGame.Short.finite_setOf_isOption (x : IGame) [x.Short] :
      {y : IGame | y.IsOption x}.Finite
      source
      instance IGame.Short.instFiniteElemMoves (p : Player) (x : IGame) [x.Short] :
      Finite ↑(moves p x)
      source
      instance IGame.Short.instFiniteSubtypeIsOption (x : IGame) [x.Short] :
      Finite { y : IGame // y.IsOption x }
      source
      theorem IGame.Short.of_mem_moves {x y : IGame} [h : x.Short] {p : Player} (hy : y ∈ moves p x) :
      y.Short
      source
      def IGame.Short.tacticShort :
      Lean.ParserDescr

      short eagerly adds all possible Short hypotheses.

      Equations
      Instances For
        source
        theorem IGame.Short.isOption {x y : IGame} [x.Short] (h : y.IsOption x) :
        y.Short
        source
        theorem IGame.IsOption.short {x y : IGame} [x.Short] (h : y.IsOption x) :
        y.Short

        Alias of IGame.Short.isOption.

        source
        @[irreducible]
        theorem IGame.Short.subposition {y x : IGame} [x.Short] (h : y.Subposition x) :
        y.Short
        source
        theorem IGame.IsOption.subposition {y x : IGame} [x.Short] (h : y.Subposition x) :
        y.Short

        Alias of IGame.Short.subposition.

        source
        @[irreducible]
        theorem IGame.Short.finite_setOf_subposition (x : IGame) [x.Short] :
        {y : IGame | y.Subposition x}.Finite
        source
        instance IGame.Short.instFiniteSubtypeSubposition (x : IGame) [x.Short] :
        Finite { y : IGame // y.Subposition x }
        source
        @[irreducible]
        theorem IGame.short_iff_finite_setOf_subposition {x : IGame} :
        x.Short ↔ {y : IGame | y.Subposition x}.Finite
        source
        @[simp]
        instance IGame.Short.zero :
        Short 0
        source
        @[simp]
        instance IGame.Short.one :
        Short 1
        source
        @[irreducible]
        instance IGame.Short.neg (x : IGame) [x.Short] :
        (-x).Short
        source
        @[simp]
        theorem IGame.Short.neg_iff {x : IGame} :
        (-x).Short ↔ x.Short
        source
        @[irreducible]
        instance IGame.Short.add (x y : IGame) [x.Short] [y.Short] :
        (x + y).Short
        source
        instance IGame.Short.sub (x y : IGame) [x.Short] [y.Short] :
        (x - y).Short
        source
        instance IGame.Short.natCast (n : ℕ) :
        (↑n).Short
        source
        instance IGame.Short.ofNat (n : ℕ) [n.AtLeastTwo] :
        (OfNat.ofNat n).Short
        source
        instance IGame.Short.intCast (n : ℤ) :
        (↑n).Short
        source
        @[irreducible]
        instance IGame.Short.mul (x y : IGame) [x.Short] [y.Short] :
        (x * y).Short
        source
        instance IGame.Short.mulOption (x y a b : IGame) [x.Short] [y.Short] [a.Short] [b.Short] :
        (mulOption x y a b).Short