mathlib documentation

set_theory.pgame

Combinatorial (pre-)games.

The basic theory of combinatorial games, following Conway's book On Numbers and Games. We construct "pregames", define an ordering and arithmetic operations on them, then show that the operations descend to "games", defined via the equivalence relation p ≈ q ↔ p ≤ q ∧ q ≤ p.

The surreal numbers will be built as a quotient of a subtype of pregames.

A pregame (pgame below) is axiomatised via an inductive type, whose sole constructor takes two types (thought of as indexing the the possible moves for the players Left and Right), and a pair of functions out of these types to pgame (thought of as describing the resulting game after making a move).

Combinatorial games themselves, as a quotient of pregames, are constructed in game.lean.

Conway induction

By construction, the induction principle for pregames is exactly "Conway induction". That is, to prove some predicate pgame → Prop holds for all pregames, it suffices to prove that for every pregame g, if the predicate holds for every game resulting from making a move, then it also holds for g.

While it is often convenient to work "by induction" on pregames, in some situations this becomes awkward, so we also define accessor functions left_moves, right_moves, move_left and move_right. There is a relation subsequent p q, saying that p can be reached by playing some non-empty sequence of moves starting from q, an instance well_founded subsequent, and a local tactic pgame_wf_tac which is helpful for discharging proof obligations in inductive proofs relying on this relation.

Order properties

Pregames have both a and a < relation, which are related in quite a subtle way. In particular, it is worth noting that in Lean's (perhaps unfortunate?) definition of a preorder, we have lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a), but this is _not_ satisfied by the usual and < relations on pregames. (It is satisfied once we restrict to the surreal numbers.) In particular, < is not transitive; there is an example below showing 0 < star ∧ star < 0.

We do have

theorem not_le {x y : pgame} : ¬ x  y  y < x := ...
theorem not_lt {x y : pgame} : ¬ x < y  y  x := ...

The statement 0 ≤ x means that Left has a good response to any move by Right; in particular, the theorem zero_le below states

0  x   j : x.right_moves,  i : (x.move_right j).left_moves, 0  (x.move_right j).move_left i

On the other hand the statement 0 < x means that Left has a good move right now; in particular the theorem zero_lt below states

0 < x   i : left_moves x,  j : right_moves (x.move_left i), 0 < (x.move_left i).move_right j

The theorems le_def, lt_def, give a recursive characterisation of each relation, in terms of themselves two moves later. The theorems le_def_lt and lt_def_lt give recursive characterisations of each relation in terms of the other relation one move later.

We define an equivalence relation equiv p q ↔ p ≤ q ∧ q ≤ p. Later, games will be defined as the quotient by this relation.

Algebraic structures

We next turn to defining the operations necessary to make games into a commutative additive group. Addition is defined for $x = {xL | xR}$ and $y = {yL | yR}$ by $x + y = {xL + y, x + yL | xR + y, x + yR}$. Negation is defined by ${xL | xR} = {-xR | -xL}$.

The order structures interact in the expected way with addition, so we have

theorem le_iff_sub_nonneg {x y : pgame} : x  y  0  y - x := sorry
theorem lt_iff_sub_pos {x y : pgame} : x < y  0 < y - x := sorry

We show that these operations respect the equivalence relation, and hence descend to games. At the level of games, these operations satisfy all the laws of a commutative group. To prove the necessary equivalence relations at the level of pregames, we introduce the notion of a relabelling of a game, and show, for example, that there is a relabelling between x + (y + z) and (x + y) + z.

Future work

References

The material here is all drawn from

An interested reader may like to formalise some of the material from

inductive pgame  :
Type (u+1)

The type of pre-games, before we have quotiented by extensionality. 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 pre-game is built inductively from two families of pre-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.

Construct a pre-game from list of pre-games describing the available moves for Left and Right.

Equations
def pgame.left_moves  :
pgameType u

The indexing type for allowable moves by Left.

Equations
def pgame.right_moves  :
pgameType u

The indexing type for allowable moves by Right.

Equations
def pgame.move_left (g : pgame) :

The new game after Left makes an allowed move.

Equations

The new game after Right makes an allowed move.

Equations
@[simp]
theorem pgame.left_moves_mk {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} :
(pgame.mk xl xr xL xR).left_moves = xl

