mathlib3 documentation

set_theory.game.short

Short games #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 dec_trivial doesn't seem to be able to prove anything using these instances.

source
@[class]
inductive pgame.short  :
pgame → Type (u+1)

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

Instances of this typeclass
Instances of other typeclasses for pgame.short
source
@[protected, instance]
def pgame.subsingleton_short (x : pgame) :
subsingleton x.short
source
def pgame.short.mk' {x : pgame} [fintype x.left_moves] [fintype x.right_moves] (sL : Π (i : x.left_moves), (x.move_left i).short) (sR : Π (j : x.right_moves), (x.move_right j).short) :
x.short

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

Equations
source
def pgame.fintype_left {α β : Type u} {L : α → pgame} {R : β → pgame} [S : (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
source
@[protected, instance]
def pgame.fintype_left_moves (x : pgame) [S : x.short] :
fintype x.left_moves
Equations
source
def pgame.fintype_right {α β : Type u} {L : α → pgame} {R : β → pgame} [S : (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
source
@[protected, instance]
def pgame.fintype_right_moves (x : pgame) [S : x.short] :
fintype x.right_moves
Equations
source
@[protected, instance]
def pgame.move_left_short (x : pgame) [S : x.short] (i : x.left_moves) :
(x.move_left i).short
Equations
source
def pgame.move_left_short' {xl xr : Type u_1} (xL : xl → pgame) (xR : xr → pgame) [S : (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
source
@[protected, instance]
def pgame.move_right_short (x : pgame) [S : x.short] (j : x.right_moves) :
(x.move_right j).short
Equations
source
def pgame.move_right_short' {xl xr : Type u_1} (xL : xl → pgame) (xR : xr → pgame) [S : (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
source
theorem pgame.short_birthday (x : pgame) [x.short] :
x.birthday < ordinal.omega
source
def pgame.short.of_is_empty {l r : Type u_1} {xL : l → pgame} {xR : r → pgame} [is_empty l] [is_empty r] :
(pgame.mk l r xL xR).short

This leads to infinite loops if made into an instance.

Equations
source
@[protected, instance]
def pgame.short_0  :
0.short
Equations
source
@[protected, instance]
def pgame.short_1  :
1.short
Equations
source
@[class]
inductive pgame.list_short  :
list pgame → Type (u+1)

Evidence that every pgame in a list is short.

Instances of this typeclass
Instances of other typeclasses for pgame.list_short
  • pgame.list_short.has_sizeof_inst
source
@[protected, instance]
def pgame.list_short_nth_le (L : list pgame) [pgame.list_short L] (i : fin L.length) :
(L.nth_le ↑i _).short
Equations
source
@[protected, instance]
def pgame.short_of_lists (L R : list pgame) [pgame.list_short L] [pgame.list_short R] :
(pgame.of_lists L R).short
Equations
source
def pgame.short_of_relabelling {x y : pgame} (R : x.relabelling y) (S : x.short) :
y.short

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

Equations
source
@[protected, instance]
def pgame.short_neg (x : pgame) [x.short] :
(-x).short
Equations
source
@[protected, instance]
def pgame.short_add (x y : pgame) [x.short] [y.short] :
(x + y).short
Equations
source
@[protected, instance]
def pgame.short_nat (n : ℕ) :
↑n.short
Equations
source
@[protected, instance]
def pgame.short_bit0 (x : pgame) [x.short] :
(bit0 x).short
Equations
source
@[protected, instance]
def pgame.short_bit1 (x : pgame) [x.short] :
(bit1 x).short
Equations
source
def pgame.le_lf_decidable (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
source
@[protected, instance]
def pgame.le_decidable (x y : pgame) [x.short] [y.short] :
decidable (x ≤ y)
Equations
source
@[protected, instance]
def pgame.lf_decidable (x y : pgame) [x.short] [y.short] :
decidable (x.lf y)
Equations
source
@[protected, instance]
def pgame.lt_decidable (x y : pgame) [x.short] [y.short] :
decidable (x < y)
Equations
source
@[protected, instance]
def pgame.equiv_decidable (x y : pgame) [x.short] [y.short] :
decidable (x.equiv y)
Equations