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
@[class]
def pgame.impartial (a : pgame) :
Prop

The definition for a impartial game, defined using Conway induction

Equations
Instances
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
@[instance]
def pgame.impartial.impartial_zero  :
0.impartial

source
theorem pgame.impartial.neg_equiv_self (G : pgame) [h : G.impartial] :
G.equiv (-G)

source
@[instance]
def pgame.impartial.move_left_impartial {G : pgame} [h : G.impartial] (i : G.left_moves) :
(G.move_left i).impartial

source
@[instance]
def pgame.impartial.move_right_impartial {G : pgame} [h : G.impartial] (j : G.right_moves) :
(G.move_right j).impartial

source
@[instance]
def pgame.impartial.impartial_add (G H : pgame) [G.impartial] [H.impartial] :
(G + H).impartial

source
@[instance]
def pgame.impartial.impartial_neg (G : pgame) [G.impartial] :
(-G).impartial

source
theorem pgame.impartial.winner_cases (G : pgame) [G.impartial] :
G.first_loses ∨ G.first_wins

source
theorem pgame.impartial.not_first_wins (G : pgame) [G.impartial] :
¬G.first_wins ↔ G.first_loses

source
theorem pgame.impartial.not_first_loses (G : pgame) [G.impartial] :
¬G.first_loses ↔ G.first_wins

source
theorem pgame.impartial.add_self (G : pgame) [G.impartial] :
(G + G).first_loses

source
theorem pgame.impartial.equiv_iff_sum_first_loses (G H : pgame) [G.impartial] [H.impartial] :
G.equiv H ↔ (G + H).first_loses

source
theorem pgame.impartial.le_zero_iff {G : pgame} [G.impartial] :
G ≤ 0 ↔ 0 ≤ G

source
theorem pgame.impartial.lt_zero_iff {G : pgame} [G.impartial] :
G < 0 ↔ 0 < G

source
theorem pgame.impartial.first_loses_symm (G : pgame) [G.impartial] :
G.first_loses ↔ G ≤ 0

source
theorem pgame.impartial.first_wins_symm (G : pgame) [G.impartial] :
G.first_wins ↔ G < 0

source
theorem pgame.impartial.first_loses_symm' (G : pgame) [G.impartial] :
G.first_loses ↔ 0 ≤ G

source
theorem pgame.impartial.first_wins_symm' (G : pgame) [G.impartial] :
G.first_wins ↔ 0 < G

source
theorem pgame.impartial.no_good_left_moves_iff_first_loses (G : pgame) [G.impartial] :
(∀ (i : G.left_moves), (G.move_left i).first_wins) ↔ G.first_loses

source
theorem pgame.impartial.no_good_right_moves_iff_first_loses (G : pgame) [G.impartial] :
(∀ (j : G.right_moves), (G.move_right j).first_wins) ↔ G.first_loses

source
theorem pgame.impartial.good_left_move_iff_first_wins (G : pgame) [G.impartial] :
(∃ (i : G.left_moves), (G.move_left i).first_loses) ↔ G.first_wins

source
theorem pgame.impartial.good_right_move_iff_first_wins (G : pgame) [G.impartial] :
(∃ (j : G.right_moves), (G.move_right j).first_loses) ↔ G.first_wins