mathlib3 documentation

set_theory.game.impartial

Basic definitions about impartial (pre-)games #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

def pgame.impartial_aux :

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

Equations

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)

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

@[class]

structure pgame.impartial (G : pgame) :

Prop

out : G.impartial_aux

A typeclass on impartial games.

Instances of this typeclass

theorem pgame.impartial_iff_aux {G : pgame} :

G.impartial ↔ G.impartial_aux

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

@[protected, instance]

def pgame.impartial.impartial_zero :

@[protected, instance]

def pgame.impartial.impartial_star :

pgame.star.impartial

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

G.equiv (-G)

@[simp]

theorem pgame.impartial.mk_neg_equiv_self (G : pgame) [h : G.impartial] :

-⟦G⟧ = ⟦G⟧

@[protected, instance]

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

(G.move_left i).impartial

@[protected, instance]

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

(G.move_right j).impartial

theorem pgame.impartial.impartial_congr {G H : pgame} (e : G.relabelling H) [G.impartial] :

@[protected, instance]

def pgame.impartial.impartial_add (G H : pgame) [G.impartial] [H.impartial] :

(G + H).impartial

@[protected, instance]

def pgame.impartial.impartial_neg (G : pgame) [G.impartial] :

theorem pgame.impartial.nonpos (G : pgame) [G.impartial] :

¬0 < G

theorem pgame.impartial.nonneg (G : pgame) [G.impartial] :

¬G < 0

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.

@[simp]

theorem pgame.impartial.not_equiv_zero_iff (G : pgame) [G.impartial] :

¬G.equiv 0 ↔ G.fuzzy 0

@[simp]

theorem pgame.impartial.not_fuzzy_zero_iff (G : pgame) [G.impartial] :

¬G.fuzzy 0 ↔ G.equiv 0

theorem pgame.impartial.add_self (G : pgame) [G.impartial] :

(G + G).equiv 0

@[simp]

theorem pgame.impartial.mk_add_self (G : pgame) [G.impartial] :

⟦G⟧ + ⟦G⟧ = 0

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.

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.

theorem pgame.impartial.le_zero_iff {G : pgame} [G.impartial] :

G ≤ 0 ↔ 0 ≤ G

theorem pgame.impartial.lf_zero_iff {G : pgame} [G.impartial] :

G.lf 0 ↔ 0.lf G

theorem pgame.impartial.equiv_zero_iff_le (G : pgame) [G.impartial] :

G.equiv 0 ↔ G ≤ 0

theorem pgame.impartial.fuzzy_zero_iff_lf (G : pgame) [G.impartial] :

G.fuzzy 0 ↔ G.lf 0

theorem pgame.impartial.equiv_zero_iff_ge (G : pgame) [G.impartial] :

G.equiv 0 ↔ 0 ≤ G

theorem pgame.impartial.fuzzy_zero_iff_gf (G : pgame) [G.impartial] :

G.fuzzy 0 ↔ 0.lf G

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

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

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

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