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 #
- The theory of dominated and reversible positions, and unique normal form for short games.
- Analysis of basic domineering positions.
- Hex.
- Temperature.
- The development of surreal numbers, based on this development of combinatorial games, is still quite incomplete.
References #
The material here is all drawn from
An interested reader may like to formalise some of the material from
- Andreas Blass, A game semantics for linear logic
- [André Joyal, Remarques sur la théorie des jeux à deux personnes][joyal1997]
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.
The indexing type for allowable moves by Left.
Equations
- (pgame.mk l _x _x_1 _x_2).left_moves = l
The indexing type for allowable moves by Right.
Equations
- (pgame.mk _x r _x_1 _x_2).right_moves = r
The new game after Left makes an allowed move.
The new game after Right makes an allowed move.
Equations
- (pgame.mk _x r _x_1 R).move_right j = R j
- left : ∀ (x : pgame) (i : x.left_moves), (x.move_left i).subsequent x
- right : ∀ (x : pgame) (j : x.right_moves), (x.move_right j).subsequent x
- trans : ∀ (x y z : pgame), x.subsequent y → y.subsequent z → x.subsequent z
subsequent p q
says that p
can be obtained by playing
some nonempty sequence of moves from q
.
Equations
A move by Left produces a subsequent game. (For use in pgame_wf_tac.)
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.
The pre-game zero
is defined by 0 = { | }
.
Equations
Equations
- pgame.inhabited = {default := 0}
The pre-game one
is defined by 1 = { 0 | }
.
Equations
- pgame.has_one = {one := pgame.mk punit pempty (λ (_x : punit), 0) pempty.elim}
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.
Definition of x ≤ y
on pre-games built using the constructor.
Definition of x ≤ y
on pre-games, in terms of <
Definition of x < y
on pre-games built using the constructor.
Definition of x < y
on pre-games, in terms of ≤
The definition of x ≤ y
on pre-games, in terms of ≤
two moves later.
The definition of x < y
on pre-games, in terms of <
two moves later.
The definition of x ≤ 0
on pre-games, in terms of ≤ 0
two moves later.
The definition of 0 ≤ x
on pre-games, in terms of 0 ≤
two moves later.
The definition of x < 0
on pre-games, in terms of < 0
two moves later.
The definition of 0 < x
on pre-games, in terms of < x
two moves later.
Given a right-player-wins game, provide a response to any move by left.
Equations
Show that the response for right provided by right_response
preserves the right-player-wins condition.
Given a left-player-wins game, provide a response to any move by right.
Equations
Show that the response for left provided by left_response
preserves the left-player-wins condition.
- mk : Π {x y : pgame} (L : x.left_moves → y.left_moves) (R : y.right_moves → x.right_moves), (Π (i : x.left_moves), (x.move_left i).restricted (y.move_left (L i))) → (Π (j : y.right_moves), (x.move_right (R j)).restricted (y.move_right j)) → x.restricted y
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
- pgame.restricted.refl (pgame.mk xl xr xL xR) = pgame.restricted.mk id id (λ (i : (pgame.mk xl xr xL xR).left_moves), pgame.restricted.refl ((pgame.mk xl xr xL xR).move_left i)) (λ (j : (pgame.mk xl xr xL xR).right_moves), pgame.restricted.refl ((pgame.mk xl xr xL xR).move_right (id j)))
- mk : Π {x y : pgame} (L : x.left_moves ≃ y.left_moves) (R : x.right_moves ≃ y.right_moves), (Π (i : x.left_moves), (x.move_left i).relabelling (y.move_left (⇑L i))) → (Π (j : y.right_moves), (x.move_right (⇑(R.symm) j)).relabelling (y.move_right j)) → x.relabelling y
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 relabelling
s 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
- (pgame.relabelling.mk L_equiv R_equiv L_relabelling R_relabelling).restricted = pgame.restricted.mk ⇑(L_equiv.to_embedding) ⇑(R_equiv.symm.to_embedding) (λ (i : (pgame.mk xl xr xL xR).left_moves), (L_relabelling i).restricted) (λ (j : (pgame.mk yl yr yL yR).right_moves), (R_relabelling j).restricted)
The identity relabelling.
Equations
- pgame.relabelling.refl (pgame.mk xl xr xL xR) = pgame.relabelling.mk (equiv.refl (pgame.mk xl xr xL xR).left_moves) (equiv.refl (pgame.mk xl xr xL xR).right_moves) (λ (i : (pgame.mk xl xr xL xR).left_moves), pgame.relabelling.refl ((pgame.mk xl xr xL xR).move_left i)) (λ (j : (pgame.mk xl xr xL xR).right_moves), pgame.relabelling.refl ((pgame.mk xl xr xL xR).move_right (⇑((equiv.refl (pgame.mk xl xr xL xR).right_moves).symm) j)))
Reverse a relabelling.
Equations
- (pgame.relabelling.mk L_equiv R_equiv L_relabelling R_relabelling).symm = pgame.relabelling.mk L_equiv.symm R_equiv.symm (λ (i : (pgame.mk yl yr yL yR).left_moves), _.mpr (_.mp (L_relabelling (⇑(L_equiv.symm) i)).symm)) (λ (j : (pgame.mk xl xr xL xR).right_moves), _.mpr (_.mp (R_relabelling (⇑R_equiv j)).symm))
Transitivity of relabelling
Equations
- (pgame.relabelling.mk L_equiv₁ R_equiv₁ L_relabelling₁ R_relabelling₁).trans (pgame.relabelling.mk L_equiv₂ R_equiv₂ L_relabelling₂ R_relabelling₂) = pgame.relabelling.mk (L_equiv₁.trans L_equiv₂) (R_equiv₁.trans R_equiv₂) (λ (i : (pgame.mk xl xr xL xR).left_moves), _.mpr (_.mp ((L_relabelling₁ i).trans (L_relabelling₂ (⇑L_equiv₁ i))))) (λ (j : (pgame.mk zl zr zL zR).right_moves), _.mpr (_.mp ((R_relabelling₁ (⇑(R_equiv₂.symm) j)).trans (R_relabelling₂ j))))
A relabelling lets us prove equivalence of games.
Equations
- pgame.equiv.has_coe = {coe := _}
Replace the types indexing the next moves for Left and Right by equivalent types.
Equations
- pgame.relabel el er = pgame.mk xl' xr' (λ (i : xl'), x.move_left (⇑(el.symm) i)) (λ (j : xr'), x.move_right (⇑(er.symm) j))
The game obtained by relabelling the next moves is a relabelling of the original game.
Equations
- pgame.relabel_relabelling el er = pgame.relabelling.mk el er (λ (i : x.left_moves), _.mpr (pgame.relabelling.refl (x.move_left i))) (λ (j : (pgame.relabel el er).right_moves), _.mpr (pgame.relabelling.refl (x.move_right (⇑(er.symm) j))))
Equations
- pgame.has_neg = {neg := pgame.neg}
An explicit equivalence between the moves for Left in -x
and the moves for Right in x
.
Equations
- x.left_moves_neg = x.cases_on (λ (x_α x_β : Type u_1) (x_ᾰ : x_α → pgame) (x_ᾰ_1 : x_β → pgame), equiv.refl (-pgame.mk x_α x_β x_ᾰ x_ᾰ_1).left_moves)
An explicit equivalence between the moves for Right in -x
and the moves for Left in x
.
Equations
- x.right_moves_neg = x.cases_on (λ (x_α x_β : Type u_1) (x_ᾰ : x_α → pgame) (x_ᾰ_1 : x_β → pgame), equiv.refl (-pgame.mk x_α x_β x_ᾰ x_ᾰ_1).right_moves)
If x
has the same moves as y
, then -x
has the sames moves as -y
.
Equations
- (pgame.relabelling.mk L_equiv R_equiv L_relabelling R_relabelling).neg_congr = pgame.relabelling.mk R_equiv L_equiv (λ (i : (-pgame.mk xl xr xL xR).left_moves), (_.mpr (_.mp (R_relabelling (⇑R_equiv i)))).neg_congr) (λ (i : (-pgame.mk yl yr yL yR).right_moves), (_.mpr (_.mp (L_relabelling (⇑(L_equiv.symm) i)))).neg_congr)
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 : Π (ᾰ : xl), (λ (x : pgame), pgame → pgame) (xL ᾰ)) (IHxr : Π (ᾰ : xr), (λ (x : pgame), pgame → 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) (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
Equations
- pgame.has_add = {add := pgame.add}
x + 0
has exactly the same moves as x
.
Equations
- (pgame.mk xl xr xL xR).add_zero_relabelling = pgame.relabelling.mk (equiv.sum_pempty xl) (equiv.sum_pempty xr) (λ (i : (pgame.mk xl xr xL xR + 0).left_moves), sum.cases_on i (λ (i : xl), (xL i).add_zero_relabelling) (λ (i : pempty), pempty.cases_on (λ (i : pempty), ((pgame.mk xl xr xL xR + 0).move_left (sum.inr i)).relabelling ((pgame.mk xl xr xL xR).move_left (⇑(equiv.sum_pempty xl) (sum.inr i)))) i)) (λ (j : (pgame.mk xl xr xL xR).right_moves), (xR j).add_zero_relabelling)
0 + x
has exactly the same moves as x
.
Equations
- (pgame.mk xl xr xL xR).zero_add_relabelling = pgame.relabelling.mk (equiv.pempty_sum xl) (equiv.pempty_sum xr) (λ (i : (0 + pgame.mk xl xr xL xR).left_moves), sum.cases_on i (λ (i : pempty), pempty.cases_on (λ (i : pempty), ((0 + pgame.mk xl xr xL xR).move_left (sum.inl i)).relabelling ((pgame.mk xl xr xL xR).move_left (⇑(equiv.pempty_sum xl) (sum.inl i)))) i) (λ (i : xl), (xL i).zero_add_relabelling)) (λ (j : (pgame.mk xl xr xL xR).right_moves), (xR j).zero_add_relabelling)
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
- x.left_moves_add y = x.cases_on (λ (x_α x_β : Type u_1) (x_ᾰ : x_α → pgame) (x_ᾰ_1 : x_β → pgame), y.cases_on (λ (y_α y_β : Type u_1) (y_ᾰ : y_α → pgame) (y_ᾰ_1 : y_β → pgame), equiv.refl (pgame.mk x_α x_β x_ᾰ x_ᾰ_1 + pgame.mk y_α y_β y_ᾰ y_ᾰ_1).left_moves))
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
- x.right_moves_add y = x.cases_on (λ (x_α x_β : Type u_1) (x_ᾰ : x_α → pgame) (x_ᾰ_1 : x_β → pgame), y.cases_on (λ (y_α y_β : Type u_1) (y_ᾰ : y_α → pgame) (y_ᾰ_1 : y_β → pgame), equiv.refl (pgame.mk x_α x_β x_ᾰ x_ᾰ_1 + pgame.mk y_α y_β y_ᾰ y_ᾰ_1).right_moves))
If w
has the same moves as x
and y
has the same moves as z
,
then w + y
has the same moves as x + z
.
Equations
- (pgame.relabelling.mk L_equiv₁ R_equiv₁ L_relabelling₁ R_relabelling₁).add_congr (pgame.relabelling.mk L_equiv₂ R_equiv₂ L_relabelling₂ R_relabelling₂) = pgame.relabelling.mk (L_equiv₁.sum_congr L_equiv₂) (R_equiv₁.sum_congr R_equiv₂) (λ (i : (pgame.mk wl wr wL wR + pgame.mk yl yr yL yR).left_moves), sum.cases_on i (λ (i : wl), (L_relabelling₁ i).add_congr (pgame.relabelling.mk L_equiv₂ R_equiv₂ L_relabelling₂ R_relabelling₂)) (λ (j : yl), (pgame.relabelling.mk L_equiv₁ R_equiv₁ L_relabelling₁ R_relabelling₁).add_congr (L_relabelling₂ j))) (λ (j : (pgame.mk xl xr xL xR + pgame.mk zl zr zL zR).right_moves), sum.cases_on j (λ (i : xr), (R_relabelling₁ i).add_congr (pgame.relabelling.mk L_equiv₂ R_equiv₂ L_relabelling₂ R_relabelling₂)) (λ (j : zr), (pgame.relabelling.mk L_equiv₁ R_equiv₁ L_relabelling₁ R_relabelling₁).add_congr (R_relabelling₂ j)))
If w
has the same moves as x
and y
has the same moves as z
,
then w - y
has the same moves as x - z
.
-(x+y)
has exactly the same moves as -x + -y
.
Equations
- (pgame.mk xl xr xL xR).neg_add_relabelling (pgame.mk yl yr yL yR) = pgame.relabelling.mk (equiv.refl (-(pgame.mk xl xr xL xR + pgame.mk yl yr yL yR)).left_moves) (equiv.refl (-(pgame.mk xl xr xL xR + pgame.mk yl yr yL yR)).right_moves) (λ (j : (-(pgame.mk xl xr xL xR + pgame.mk yl yr yL yR)).left_moves), sum.cases_on j (λ (j : xr), (xR j).neg_add_relabelling (pgame.mk yl yr yL yR)) (λ (j : yr), (pgame.mk xl xr xL xR).neg_add_relabelling (yR j))) (λ (i : (-pgame.mk xl xr xL xR + -pgame.mk yl yr yL yR).right_moves), sum.cases_on i (λ (i : xl), (xL i).neg_add_relabelling (pgame.mk yl yr yL yR)) (λ (i : yl), (pgame.mk xl xr xL xR).neg_add_relabelling (yL i)))
x+y
has exactly the same moves as y+x
.
Equations
- (pgame.mk xl xr xL xR).add_comm_relabelling (pgame.mk yl yr yL yR) = pgame.relabelling.mk (equiv.sum_comm xl yl) (equiv.sum_comm xr yr) (λ (i : (pgame.mk xl xr xL xR + pgame.mk yl yr yL yR).left_moves), sum.cases_on i (λ (i : xl), _.mpr ((xL i).add_comm_relabelling (pgame.mk yl yr yL yR))) (λ (i : yl), _.mpr ((pgame.mk xl xr xL xR).add_comm_relabelling (yL i)))) (λ (j : (pgame.mk yl yr yL yR + pgame.mk xl xr xL xR).right_moves), sum.cases_on j (λ (j : yr), _.mpr ((pgame.mk xl xr xL xR).add_comm_relabelling (yR j))) (λ (j : xr), _.mpr ((xR j).add_comm_relabelling (pgame.mk yl yr yL yR))))
(x + y) + z
has exactly the same moves as x + (y + z)
.
Equations
- (pgame.mk xl xr xL xR).add_assoc_relabelling (pgame.mk yl yr yL yR) (pgame.mk zl zr zL zR) = pgame.relabelling.mk (equiv.sum_assoc xl yl zl) (equiv.sum_assoc xr yr zr) (λ (i : (pgame.mk xl xr xL xR + pgame.mk yl yr yL yR + pgame.mk zl zr zL zR).left_moves), sum.cases_on i (λ (i : xl ⊕ yl), i.cases_on (λ (i : xl), (xL i).add_assoc_relabelling (pgame.mk yl yr yL yR) (pgame.mk zl zr zL zR)) (λ (i : yl), id ((pgame.mk xl xr xL xR).add_assoc_relabelling (yL i) (pgame.mk zl zr zL zR)))) (λ (i : zl), id ((pgame.mk xl xr xL xR).add_assoc_relabelling (pgame.mk yl yr yL yR) (zL i)))) (λ (j : (pgame.mk xl xr xL xR + (pgame.mk yl yr yL yR + pgame.mk zl zr zL zR)).right_moves), sum.cases_on j (λ (j : xr), (xR j).add_assoc_relabelling (pgame.mk yl yr yL yR) (pgame.mk zl zr zL zR)) (λ (j : yr ⊕ zr), j.cases_on (λ (j : yr), id ((pgame.mk xl xr xL xR).add_assoc_relabelling (yR j) (pgame.mk zl zr zL zR))) (λ (j : zr), id ((pgame.mk xl xr xL xR).add_assoc_relabelling (pgame.mk yl yr yL yR) (zR j)))))
The pre-game star
, which is fuzzy/confused with zero.
Equations
- pgame.star = pgame.of_lists [0] [0]
The pre-game ω
. (In fact all ordinals have game and surreal representatives.)