Short games

A combinatorial game is Short Conway, ch.9 if it has only finitely many positions. In particular, this means there is a finite set of moves at every point.

We prove that the order relations ≤ and <, and the equivalence relation ≈, are decidable on short games, although unfortunately in practice decide doesn't seem to be able to prove anything using these instances.

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

A short game is a game with a finite set of moves at every turn.

• mk: {α β : Type u} → {L : α → SetTheory.PGame} → {R : β → SetTheory.PGame} → ((i : α) → (L i).Short) → ((j : β) → (R j).Short) → [inst : Fintype α] → [inst : Fintype β] → (SetTheory.PGame.mk α β L R).Short

instance SetTheory.PGame.subsingleton_short (x : SetTheory.PGame) : Subsingleton x.Short

Equations

• ⋯ = ⋯

@[irreducible]

theorem SetTheory.PGame.subsingleton_short_example (x : SetTheory.PGame) : Subsingleton x.Short

def SetTheory.PGame.Short.mk' {x : SetTheory.PGame} [Fintype x.LeftMoves] [Fintype x.RightMoves] (sL : (i : x.LeftMoves) → (x.moveLeft i).Short) (sR : (j : x.RightMoves) → (x.moveRight j).Short) : x.Short

A synonym for Short.mk that specifies the pgame in an implicit argument.

Equations

• SetTheory.PGame.Short.mk' sL sR = ⋯.mpr (SetTheory.PGame.Short.mk sL sR)

def SetTheory.PGame.fintypeLeft {α β : Type u} {L : α → SetTheory.PGame} {R : β → SetTheory.PGame} [S : (SetTheory.PGame.mk α β L R).Short] : Fintype α

Extracting the Fintype instance for the indexing type for Left's moves in a short game. This is an unindexed typeclass, so it can't be made a global instance.

Equations

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

instance SetTheory.PGame.fintypeLeftMoves (x : SetTheory.PGame) [S : x.Short] : Fintype x.LeftMoves

Equations

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

def SetTheory.PGame.fintypeRight {α β : Type u} {L : α → SetTheory.PGame} {R : β → SetTheory.PGame} [S : (SetTheory.PGame.mk α β L R).Short] : Fintype β

Extracting the Fintype instance for the indexing type for Right's moves in a short game. This is an unindexed typeclass, so it can't be made a global instance.

Equations

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

instance SetTheory.PGame.fintypeRightMoves (x : SetTheory.PGame) [S : x.Short] : Fintype x.RightMoves

Equations

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

instance SetTheory.PGame.moveLeftShort (x : SetTheory.PGame) [S : x.Short] (i : x.LeftMoves) : (x.moveLeft i).Short

Equations

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

def SetTheory.PGame.moveLeftShort' {xl xr : Type u_1} (xL : xl → SetTheory.PGame) (xR : xr → SetTheory.PGame) [S : (SetTheory.PGame.mk xl xr xL xR).Short] (i : xl) : (xL i).Short

Extracting the Short instance for a move by Left. This would be a dangerous instance potentially introducing new metavariables in typeclass search, so we only make it an instance locally.

Equations

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

instance SetTheory.PGame.moveRightShort (x : SetTheory.PGame) [S : x.Short] (j : x.RightMoves) : (x.moveRight j).Short

Equations

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

def SetTheory.PGame.moveRightShort' {xl xr : Type u_1} (xL : xl → SetTheory.PGame) (xR : xr → SetTheory.PGame) [S : (SetTheory.PGame.mk xl xr xL xR).Short] (j : xr) : (xR j).Short

Extracting the Short instance for a move by Right. This would be a dangerous instance potentially introducing new metavariables in typeclass search, so we only make it an instance locally.

Equations

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

theorem SetTheory.PGame.short_birthday (x : SetTheory.PGame) [x.Short] : x.birthday < Ordinal.omega0

def SetTheory.PGame.Short.ofIsEmpty {l r : Type u_1} {xL : l → SetTheory.PGame} {xR : r → SetTheory.PGame} [IsEmpty l] [IsEmpty r] : (SetTheory.PGame.mk l r xL xR).Short

This leads to infinite loops if made into an instance.

Equations

• SetTheory.PGame.Short.ofIsEmpty = SetTheory.PGame.Short.mk (fun (a : l) => isEmptyElim a) fun (a : r) => isEmptyElim a

instance SetTheory.PGame.short0 : SetTheory.PGame.Short 0

Equations

