mathlib documentation

set_theory.game.basic

Combinatorial games. #

In this file we define the quotient of pre-games by the equivalence relation p ≈ q ↔ p ≤ q ∧ q ≤ p (its antisymmetrization), and construct an instance add_comm_group game, as well as an instance partial_order game.

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 ≈ y does not imply x * z ≈ 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.

@[protected, instance]
Equations
  • game.add_comm_group_with_one = {add := quotient.lift₂ (λ (x y : pgame), x + y) game.add_comm_group_with_one._proof_1, add_assoc := game.add_comm_group_with_one._proof_2, zero := 0, zero_add := game.add_comm_group_with_one._proof_3, add_zero := game.add_comm_group_with_one._proof_4, nsmul := add_comm_group.nsmul._default 0 (quotient.lift₂ (λ (x y : pgame), x + y) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_5 game.add_comm_group_with_one._proof_6, nsmul_zero' := game.add_comm_group_with_one._proof_7, nsmul_succ' := game.add_comm_group_with_one._proof_8, neg := quot.lift (λ (x : pgame), -x) game.add_comm_group_with_one._proof_9, sub := add_comm_group.sub._default (quotient.lift₂ (λ (x y : pgame), x + y) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_10 0 game.add_comm_group_with_one._proof_11 game.add_comm_group_with_one._proof_12 (add_comm_group.nsmul._default 0 (quotient.lift₂ (λ (x y : pgame), x + y) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_5 game.add_comm_group_with_one._proof_6) game.add_comm_group_with_one._proof_13 game.add_comm_group_with_one._proof_14 (quot.lift (λ (x : pgame), -x) game.add_comm_group_with_one._proof_9), sub_eq_add_neg := game.add_comm_group_with_one._proof_15, zsmul := add_comm_group.zsmul._default (quotient.lift₂ (λ (x y : pgame), x + y) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_16 0 game.add_comm_group_with_one._proof_17 game.add_comm_group_with_one._proof_18 (add_comm_group.nsmul._default 0 (quotient.lift₂ (λ (x y : pgame), x + y) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_5 game.add_comm_group_with_one._proof_6) game.add_comm_group_with_one._proof_19 game.add_comm_group_with_one._proof_20 (quot.lift (λ (x : pgame), -x) game.add_comm_group_with_one._proof_9), zsmul_zero' := game.add_comm_group_with_one._proof_21, zsmul_succ' := game.add_comm_group_with_one._proof_22, zsmul_neg' := game.add_comm_group_with_one._proof_23, add_left_neg := game.add_comm_group_with_one._proof_24, add_comm := game.add_comm_group_with_one._proof_25, int_cast := add_group_with_one.int_cast._default (add_group_with_one.nat_cast._default 1 (quotient.lift₂ (λ (x y : pgame), x + y) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_26 0 game.add_comm_group_with_one._proof_27 game.add_comm_group_with_one._proof_28 (add_comm_group.nsmul._default 0 (quotient.lift₂ (λ (x y : pgame), x + y) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_5 game.add_comm_group_with_one._proof_6) game.add_comm_group_with_one._proof_29 game.add_comm_group_with_one._proof_30) (quotient.lift₂ (λ (x y : pgame), x + y) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_31 0 game.add_comm_group_with_one._proof_32 game.add_comm_group_with_one._proof_33 (add_comm_group.nsmul._default 0 (quotient.lift₂ (λ (x y : pgame), x + y) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_5 game.add_comm_group_with_one._proof_6) game.add_comm_group_with_one._proof_34 game.add_comm_group_with_one._proof_35 1 game.add_comm_group_with_one._proof_36 game.add_comm_group_with_one._proof_37 (quot.lift (λ (x : pgame), -x) game.add_comm_group_with_one._proof_9) (add_comm_group.sub._default (quotient.lift₂ (λ (x y : pgame), x + y) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_10 0 game.add_comm_group_with_one._proof_11 game.add_comm_group_with_one._proof_12 (add_comm_group.nsmul._default 0 (quotient.lift₂ (λ (x y : pgame), x + y) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_5 game.add_comm_group_with_one._proof_6) game.add_comm_group_with_one._proof_13 game.add_comm_group_with_one._proof_14 (quot.lift (λ (x : pgame), -x) game.add_comm_group_with_one._proof_9)) game.add_comm_group_with_one._proof_38 (add_comm_group.zsmul._default (quotient.lift₂ (λ (x y : pgame), x + y) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_16 0 game.add_comm_group_with_one._proof_17 game.add_comm_group_with_one._proof_18 (add_comm_group.nsmul._default 0 (quotient.lift₂ (λ (x y : pgame), x + y) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_5 game.add_comm_group_with_one._proof_6) game.add_comm_group_with_one._proof_19 game.add_comm_group_with_one._proof_20 (quot.lift (λ (x : pgame), -x) game.add_comm_group_with_one._proof_9)) game.add_comm_group_with_one._proof_39 game.add_comm_group_with_one._proof_40 game.add_comm_group_with_one._proof_41 game.add_comm_group_with_one._proof_42, nat_cast := add_group_with_one.nat_cast._default 1 (quotient.lift₂ (λ (x y : pgame), x + y) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_26 0 game.add_comm_group_with_one._proof_27 game.add_comm_group_with_one._proof_28 (add_comm_group.nsmul._default 0 (quotient.lift₂ (λ (x y : pgame), x + y) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_5 game.add_comm_group_with_one._proof_6) game.add_comm_group_with_one._proof_29 game.add_comm_group_with_one._proof_30, one := 1, nat_cast_zero := game.add_comm_group_with_one._proof_43, nat_cast_succ := game.add_comm_group_with_one._proof_44, int_cast_of_nat := game.add_comm_group_with_one._proof_45, int_cast_neg_succ_of_nat := game.add_comm_group_with_one._proof_46}
@[protected, instance]
Equations
@[protected, instance]
Equations
def game.lf  :
gamegame → Prop

The less or fuzzy relation on games.

If 0 ⧏ x (less or fuzzy with), then Left can win x as the first player.

Equations
Instances for game.lf
@[simp]
theorem game.not_le {x y : game} :
¬x y y.lf x

On game, simp-normal inequalities should use as few negations as possible.

@[simp]
theorem game.not_lf {x y : game} :
¬x.lf y y x

On game, simp-normal inequalities should use as few negations as possible.

@[protected, instance]

It can be useful to use these lemmas to turn pgame inequalities into game inequalities, as the add_comm_group structure on game often simplifies many proofs.

theorem pgame.lt_iff_game_lt {x y : pgame} :
def game.fuzzy  :
gamegame → Prop

The fuzzy, confused, or incomparable relation on games.

If x ∥ 0, then the first player can always win x.

Equations
theorem game.add_lf_add_right {b c : game} (h : b.lf c) (a : game) :
(b + a).lf (c + a)
theorem game.add_lf_add_left {b c : game} (h : b.lf c) (a : game) :
(a + b).lf (a + c)
@[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.

@[protected, instance]

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
  • pgame.has_mul = {mul := λ (x y : pgame), pgame.rec (λ (xl xr : Type u) (xL : xl → pgame) (xR : xr → pgame) (IHxl : Π (ᾰ : xl), (λ (x : pgame), pgamepgame) (xL ᾰ)) (IHxr : Π (ᾰ : xr), (λ (x : pgame), pgamepgame) (xR ᾰ)) (y : pgame), pgame.rec (λ (yl yr : Type u) (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}

Turns two left or right moves for x and y into a left move for x * y and vice versa.

Even though these types are the same (not definitionally so), this is the preferred way to convert between them.

Equations

Turns a left and a right move for x and y into a right move for x * y and vice versa.

Even though these types are the same (not definitionally so), this is the preferred way to convert between them.

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} :
@[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]
@[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]
@[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.left_moves_mul_cases {x y : pgame} (k : (x * y).left_moves) {P : (x * y).left_moves → Prop} (hl : ∀ (ix : x.left_moves) (iy : y.left_moves), P (pgame.to_left_moves_mul (sum.inl (ix, iy)))) (hr : ∀ (jx : x.right_moves) (jy : y.right_moves), P (pgame.to_left_moves_mul (sum.inr (jx, jy)))) :
P k
theorem pgame.right_moves_mul_cases {x y : pgame} (k : (x * y).right_moves) {P : (x * y).right_moves → Prop} (hl : ∀ (ix : x.left_moves) (jy : y.right_moves), P (pgame.to_right_moves_mul (sum.inl (ix, jy)))) (hr : ∀ (jx : x.right_moves) (iy : y.left_moves), P (pgame.to_right_moves_mul (sum.inr (jx, iy)))) :
P k
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.

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]

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) :
@[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

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.

Instances for pgame.inv_ty
@[protected, instance]
def pgame.inv_ty.is_empty (l r : Type u) [is_empty l] [is_empty r] :
@[protected, instance]
Equations
@[protected, instance]
def pgame.unique_inv_ty (l r : Type u) [is_empty l] [is_empty r] :
Equations
def pgame.inv_val {l r : Type u_1} (L : l → pgame) (R : r → pgame) (IHl : l → pgame) (IHr : r → pgame) {b : bool} :

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
@[simp]
theorem pgame.inv_val_is_empty {l r : Type u} {b : bool} (L : l → pgame) (R : r → pgame) (IHl : l → pgame) (IHr : r → pgame) (i : pgame.inv_ty l r b) [is_empty l] [is_empty r] :
pgame.inv_val L R IHl IHr i = 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
theorem pgame.zero_lf_inv' (x : pgame) :
0.lf x.inv'

inv' 0 has exactly the same moves as 1.

Equations

inv' 1 has exactly the same moves as 1.

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

The inverse of a pre-game in terms of the inverse on positive pre-games.

Equations
@[protected, instance]
noncomputable def pgame.has_div  :
Equations
theorem pgame.inv_eq_of_equiv_zero {x : pgame} (h : x.equiv 0) :
x⁻¹ = 0
@[simp]
theorem pgame.inv_zero  :
0⁻¹ = 0
theorem pgame.inv_eq_of_pos {x : pgame} (h : 0 < x) :
theorem pgame.inv_eq_of_lf_zero {x : pgame} (h : x.lf 0) :

1⁻¹ has exactly the same moves as 1.

Equations