Basic deinitions 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.
The definiton for a impartial game, defined using Conway induction
Equations
- G.impartial = (G.equiv (-G) ∧ (∀ (i : G.left_moves), (G.move_left i).impartial) ∧ ∀ (j : G.right_moves), (G.move_right j).impartial)
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
theorem
pgame.impartial_move_right_impartial
{G : pgame}
(h : G.impartial)
(j : G.right_moves) :
(G.move_right j).impartial
theorem
pgame.no_good_left_moves_iff_first_loses
{G : pgame} :
G.impartial → ((∀ (i : G.left_moves), (G.move_left i).first_wins) ↔ G.first_loses)
theorem
pgame.no_good_right_moves_iff_first_loses
{G : pgame} :
G.impartial → ((∀ (j : G.right_moves), (G.move_right j).first_wins) ↔ G.first_loses)
theorem
pgame.good_left_move_iff_first_wins
{G : pgame} :
G.impartial → ((∃ (i : G.left_moves), (G.move_left i).first_loses) ↔ G.first_wins)
theorem
pgame.good_right_move_iff_first_wins
{G : pgame} :
G.impartial → ((∃ (j : G.right_moves), (G.move_right j).first_loses) ↔ G.first_wins)