• SetTheory.PGame.short0 = SetTheory.PGame.Short.ofIsEmpty

instance SetTheory.PGame.short1 : SetTheory.PGame.Short 1

Equations

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

class inductive SetTheory.PGame.ListShort : List SetTheory.PGame → Type (u + 1)

Evidence that every PGame in a list is Short.

• nil: SetTheory.PGame.ListShort []
• cons': {hd : SetTheory.PGame} → {tl : List SetTheory.PGame} → hd.Short → SetTheory.PGame.ListShort tl → SetTheory.PGame.ListShort (hd :: tl)

instance SetTheory.PGame.ListShort.cons (hd : SetTheory.PGame) [short_hd : hd.Short] (tl : List SetTheory.PGame) [short_tl : SetTheory.PGame.ListShort tl] : SetTheory.PGame.ListShort (hd :: tl)

Equations

• SetTheory.PGame.ListShort.cons hd tl = SetTheory.PGame.ListShort.cons' short_hd short_tl

instance SetTheory.PGame.listShortGet (L : List SetTheory.PGame) [SetTheory.PGame.ListShort L] (i : ℕ) (h : i < L.length) : L[i].Short

Equations

• SetTheory.PGame.listShortGet (head :: tail) 0 x_4 = S
• SetTheory.PGame.listShortGet (head :: tl) n.succ h = SetTheory.PGame.listShortGet tl n ⋯

instance SetTheory.PGame.shortOfLists (L R : List SetTheory.PGame) [SetTheory.PGame.ListShort L] [SetTheory.PGame.ListShort R] : (SetTheory.PGame.ofLists L R).Short

Equations

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

def SetTheory.PGame.shortOfRelabelling {x y : SetTheory.PGame} : x.Relabelling y → x.Short → y.Short

If x is a short game, and y is a relabelling of x, then y is also short.

Equations

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

instance SetTheory.PGame.shortNeg (x : SetTheory.PGame) [x.Short] : (-x).Short

Equations

• (SetTheory.PGame.mk xl xr xL xR).shortNeg = SetTheory.PGame.Short.mk (fun (i : xr) => (xR i).shortNeg) fun (i : xl) => (xL i).shortNeg

@[irreducible]

instance SetTheory.PGame.shortAdd (x y : SetTheory.PGame) [x.Short] [y.Short] : (x + y).Short

Equations

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

instance SetTheory.PGame.shortNat (n : ℕ) : (↑n).Short

Equations

• SetTheory.PGame.shortNat 0 = SetTheory.PGame.short0
• SetTheory.PGame.shortNat n.succ = n.unaryCast.shortAdd 1

instance SetTheory.PGame.shortOfNat (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).Short

Equations

• SetTheory.PGame.shortOfNat n = SetTheory.PGame.shortNat n

instance SetTheory.PGame.shortBit0 (x : SetTheory.PGame) [x.Short] : (x + x).Short

Equations

• x.shortBit0 = inferInstance

instance SetTheory.PGame.shortBit1 (x : SetTheory.PGame) [x.Short] : (x + x + 1).Short

Equations

• x.shortBit1 = (x + x).shortAdd 1

@[irreducible]

def SetTheory.PGame.leLFDecidable (x y : SetTheory.PGame) [x.Short] [y.Short] : Decidable (x ≤ y) × Decidable (x.LF y)

Auxiliary construction of decidability instances. We build Decidable (x ≤ y) and Decidable (x ⧏ y) in a simultaneous induction. Instances for the two projections separately are provided below.

Equations

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

instance SetTheory.PGame.leDecidable (x y : SetTheory.PGame) [x.Short] [y.Short] : Decidable (x ≤ y)

Equations

• x.leDecidable y = (x.leLFDecidable y).1

instance SetTheory.PGame.lfDecidable (x y : SetTheory.PGame) [x.Short] [y.Short] : Decidable (x.LF y)

Equations

• x.lfDecidable y = (x.leLFDecidable y).2

instance SetTheory.PGame.ltDecidable (x y : SetTheory.PGame) [x.Short] [y.Short] : Decidable (x < y)

Equations

• x.ltDecidable y = inferInstanceAs (Decidable (x ≤ y ∧ x.LF y))

instance SetTheory.PGame.equivDecidable (x y : SetTheory.PGame) [x.Short] [y.Short] : Decidable (x ≈ y)

Equations

• x.equivDecidable y = inferInstanceAs (Decidable (x ≤ y ∧ y ≤ x))