Documentation

Mathlib.SetTheory.Game.Short

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 :

PGame → Type (u + 1)

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

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

Instances

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

Subsingleton x.Short

@[irreducible]

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

Subsingleton x.Short

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

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

Equations

Instances For

def SetTheory.PGame.fintypeLeft {α β : Type u} {L : α → PGame} {R : β → PGame} [S : (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

Instances For

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

Fintype x.LeftMoves

Equations

def SetTheory.PGame.fintypeRight {α β : Type u} {L : α → PGame} {R : β → PGame} [S : (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

Instances For

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

Fintype x.RightMoves

Equations

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

(x.moveLeft i).Short

Equations

def SetTheory.PGame.moveLeftShort' {xl xr : Type u_1} (xL : xl → PGame) (xR : xr → PGame) [S : (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

Instances For

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

(x.moveRight j).Short

Equations

def SetTheory.PGame.moveRightShort' {xl xr : Type u_1} (xL : xl → PGame) (xR : xr → PGame) [S : (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

Instances For

theorem SetTheory.PGame.short_birthday (x : PGame) [x.Short] :

x.birthday < Ordinal.omega0

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

(PGame.mk l r xL xR).Short

This leads to infinite loops if made into an instance.

Equations

Instances For

instance SetTheory.PGame.short0 :

Equations

instance SetTheory.PGame.short1 :

Equations

class inductive SetTheory.PGame.ListShort :

List PGame → Type (u + 1)

Evidence that every PGame in a list is Short.

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

Instances

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

ListShort (hd :: tl)

Equations

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

Equations

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

(ofLists L R).Short

Equations

def SetTheory.PGame.shortOfRelabelling {x y : 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

Instances For

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

Equations

@[irreducible]

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

(x + y).Short

Equations

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

(x + x).Short

Equations

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

(x + x + 1).Short

Equations

@[irreducible]

def SetTheory.PGame.leLFDecidable (x y : 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

Instances For

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

Decidable (x ≤ y)

Equations

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

Decidable (x.LF y)

Equations

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

Decidable (x < y)

Equations

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

Decidable (x ≈ y)

Equations