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 (SetTheory.PGame below) is axiomatised via an inductive type, whose sole constructor takes two types (thought of as indexing the possible moves for the players Left and Right), and a pair of functions out of these types to SetTheory.PGame (thought of as describing the resulting game after making a move).

We may denote a game as $\{L | R\}$, where $L$ and $R$ stand for the collections of left and right moves. This notation is not currently used in Mathlib.

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 SetTheory.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 SetTheory.PGame.LeftMoves, SetTheory.PGame.RightMoves, SetTheory.PGame.moveLeft and SetTheory.PGame.moveRight. There is a relation PGame.Subsequent p q, saying that p can be reached by playing some non-empty sequence of moves starting from q, an instance WellFounded 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, satisfying the usual properties of a Preorder. The relation 0 < x means that x can always be won by Left, while 0 ≤ x means that x can be won by Left as the second player.

It turns out to be quite convenient to define various relations on top of these. We define the "less or fuzzy" relation x ⧏ y as ¬ y ≤ x, the equivalence relation x ≈ y as x ≤ y ∧ y ≤ x, and the fuzzy relation x ‖ y as x ⧏ y ∧ y ⧏ x. If 0 ⧏ x, then x can be won by Left as the first player. If x ≈ 0, then x can be won by the second player. If x ‖ 0, then x can be won by the first player.

Statements like zero_le_lf, zero_lf_le, etc. unfold these definitions. The theorems le_def and lf_def give a recursive characterisation of each relation in terms of themselves two moves later. The theorems zero_le, zero_lf, etc. also take into account that 0 has no moves.

Later, games will be defined as the quotient by the ≈ relation; that is to say, the Antisymmetrization of SetTheory.PGame.

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

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]

Combinatorial (pre-)games. #

Conway induction #

Order properties #

Algebraic structures #

Future work #

References #

Pre-game moves #

Basic pre-games #

Pre-game order relations #

Relabellings #

Negation #

Addition and subtraction #

Inserting an option #

Special pre-games #