Short games

A combinatorial game is Short [Conway, ch.9][conway2001] 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 : α) → SetTheory.PGame.Short (L i)) → ((j : β) → SetTheory.PGame.Short (R j)) → [inst : Fintype α] → [inst : Fintype β] → SetTheory.PGame.Short (SetTheory.PGame.mk α β L R)

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

Equations

• ⋯ = ⋯

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

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

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

Equations

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

def SetTheory.PGame.fintypeLeft {α : Type u} {β : Type u} {L : α → SetTheory.PGame} {R : β → SetTheory.PGame} [S : SetTheory.PGame.Short (SetTheory.PGame.mk α β L R)] : 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 : SetTheory.PGame.Short x] : Fintype (SetTheory.PGame.LeftMoves x)

Equations

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

def SetTheory.PGame.fintypeRight {α : Type u} {β : Type u} {L : α → SetTheory.PGame} {R : β → SetTheory.PGame} [S : SetTheory.PGame.Short (SetTheory.PGame.mk α β L R)] : 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 : SetTheory.PGame.Short x] : Fintype (SetTheory.PGame.RightMoves x)

Equations

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

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

Equations

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

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

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 : SetTheory.PGame.Short x] (j : SetTheory.PGame.RightMoves x) : SetTheory.PGame.Short (SetTheory.PGame.moveRight x j)

Equations

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

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

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) [SetTheory.PGame.Short x] : SetTheory.PGame.birthday x < Ordinal.omega

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

This leads to infinite loops if made into an instance.

Equations

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

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} → SetTheory.PGame.Short hd → SetTheory.PGame.ListShort tl → SetTheory.PGame.ListShort (hd :: tl)

instance SetTheory.PGame.ListShort.cons (hd : SetTheory.PGame) [short_hd : SetTheory.PGame.Short hd] (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 : Fin (List.length L)) : SetTheory.PGame.Short (List.get L i)

Equations

• SetTheory.PGame.listShortGet [] n = ⋯.elim
• SetTheory.PGame.listShortGet (head :: tail) { val := 0, isLt := isLt } = S
• SetTheory.PGame.listShortGet (hd :: tl) { val := Nat.succ n, isLt := h } = SetTheory.PGame.listShortGet tl { val := n, isLt := ⋯ }

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

Equations

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

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

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) [SetTheory.PGame.Short x] : SetTheory.PGame.Short (-x)

Equations

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

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

Equations

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

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

Equations

• SetTheory.PGame.shortNat 0 = SetTheory.PGame.short0
• SetTheory.PGame.shortNat (Nat.succ n) = SetTheory.PGame.shortAdd (Nat.unaryCast (Nat.add n 0)) 1

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

Equations

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

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

Equations

• SetTheory.PGame.shortBit0 x = id inferInstance

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

Equations

• SetTheory.PGame.shortBit1 x = id inferInstance

def SetTheory.PGame.leLFDecidable (x : SetTheory.PGame) (y : SetTheory.PGame) [SetTheory.PGame.Short x] [SetTheory.PGame.Short y] : Decidable (x ≤ y) × Decidable (SetTheory.PGame.LF x 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 : SetTheory.PGame) (y : SetTheory.PGame) [SetTheory.PGame.Short x] [SetTheory.PGame.Short y] : Decidable (x ≤ y)

Equations

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

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

Equations

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

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

Equations

• SetTheory.PGame.ltDecidable x y = And.decidable

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

Equations

• SetTheory.PGame.equivDecidable x y = And.decidable