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 pregames
• Mathlib/SetTheory/PGame/Algebra.lean defines an AddCommGroup structure on pregames
• Mathlib/SetTheory/Game/Basic.lean defines games as the quotient of pregames by 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.

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

• [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][joyal1977]

Pre-game moves

inductive SetTheory.PGame : Type (u + 1)

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.

• mk (α β : Type u) : (α → PGame) → (β → PGame) → PGame

def SetTheory.PGame.LeftMoves : PGame → Type u

The indexing type for allowable moves by Left.

Equations

• (SetTheory.PGame.mk l β a a_1).LeftMoves = l

def SetTheory.PGame.RightMoves : PGame → Type u

The indexing type for allowable moves by Right.

Equations

• (SetTheory.PGame.mk l β a a_1).RightMoves = β

def SetTheory.PGame.moveLeft (g : PGame) : g.LeftMoves → PGame

The new game after Left makes an allowed move.

Equations

• (SetTheory.PGame.mk l β a a_1).moveLeft = a

def SetTheory.PGame.moveRight (g : PGame) : g.RightMoves → PGame

The new game after Right makes an allowed move.

Equations

• (SetTheory.PGame.mk l β a a_1).moveRight = a_1

@[simp]

theorem SetTheory.PGame.leftMoves_mk {xl xr : Type u_1} {xL : xl → PGame} {xR : xr → PGame} : (mk xl xr xL xR).LeftMoves = xl

@[simp]

theorem SetTheory.PGame.moveLeft_mk {xl xr : Type u_1} {xL : xl → PGame} {xR : xr → PGame} : (mk xl xr xL xR).moveLeft = xL

@[simp]

theorem SetTheory.PGame.rightMoves_mk {xl xr : Type u_1} {xL : xl → PGame} {xR : xr → PGame} : (mk xl xr xL xR).RightMoves = xr

@[simp]

theorem SetTheory.PGame.moveRight_mk {xl xr : Type u_1} {xL : xl → PGame} {xR : xr → PGame} : (mk xl xr xL xR).moveRight = xR

theorem SetTheory.PGame.ext {x y : PGame} (hl : x.LeftMoves = y.LeftMoves) (hr : x.RightMoves = y.RightMoves) (hL : ∀ (i : x.LeftMoves) (j : y.LeftMoves), HEq i j → x.moveLeft i = y.moveLeft j) (hR : ∀ (i : x.RightMoves) (j : y.RightMoves), HEq i j → x.moveRight i = y.moveRight j) : x = y

def SetTheory.PGame.ofLists (L R : List PGame) : PGame

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.

theorem SetTheory.PGame.leftMoves_ofLists (L R : List PGame) : (ofLists L R).LeftMoves = ULift.{u_1, 0} (Fin L.length)

theorem SetTheory.PGame.rightMoves_ofLists (L R : List PGame) : (ofLists L R).RightMoves = ULift.{u_1, 0} (Fin R.length)

@[reducible, inline]

abbrev SetTheory.PGame.toOfListsLeftMoves {L R : List PGame} : Fin L.length ≃ (ofLists L R).LeftMoves

Converts a number into a left move for ofLists.

This is just an abbreviation for Equiv.ulift.symm

Equations

• SetTheory.PGame.toOfListsLeftMoves = Equiv.ulift.symm

@[reducible, inline]

abbrev SetTheory.PGame.toOfListsRightMoves {L R : List PGame} : Fin R.length ≃ (ofLists L R).RightMoves

Converts a number into a right move for ofLists.

This is just an abbreviation for Equiv.ulift.symm

Equations

• SetTheory.PGame.toOfListsRightMoves = Equiv.ulift.symm

@[simp]

theorem SetTheory.PGame.ofLists_moveLeft' {L R : List PGame} (i : (ofLists L R).LeftMoves) : (ofLists L R).moveLeft i = L[↑i.down]

theorem SetTheory.PGame.ofLists_moveLeft {L R : List PGame} (i : Fin L.length) : (ofLists L R).moveLeft { down := i } = L[i]

@[simp]

theorem SetTheory.PGame.ofLists_moveRight' {L R : List PGame} (i : (ofLists L R).RightMoves) : (ofLists L R).moveRight i = R[↑i.down]

