Documentation

CombinatorialGames.Game.Impartial

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 ∧ (∀ i ∈ x.leftMoves, i.Impartial) ∧ ∀ j ∈ x.rightMoves, j.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
    @[simp]
    theorem IGame.Impartial.neg_mk (x : IGame) [hx : x.Impartial] :
    -Game.mk x = Game.mk x
    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_leftMoves {x y : IGame} [h : x.Impartial] :
    y ∈ x.leftMoves → y.Impartial
    source
    theorem IGame.Impartial.of_mem_rightMoves {x y : IGame} [h : x.Impartial] :
    y ∈ x.rightMoves → y.Impartial
    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
    theorem IGame.Impartial.le_comm {x y : IGame} [x.Impartial] [y.Impartial] :
    x ≤ y ↔ y ≤ x
    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 (y : IGame) [hy : y.Impartial] (x : IGame) :
    x ≈ y ↔ x + y ≈ 0

    This lemma doesn't require x to be impartial.

    source
    theorem IGame.Impartial.equiv_iff_add_equiv_zero' (x : IGame) [hx : x.Impartial] (y : IGame) :
    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
    @[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_leftMove {x : IGame} [hx : x.Impartial] {y : IGame} (hy : y ∈ x.leftMoves) :
    x ‖ y
    source
    theorem IGame.Impartial.leftMove_fuzzy {x : IGame} [hx : x.Impartial] {y : IGame} (hy : y ∈ x.leftMoves) :
    y ‖ x
    source
    theorem IGame.Impartial.rightMove_fuzzy {x : IGame} [hx : x.Impartial] {y : IGame} (hy : y ∈ x.rightMoves) :
    y ‖ x
    source
    theorem IGame.Impartial.fuzzy_rightMove {x : IGame} [hx : x.Impartial] {y : IGame} (hy : y ∈ x.rightMoves) :
    x ‖ y
    source
    theorem IGame.Impartial.equiv_iff_forall_fuzzy {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] :
    x ≈ y ↔ (∀ z ∈ x.leftMoves, z ‖ y) ∧ ∀ z ∈ y.rightMoves, x ‖ z

    This version is stated in terms of left moves of x and right moves of y.

    source
    theorem IGame.Impartial.equiv_iff_forall_fuzzy' {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] :
    x ≈ y ↔ (∀ z ∈ x.rightMoves, z ‖ y) ∧ ∀ z ∈ y.leftMoves, x ‖ z

    This version is stated in terms of right moves of x and left moves of y.

    source
    theorem IGame.Impartial.fuzzy_iff_exists_equiv' {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] :
    x ‖ y ↔ (∃ z ∈ y.leftMoves, x ≈ z) ∨ ∃ z ∈ x.rightMoves, z ≈ y

    This version is stated in terms of left moves of y and right moves of x.

    source
    theorem IGame.Impartial.fuzzy_iff_exists_equiv {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] :
    x ‖ y ↔ (∃ z ∈ y.rightMoves, x ≈ z) ∨ ∃ z ∈ x.leftMoves, z ≈ y

    This version is stated in terms of right moves of y and left moves of x.

    source
    theorem IGame.Impartial.equiv_zero {x : IGame} [hx : x.Impartial] :
    x ≈ 0 ↔ ∀ y ∈ x.leftMoves, y ‖ 0

    This version is stated in terms of left moves of x.

    source
    theorem IGame.Impartial.equiv_zero' {x : IGame} [hx : x.Impartial] :
    x ≈ 0 ↔ ∀ y ∈ x.rightMoves, y ‖ 0

    This version is stated in terms of right moves of x.

    source
    theorem IGame.Impartial.fuzzy_zero {x : IGame} [hx : x.Impartial] :
    x ‖ 0 ↔ ∃ y ∈ x.leftMoves, y ≈ 0

    This version is stated in terms of left moves of x.

    source
    theorem IGame.Impartial.fuzzy_zero' {x : IGame} [hx : x.Impartial] :
    x ‖ 0 ↔ ∃ y ∈ x.rightMoves, y ≈ 0

    This version is stated in terms of right moves of x.

    source
    theorem IGame.Impartial.fuzzy_zero_of_forall_exists_moveLeft {x : IGame} [hx : x.Impartial] {y : IGame} (hy : y ∈ x.leftMoves) (H : ∀ z ∈ y.leftMoves, ∃ w ∈ x.leftMoves, 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.

    This version of the theorem is stated exclusively in terms of left moves; see fuzzy_zero_of_forall_exists_moveRight for a version stated with right moves.

    source
    theorem IGame.Impartial.fuzzy_zero_of_forall_exists_moveRight {x : IGame} [hx : x.Impartial] {y : IGame} (hy : y ∈ x.rightMoves) (H : ∀ z ∈ y.rightMoves, ∃ w ∈ x.rightMoves, 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.

    This version of the theorem is stated exclusively in terms of right moves; see fuzzy_zero_of_forall_exists_moveLeft for a version stated with left moves.