set_theory.game

# Combinatorial games. #

In this file we define the quotient of pre-games by the equivalence relation p ≈ q ↔ p ≤ q ∧ q ≤ p, and construct an instance add_comm_group game, as well as an instance partial_order game (although note carefully the warning that the < field in this instance is not the usual relation on combinatorial games).

## Multiplication on pre-games #

We define the operations of multiplication and inverse on pre-games, and prove a few basic theorems about them. Multiplication is not well-behaved under equivalence of pre-games i.e. x.equiv y does not imply (x*z).equiv (y*z). Hence, multiplication is not a well-defined operation on games. Nevertheless, the abelian group structure on games allows us to simplify many proofs for pre-games.

@[protected, instance]
Equations
def game  :
Type (u_1+1)

The type of combinatorial games. In ZFC, a combinatorial game is constructed from two sets of combinatorial games that have been constructed at an earlier stage. To do this in type theory, we say that a combinatorial pre-game is built inductively from two families of combinatorial games indexed over any type in Type u. The resulting type pgame.{u} lives in Type (u+1), reflecting that it is a proper class in ZFC. A combinatorial game is then constructed by quotienting by the equivalence x ≈ y ↔ x ≤ y ∧ y ≤ x.

def game.le  :
gamegame → Prop

The relation x ≤ y on games.

Equations
@[protected, instance]
Equations
theorem game.le_refl (x : game) :
x x
theorem game.le_trans (x y z : game) :
x yy zx z
theorem game.le_antisymm (x y : game) :
x yy xx = y
def game.lt  :
gamegame → Prop

The relation x < y on games.

Equations
theorem game.not_le {x y : game} :
¬x y y.lt x
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def game.neg  :

The negation of {L | R} is {-R | -L}.

Equations
@[protected, instance]
Equations
game

The sum of x = {xL | xR} and y = {yL | yR} is {xL + y, x + yL | xR + y, x + yR}.

Equations
@[protected, instance]
Equations
theorem game.add_assoc (x y z : game) :
x + y + z = x + (y + z)
@[protected, instance]
Equations
theorem game.add_zero (x : game) :
x + 0 = x
theorem game.zero_add (x : game) :
0 + x = x
@[protected, instance]
Equations
theorem game.add_left_neg (x : game) :
-x + x = 0
@[protected, instance]
Equations
theorem game.add_comm (x y : game) :
x + y = y + x
@[protected, instance]
Equations
@[protected, instance]
Equations
a b∀ (c : game), c + a c + b

The < operation provided by this partial order is not the usual < on games!

Equations

The < operation provided by this ordered_add_comm_group is not the usual < on games!

Equations
@[simp]
theorem pgame.quot_neg (a : pgame) :
@[simp]
theorem pgame.quot_add (a b : pgame) :
@[simp]
theorem pgame.quot_sub (a b : pgame) :

Multiplicative operations can be defined at the level of pre-games, but to prove their properties we need to use the abelian group structure of games. Hence we define them here.

def pgame.mul (x : pgame) (y : pgame) :

The product of x = {xL | xR} and y = {yL | yR} is {xL*y + x*yL - xL*yL, xR*y + x*yR - xR*yR | xL*y + x*yR - xL*yR, x*yL + xR*y - xR*yL }.