theorem SetTheory.PGame.ofLists_moveRight {L R : List PGame} (i : Fin R.length) : (ofLists L R).moveRight { down := i } = R[i]

def SetTheory.PGame.moveRecOn {C : PGame → Sort u_1} (x : PGame) (IH : (y : PGame) → ((i : y.LeftMoves) → C (y.moveLeft i)) → ((j : y.RightMoves) → C (y.moveRight j)) → C y) : C x

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)

inductive SetTheory.PGame.IsOption : PGame → PGame → Prop

IsOption x y means that x is either a left or right option for y.

• moveLeft {x : PGame} (i : x.LeftMoves) : (x.moveLeft i).IsOption x
• moveRight {x : PGame} (i : x.RightMoves) : (x.moveRight i).IsOption x

theorem SetTheory.PGame.isOption_iff (a✝ a✝¹ : PGame) : a✝.IsOption a✝¹ ↔ (∃ (i : a✝¹.LeftMoves), a✝ = a✝¹.moveLeft i) ∨ ∃ (i : a✝¹.RightMoves), a✝ = a✝¹.moveRight i

theorem SetTheory.PGame.IsOption.mk_left {xl xr : Type u} (xL : xl → PGame) (xR : xr → PGame) (i : xl) : (xL i).IsOption (mk xl xr xL xR)

theorem SetTheory.PGame.IsOption.mk_right {xl xr : Type u} (xL : xl → PGame) (xR : xr → PGame) (i : xr) : (xR i).IsOption (mk xl xr xL xR)

theorem SetTheory.PGame.wf_isOption : WellFounded IsOption

def SetTheory.PGame.Subsequent : PGame → PGame → Prop

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.

Equations

• SetTheory.PGame.Subsequent = Relation.TransGen SetTheory.PGame.IsOption

instance SetTheory.PGame.instIsTransSubsequent : IsTrans PGame Subsequent

theorem SetTheory.PGame.Subsequent.trans {x y z : PGame} : x.Subsequent y → y.Subsequent z → x.Subsequent z

theorem SetTheory.PGame.wf_subsequent : WellFounded Subsequent

instance SetTheory.PGame.instWellFoundedRelation : WellFoundedRelation PGame

Equations

• SetTheory.PGame.instWellFoundedRelation = { rel := SetTheory.PGame.Subsequent, wf := SetTheory.PGame.wf_subsequent }

@[simp]

theorem SetTheory.PGame.Subsequent.moveLeft {x : PGame} (i : x.LeftMoves) : (x.moveLeft i).Subsequent x

@[simp]

theorem SetTheory.PGame.Subsequent.moveRight {x : PGame} (j : x.RightMoves) : (x.moveRight j).Subsequent x

@[simp]

theorem SetTheory.PGame.Subsequent.mk_left {xl xr : Type u_1} (xL : xl → PGame) (xR : xr → PGame) (i : xl) : (xL i).Subsequent (mk xl xr xL xR)

@[simp]

theorem SetTheory.PGame.Subsequent.mk_right {xl xr : Type u_1} (xL : xl → PGame) (xR : xr → PGame) (j : xr) : (xR j).Subsequent (mk xl xr xL xR)

def SetTheory.PGame.tacticPgame_wf_tac : Lean.ParserDescr

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)

@[simp]

theorem SetTheory.PGame.Subsequent.mk_right' {xl xr : Type u} (xL : xl → PGame) (xR : xr → PGame) (j : (mk xl xr xL xR).RightMoves) : (xR j).Subsequent (mk xl xr xL xR)

@[simp]

theorem SetTheory.PGame.Subsequent.moveRight_mk_left {xl xr : Type u} {xR : xr → PGame} {i : xl} (xL : xl → PGame) (j : (xL i).RightMoves) : ((xL i).moveRight j).Subsequent (mk xl xr xL xR)

@[simp]

theorem SetTheory.PGame.Subsequent.moveRight_mk_right {xl xr : Type u} {xL : xl → PGame} {i : xr} (xR : xr → PGame) (j : (xR i).RightMoves) : ((xR i).moveRight j).Subsequent (mk xl xr xL xR)

@[simp]

