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.PGameType (u + 1)

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

• mk: {α β : Type u} → {L : } → {R : } → ((i : α) → (L i).Short)((j : β) → (R j).Short)[inst : ] → [inst : ] → (SetTheory.PGame.mk α β L R).Short
Instances
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
Instances For
def SetTheory.PGame.fintypeLeft {α : Type u} {β : Type u} {L : } {R : } [S : (SetTheory.PGame.mk α β L R).Short] :

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.
Instances For
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} {β : Type u} {L : } {R : } [S : (SetTheory.PGame.mk α β L R).Short] :

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.
Instances For
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 : Type u_1} {xr : Type u_1} (xL : ) (xR : ) [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.
Instances For
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 : Type u_1} {xr : Type u_1} (xL : ) (xR : ) [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.
Instances For
def SetTheory.PGame.Short.ofIsEmpty {l : Type u_1} {r : Type u_1} {xL : } {xR : } [] [] :
(SetTheory.PGame.mk l r xL xR).Short

Equations
Instances For
Equations
Equations
• One or more equations did not get rendered due to their size.
class inductive SetTheory.PGame.ListShort :
Type (u + 1)

Evidence that every PGame in a list is Short.

Instances
instance SetTheory.PGame.ListShort.cons (hd : SetTheory.PGame) [short_hd : hd.Short] (tl : ) [short_tl : ] :
Equations
instance SetTheory.PGame.listShortGet (L : ) (i : ) (h : i < L.length) :
L[i].Short
Equations
instance SetTheory.PGame.shortOfLists (L : ) (R : ) :
.Short
Equations
• One or more equations did not get rendered due to their size.
def SetTheory.PGame.shortOfRelabelling {x : SetTheory.PGame} {y : SetTheory.PGame} :
x.Relabelling yx.Shorty.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.
Instances For
instance SetTheory.PGame.shortNeg (x : SetTheory.PGame) [x.Short] :
(-x).Short
Equations
@[irreducible]
instance SetTheory.PGame.shortAdd (x : SetTheory.PGame) (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
instance SetTheory.PGame.shortOfNat (n : ) [n.AtLeastTwo] :
(OfNat.ofNat n).Short
Equations
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 : SetTheory.PGame) (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.
Instances For
instance SetTheory.PGame.leDecidable (x : SetTheory.PGame) (y : SetTheory.PGame) [x.Short] [y.Short] :
Equations
• x.leDecidable y = (x.leLFDecidable y).1
instance SetTheory.PGame.lfDecidable (x : SetTheory.PGame) (y : SetTheory.PGame) [x.Short] [y.Short] :
Decidable (x.LF y)
Equations
• x.lfDecidable y = (x.leLFDecidable y).2
instance SetTheory.PGame.ltDecidable (x : SetTheory.PGame) (y : SetTheory.PGame) [x.Short] [y.Short] :
Decidable (x < y)
Equations
• x.ltDecidable y = And.decidable
instance SetTheory.PGame.equivDecidable (x : SetTheory.PGame) (y : SetTheory.PGame) [x.Short] [y.Short] :
Equations
• x.equivDecidable y = And.decidable