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.
- mk : Π {α β : Type ?} {L : α → pgame} {R : β → pgame}, (Π (i : α), (L i).short) → (Π (j : β), (R j).short) → Π [_inst_1 : fintype α] [_inst_2 : fintype β], (pgame.mk α β L R).short
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
- pgame.short.has_sizeof_inst
- pgame.subsingleton_short
A synonym for short.mk
that specifies the pgame in an implicit argument.
Equations
- pgame.short.mk' sL sR = x.cases_on (λ (x_α x_β : Type u_1) (x_ᾰ : x_α → pgame) (x_ᾰ_1 : x_β → pgame) [_inst_1 : fintype (pgame.mk x_α x_β x_ᾰ x_ᾰ_1).left_moves] [_inst_2 : fintype (pgame.mk x_α x_β x_ᾰ x_ᾰ_1).right_moves] (sL : Π (i : (pgame.mk x_α x_β x_ᾰ x_ᾰ_1).left_moves), ((pgame.mk x_α x_β x_ᾰ x_ᾰ_1).move_left i).short) (sR : Π (j : (pgame.mk x_α x_β x_ᾰ x_ᾰ_1).right_moves), ((pgame.mk x_α x_β x_ᾰ x_ᾰ_1).move_right j).short), id (λ (x_α x_β : Type u_1) (x_ᾰ : x_α → pgame) (x_ᾰ_1 : x_β → pgame) [_inst_1 : fintype x_α] [_inst_2 : fintype x_β] (sL : Π (i : x_α), (x_ᾰ i).short) (sR : Π (j : x_β), (x_ᾰ_1 j).short), pgame.short.mk sL sR) x_α x_β x_ᾰ x_ᾰ_1 sL sR) sL sR
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
Equations
- x.fintype_left_moves = x.cases_on (λ (x_α x_β : Type u_1) (x_ᾰ : x_α → pgame) (x_ᾰ_1 : x_β → pgame) [S : (pgame.mk x_α x_β x_ᾰ x_ᾰ_1).short], id pgame.fintype_left)
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
Equations
- x.fintype_right_moves = x.cases_on (λ (x_α x_β : Type u_1) (x_ᾰ : x_α → pgame) (x_ᾰ_1 : x_β → pgame) [S : (pgame.mk x_α x_β x_ᾰ x_ᾰ_1).short], id pgame.fintype_right)
Equations
- x.move_left_short 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 : x = pgame.mk S_α S_β S_L S_R), eq.rec (λ [S : (pgame.mk S_α S_β S_L S_R).short] (i : (pgame.mk S_α S_β S_L S_R).left_moves) (H_2 : S == pgame.short.mk L S_sR), eq.rec (L i) _) _ i) _ _
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)) _ _
Equations
- x.move_right_short 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 : x = pgame.mk S_α S_β S_L S_R), eq.rec (λ [S : (pgame.mk S_α S_β S_L S_R).short] (j : (pgame.mk S_α S_β S_L S_R).right_moves) (H_2 : S == pgame.short.mk S_sL R), eq.rec (R j) _) _ j) _ _
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)) _ _
This leads to infinite loops if made into an instance.
Equations
Equations
- pgame.short_1 = pgame.short.mk (λ (i : punit), i.cases_on pgame.short_0) (λ (j : pempty), pempty.cases_on (λ (j : pempty), j.elim.short) j)
- nil : pgame.list_short list.nil
- cons : Π (hd : pgame) [_inst_1 : hd.short] (tl : list pgame) [_inst_2 : pgame.list_short tl], pgame.list_short (hd :: tl)
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
Equations
- pgame.list_short_nth_le (hd :: tl) ⟨n + 1, h⟩ = pgame.list_short_nth_le tl ⟨n, _⟩
- pgame.list_short_nth_le (hd :: tl) ⟨0, _x⟩ = S
- pgame.list_short_nth_le list.nil n = false.rec (list.nil.nth_le ↑n _).short _
Equations
- pgame.short_of_lists L R = pgame.short.mk (λ (i : ulift (fin L.length)), pgame.list_short_nth_le L i.down) (λ (j : ulift (fin R.length)), pgame.list_short_nth_le R j.down)
If x
is a short game, and y
is a relabelling of x
, then y
is also short.
Equations
- pgame.short_of_relabelling (pgame.relabelling.mk L R rL rR) S = pgame.short.mk' (λ (i : y.left_moves), _.mpr (pgame.short_of_relabelling (rL (⇑(L.symm) i)) infer_instance)) (λ (j : y.right_moves), _.mpr (_.mp (pgame.short_of_relabelling (rR (⇑(R.symm) j)) infer_instance)))
Equations
- (pgame.mk xl xr xL xR).short_add (pgame.mk yl yr yL yR) = pgame.short.mk (λ (i : xl ⊕ yl), i.cases_on (λ (i : xl), (xL i).short_add (pgame.mk yl yr yL yR)) (λ (i : yl), id ((pgame.mk xl xr xL xR).short_add (yL i)))) (λ (j : xr ⊕ yr), j.cases_on (λ (i : xr), (xR i).short_add (pgame.mk yl yr yL yR)) (λ (j : yr), id ((pgame.mk xl xr xL xR).short_add (yR j))))
Equations
- pgame.short_nat (n + 1) = ↑n.short_add 1
- pgame.short_nat 0 = pgame.short_0
Equations
- x.short_bit0 = id (x.short_add x)
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
- (pgame.mk xl xr xL xR).le_lf_decidable (pgame.mk yl yr yL yR) = (decidable_of_iff' ((∀ (i : xl), (xL i).lf (pgame.mk yl yr yL yR)) ∧ ∀ (j : yr), (pgame.mk xl xr xL xR).lf (yR j)) pgame.mk_le_mk (id and.decidable), decidable_of_iff' ((∃ (i : yl), pgame.mk xl xr xL xR ≤ yL i) ∨ ∃ (j : xr), xR j ≤ pgame.mk yl yr yL yR) pgame.mk_lf_mk (id or.decidable))
Equations
- x.le_decidable y = (x.le_lf_decidable y).fst
Equations
- x.lf_decidable y = (x.le_lf_decidable y).snd