mathlib docs: set_theory.game.short

source

@[class]

inductive pgame.short :

pgame → Type (u+1)

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

source

@[instance]

def pgame.subsingleton_short (x : pgame) :

subsingleton x.short

Equations

_ = _

source

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

pgame.short.mk' sL sR = x.cases_on (λ (x_α x_β : Type u_1) (x_a : x_α → pgame) (x_a_1 : x_β → pgame) [_inst_1 : fintype (pgame.mk x_α x_β x_a x_a_1).left_moves] [_inst_2 : fintype (pgame.mk x_α x_β x_a x_a_1).right_moves] (sL : Π (i : (pgame.mk x_α x_β x_a x_a_1).left_moves), ((pgame.mk x_α x_β x_a x_a_1).move_left i).short) (sR : Π (j : (pgame.mk x_α x_β x_a x_a_1).right_moves), ((pgame.mk x_α x_β x_a x_a_1).move_right j).short), id (λ (x_α x_β : Type u_1) (x_a : x_α → pgame) (x_a_1 : x_β → pgame) [_inst_1 : fintype x_α] [_inst_2 : fintype x_β] (sL : Π (i : x_α), (x_a i).short) (sR : Π (j : x_β), (x_a_1 j).short), pgame.short.mk sL sR) x_α x_β x_a x_a_1 sL sR) sL sR

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

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

source

@[instance]

def pgame.fintype_left_moves (x : pgame) [S : x.short] :

fintype x.left_moves

Equations

x.fintype_left_moves = x.cases_on (λ (x_α x_β : Type u_1) (x_a : x_α → pgame) (x_a_1 : x_β → pgame) [S : (pgame.mk x_α x_β x_a x_a_1).short], id pgame.fintype_left)

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

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

source

@[instance]

def pgame.fintype_right_moves (x : pgame) [S : x.short] :

fintype x.right_moves

Equations

x.fintype_right_moves = x.cases_on (λ (x_α x_β : Type u_1) (x_a : x_α → pgame) (x_a_1 : x_β → pgame) [S : (pgame.mk x_α x_β x_a x_a_1).short], id pgame.fintype_right)

source

@[instance]

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

(x.move_left i).short

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) _ _

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

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)) _ _

source

@[instance]

def pgame.move_right_short (x : pgame) [S : x.short] (j : x.right_moves) :

(x.move_right j).short

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) _ _

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

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)) _ _

source

@[instance]

def pgame.short.of_pempty {xL xR : pempty → pgame} :

(pgame.mk pempty pempty xL xR).short

Equations

pgame.short.of_pempty = pgame.short.mk (λ (i : pempty), i.elim) (λ (j : pempty), j.elim)

source

@[instance]

def pgame.short_0 :

0.short

Equations

pgame.short_0 = pgame.short.mk (λ (i : pempty), pempty.cases_on (λ (i : pempty), i.elim.short) i) (λ (j : pempty), pempty.cases_on (λ (j : pempty), j.elim.short) j)

source

@[instance]

def pgame.short_1 :

1.short

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)

source

@[class]

inductive pgame.list_short :

list pgame → Type (u+1)

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

source

@[instance]

def pgame.list_short_nth_le (L : list pgame) [pgame.list_short L] (i : fin L.length) :

(L.nth_le i.val _).short

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.val _).short _

source

@[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

pgame.short_of_lists L R = pgame.short.mk (λ (i : fin L.length), pgame.list_short_nth_le L i) (λ (j : fin R.length), pgame.list_short_nth_le R j)

source

def pgame.short_of_relabelling {x y : pgame} :

x.relabelling y → x.short → y.short

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), pgame.short_of_relabelling (rR j) infer_instance)

source

def pgame.short_of_equiv_empty {x : pgame} :

x.left_moves ≃ pempty → x.right_moves ≃ pempty → x.short

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

Equations

pgame.short_of_equiv_empty el er = pgame.short_of_relabelling (pgame.relabel_relabelling el er).symm pgame.short.of_pempty

source

@[instance]

def pgame.short_neg (x : pgame) [x.short] :

(-x).short

Equations

(pgame.mk xl xr xL xR).short_neg = pgame.short.mk (λ (i : xr), (xR i).short_neg) (λ (j : xl), (xL j).short_neg)

source

@[instance]

def pgame.short_add (x y : pgame) [x.short] [y.short] :

(x + y).short

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 (λ (j : xr), (xR j).short_add (pgame.mk yl yr yL yR)) (λ (j : yr), id ((pgame.mk xl xr xL xR).short_add (yR j))))

source

@[instance]

def pgame.short_nat (n : ℕ) :

↑n.short

Equations

pgame.short_nat (n + 1) = ↑n.short_add 1
pgame.short_nat 0 = pgame.short_0

source

@[instance]

def pgame.short_bit0 (x : pgame) [x.short] :

(bit0 x).short

Equations

x.short_bit0 = id (x.short_add x)

source

@[instance]

def pgame.short_bit1 (x : pgame) [x.short] :

(bit1 x).short

Equations

x.short_bit1 = id ((bit0 x).short_add 1)

source

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