mathlib documentation

set_theory.game.short

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 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 of this typeclass
Instances of other typeclasses for pgame.short
@[protected, instance]
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) :

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 β] (ᾰ_eq : L == S_L), eq.rec (λ (S_sL : Π (i : α), (L i).short) (ᾰ_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
@[protected, 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 β] (ᾰ_eq : L == S_L), eq.rec (λ (S_sL : Π (i : α), (L i).short) (ᾰ_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
@[protected, instance]
Equations
@[protected, 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] (ᾰ_eq : xL == S_L), eq.rec (λ (L : Π (i : xl), (xL i).short) (ᾰ_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)) _ _
@[protected, 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] (ᾰ_eq : xL == S_L), eq.rec (λ (S_sL : Π (i : xl), (xL i).short) (ᾰ_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)) _ _
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
@[protected, instance]
def pgame.short_0  :
Equations
@[protected, 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 of this typeclass
Instances of other typeclasses for pgame.list_short
  • pgame.list_short.has_sizeof_inst
@[protected, instance]
Equations
def pgame.short_of_relabelling {x y : pgame} (R : x.relabelling y) (S : x.short) :

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

Equations
@[protected, instance]
def pgame.short_neg (x : pgame) [x.short] :
(-x).short
Equations
@[protected, instance]
def pgame.short_add (x y : pgame) [x.short] [y.short] :
(x + y).short
Equations
@[protected, instance]
def pgame.short_nat (n : ) :
Equations
@[protected, instance]
def pgame.short_bit0 (x : pgame) [x.short] :
Equations
@[protected, instance]
def pgame.short_bit1 (x : pgame) [x.short] :
Equations
def pgame.le_lf_decidable (x y : pgame) [x.short] [y.short] :

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
@[protected, instance]
def pgame.le_decidable (x y : pgame) [x.short] [y.short] :
Equations
@[protected, instance]
def pgame.lf_decidable (x y : pgame) [x.short] [y.short] :
Equations
@[protected, instance]
def pgame.lt_decidable (x y : pgame) [x.short] [y.short] :
decidable (x < y)
Equations
@[protected, instance]
def pgame.equiv_decidable (x y : pgame) [x.short] [y.short] :
Equations