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

[Conway, On numbers and games][conway2001]

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

[Andreas Blass, A game semantics for linear logic][MR1167694]
[André Joyal, Remarques sur la théorie des jeux à deux personnes][joyal1997]

mathlib documentation

set_theory.​pgame

Combinatorial (pre-)games.

Conway induction

Order properties

Algebraic structures

Future work

References

General documentation

Additional documentation

Library

set_theory.pgame