theorem SetTheory.PGame.Subsequent.moveLeft_mk_left {xl xr : Type u} {xR : xr → PGame} {i : xl} (xL : xl → PGame) (j : (xL i).LeftMoves) : ((xL i).moveLeft j).Subsequent (mk xl xr xL xR)

@[simp]

theorem SetTheory.PGame.Subsequent.moveLeft_mk_right {xl xr : Type u} {xL : xl → PGame} {i : xr} (xR : xr → PGame) (j : (xR i).LeftMoves) : ((xR i).moveLeft j).Subsequent (mk xl xr xL xR)

Basic pre-games

instance SetTheory.PGame.instZero : Zero PGame

The pre-game Zero is defined by 0 = { | }.

Equations

• SetTheory.PGame.instZero = { zero := SetTheory.PGame.mk PEmpty.{?u.2 + 1} PEmpty.{?u.2 + 1} PEmpty.elim PEmpty.elim }

@[simp]

theorem SetTheory.PGame.zero_leftMoves : LeftMoves 0 = PEmpty.{u_1 + 1}

@[simp]

theorem SetTheory.PGame.zero_rightMoves : RightMoves 0 = PEmpty.{u_1 + 1}

instance SetTheory.PGame.isEmpty_zero_leftMoves : IsEmpty (LeftMoves 0)

instance SetTheory.PGame.isEmpty_zero_rightMoves : IsEmpty (RightMoves 0)

instance SetTheory.PGame.instInhabited : Inhabited PGame

Equations

• SetTheory.PGame.instInhabited = { default := 0 }

instance SetTheory.PGame.instOnePGame : One PGame

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 }

@[simp]

theorem SetTheory.PGame.one_leftMoves : LeftMoves 1 = PUnit.{u_1 + 1}

@[simp]

theorem SetTheory.PGame.one_moveLeft (x : LeftMoves 1) : moveLeft 1 x = 0

@[simp]

theorem SetTheory.PGame.one_rightMoves : RightMoves 1 = PEmpty.{u_1 + 1}

instance SetTheory.PGame.uniqueOneLeftMoves : Unique (LeftMoves 1)

Equations

• SetTheory.PGame.uniqueOneLeftMoves = PUnit.instUnique

instance SetTheory.PGame.isEmpty_one_rightMoves : IsEmpty (RightMoves 1)

Identity

def SetTheory.PGame.Identical : PGame → PGame → Prop

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.

def SetTheory.PGame.«term_≡_» : Lean.TrailingParserDescr

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))

theorem SetTheory.PGame.identical_iff {x y : PGame} : x.Identical y ↔ (Relator.BiTotal fun (x1 : x.LeftMoves) (x2 : y.LeftMoves) => (x.moveLeft x1).Identical (y.moveLeft x2)) ∧ Relator.BiTotal fun (x1 : x.RightMoves) (x2 : y.RightMoves) => (x.moveRight x1).Identical (y.moveRight x2)

@[simp]

theorem SetTheory.PGame.Identical.refl (x : PGame) : x.Identical x

theorem SetTheory.PGame.Identical.rfl {x : PGame} : x.Identical x

theorem SetTheory.PGame.Identical.symm {x y : PGame} : x.Identical y → y.Identical x

theorem SetTheory.PGame.identical_comm {x y : PGame} : x.Identical y ↔ y.Identical x

theorem SetTheory.PGame.Identical.trans {x y z : PGame} : x.Identical y → y.Identical z → x.Identical z

def SetTheory.PGame.memₗ (x y : PGame) : Prop

x ∈ₗ y if x is identical to some left move of y.

Equations

• x.memₗ y = ∃ (b : y.LeftMoves), x.Identical (y.moveLeft b)

def SetTheory.PGame.memᵣ (x y : PGame) : Prop

x ∈ᵣ y if x is identical to some right move of y.

Equations

• x.memᵣ y = ∃ (b : y.RightMoves), x.Identical (y.moveRight b)

def SetTheory.PGame.«term_∈ₗ_» : Lean.TrailingParserDescr

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))

def SetTheory.PGame.«term_∈ᵣ_» : Lean.TrailingParserDescr

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))

def SetTheory.PGame.«binderTerm∈ₗ_» : Lean.ParserDescr

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))

def SetTheory.PGame.«binderTerm∈ᵣ_» : Lean.ParserDescr

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))

