mathlib documentation

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

@[class]
inductive pgame.short  :
pgameType (u+1)

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

Instances
def pgame.short.mk' {x : pgame} [fintype x.left_moves] [fintype x.right_moves] :
(Π (i : x.left_moves), (x.move_left i).short)(Π (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
def pgame.fintype_left {α β : Type u} {L : α → pgame} {R : β → pgame} [S : (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
  • pgame.fintype_left = S.cases_on (λ {S_α S_β : Type u} {S_L : S_α → pgame} {S_R : S_β → pgame} (S_sL : Π (i : S_α), (S_L i).short) (S_sR : Π (j : S_β), (S_R j).short) [F : fintype S_α] [S__inst_2 : fintype S_β] (H_1 : pgame.mk α β L R = pgame.mk S_α S_β S_L S_R), pgame.no_confusion H_1 (λ (α_eq : α = S_α), eq.rec (λ {S_L : α → pgame} (S_sL : Π (i : α), (S_L i).short) [F : fintype α] (β_eq : β = S_β), eq.rec (λ {S_R : β → pgame} (S_sR : Π (j : β), (S_R j).short) [S__inst_2 : fintype β] (a_eq : L == S_L), eq.rec (λ (S_sL : Π (i : α), (L i).short) (a_eq : R == S_R), eq.rec (λ (S_sR : Π (j : β), (R j).short) (H_2 : S == pgame.short.mk S_sL S_sR), eq.rec F _) _ S_sR) _ S_sL) β_eq S_sR) α_eq S_sL)) pgame.fintype_left._proof_4 pgame.fintype_left._proof_5
@[instance]

Equations
def pgame.fintype_right {α β : Type u} {L : α → pgame} {R : β → pgame} [S : (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
  • pgame.fintype_right = S.cases_on (λ {S_α S_β : Type u} {S_L : S_α → pgame} {S_R : S_β → pgame} (S_sL : Π (i : S_α), (S_L i).short) (S_sR : Π (j : S_β), (S_R j).short) [S__inst_1 : fintype S_α] [F : fintype S_β] (H_1 : pgame.mk α β L R = pgame.mk S_α S_β S_L S_R), pgame.no_confusion H_1 (λ (α_eq : α = S_α), eq.rec (λ {S_L : α → pgame} (S_sL : Π (i : α), (S_L i).short) [S__inst_1 : fintype α] (β_eq : β = S_β), eq.rec (λ {S_R : β → pgame} (S_sR : Π (j : β), (S_R j).short) [F : fintype β] (a_eq : L == S_L), eq.rec (λ (S_sL : Π (i : α), (L i).short) (a_eq : R == S_R), eq.rec (λ (S_sR : Π (j : β), (R j).short) (H_2 : S == pgame.short.mk S_sL S_sR), eq.rec F _) _ S_sR) _ S_sL) β_eq S_sR) α_eq S_sL)) pgame.fintype_right._proof_4 pgame.fintype_right._proof_5
@[instance]

Equations
@[instance]
def pgame.move_left_short (x : pgame) [S : x.short] (i : x.left_moves) :

Equations
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
  • pgame.move_left_short' xL xR i = S.cases_on (λ {S_α S_β : Type u_1} {S_L : S_α → pgame} {S_R : S_β → pgame} (L : Π (i : S_α), (S_L i).short) (S_sR : Π (j : S_β), (S_R j).short) [S__inst_1 : fintype S_α] [S__inst_2 : fintype S_β] (H_1 : pgame.mk xl xr xL xR = pgame.mk S_α S_β S_L S_R), pgame.no_confusion H_1 (λ (α_eq : xl = S_α), eq.rec (λ {S_L : xl → pgame} (L : Π (i : xl), (S_L i).short) [S__inst_1 : fintype xl] (β_eq : xr = S_β), eq.rec (λ {S_R : xr → pgame} (S_sR : Π (j : xr), (S_R j).short) [S__inst_2 : fintype xr] (a_eq : xL == S_L), eq.rec (λ (L : Π (i : xl), (xL i).short) (a_eq : xR == S_R), eq.rec (λ (S_sR : Π (j : xr), (xR j).short) (H_2 : S == pgame.short.mk L S_sR), eq.rec (L i) _) _ S_sR) _ L) β_eq S_sR) α_eq L)) _ _
@[instance]
def pgame.move_right_short (x : pgame) [S : x.short] (j : x.right_moves) :

Equations
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
  • pgame.move_right_short' xL xR j = S.cases_on (λ {S_α S_β : Type u_1} {S_L : S_α → pgame} {S_R : S_β → pgame} (S_sL : Π (i : S_α), (S_L i).short) (R : Π (j : S_β), (S_R j).short) [S__inst_1 : fintype S_α] [S__inst_2 : fintype S_β] (H_1 : pgame.mk xl xr xL xR = pgame.mk S_α S_β S_L S_R), pgame.no_confusion H_1 (λ (α_eq : xl = S_α), eq.rec (λ {S_L : xl → pgame} (S_sL : Π (i : xl), (S_L i).short) [S__inst_1 : fintype xl] (β_eq : xr = S_β), eq.rec (λ {S_R : xr → pgame} (R : Π (j : xr), (S_R j).short) [S__inst_2 : fintype xr] (a_eq : xL == S_L), eq.rec (λ (S_sL : Π (i : xl), (xL i).short) (a_eq : xR == S_R), eq.rec (λ (R : Π (j : xr), (xR j).short) (H_2 : S == pgame.short.mk S_sL R), eq.rec (R j) _) _ R) _ S_sL) β_eq R) α_eq S_sL)) _ _
@[instance]

Equations
@[instance]
def pgame.short_0  :

Equations
@[instance]
def pgame.short_1  :

Equations
@[class]
inductive pgame.list_short  :
list pgameType (u+1)

Evidence that every pgame in a list is short.

Instances
@[instance]

Equations
def pgame.short_of_relabelling {x y : pgame} :
x.relabelling yx.short → y.short

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

Equations

If x has no left move or right moves, it is (very!) short.

Equations
@[instance]
def pgame.short_neg (x : pgame) [x.short] :
(-x).short

Equations
@[instance]
def pgame.short_add (x y : pgame) [x.short] [y.short] :
(x + y).short

Equations
@[instance]
def pgame.short_nat (n : ) :

Equations
@[instance]
def pgame.short_bit0 (x : pgame) [x.short] :

Equations
@[instance]
def pgame.short_bit1 (x : pgame) [x.short] :

Equations
def pgame.le_lt_decidable (x y : pgame) [x.short] [y.short] :
decidable (x y) × decidable (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
@[instance]
def pgame.le_decidable (x y : pgame) [x.short] [y.short] :

Equations
@[instance]
def pgame.lt_decidable (x y : pgame) [x.short] [y.short] :
decidable (x < y)

Equations
@[instance]
def pgame.equiv_decidable (x y : pgame) [x.short] [y.short] :

Equations