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.
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.
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.
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.
The material here is all drawn from
An interested reader may like to formalise some of the material from
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.
The indexing type for allowable moves by Left.
The indexing type for allowable moves by Right.
The new game after Left makes an allowed move.
The new game after Right makes an allowed move.
subsequent p q says that p can be obtained by playing some nonempty sequence of moves from q.
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 = { | }.
The pre-game one is defined by 1 = { 0 | }.
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.
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.
Show that the response for left provided by left_response preserves the left-player-wins condition.
Define the equivalence relation on pre-games. Two pre-games x, y are equivalent if x ≤ y and y ≤ x.
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.
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.
The identity relabelling.
Reverse a relabelling.
A relabelling lets us prove equivalence of games.
Replace the types indexing the next moves for Left and Right by equivalent types.
The game obtained by relabelling the next moves is a relabelling of the original game.
The negation of {L | R} is {-R | -L}.
An explicit equivalence between the moves for Left in -x and the moves for Right in x.
An explicit equivalence between the moves for Right in -x and the moves for Left in x.
The sum of x = {xL | xR} and y = {yL | yR} is {xL + y, x + yL | xR + y, x + yR}.
x + 0 has exactly the same moves as x.
x + 0 is equivalent to x.
0 + x has exactly the same moves as 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.
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.
-(x+y) has exactly the same moves as -x + -y.
x+y has exactly the same moves as y+x.
(x + y) + z has exactly the same moves as x + (y + z).
The pre-game star, which is fuzzy/confused with zero.
The pre-game ω. (In fact all ordinals have game and surreal representatives.)