theorem SetTheory.PGame.memₗ_def {x y : PGame} : x.memₗ y ↔ ∃ (b : y.LeftMoves), x.Identical (y.moveLeft b)

theorem SetTheory.PGame.memᵣ_def {x y : PGame} : x.memᵣ y ↔ ∃ (b : y.RightMoves), x.Identical (y.moveRight b)

theorem SetTheory.PGame.moveLeft_memₗ (x : PGame) (b : x.LeftMoves) : (x.moveLeft b).memₗ x

theorem SetTheory.PGame.moveRight_memᵣ (x : PGame) (b : x.RightMoves) : (x.moveRight b).memᵣ x

theorem SetTheory.PGame.identical_of_isEmpty (x y : PGame) [IsEmpty x.LeftMoves] [IsEmpty x.RightMoves] [IsEmpty y.LeftMoves] [IsEmpty y.RightMoves] : x.Identical y

def SetTheory.PGame.identicalSetoid : Setoid PGame

Identical as a Setoid.

Equations

• SetTheory.PGame.identicalSetoid = { r := SetTheory.PGame.Identical, iseqv := SetTheory.PGame.identicalSetoid._proof_12 }

instance SetTheory.PGame.instIsReflIdentical : IsRefl PGame fun (x1 x2 : PGame) => x1.Identical x2

instance SetTheory.PGame.instIsSymmIdentical : IsSymm PGame fun (x1 x2 : PGame) => x1.Identical x2

instance SetTheory.PGame.instIsTransIdentical : IsTrans PGame fun (x1 x2 : PGame) => x1.Identical x2

instance SetTheory.PGame.instIsEquivIdentical : IsEquiv PGame fun (x1 x2 : PGame) => x1.Identical x2

theorem SetTheory.PGame.Identical.moveLeft {x y : PGame} : x.Identical y → ∀ (i : x.LeftMoves), ∃ (j : y.LeftMoves), (x.moveLeft i).Identical (y.moveLeft j)

If x and y are identical, then a left move of x is identical to some left move of y.

theorem SetTheory.PGame.Identical.moveRight {x y : PGame} : x.Identical y → ∀ (i : x.RightMoves), ∃ (j : y.RightMoves), (x.moveRight i).Identical (y.moveRight j)

If x and y are identical, then a right move of x is identical to some right move of y.

theorem SetTheory.PGame.identical_of_eq {x y : PGame} (h : x = y) : x.Identical y

theorem SetTheory.PGame.identical_iff' {x y : PGame} : x.Identical y ↔ ((∀ (i : x.LeftMoves), (x.moveLeft i).memₗ y) ∧ ∀ (j : y.LeftMoves), (y.moveLeft j).memₗ x) ∧ (∀ (i : x.RightMoves), (x.moveRight i).memᵣ y) ∧ ∀ (j : y.RightMoves), (y.moveRight j).memᵣ x

Uses ∈ₗ and ∈ᵣ instead of ≡.

theorem SetTheory.PGame.memₗ.congr_right {x y : PGame} : x.Identical y → ∀ {w : PGame}, w.memₗ x ↔ w.memₗ y

theorem SetTheory.PGame.memᵣ.congr_right {x y : PGame} : x.Identical y → ∀ {w : PGame}, w.memᵣ x ↔ w.memᵣ y

theorem SetTheory.PGame.memₗ.congr_left {x y : PGame} : x.Identical y → ∀ {w : PGame}, x.memₗ w ↔ y.memₗ w

theorem SetTheory.PGame.memᵣ.congr_left {x y : PGame} : x.Identical y → ∀ {w : PGame}, x.memᵣ w ↔ y.memᵣ w

theorem SetTheory.PGame.Identical.ext {x y : PGame} : (∀ (z : PGame), z.memₗ x ↔ z.memₗ y) → (∀ (z : PGame), z.memᵣ x ↔ z.memᵣ y) → x.Identical y

theorem SetTheory.PGame.Identical.ext_iff {x y : PGame} : x.Identical y ↔ (∀ (z : PGame), z.memₗ x ↔ z.memₗ y) ∧ ∀ (z : PGame), z.memᵣ x ↔ z.memᵣ y

theorem SetTheory.PGame.Identical.congr_right {x y z : PGame} (h : x.Identical y) : z.Identical x ↔ z.Identical y

