Documentation

CombinatorialGames.Game.Impartial.Basic

Basic definitions about impartial games #

We will define an impartial game, one in which left and right can make exactly the same moves. Our definition differs slightly by saying that the game is always equivalent to its negative, no matter what moves are played. This allows for games such as poker-nim to be classified as impartial.

source
class IGame.Impartial (x : IGame) :
Prop

An impartial game is one that's equivalent to its negative, such that each left and right move is also impartial.

Note that this is a slightly more general definition than the one that's usually in the literature, as we don't require x = -x. Despite this, the Sprague-Grundy theorem still holds: see IGame.equiv_nim_grundyValue.

In such a game, both players have the same payoffs at any subposition.

Instances
    source
    theorem IGame.impartial_iff_aux (x : IGame) :
    x.Impartial ↔ IGame.ImpartialAux✝ x
    source
    theorem IGame.impartial_def {x : IGame} :
    x.Impartial ↔ -x ≈ x ∧ ∀ (p : Player), ∀ y ∈ moves p x, y.Impartial
    source
    theorem IGame.Impartial.mk {x : IGame} (h₁ : -x ≈ x) (h₂ : ∀ (p : Player), ∀ y ∈ moves p x, y.Impartial) :
    x.Impartial
    source
    @[simp]
    theorem IGame.Impartial.neg_equiv (x : IGame) [hx : x.Impartial] :
    -x ≈ x
    source
    @[simp]
    theorem IGame.Impartial.equiv_neg (x : IGame) [hx : x.Impartial] :
    x ≈ -x
    source
    theorem IGame.Impartial.sub_equiv (x y : IGame) [hy : y.Impartial] :
    x - y ≈ x + y
    source
    @[simp]
    theorem IGame.Impartial.neg_mk (x : IGame) [hx : x.Impartial] :
    -Game.mk x = Game.mk x
    source
    @[simp]
    theorem IGame.Impartial.sub_mk (y : IGame) [hy : y.Impartial] (x : Game) :
    x - Game.mk y = x + Game.mk y
    source
    @[simp]
    theorem IGame.Impartial.mk_add_self (x : IGame) [hx : x.Impartial] :
    Game.mk x + Game.mk x = 0
    source
    theorem IGame.Impartial.add_self_equiv (x : IGame) [x.Impartial] :
    x + x ≈ 0
    source
    theorem IGame.Impartial.of_mem_moves {p : Player} {x y : IGame} [h : x.Impartial] :
    y ∈ moves p x → y.Impartial
    source
    def IGame.Impartial.tacticImpartial :
    Lean.ParserDescr

    impartial eagerly adds all possible Impartial hypotheses.

    Equations
    Instances For
      source
      instance IGame.Impartial.zero :
      Impartial 0
      source
      instance IGame.Impartial.star :
      ⋆.Impartial
      source
      @[irreducible]
      instance IGame.Impartial.neg (x : IGame) [x.Impartial] :
      (-x).Impartial
      source
      @[irreducible]
      instance IGame.Impartial.add (x y : IGame) [x.Impartial] [y.Impartial] :
      (x + y).Impartial
      source
      instance IGame.Impartial.sub (x y : IGame) [x.Impartial] [y.Impartial] :
      (x - y).Impartial
      source
      theorem IGame.Impartial.le_comm {x y : IGame} [x.Impartial] [y.Impartial] :
      x ≤ y ↔ y ≤ x

      The product instance is proven in Game.Impartial.Grundy.

      source
      @[simp]
      theorem IGame.Impartial.not_lt (x y : IGame) [hx : x.Impartial] [hy : y.Impartial] :
      ¬x < y
      source
      theorem IGame.Impartial.equiv_or_fuzzy (x y : IGame) [hx : x.Impartial] [hy : y.Impartial] :
      x ≈ y ∨ x ‖ y

      By setting y = 0, we find that in an impartial game, either the first player always wins, or the second player always wins.

      source
      theorem IGame.Impartial.equiv_iff_add_equiv_zero {x y : IGame} [y.Impartial] :
      x ≈ y ↔ x + y ≈ 0

      This lemma doesn't require x to be impartial.

      source
      theorem IGame.Impartial.equiv_iff_add_equiv_zero' {x y : IGame} [x.Impartial] :
      x ≈ y ↔ x + y ≈ 0

      This lemma doesn't require y to be impartial.

      source
      @[simp]
      theorem IGame.Impartial.not_equiv_iff {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] :
      ¬x ≈ y ↔ x ‖ y
      source
      @[simp]
      theorem IGame.Impartial.not_fuzzy_iff {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] :
      ¬x ‖ y ↔ x ≈ y
      source
      theorem IGame.Impartial.fuzzy_iff_add_fuzzy_zero {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] :
      x ‖ y ↔ x + y ‖ 0
      source
      @[simp]
      theorem IGame.Impartial.le_iff_equiv {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] :
      x ≤ y ↔ x ≈ y
      source
      theorem IGame.Impartial.ge_iff_equiv {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] :
      y ≤ x ↔ x ≈ y
      source
      theorem IGame.Impartial.lf_iff_fuzzy {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] :
      ¬y ≤ x ↔ x ‖ y
      source
      theorem IGame.Impartial.gf_iff_fuzzy {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] :
      ¬x ≤ y ↔ x ‖ y
      source
      theorem IGame.Impartial.fuzzy_of_mem_moves {x : IGame} [hx : x.Impartial] {y : IGame} {p : Player} (hy : y ∈ moves p x) :
      y ‖ x
      source
      theorem IGame.Impartial.equiv_iff_forall_fuzzy {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] (p : Player) :
      x ≈ y ↔ (∀ z ∈ moves p x, z ‖ y) ∧ ∀ z ∈ moves (-p) y, x ‖ z
      source
      theorem IGame.Impartial.fuzzy_iff_exists_equiv {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] (p : Player) :
      x ‖ y ↔ (∃ z ∈ moves p x, z ≈ y) ∨ ∃ z ∈ moves (-p) y, x ≈ z
      source
      theorem IGame.Impartial.equiv_zero {x : IGame} [hx : x.Impartial] (p : Player) :
      x ≈ 0 ↔ ∀ y ∈ moves p x, y ‖ 0
      source
      theorem IGame.Impartial.fuzzy_zero {x : IGame} [hx : x.Impartial] (p : Player) :
      x ‖ 0 ↔ ∃ y ∈ moves p x, y ≈ 0
      source
      theorem IGame.Impartial.fuzzy_zero_of_forall_exists {x : IGame} [hx : x.Impartial] {p : Player} {y : IGame} (hy : y ∈ moves p x) (H : ∀ z ∈ moves p y, ∃ w ∈ moves p x, z ≈ w) :
      x ‖ 0

      A strategy stealing argument. If there's a move in x, such that any immediate move could have also been reached in the first turn, then x is won by the first player.