mathlib documentation

set_theory.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 classifed as impartial.

source
def pgame.impartial_aux  :
pgame → Prop

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

Equations
source
theorem pgame.impartial_aux_def {G : pgame} :
G.impartial_aux ↔ G.equiv (-G) ∧ (∀ (i : G.left_moves), (G.move_left i).impartial_aux) ∧ ∀ (j : G.right_moves), (G.move_right j).impartial_aux
source
@[class]
structure pgame.impartial (G : pgame) :
Prop

A typeclass on impartial games.

Instances of this typeclass
source
theorem pgame.impartial_iff_aux {G : pgame} :
G.impartial ↔ G.impartial_aux
source
theorem pgame.impartial_def {G : pgame} :
G.impartial ↔ G.equiv (-G) ∧ (∀ (i : G.left_moves), (G.move_left i).impartial) ∧ ∀ (j : G.right_moves), (G.move_right j).impartial
source
@[protected, instance]
def pgame.impartial.impartial_zero  :
0.impartial
source
@[protected, instance]
def pgame.impartial.impartial_star  :
pgame.star.impartial
source
theorem pgame.impartial.neg_equiv_self (G : pgame) [h : G.impartial] :
G.equiv (-G)
source
@[simp]
theorem pgame.impartial.mk_neg_equiv_self (G : pgame) [h : G.impartial] :
-⟦G⟧ = ⟦G⟧
source
@[protected, instance]
def pgame.impartial.move_left_impartial {G : pgame} [h : G.impartial] (i : G.left_moves) :
(G.move_left i).impartial
source
@[protected, instance]
def pgame.impartial.move_right_impartial {G : pgame} [h : G.impartial] (j : G.right_moves) :
(G.move_right j).impartial
source
theorem pgame.impartial.impartial_congr {G H : pgame} (e : G.relabelling H) [G.impartial] :
H.impartial
source
@[protected, instance]
def pgame.impartial.impartial_add (G H : pgame) [G.impartial] [H.impartial] :
(G + H).impartial
source
@[protected, instance]
def pgame.impartial.impartial_neg (G : pgame) [G.impartial] :
(-G).impartial
source
theorem pgame.impartial.nonpos (G : pgame) [G.impartial] :
¬0 < G
source
theorem pgame.impartial.nonneg (G : pgame) [G.impartial] :
¬G < 0
source
theorem pgame.impartial.equiv_or_fuzzy_zero (G : pgame) [G.impartial] :
G.equiv 0 ∨ G.fuzzy 0

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

source
@[simp]
theorem pgame.impartial.not_equiv_zero_iff (G : pgame) [G.impartial] :
¬G.equiv 0 ↔ G.fuzzy 0
source
@[simp]
theorem pgame.impartial.not_fuzzy_zero_iff (G : pgame) [G.impartial] :
¬G.fuzzy 0 ↔ G.equiv 0
source
theorem pgame.impartial.add_self (G : pgame) [G.impartial] :
(G + G).equiv 0
source
@[simp]
theorem pgame.impartial.mk_add_self (G : pgame) [G.impartial] :
⟦G⟧ + ⟦G⟧ = 0
source
theorem pgame.impartial.equiv_iff_add_equiv_zero (G : pgame) [G.impartial] (H : pgame) :
H.equiv G ↔ (H + G).equiv 0

This lemma doesn't require H to be impartial.

source
theorem pgame.impartial.equiv_iff_add_equiv_zero' (G : pgame) [G.impartial] (H : pgame) :
G.equiv H ↔ (G + H).equiv 0

This lemma doesn't require H to be impartial.

source
theorem pgame.impartial.le_zero_iff {G : pgame} [G.impartial] :
G ≤ 0 ↔ 0 ≤ G
source
theorem pgame.impartial.lf_zero_iff {G : pgame} [G.impartial] :
G.lf 0 ↔ 0.lf G
source
theorem pgame.impartial.equiv_zero_iff_le (G : pgame) [G.impartial] :
G.equiv 0 ↔ G ≤ 0
source
theorem pgame.impartial.fuzzy_zero_iff_lf (G : pgame) [G.impartial] :
G.fuzzy 0 ↔ G.lf 0
source
theorem pgame.impartial.equiv_zero_iff_ge (G : pgame) [G.impartial] :
G.equiv 0 ↔ 0 ≤ G
source
theorem pgame.impartial.fuzzy_zero_iff_gf (G : pgame) [G.impartial] :
G.fuzzy 0 ↔ 0.lf G
source
theorem pgame.impartial.forall_left_moves_fuzzy_iff_equiv_zero (G : pgame) [G.impartial] :
(∀ (i : G.left_moves), (G.move_left i).fuzzy 0) ↔ G.equiv 0
source
theorem pgame.impartial.forall_right_moves_fuzzy_iff_equiv_zero (G : pgame) [G.impartial] :
(∀ (j : G.right_moves), (G.move_right j).fuzzy 0) ↔ G.equiv 0
source
theorem pgame.impartial.exists_left_move_equiv_iff_fuzzy_zero (G : pgame) [G.impartial] :
(∃ (i : G.left_moves), (G.move_left i).equiv 0) ↔ G.fuzzy 0
source
theorem pgame.impartial.exists_right_move_equiv_iff_fuzzy_zero (G : pgame) [G.impartial] :
(∃ (j : G.right_moves), (G.move_right j).equiv 0) ↔ G.fuzzy 0