theorem SetTheory.PGame.Identical.congr_left {x y z : PGame} (h : x.Identical y) : x.Identical z ↔ y.Identical z

theorem SetTheory.PGame.Identical.of_fn {x y : PGame} (l : x.LeftMoves → y.LeftMoves) (il : y.LeftMoves → x.LeftMoves) (r : x.RightMoves → y.RightMoves) (ir : y.RightMoves → x.RightMoves) (hl : ∀ (i : x.LeftMoves), (x.moveLeft i).Identical (y.moveLeft (l i))) (hil : ∀ (i : y.LeftMoves), (x.moveLeft (il i)).Identical (y.moveLeft i)) (hr : ∀ (i : x.RightMoves), (x.moveRight i).Identical (y.moveRight (r i))) (hir : ∀ (i : y.RightMoves), (x.moveRight (ir i)).Identical (y.moveRight i)) : x.Identical y

Show x ≡ y by giving an explicit correspondence between the moves of x and y.

theorem SetTheory.PGame.Identical.of_equiv {x y : PGame} (l : x.LeftMoves ≃ y.LeftMoves) (r : x.RightMoves ≃ y.RightMoves) (hl : ∀ (i : x.LeftMoves), (x.moveLeft i).Identical (y.moveLeft (l i))) (hr : ∀ (i : x.RightMoves), (x.moveRight i).Identical (y.moveRight (r i))) : x.Identical y

Relabellings

inductive SetTheory.PGame.Relabelling : PGame → PGame → Type (u + 1)

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.

• 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

def SetTheory.PGame.«term_≡r_» : Lean.TrailingParserDescr

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.

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))

def SetTheory.PGame.Relabelling.mk' {x y : PGame} (L : y.LeftMoves ≃ x.LeftMoves) (R : y.RightMoves ≃ x.RightMoves) (hL : (i : y.LeftMoves) → (x.moveLeft (L i)).Relabelling (y.moveLeft i)) (hR : (j : y.RightMoves) → (x.moveRight (R j)).Relabelling (y.moveRight j)) : x.Relabelling y

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))

def SetTheory.PGame.Relabelling.leftMovesEquiv {x y : PGame} : x.Relabelling y → x.LeftMoves ≃ y.LeftMoves

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

@[simp]

theorem SetTheory.PGame.Relabelling.mk_leftMovesEquiv {x y : PGame} {L : x.LeftMoves ≃ y.LeftMoves} {R : x.RightMoves ≃ y.RightMoves} {hL : (i : x.LeftMoves) → (x.moveLeft i).Relabelling (y.moveLeft (L i))} {hR : (j : x.RightMoves) → (x.moveRight j).Relabelling (y.moveRight (R j))} : (mk L R hL hR).leftMovesEquiv = L

@[simp]

theorem SetTheory.PGame.Relabelling.mk'_leftMovesEquiv {x y : PGame} {L : y.LeftMoves ≃ x.LeftMoves} {R : y.RightMoves ≃ x.RightMoves} {hL : (i : y.LeftMoves) → (x.moveLeft (L i)).Relabelling (y.moveLeft i)} {hR : (j : y.RightMoves) → (x.moveRight (R j)).Relabelling (y.moveRight j)} : (mk' L R hL hR).leftMovesEquiv = L.symm

def SetTheory.PGame.Relabelling.rightMovesEquiv {x y : PGame} : x.Relabelling y → x.RightMoves ≃ y.RightMoves

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

@[simp]

theorem SetTheory.PGame.Relabelling.mk_rightMovesEquiv {x y : PGame} {L : x.LeftMoves ≃ y.LeftMoves} {R : x.RightMoves ≃ y.RightMoves} {hL : (i : x.LeftMoves) → (x.moveLeft i).Relabelling (y.moveLeft (L i))} {hR : (j : x.RightMoves) → (x.moveRight j).Relabelling (y.moveRight (R j))} : (mk L R hL hR).rightMovesEquiv = R

@[simp]

theorem SetTheory.PGame.Relabelling.mk'_rightMovesEquiv {x y : PGame} {L : y.LeftMoves ≃ x.LeftMoves} {R : y.RightMoves ≃ x.RightMoves} {hL : (i : y.LeftMoves) → (x.moveLeft (L i)).Relabelling (y.moveLeft i)} {hR : (j : y.RightMoves) → (x.moveRight (R j)).Relabelling (y.moveRight j)} : (mk' L R hL hR).rightMovesEquiv = R.symm

