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
@[irreducible]
def SetTheory.PGame.ImpartialAux (G : SetTheory.PGame) :
Prop

The definition for an impartial game, defined using Conway induction.

Equations
  • G.ImpartialAux = (G ≈ -G ∧ (∀ (i : G.LeftMoves), (G.moveLeft i).ImpartialAux) ∧ ∀ (j : G.RightMoves), (G.moveRight j).ImpartialAux)
source
theorem SetTheory.PGame.impartialAux_def {G : SetTheory.PGame} :
G.ImpartialAux ↔ G ≈ -G ∧ (∀ (i : G.LeftMoves), (G.moveLeft i).ImpartialAux) ∧ ∀ (j : G.RightMoves), (G.moveRight j).ImpartialAux
source
class SetTheory.PGame.Impartial (G : SetTheory.PGame) :
Prop

A typeclass on impartial games.

  • out : G.ImpartialAux
Instances
    source
    theorem SetTheory.PGame.impartial_iff_aux {G : SetTheory.PGame} :
    G.Impartial ↔ G.ImpartialAux
    source
    theorem SetTheory.PGame.impartial_def {G : SetTheory.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 :
    SetTheory.PGame.Impartial 0
    Equations
    source
    instance SetTheory.PGame.Impartial.impartial_star :
    SetTheory.PGame.star.Impartial
    Equations
    source
    theorem SetTheory.PGame.Impartial.neg_equiv_self (G : SetTheory.PGame) [h : G.Impartial] :
    G ≈ -G
    source
    @[simp]
    theorem SetTheory.PGame.Impartial.mk'_neg_equiv_self (G : SetTheory.PGame) [G.Impartial] :
    -⟦G⟧ = ⟦G⟧
    source
    instance SetTheory.PGame.Impartial.moveLeft_impartial {G : SetTheory.PGame} [h : G.Impartial] (i : G.LeftMoves) :
    (G.moveLeft i).Impartial
    Equations
    • ⋯ = ⋯
    source
    instance SetTheory.PGame.Impartial.moveRight_impartial {G : SetTheory.PGame} [h : G.Impartial] (j : G.RightMoves) :
    (G.moveRight j).Impartial
    Equations
    • ⋯ = ⋯
    source
    @[irreducible]
    theorem SetTheory.PGame.Impartial.impartial_congr {G H : SetTheory.PGame} (e : G.Relabelling H) [G.Impartial] :
    H.Impartial
    source
    @[irreducible]
    instance SetTheory.PGame.Impartial.impartial_add (G H : SetTheory.PGame) [G.Impartial] [H.Impartial] :
    (G + H).Impartial
    Equations
    • ⋯ = ⋯
    source
    @[irreducible]
    instance SetTheory.PGame.Impartial.impartial_neg (G : SetTheory.PGame) [G.Impartial] :
    (-G).Impartial
    Equations
    • ⋯ = ⋯
    source
    theorem SetTheory.PGame.Impartial.nonpos (G : SetTheory.PGame) [G.Impartial] :
    ¬0 < G
    source
    theorem SetTheory.PGame.Impartial.nonneg (G : SetTheory.PGame) [G.Impartial] :
    ¬G < 0
    source
    theorem SetTheory.PGame.Impartial.equiv_or_fuzzy_zero (G : SetTheory.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 : SetTheory.PGame) [G.Impartial] :
    ¬G ≈ 0 ↔ G.Fuzzy 0
    source
    @[simp]
    theorem SetTheory.PGame.Impartial.not_fuzzy_zero_iff (G : SetTheory.PGame) [G.Impartial] :
    ¬G.Fuzzy 0 ↔ G ≈ 0
    source
    theorem SetTheory.PGame.Impartial.add_self (G : SetTheory.PGame) [G.Impartial] :
    G + G ≈ 0
    source
    @[simp]
    theorem SetTheory.PGame.Impartial.mk'_add_self (G : SetTheory.PGame) [G.Impartial] :
    ⟦G⟧ + ⟦G⟧ = 0
    source
    theorem SetTheory.PGame.Impartial.equiv_iff_add_equiv_zero (G : SetTheory.PGame) [G.Impartial] (H : SetTheory.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 : SetTheory.PGame) [G.Impartial] (H : SetTheory.PGame) :
    G ≈ H ↔ G + H ≈ 0

    This lemma doesn't require H to be impartial.

    source
    theorem SetTheory.PGame.Impartial.le_zero_iff {G : SetTheory.PGame} [G.Impartial] :
    G ≤ 0 ↔ 0 ≤ G
    source
    theorem SetTheory.PGame.Impartial.lf_zero_iff {G : SetTheory.PGame} [G.Impartial] :
    G.LF 0 ↔ SetTheory.PGame.LF 0 G
    source
    theorem SetTheory.PGame.Impartial.equiv_zero_iff_le (G : SetTheory.PGame) [G.Impartial] :
    G ≈ 0 ↔ G ≤ 0
    source
    theorem SetTheory.PGame.Impartial.fuzzy_zero_iff_lf (G : SetTheory.PGame) [G.Impartial] :
    G.Fuzzy 0 ↔ G.LF 0
    source
    theorem SetTheory.PGame.Impartial.equiv_zero_iff_ge (G : SetTheory.PGame) [G.Impartial] :
    G ≈ 0 ↔ 0 ≤ G
    source
    theorem SetTheory.PGame.Impartial.fuzzy_zero_iff_gf (G : SetTheory.PGame) [G.Impartial] :
    G.Fuzzy 0 ↔ SetTheory.PGame.LF 0 G
    source
    theorem SetTheory.PGame.Impartial.forall_leftMoves_fuzzy_iff_equiv_zero (G : SetTheory.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 : SetTheory.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 : SetTheory.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 : SetTheory.PGame) [G.Impartial] :
    (∃ (j : G.RightMoves), G.moveRight j ≈ 0) ↔ G.Fuzzy 0