Equations
• x.mul y = pgame.rec (λ (xl xr : Type u_1) (xL : xl → pgame) (xR : xr → pgame) (IHxl : Π (ᾰ : xl), (λ (x : pgame), (xL ᾰ)) (IHxr : Π (ᾰ : xr), (λ (x : pgame), (xR ᾰ)) (y : pgame), pgame.rec (λ (yl yr : Type u_2) (yL : yl → pgame) (yR : yr → pgame) (IHyl : Π (ᾰ : yl), (λ (y : pgame), pgame) (yL ᾰ)) (IHyr : Π (ᾰ : yr), (λ (y : pgame), pgame) (yR ᾰ)), pgame.mk (xl × yl xr × yr) (xl × yr xr × yl) (λ (ᾰ : xl × yl xr × yr), ᾰ.cases_on (λ (ᾰ : xl × yl), ᾰ.cases_on (λ (i : xl) (j : yl), IHxl i (pgame.mk yl yr yL yR) + IHyl j - IHxl i (yL j))) (λ (ᾰ : xr × yr), ᾰ.cases_on (λ (i : xr) (j : yr), IHxr i (pgame.mk yl yr yL yR) + IHyr j - IHxr i (yR j)))) (λ (ᾰ : xl × yr xr × yl), ᾰ.cases_on (λ (ᾰ : xl × yr), ᾰ.cases_on (λ (i : xl) (j : yr), IHxl i (pgame.mk yl yr yL yR) + IHyr j - IHxl i (yR j))) (λ (ᾰ : xr × yl), ᾰ.cases_on (λ (i : xr) (j : yl), IHxr i (pgame.mk yl yr yL yR) + IHyl j - IHxr i (yL j))))) y) x y
@[protected, instance]
Equations
def pgame.left_moves_mul (x y : pgame) :

An explicit description of the moves for Left in x * y.

Equations

An explicit description of the moves for Right in x * y.

Equations
@[simp]
theorem pgame.mk_mul_move_left_inl {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xl} {j : yl} :
((pgame.mk xl xr xL xR) * pgame.mk yl yr yL yR).move_left (sum.inl (i, j)) = (xL i) * pgame.mk yl yr yL yR + (pgame.mk xl xr xL xR) * yL j - (xL i) * yL j
@[simp]
theorem pgame.mul_move_left_inl {x y : pgame} {i : x.left_moves} {j : y.left_moves} :
(x * y).move_left (((x.left_moves_mul y).symm) (sum.inl (i, j))) = (x.move_left i) * y + x * y.move_left j - (x.move_left i) * y.move_left j
@[simp]
theorem pgame.mk_mul_move_left_inr {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xr} {j : yr} :
((pgame.mk xl xr xL xR) * pgame.mk yl yr yL yR).move_left (sum.inr (i, j)) = (xR i) * pgame.mk yl yr yL yR + (pgame.mk xl xr xL xR) * yR j - (xR i) * yR j
@[simp]
theorem pgame.mul_move_left_inr {x y : pgame} {i : x.right_moves} {j : y.right_moves} :
(x * y).move_left (((x.left_moves_mul y).symm) (sum.inr (i, j))) = (x.move_right i) * y + x * y.move_right j - (x.move_right i) * y.move_right j
@[simp]
theorem pgame.mk_mul_move_right_inl {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xl} {j : yr} :
((pgame.mk xl xr xL xR) * pgame.mk yl yr yL yR).move_right (sum.inl (i, j)) = (xL i) * pgame.mk yl yr yL yR + (pgame.mk xl xr xL xR) * yR j - (xL i) * yR j
@[simp]
theorem pgame.mul_move_right_inl {x y : pgame} {i : x.left_moves} {j : y.right_moves} :
(x * y).move_right (((x.right_moves_mul y).symm) (sum.inl (i, j))) = (x.move_left i) * y + x * y.move_right j - (x.move_left i) * y.move_right j
@[simp]
theorem pgame.mk_mul_move_right_inr {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xr} {j : yl} :
((pgame.mk xl xr xL xR) * pgame.mk yl yr yL yR).move_right (sum.inr (i, j)) = (xR i) * pgame.mk yl yr yL yR + (pgame.mk xl xr xL xR) * yL j - (xR i) * yL j
@[simp]
theorem pgame.mul_move_right_inr {x y : pgame} {i : x.right_moves} {j : y.left_moves} :
(x * y).move_right (((x.right_moves_mul y).symm) (sum.inr (i, j))) = (x.move_right i) * y + x * y.move_left j - (x.move_right i) * y.move_left j
theorem pgame.quot_mul_comm (x y : pgame) :
x * y = y * x
theorem pgame.mul_comm_equiv (x y : pgame) :
(x * y).equiv (y * x)

x * y is equivalent to y * x.

x * 0 has exactly the same moves as 0.

Equations
theorem pgame.mul_zero_equiv (x : pgame) :
(x * 0).equiv 0

x * 0 is equivalent to 0.

@[simp]
theorem pgame.quot_mul_zero (x : pgame) :

0 * x has exactly the same moves as 0.

Equations
theorem pgame.zero_mul_equiv (x : pgame) :
(0 * x).equiv 0

0 * x is equivalent to 0.

@[simp]
theorem pgame.quot_zero_mul (x : pgame) :
@[simp]
theorem pgame.quot_neg_mul (x y : pgame) :
(-x) * y = -x * y
@[simp]
theorem pgame.quot_mul_neg (x y : pgame) :
@[simp]
theorem pgame.quot_left_distrib (x y z : pgame) :
x * (y + z) = x * y + x * z
theorem pgame.left_distrib_equiv (x y z : pgame) :
(x * (y + z)).equiv (x * y + x * z)

x * (y + z) is equivalent to x * y + x * z.

@[simp]
theorem pgame.quot_left_distrib_sub (x y z : pgame) :
x * (y - z) = x * y - x * z
@[simp]
theorem pgame.quot_right_distrib (x y z : pgame) :
(x + y) * z = x * z + y * z
theorem pgame.right_distrib_equiv (x y z : pgame) :
((x + y) * z).equiv (x * z + y * z)

(x + y) * z is equivalent to x * z + y * z.

@[simp]
theorem pgame.quot_right_distrib_sub (x y z : pgame) :
(y - z) * x = y * x - z * x
@[simp]
theorem pgame.quot_mul_one (x : pgame) :
theorem pgame.mul_one_equiv (x : pgame) :
(x * 1).equiv x

x * 1 is equivalent to x.

@[simp]
theorem pgame.quot_one_mul (x : pgame) :
theorem pgame.one_mul_equiv (x : pgame) :
(1 * x).equiv x

1 * x is equivalent to x.

theorem pgame.quot_mul_assoc (x y z : pgame) :
(x * y) * z = x * y * z
theorem pgame.mul_assoc_equiv (x y z : pgame) :
((x * y) * z).equiv (x * y * z)

x * y * z is equivalent to x * (y * z).

inductive pgame.inv_ty (l r : Type u) :
boolType u
• zero : Π {l r : Type u}, r ff
• left₁ : Π {l r : Type u}, r → r ff r ff
• left₂ : Π {l r : Type u}, l → r tt r ff
• right₁ : Π {l r : Type u}, l → r ff r tt
• right₂ : Π {l r : Type u}, r → r tt r tt

Because the two halves of the definition of inv produce more elements on each side, we have to define the two families inductively. This is the indexing set for the function, and inv_val is the function part.

def pgame.inv_val {l r : Type u_1} (L : l → pgame) (R : r → pgame) (IHl : l → pgame) (IHr : r → pgame) {b : bool} :
r bpgame

Because the two halves of the definition of inv produce more elements of each side, we have to define the two families inductively. This is the function part, defined by recursion on inv_ty.

Equations
• IHl IHr j) = (1 + (R i - r L R) * IHl IHr j) * IHr i
• IHl IHr j) = (1 + (L i - r L R) * IHl IHr j) * IHl i
• IHl IHr j) = (1 + (L i - r L R) * IHl IHr j) * IHl i
• IHl IHr j) = (1 + (R i - r L R) * IHl IHr j) * IHr i
• IHl IHr pgame.inv_ty.zero = 0
def pgame.inv'  :

The inverse of a positive surreal number x = {L | R} is given by x⁻¹ = {0, (1 + (R - x) * x⁻¹L) * R, (1 + (L - x) * x⁻¹R) * L | (1 + (L - x) * x⁻¹L) * L, (1 + (R - x) * x⁻¹R) * R}. Because the two halves x⁻¹L, x⁻¹R of x⁻¹ are used in their own definition, the sets and elements are inductively generated.

Equations
noncomputable def pgame.inv (x : pgame) :

The inverse of a surreal number in terms of the inverse on positive surreals.

Equations
@[protected, instance]
noncomputable def pgame.has_inv  :
Equations
@[protected, instance]
noncomputable def pgame.has_div  :
Equations