def SetTheory.PGame.Relabelling.moveLeft {x y : PGame} (r : x.Relabelling y) (i : x.LeftMoves) : (x.moveLeft i).Relabelling (y.moveLeft (r.leftMovesEquiv i))

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

def SetTheory.PGame.Relabelling.moveLeftSymm {x y : PGame} (r : x.Relabelling y) (i : y.LeftMoves) : (x.moveLeft (r.leftMovesEquiv.symm i)).Relabelling (y.moveLeft i)

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✝)))

def SetTheory.PGame.Relabelling.moveRight {x y : PGame} (r : x.Relabelling y) (i : x.RightMoves) : (x.moveRight i).Relabelling (y.moveRight (r.rightMovesEquiv i))

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

def SetTheory.PGame.Relabelling.moveRightSymm {x y : PGame} (r : x.Relabelling y) (i : y.RightMoves) : (x.moveRight (r.rightMovesEquiv.symm i)).Relabelling (y.moveRight i)

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✝)))

@[irreducible]

def SetTheory.PGame.Relabelling.refl (x : PGame) : x.Relabelling x

The identity relabelling.

Equations

• One or more equations did not get rendered due to their size.

instance SetTheory.PGame.Relabelling.instInhabited (x : PGame) : Inhabited (x.Relabelling x)

Equations

• SetTheory.PGame.Relabelling.instInhabited x = { default := SetTheory.PGame.Relabelling.refl x }

def SetTheory.PGame.Relabelling.symm {x y : PGame} : x.Relabelling y → y.Relabelling 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

def SetTheory.PGame.Relabelling.trans {x y z : PGame} : x.Relabelling y → y.Relabelling z → x.Relabelling z

Transitivity of relabelling.

Equations

• One or more equations did not get rendered due to their size.

def SetTheory.PGame.Relabelling.isEmpty (x : PGame) [IsEmpty x.LeftMoves] [IsEmpty x.RightMoves] : x.Relabelling 0

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.

def SetTheory.PGame.relabel {x : PGame} {xl' xr' : Type u_1} (el : xl' ≃ x.LeftMoves) (er : xr' ≃ x.RightMoves) : PGame

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)

@[simp]

theorem SetTheory.PGame.relabel_moveLeft' {x : PGame} {xl' xr' : Type u_1} (el : xl' ≃ x.LeftMoves) (er : xr' ≃ x.RightMoves) (i : xl') : (relabel el er).moveLeft i = x.moveLeft (el i)

theorem SetTheory.PGame.relabel_moveLeft {x : PGame} {xl' xr' : Type u_1} (el : xl' ≃ x.LeftMoves) (er : xr' ≃ x.RightMoves) (i : x.LeftMoves) : (relabel el er).moveLeft (el.symm i) = x.moveLeft i

@[simp]

theorem SetTheory.PGame.relabel_moveRight' {x : PGame} {xl' xr' : Type u_1} (el : xl' ≃ x.LeftMoves) (er : xr' ≃ x.RightMoves) (j : xr') : (relabel el er).moveRight j = x.moveRight (er j)

theorem SetTheory.PGame.relabel_moveRight {x : PGame} {xl' xr' : Type u_1} (el : xl' ≃ x.LeftMoves) (er : xr' ≃ x.RightMoves) (j : x.RightMoves) : (relabel el er).moveRight (er.symm j) = x.moveRight j

def SetTheory.PGame.relabelRelabelling {x : PGame} {xl' xr' : Type u_1} (el : xl' ≃ x.LeftMoves) (er : xr' ≃ x.RightMoves) : x.Relabelling (relabel el er)

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.

Inserting an option

def SetTheory.PGame.insertLeft (x x' : PGame) : PGame

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

def SetTheory.PGame.insertRight (x x' : PGame) : PGame

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')

theorem SetTheory.PGame.insertRight_insertLeft {x x' x'' : PGame} : (x.insertLeft x').insertRight x'' = (x.insertRight x'').insertLeft x'

Inserting on the left and right commutes.