Combinatorial pregames #
This is the first in a series of files developing the basic theory of combinatorial games,
following Conway's book On Numbers and Games
:
- this file defines pregames and elementary operations on them (relabelling, option insertion)
Mathlib/SetTheory/PGame/Order.lean
defines an ordering on pregamesMathlib/SetTheory/PGame/Algebra.lean
defines anAddCommGroup
structure on pregamesMathlib/SetTheory/Game/Basic.lean
defines games as the quotient of pregames by the equivalence relationp ≈ 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.
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.
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]
Pre-game moves #
The type of pre-games, before we have quotiented
by equivalence (PGame.Setoid
). 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.
Instances For
The indexing type for allowable moves by Left.
Equations
- (SetTheory.PGame.mk l β a a_1).LeftMoves = l
Instances For
The indexing type for allowable moves by Right.
Equations
- (SetTheory.PGame.mk l β a a_1).RightMoves = β
Instances For
The new game after Left makes an allowed move.
Equations
- (SetTheory.PGame.mk l β a a_1).moveLeft = a
Instances For
The new game after Right makes an allowed move.
Equations
- (SetTheory.PGame.mk l β a a_1).moveRight = a_1
Instances For
Construct a pre-game from list of pre-games describing the available moves for Left and Right.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Converts a number into a left move for ofLists
.
This is just an abbreviation for Equiv.ulift.symm
Instances For
Converts a number into a right move for ofLists
.
This is just an abbreviation for Equiv.ulift.symm
Instances For
A variant of PGame.recOn
expressed in terms of PGame.moveLeft
and PGame.moveRight
.
Both this and PGame.recOn
describe Conway induction on games.
Equations
- x.moveRecOn IH = SetTheory.PGame.recOn x fun (yl yr : Type ?u.44) (yL : yl → SetTheory.PGame) (yR : yr → SetTheory.PGame) => IH (SetTheory.PGame.mk yl yr yL yR)
Instances For
Subsequent x y
says that x
can be obtained by playing some nonempty sequence of moves from
y
. It is the transitive closure of IsOption
.
Instances For
Discharges proof obligations of the form ⊢ Subsequent ..
arising in termination proofs
of definitions using well-founded recursion on PGame
.
Equations
- SetTheory.PGame.tacticPgame_wf_tac = Lean.ParserDescr.node `SetTheory.PGame.tacticPgame_wf_tac 1024 (Lean.ParserDescr.nonReservedSymbol "pgame_wf_tac" false)
Instances For
Basic pre-games #
The pre-game Zero
is defined by 0 = { | }
.
Equations
- SetTheory.PGame.instInhabited = { default := 0 }
The pre-game One
is defined by 1 = { 0 | }
.
Equations
- SetTheory.PGame.instOnePGame = { one := SetTheory.PGame.mk PUnit.{?u.3 + 1} PEmpty.{?u.3 + 1} (fun (x : PUnit.{?u.3 + 1}) => 0) PEmpty.elim }
Identity #
Two pre-games are identical if their left and right sets are identical.
That is, Identical x y
if every left move of x
is identical to some left move of y
,
every right move of x
is identical to some right move of y
, and vice versa.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Two pre-games are identical if their left and right sets are identical.
That is, Identical x y
if every left move of x
is identical to some left move of y
,
every right move of x
is identical to some right move of y
, and vice versa.
Equations
- SetTheory.PGame.«term_≡_» = Lean.ParserDescr.trailingNode `SetTheory.PGame.«term_≡_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≡ ") (Lean.ParserDescr.cat `term 51))
Instances For
x ∈ₗ y
if x
is identical to some left move of y
.
Equations
- SetTheory.PGame.«term_∈ₗ_» = Lean.ParserDescr.trailingNode `SetTheory.PGame.«term_∈ₗ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∈ₗ ") (Lean.ParserDescr.cat `term 51))
Instances For
x ∈ᵣ y
if x
is identical to some right move of y
.
Equations
- SetTheory.PGame.«term_∈ᵣ_» = Lean.ParserDescr.trailingNode `SetTheory.PGame.«term_∈ᵣ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∈ᵣ ") (Lean.ParserDescr.cat `term 51))
Instances For
x ∈ₗ y
if x
is identical to some left move of y
.
Equations
- SetTheory.PGame.«binderTerm∈ₗ_» = Lean.ParserDescr.node `SetTheory.PGame.«binderTerm∈ₗ_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∈ₗ ") (Lean.ParserDescr.cat `term 0))
Instances For
x ∈ᵣ y
if x
is identical to some right move of y
.
Equations
- SetTheory.PGame.«binderTerm∈ᵣ_» = Lean.ParserDescr.node `SetTheory.PGame.«binderTerm∈ᵣ_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∈ᵣ ") (Lean.ParserDescr.cat `term 0))
Instances For
Equations
Instances For
If x
and y
are identical, then a right move of x
is identical to some right move of y
.
Show x ≡ y
by giving an explicit correspondence between the moves of x
and y
.
Relabellings #
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.
- mk {x y : PGame} (L : x.LeftMoves ≃ y.LeftMoves) (R : x.RightMoves ≃ y.RightMoves) : ((i : x.LeftMoves) → (x.moveLeft i).Relabelling (y.moveLeft (L i))) → ((j : x.RightMoves) → (x.moveRight j).Relabelling (y.moveRight (R j))) → x.Relabelling y
Instances For
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.
Equations
- SetTheory.PGame.«term_≡r_» = Lean.ParserDescr.trailingNode `SetTheory.PGame.«term_≡r_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≡r ") (Lean.ParserDescr.cat `term 51))
Instances For
A constructor for relabellings swapping the equivalences.
Equations
- SetTheory.PGame.Relabelling.mk' L R hL hR = SetTheory.PGame.Relabelling.mk L.symm R.symm (fun (i : x.LeftMoves) => ⋯.mp (hL (L.symm i))) fun (j : x.RightMoves) => ⋯.mp (hR (R.symm j))
Instances For
The equivalence between left moves of x
and y
given by the relabelling.
Equations
- (SetTheory.PGame.Relabelling.mk L R a a_1).leftMovesEquiv = L
Instances For
The equivalence between right moves of x
and y
given by the relabelling.
Equations
- (SetTheory.PGame.Relabelling.mk L R a a_1).rightMovesEquiv = R
Instances For
A left move of x
is a relabelling of a left move of y
.
Equations
- (SetTheory.PGame.Relabelling.mk L R a a_1).moveLeft = a
Instances For
A left move of y
is a relabelling of a left move of x
.
Equations
- (SetTheory.PGame.Relabelling.mk L R hL hR).moveLeftSymm x✝ = id (⋯.mp (hL (L.symm x✝)))
Instances For
A right move of x
is a relabelling of a right move of y
.
Equations
- (SetTheory.PGame.Relabelling.mk L R a a_1).moveRight = a_1
Instances For
A right move of y
is a relabelling of a right move of x
.
Equations
- (SetTheory.PGame.Relabelling.mk L R hL hR).moveRightSymm x✝ = id (⋯.mp (hR (R.symm x✝)))
Instances For
The identity relabelling.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- SetTheory.PGame.Relabelling.instInhabited x = { default := SetTheory.PGame.Relabelling.refl x }
Flip a relabelling.
Equations
- (SetTheory.PGame.Relabelling.mk L R hL hR).symm = SetTheory.PGame.Relabelling.mk' L R (fun (i : x✝¹.LeftMoves) => (hL i).symm) fun (j : x✝¹.RightMoves) => (hR j).symm
Instances For
Transitivity of relabelling.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Any game without left or right moves is a relabelling of 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Replace the types indexing the next moves for Left and Right by equivalent types.
Equations
- SetTheory.PGame.relabel el er = SetTheory.PGame.mk xl' xr' (x.moveLeft ∘ ⇑el) (x.moveRight ∘ ⇑er)
Instances For
The game obtained by relabelling the next moves is a relabelling of the original game.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Inserting an option #
The pregame constructed by inserting x'
as a new left option into x.
Equations
- (SetTheory.PGame.mk l β a a_1).insertLeft x' = SetTheory.PGame.mk (l ⊕ PUnit.{?u.90 + 1}) β (Sum.elim a fun (x : PUnit.{?u.90 + 1}) => x') a_1
Instances For
The pregame constructed by inserting x'
as a new right option into x.
Equations
- (SetTheory.PGame.mk l β a a_1).insertRight x' = SetTheory.PGame.mk l (β ⊕ PUnit.{?u.90 + 1}) a (Sum.elim a_1 fun (x : PUnit.{?u.90 + 1}) => x')
Instances For
Inserting on the left and right commutes.