@[simp]
theorem pgame.move_left_mk {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {i : (pgame.mk xl xr xL xR).left_moves} :
(pgame.mk xl xr xL xR).move_left i = xL i

@[simp]
theorem pgame.right_moves_mk {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} :
(pgame.mk xl xr xL xR).right_moves = xr

@[simp]
theorem pgame.move_right_mk {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {j : (pgame.mk xl xr xL xR).right_moves} :
(pgame.mk xl xr xL xR).move_right j = xR j

inductive pgame.subsequent  :
pgamepgame → Prop

subsequent p q says that p can be obtained by playing some nonempty sequence of moves from q.

theorem pgame.subsequent.left_move {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {i : xl} :
(xL i).subsequent (pgame.mk xl xr xL xR)

A move by Left produces a subsequent game. (For use in pgame_wf_tac.)

theorem pgame.subsequent.right_move {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {j : xr} :
(xR j).subsequent (pgame.mk xl xr xL xR)

A move by Right produces a subsequent game. (For use in pgame_wf_tac.)

A local tactic for proving well-foundedness of recursive definitions involving pregames.

@[instance]

The pre-game zero is defined by 0 = { | }.

Equations
@[instance]

Equations
@[instance]

The pre-game one is defined by 1 = { 0 | }.

Equations
@[simp]

@[simp]

def pgame.le_lt  :
pgamepgameProp × Prop

Define simultaneously by mutual induction the <= and < relation on pre-games. The ZFC definition says that x = {xL | xR} is less or equal to y = {yL | yR} if ∀ x₁ ∈ xL, x₁ < y and ∀ y₂ ∈ yR, x < y₂, where x < y is the same as ¬ y <= x. This is a tricky induction because it only decreases one side at a time, and it also swaps the arguments in the definition of <. The solution is to define x < y and x <= y simultaneously.

Equations
@[instance]

Equations
@[instance]

Equations
@[simp]
theorem pgame.mk_le_mk {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yl yr : Type u_1} {yL : yl → pgame} {yR : yr → pgame} :
pgame.mk xl xr xL xR pgame.mk yl yr yL yR (∀ (i : xl), xL i < pgame.mk yl yr yL yR) ∀ (j : yr), pgame.mk xl xr xL xR < yR j

Definition of x ≤ y on pre-games built using the constructor.

theorem pgame.le_def_lt {x y : pgame} :
x y (∀ (i : x.left_moves), x.move_left i < y) ∀ (j : y.right_moves), x < y.move_right j

Definition of x ≤ y on pre-games, in terms of <

@[simp]
theorem pgame.mk_lt_mk {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yl yr : Type u_1} {yL : yl → pgame} {yR : yr → pgame} :
pgame.mk xl xr xL xR < pgame.mk yl yr yL yR (∃ (i : yl), pgame.mk xl xr xL xR yL i) ∃ (j : xr), xR j pgame.mk yl yr yL yR

Definition of x < y on pre-games built using the constructor.

theorem pgame.lt_def_le {x y : pgame} :
x < y (∃ (i : y.left_moves), x y.move_left i) ∃ (j : x.right_moves), x.move_right j y

Definition of x < y on pre-games, in terms of

theorem pgame.le_def {x y : pgame} :
x y (∀ (i : x.left_moves), (∃ (i' : y.left_moves), x.move_left i y.move_left i') ∃ (j : (x.move_left i).right_moves), (x.move_left i).move_right j y) ∀ (j : y.right_moves), (∃ (i : (y.move_right j).left_moves), x (y.move_right j).move_left i) ∃ (j' : x.right_moves), x.move_right j' y.move_right j

The definition of x ≤ y on pre-games, in terms of two moves later.

theorem pgame.lt_def {x y : pgame} :
x < y (∃ (i : y.left_moves), (∀ (i' : x.left_moves), x.move_left i' < y.move_left i) ∀ (j : (y.move_left i).right_moves), x < (y.move_left i).move_right j) ∃ (j : x.right_moves), (∀ (i : (x.move_right j).left_moves), (x.move_right j).move_left i < y) ∀ (j' : y.right_moves), x.move_right j < y.move_right j'

The definition of x < y on pre-games, in terms of < two moves later.

theorem pgame.le_zero {x : pgame} :
x 0 ∀ (i : x.left_moves), ∃ (j : (x.move_left i).right_moves), (x.move_left i).move_right j 0

The definition of x ≤ 0 on pre-games, in terms of ≤ 0 two moves later.

theorem pgame.zero_le {x : pgame} :
0 x ∀ (j : x.right_moves), ∃ (i : (x.move_right j).left_moves), 0 (x.move_right j).move_left i

The definition of 0 ≤ x on pre-games, in terms of 0 ≤ two moves later.

theorem pgame.lt_zero {x : pgame} :
x < 0 ∃ (j : x.right_moves), ∀ (i : (x.move_right j).left_moves), (x.move_right j).move_left i < 0

The definition of x < 0 on pre-games, in terms of < 0 two moves later.

theorem pgame.zero_lt {x : pgame} :
0 < x ∃ (i : x.left_moves), ∀ (j : (x.move_left i).right_moves), 0 < (x.move_left i).move_right j

The definition of 0 < x on pre-games, in terms of < x two moves later.

def pgame.right_response {x : pgame} (h : x 0) (i : x.left_moves) :

Given a right-player-wins game, provide a response to any move by left.

Equations
theorem pgame.right_response_spec {x : pgame} (h : x 0) (i : x.left_moves) :

Show that the response for right provided by right_response preserves the right-player-wins condition.

def pgame.left_response {x : pgame} (h : 0 x) (j : x.right_moves) :

Given a left-player-wins game, provide a response to any move by right.

Equations
theorem pgame.left_response_spec {x : pgame} (h : 0 x) (j : x.right_moves) :

Show that the response for left provided by left_response preserves the left-player-wins condition.

theorem pgame.lt_of_le_mk {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {y : pgame} {i : xl} :
pgame.mk xl xr xL xR yxL i < y

theorem pgame.lt_of_mk_le {x : pgame} {yl yr : Type u_1} {yL : yl → pgame} {yR : yr → pgame} {i : yr} :
x pgame.mk yl yr yL yRx < yR i

theorem pgame.mk_lt_of_le {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {y : pgame} {i : xr} :
xR i ypgame.mk xl xr xL xR < y

theorem pgame.lt_mk_of_le {x : pgame} {yl yr : Type u_1} {yL : yl → pgame} {yR : yr → pgame} {i : yl} :
x yL ix < pgame.mk yl yr yL yR

theorem pgame.not_le_lt {x y : pgame} :
(¬x y y < x) (¬x < y y x)

theorem pgame.not_le {x y : pgame} :
¬x y y < x

theorem pgame.not_lt {x y : pgame} :
¬x < y y x

theorem pgame.le_refl (x : pgame) :
x x

theorem pgame.lt_irrefl (x : pgame) :
¬x < x

theorem pgame.ne_of_lt {x y : pgame} :
x < yx y

theorem pgame.le_trans_aux {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yl yr : Type u_1} {yL : yl → pgame} {yR : yr → pgame} {zl zr : Type u_1} {zL : zl → pgame} {zR : zr → pgame} :
(∀ (i : xl), pgame.mk yl yr yL yR pgame.mk zl zr zL zRpgame.mk zl zr zL zR xL ipgame.mk yl yr yL yR xL i)(∀ (i : zr), zR i pgame.mk xl xr xL xRpgame.mk xl xr xL xR pgame.mk yl yr yL yRzR i pgame.mk yl yr yL yR)pgame.mk xl xr xL xR pgame.mk yl yr yL yRpgame.mk yl yr yL yR pgame.mk zl zr zL zRpgame.mk xl xr xL xR pgame.mk zl zr zL zR

theorem pgame.le_trans {x y z : pgame} :
x yy zx z

theorem pgame.lt_of_le_of_lt {x y z : pgame} :
x yy < zx < z

theorem pgame.lt_of_lt_of_le {x y z : pgame} :
x < yy zx < z

def pgame.equiv  :
pgamepgame → Prop

Define the equivalence relation on pre-games. Two pre-games x, y are equivalent if x ≤ y and y ≤ x.

Equations
theorem pgame.equiv_refl (x : pgame) :
x.equiv x

theorem pgame.equiv_symm {x y : pgame} :
x.equiv yy.equiv x

theorem pgame.equiv_trans {x y z : pgame} :
x.equiv yy.equiv zx.equiv z

theorem pgame.lt_of_lt_of_equiv {x y z : pgame} :
x < yy.equiv zx < z

theorem pgame.le_of_le_of_equiv {x y z : pgame} :
x yy.equiv zx z

theorem pgame.lt_of_equiv_of_lt {x y z : pgame} :
x.equiv yy < zx < z

theorem pgame.le_of_equiv_of_le {x y z : pgame} :
x.equiv yy zx z

theorem pgame.le_congr {x₁ y₁ x₂ y₂ : pgame} :
x₁.equiv x₂y₁.equiv y₂(x₁ y₁ x₂ y₂)

theorem pgame.lt_congr {x₁ y₁ x₂ y₂ : pgame} :
x₁.equiv x₂y₁.equiv y₂(x₁ < y₁ x₂ < y₂)

theorem pgame.equiv_congr_left {y₁ y₂ : pgame} :
y₁.equiv y₂ ∀ (x₁ : pgame), x₁.equiv y₁ x₁.equiv y₂

theorem pgame.equiv_congr_right {x₁ x₂ : pgame} :
x₁.equiv x₂ ∀ (y₁ : pgame), x₁.equiv y₁ x₂.equiv y₁

inductive pgame.restricted  :
pgamepgameType (u+1)

restricted x y says that Left always has no more moves in x than in y, and Right always has no more moves in y than in x

The identity restriction.

Equations
theorem pgame.le_of_restricted {x y : pgame} :
x.restricted yx y

inductive pgame.relabelling  :
pgamepgameType (u+1)

relabelling x y says that x and y are really the same game, just dressed up differently. Specifically, there is a bijection between the moves for Left in x and in y, and similarly for Right, and under these bijections we inductively have relabellings for the consequent games.

If x is a relabelling of y, then Left and Right have the same moves in either game, so x is a restriction of y.

Equations

The identity relabelling.

Equations

Reverse a relabelling.

Equations
def pgame.relabelling.trans {x y z : pgame} :
x.relabelling yy.relabelling zx.relabelling z

Transitivity of relabelling

Equations
theorem pgame.le_of_relabelling {x y : pgame} :
x.relabelling yx y

theorem pgame.equiv_of_relabelling {x y : pgame} :
x.relabelling yx.equiv y

A relabelling lets us prove equivalence of games.

@[instance]
def pgame.has_coe {x y : pgame} :

Equations
def pgame.relabel {x : pgame} {xl' xr' : Type u_1} :
x.left_moves xl'x.right_moves xr'pgame

Replace the types indexing the next moves for Left and Right by equivalent types.

Equations
@[simp]
theorem pgame.relabel_move_left' {x : pgame} {xl' xr' : Type u_1} (el : x.left_moves xl') (er : x.right_moves xr') (i : xl') :

@[simp]
theorem pgame.relabel_move_left {x : pgame} {xl' xr' : Type u_1} (el : x.left_moves xl') (er : x.right_moves xr') (i : x.left_moves) :

@[simp]
theorem pgame.relabel_move_right' {x : pgame} {xl' xr' : Type u_1} (el : x.left_moves xl') (er : x.right_moves xr') (j : xr') :

@[simp]
theorem pgame.relabel_move_right {x : pgame} {xl' xr' : Type u_1} (el : x.left_moves xl') (er : x.right_moves xr') (j : x.right_moves) :

def pgame.relabel_relabelling {x : pgame} {xl' xr' : Type u_1} (el : x.left_moves xl') (er : x.right_moves xr') :

The game obtained by relabelling the next moves is a relabelling of the original game.

Equations
def pgame.neg  :

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

Equations
@[instance]

Equations
@[simp]
theorem pgame.neg_def {xl xr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} :
-pgame.mk xl xr xL xR = pgame.mk xr xl (λ (j : xr), -xR j) (λ (i : xl), -xL i)

@[simp]
theorem pgame.neg_neg {x : pgame} :
--x = x

@[simp]
theorem pgame.neg_zero  :
-0 = 0

An explicit equivalence between the moves for Left in -x and the moves for Right in x.

Equations

An explicit equivalence between the moves for Right in -x and the moves for Left in x.

Equations
theorem pgame.le_iff_neg_ge {x y : pgame} :
x y -y -x

theorem pgame.neg_congr {x y : pgame} :
x.equiv y(-x).equiv (-y)

theorem pgame.lt_iff_neg_gt {x y : pgame} :
x < y -y < -x

def pgame.add  :
pgamepgamepgame

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

Equations
  • x.add y = pgame.rec (λ (xl xr : Type u_1) (xL : xl → pgame) (xR : xr → pgame) (IHxl : Π (a : xl), (λ (x : pgame), pgamepgame) (xL a)) (IHxr : Π (a : xr), (λ (x : pgame), pgamepgame) (xR a)) (y : pgame), pgame.rec (λ (yl yr : Type u_2) (yL : yl → pgame) (yR : yr → pgame) (IHyl : Π (a : yl), (λ (y : pgame), pgame) (yL a)) (IHyr : Π (a : yr), (λ (y : pgame), pgame) (yR a)), pgame.mk (xl yl) (xr yr) (sum.rec (λ (i : xl), IHxl i (pgame.mk yl yr yL yR)) (λ (i : yl), IHyl i)) (sum.rec (λ (i : xr), IHxr i (pgame.mk yl yr yL yR)) (λ (i : yr), IHyr i))) y) x y
@[instance]

Equations

x + 0 has exactly the same moves as x.

Equations
theorem pgame.add_zero_equiv (x : pgame) :
(x + 0).equiv x

x + 0 is equivalent to x.

0 + x has exactly the same moves as x.

Equations
theorem pgame.zero_add_equiv (x : pgame) :
(0 + x).equiv x

0 + x is equivalent to x.

An explicit equivalence between the moves for Left in x + y and the type-theory sum of the moves for Left in x and in y.

Equations

An explicit equivalence between the moves for Right in x + y and the type-theory sum of the moves for Right in x and in y.

Equations
@[simp]
theorem pgame.mk_add_move_left_inl {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xl} :
(pgame.mk xl xr xL xR + pgame.mk yl yr yL yR).move_left (sum.inl i) = (pgame.mk xl xr xL xR).move_left i + pgame.mk yl yr yL yR

@[simp]
theorem pgame.add_move_left_inl {x y : pgame} {i : x.left_moves} :
(x + y).move_left (((x.left_moves_add y).symm) (sum.inl i)) = x.move_left i + y

@[simp]
theorem pgame.mk_add_move_right_inl {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xr} :
(pgame.mk xl xr xL xR + pgame.mk yl yr yL yR).move_right (sum.inl i) = (pgame.mk xl xr xL xR).move_right i + pgame.mk yl yr yL yR

@[simp]
theorem pgame.add_move_right_inl {x y : pgame} {i : x.right_moves} :

@[simp]
theorem pgame.mk_add_move_left_inr {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : yl} :
(pgame.mk xl xr xL xR + pgame.mk yl yr yL yR).move_left (sum.inr i) = pgame.mk xl xr xL xR + (pgame.mk yl yr yL yR).move_left i

@[simp]
theorem pgame.add_move_left_inr {x y : pgame} {i : y.left_moves} :
(x + y).move_left (((x.left_moves_add y).symm) (sum.inr i)) = x + y.move_left i

@[simp]
theorem pgame.mk_add_move_right_inr {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : yr} :
(pgame.mk xl xr xL xR + pgame.mk yl yr yL yR).move_right (sum.inr i) = pgame.mk xl xr xL xR + (pgame.mk yl yr yL yR).move_right i

@[simp]
theorem pgame.add_move_right_inr {x y : pgame} {i : y.right_moves} :

@[instance]

Equations
def pgame.neg_add_relabelling (x y : pgame) :
(-(x + y)).relabelling (-x + -y)

-(x+y) has exactly the same moves as -x + -y.

Equations
theorem pgame.neg_add_le {x y : pgame} :
-(x + y) -x + -y

def pgame.add_comm_relabelling (x y : pgame) :
(x + y).relabelling (y + x)

x+y has exactly the same moves as y+x.

Equations
theorem pgame.add_comm_le {x y : pgame} :
x + y y + x

theorem pgame.add_comm_equiv {x y : pgame} :
(x + y).equiv (y + x)

def pgame.add_assoc_relabelling (x y z : pgame) :
(x + y + z).relabelling (x + (y + z))

(x + y) + z has exactly the same moves as x + (y + z).

Equations
theorem pgame.add_assoc_equiv {x y z : pgame} :
(x + y + z).equiv (x + (y + z))

theorem pgame.add_le_add_right {x y z : pgame} :
x yx + z y + z

theorem pgame.add_le_add_left {x y z : pgame} :
y zx + y x + z

theorem pgame.add_congr {w x y z : pgame} :
w.equiv xy.equiv z(w + y).equiv (x + z)

theorem pgame.add_left_neg_le_zero {x : pgame} :
-x + x 0

theorem pgame.zero_le_add_left_neg {x : pgame} :
0 -x + x

theorem pgame.add_left_neg_equiv {x : pgame} :
(-x + x).equiv 0

theorem pgame.add_right_neg_le_zero {x : pgame} :
x + -x 0

theorem pgame.zero_le_add_right_neg {x : pgame} :
0 x + -x

theorem pgame.add_lt_add_right {x y z : pgame} :
x < yx + z < y + z

theorem pgame.add_lt_add_left {x y z : pgame} :
y < zx + y < x + z

theorem pgame.le_iff_sub_nonneg {x y : pgame} :
x y 0 y - x

theorem pgame.lt_iff_sub_pos {x y : pgame} :
x < y 0 < y - x

def pgame.star  :

The pre-game star, which is fuzzy/confused with zero.

Equations
def pgame.omega  :

The pre-game ω. (In fact all ordinals have game and surreal representatives.)

Equations