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.
- 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)
A short game is a game with a finite set of moves at every turn.
Instances
A synonym for Short.mk
that specifies the pgame in an implicit argument.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
This leads to infinite loops if made into an instance.
Instances For
- 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)
Evidence that every PGame
in a list is Short
.
Instances
Equations
- SetTheory.PGame.listShortGet [] n = False.elim (_ : False)
- 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 := (_ : n < List.length tl) }
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
Equations
- SetTheory.PGame.shortNeg (SetTheory.PGame.mk xl xr xL xR) = SetTheory.PGame.Short.mk (fun i => SetTheory.PGame.shortNeg (xR i)) fun i => SetTheory.PGame.shortNeg (xL i)
Equations
- One or more equations did not get rendered due to their size.
Equations
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.