Documentation

Mathlib.SetTheory.Game.Impartial

Basic definitions about impartial (pre-)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 SetTheory.PGame.Impartial (G : PGame) :
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 G ≡ -G. Despite this, the Sprague-Grundy theorem still holds: see SetTheory.PGame.equiv_nim_grundyValue.

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

Instances
    source
    theorem SetTheory.PGame.impartial_def {G : PGame} :
    G.Impartial ↔ G ≈ -G ∧ (∀ (i : G.LeftMoves), (G.moveLeft i).Impartial) ∧ ∀ (j : G.RightMoves), (G.moveRight j).Impartial
    source
    instance SetTheory.PGame.Impartial.impartial_zero :
    Impartial 0
    source
    instance SetTheory.PGame.Impartial.impartial_star :
    star.Impartial
    source
    theorem SetTheory.PGame.Impartial.neg_equiv_self (G : PGame) [h : G.Impartial] :
    G ≈ -G
    source
    @[simp]
    theorem SetTheory.PGame.Impartial.mk'_neg_equiv_self (G : PGame) [G.Impartial] :
    -⟦G⟧ = ⟦G⟧
    source
    instance SetTheory.PGame.Impartial.moveLeft_impartial {G : PGame} [h : G.Impartial] (i : G.LeftMoves) :
    (G.moveLeft i).Impartial
    source
    instance SetTheory.PGame.Impartial.moveRight_impartial {G : PGame} [h : G.Impartial] (j : G.RightMoves) :
    (G.moveRight j).Impartial
    source
    @[irreducible]
    theorem SetTheory.PGame.Impartial.impartial_congr {G H : PGame} (e : G.Relabelling H) [G.Impartial] :
    H.Impartial
    source
    @[irreducible]
    instance SetTheory.PGame.Impartial.impartial_add (G H : PGame) [G.Impartial] [H.Impartial] :
    (G + H).Impartial
    source
    @[irreducible]
    instance SetTheory.PGame.Impartial.impartial_neg (G : PGame) [G.Impartial] :
    (-G).Impartial
    source
    theorem SetTheory.PGame.Impartial.nonpos (G : PGame) [G.Impartial] :
    ¬0 < G
    source
    theorem SetTheory.PGame.Impartial.nonneg (G : PGame) [G.Impartial] :
    ¬G < 0
    source
    theorem SetTheory.PGame.Impartial.equiv_or_fuzzy_zero (G : PGame) [G.Impartial] :
    G ≈ 0 ∨ G.Fuzzy 0

    In an impartial game, either the first player always wins, or the second player always wins.

    source
    @[simp]
    theorem SetTheory.PGame.Impartial.not_equiv_zero_iff (G : PGame) [G.Impartial] :
    ¬G ≈ 0 ↔ G.Fuzzy 0
    source
    @[simp]
    theorem SetTheory.PGame.Impartial.not_fuzzy_zero_iff (G : PGame) [G.Impartial] :
    ¬G.Fuzzy 0 ↔ G ≈ 0
    source
    theorem SetTheory.PGame.Impartial.add_self (G : PGame) [G.Impartial] :
    G + G ≈ 0
    source
    @[simp]
    theorem SetTheory.PGame.Impartial.mk'_add_self (G : PGame) [G.Impartial] :
    ⟦G⟧ + ⟦G⟧ = 0
    source
    theorem SetTheory.PGame.Impartial.equiv_iff_add_equiv_zero (G : PGame) [G.Impartial] (H : PGame) :
    H ≈ G ↔ H + G ≈ 0

    This lemma doesn't require H to be impartial.

    source
    theorem SetTheory.PGame.Impartial.equiv_iff_add_equiv_zero' (G : PGame) [G.Impartial] (H : PGame) :
    G ≈ H ↔ G + H ≈ 0

    This lemma doesn't require H to be impartial.

    source
    theorem SetTheory.PGame.Impartial.le_zero_iff {G : PGame} [G.Impartial] :
    G ≤ 0 ↔ 0 ≤ G
    source
    theorem SetTheory.PGame.Impartial.lf_zero_iff {G : PGame} [G.Impartial] :
    G.LF 0 ↔ LF 0 G
    source
    theorem SetTheory.PGame.Impartial.equiv_zero_iff_le (G : PGame) [G.Impartial] :
    G ≈ 0 ↔ G ≤ 0
    source
    theorem SetTheory.PGame.Impartial.fuzzy_zero_iff_lf (G : PGame) [G.Impartial] :
    G.Fuzzy 0 ↔ G.LF 0
    source
    theorem SetTheory.PGame.Impartial.equiv_zero_iff_ge (G : PGame) [G.Impartial] :
    G ≈ 0 ↔ 0 ≤ G
    source
    theorem SetTheory.PGame.Impartial.fuzzy_zero_iff_gf (G : PGame) [G.Impartial] :
    G.Fuzzy 0 ↔ LF 0 G
    source
    theorem SetTheory.PGame.Impartial.forall_leftMoves_fuzzy_iff_equiv_zero (G : PGame) [G.Impartial] :
    (∀ (i : G.LeftMoves), (G.moveLeft i).Fuzzy 0) ↔ G ≈ 0
    source
    theorem SetTheory.PGame.Impartial.forall_rightMoves_fuzzy_iff_equiv_zero (G : PGame) [G.Impartial] :
    (∀ (j : G.RightMoves), (G.moveRight j).Fuzzy 0) ↔ G ≈ 0
    source
    theorem SetTheory.PGame.Impartial.exists_left_move_equiv_iff_fuzzy_zero (G : PGame) [G.Impartial] :
    (∃ (i : G.LeftMoves), G.moveLeft i ≈ 0) ↔ G.Fuzzy 0
    source
    theorem SetTheory.PGame.Impartial.exists_right_move_equiv_iff_fuzzy_zero (G : PGame) [G.Impartial] :
    (∃ (j : G.RightMoves), G.moveRight j ≈ 0) ↔ G.Fuzzy 0