Games described via "the state of the board".

We provide a simple mechanism for constructing combinatorial (pre-)games, by describing "the state of the board", and providing an upper bound on the number of turns remaining.

Implementation notes

We're very careful to produce a computable definition, so small games can be evaluated using decide. To achieve this, I've had to rely solely on induction on natural numbers: relying on general well-foundedness seems to be poisonous to computation?

See SetTheory/Game/Domineering for an example using this construction.

class SetTheory.PGame.State (S : Type u) : Type u

SetTheory.PGame.State S describes how to interpret s : S as a state of a combinatorial game. Use SetTheory.PGame.ofState s or SetTheory.Game.ofState s to construct the game.

SetTheory.PGame.State.l : S → Finset S and SetTheory.PGame.State.r : S → Finset S describe the states reachable by a move by Left or Right. SetTheory.PGame.State.turnBound : S → ℕ gives an upper bound on the number of possible turns remaining from this state.

• turnBound : S → ℕ
• l : S → Finset S
• r : S → Finset S
• left_bound {s t : S} : t ∈ SetTheory.PGame.State.l s → SetTheory.PGame.State.turnBound t < SetTheory.PGame.State.turnBound s
• right_bound {s t : S} : t ∈ SetTheory.PGame.State.r s → SetTheory.PGame.State.turnBound t < SetTheory.PGame.State.turnBound s

theorem SetTheory.PGame.turnBound_ne_zero_of_left_move {S : Type u} [SetTheory.PGame.State S] {s t : S} (m : t ∈ SetTheory.PGame.State.l s) : SetTheory.PGame.State.turnBound s ≠ 0

theorem SetTheory.PGame.turnBound_ne_zero_of_right_move {S : Type u} [SetTheory.PGame.State S] {s t : S} (m : t ∈ SetTheory.PGame.State.r s) : SetTheory.PGame.State.turnBound s ≠ 0

theorem SetTheory.PGame.turnBound_of_left {S : Type u} [SetTheory.PGame.State S] {s t : S} (m : t ∈ SetTheory.PGame.State.l s) (n : ℕ) (h : SetTheory.PGame.State.turnBound s ≤ n + 1) : SetTheory.PGame.State.turnBound t ≤ n

theorem SetTheory.PGame.turnBound_of_right {S : Type u} [SetTheory.PGame.State S] {s t : S} (m : t ∈ SetTheory.PGame.State.r s) (n : ℕ) (h : SetTheory.PGame.State.turnBound s ≤ n + 1) : SetTheory.PGame.State.turnBound t ≤ n

def SetTheory.PGame.ofStateAux {S : Type u} [SetTheory.PGame.State S] (n : ℕ) (s : S) : SetTheory.PGame.State.turnBound s ≤ n → SetTheory.PGame

Construct a PGame from a state and a (not necessarily optimal) bound on the number of turns remaining.

Equations

• One or more equations did not get rendered due to their size.

def SetTheory.PGame.ofStateAuxRelabelling {S : Type u} [SetTheory.PGame.State S] (s : S) (n m : ℕ) (hn : SetTheory.PGame.State.turnBound s ≤ n) (hm : SetTheory.PGame.State.turnBound s ≤ m) : (SetTheory.PGame.ofStateAux n s hn).Relabelling (SetTheory.PGame.ofStateAux m s hm)

Two different (valid) turn bounds give equivalent games.

Equations

• One or more equations did not get rendered due to their size.

def SetTheory.PGame.ofState {S : Type u} [SetTheory.PGame.State S] (s : S) : SetTheory.PGame

Construct a combinatorial PGame from a state.

Equations

• SetTheory.PGame.ofState s = SetTheory.PGame.ofStateAux (SetTheory.PGame.State.turnBound s) s ⋯

def SetTheory.PGame.leftMovesOfStateAux {S : Type u} [SetTheory.PGame.State S] (n : ℕ) {s : S} (h : SetTheory.PGame.State.turnBound s ≤ n) : (SetTheory.PGame.ofStateAux n s h).LeftMoves ≃ { t : S // t ∈ SetTheory.PGame.State.l s }

The equivalence between leftMoves for a PGame constructed using ofStateAux _ s _, and L s.

Equations

• One or more equations did not get rendered due to their size.

def SetTheory.PGame.leftMovesOfState {S : Type u} [SetTheory.PGame.State S] (s : S) : (SetTheory.PGame.ofState s).LeftMoves ≃ { t : S // t ∈ SetTheory.PGame.State.l s }

The equivalence between leftMoves for a PGame constructed using ofState s, and l s.

Equations

• SetTheory.PGame.leftMovesOfState s = SetTheory.PGame.leftMovesOfStateAux (SetTheory.PGame.State.turnBound s) ⋯

def SetTheory.PGame.rightMovesOfStateAux {S : Type u} [SetTheory.PGame.State S] (n : ℕ) {s : S} (h : SetTheory.PGame.State.turnBound s ≤ n) : (SetTheory.PGame.ofStateAux n s h).RightMoves ≃ { t : S // t ∈ SetTheory.PGame.State.r s }

The equivalence between rightMoves for a PGame constructed using ofStateAux _ s _, and R s.

Equations

• One or more equations did not get rendered due to their size.

def SetTheory.PGame.rightMovesOfState {S : Type u} [SetTheory.PGame.State S] (s : S) : (SetTheory.PGame.ofState s).RightMoves ≃ { t : S // t ∈ SetTheory.PGame.State.r s }

The equivalence between rightMoves for a PGame constructed using ofState s, and R s.

Equations

• SetTheory.PGame.rightMovesOfState s = SetTheory.PGame.rightMovesOfStateAux (SetTheory.PGame.State.turnBound s) ⋯

def SetTheory.PGame.relabellingMoveLeftAux {S : Type u} [SetTheory.PGame.State S] (n : ℕ) {s : S} (h : SetTheory.PGame.State.turnBound s ≤ n) (t : (SetTheory.PGame.ofStateAux n s h).LeftMoves) : ((SetTheory.PGame.ofStateAux n s h).moveLeft t).Relabelling (SetTheory.PGame.ofStateAux (n - 1) ↑((SetTheory.PGame.leftMovesOfStateAux n h) t) ⋯)

The relabelling showing moveLeft applied to a game constructed using ofStateAux has itself been constructed using ofStateAux.

Equations

• One or more equations did not get rendered due to their size.

def SetTheory.PGame.relabellingMoveLeft {S : Type u} [SetTheory.PGame.State S] (s : S) (t : (SetTheory.PGame.ofState s).LeftMoves) : ((SetTheory.PGame.ofState s).moveLeft t).Relabelling (SetTheory.PGame.ofState ↑((SetTheory.PGame.leftMovesOfState s).toFun t))

The relabelling showing moveLeft applied to a game constructed using of has itself been constructed using of.

Equations

• One or more equations did not get rendered due to their size.

def SetTheory.PGame.relabellingMoveRightAux {S : Type u} [SetTheory.PGame.State S] (n : ℕ) {s : S} (h : SetTheory.PGame.State.turnBound s ≤ n) (t : (SetTheory.PGame.ofStateAux n s h).RightMoves) : ((SetTheory.PGame.ofStateAux n s h).moveRight t).Relabelling (SetTheory.PGame.ofStateAux (n - 1) ↑((SetTheory.PGame.rightMovesOfStateAux n h) t) ⋯)

The relabelling showing moveRight applied to a game constructed using ofStateAux has itself been constructed using ofStateAux.

Equations

• One or more equations did not get rendered due to their size.

def SetTheory.PGame.relabellingMoveRight {S : Type u} [SetTheory.PGame.State S] (s : S) (t : (SetTheory.PGame.ofState s).RightMoves) : ((SetTheory.PGame.ofState s).moveRight t).Relabelling (SetTheory.PGame.ofState ↑((SetTheory.PGame.rightMovesOfState s).toFun t))

The relabelling showing moveRight applied to a game constructed using of has itself been constructed using of.

Equations

• One or more equations did not get rendered due to their size.

instance SetTheory.PGame.fintypeLeftMovesOfStateAux {S : Type u} [SetTheory.PGame.State S] (n : ℕ) (s : S) (h : SetTheory.PGame.State.turnBound s ≤ n) : Fintype (SetTheory.PGame.ofStateAux n s h).LeftMoves

Equations

• SetTheory.PGame.fintypeLeftMovesOfStateAux n s h = Fintype.ofEquiv { t : S // t ∈ SetTheory.PGame.State.l s } (SetTheory.PGame.leftMovesOfStateAux n h).symm

instance SetTheory.PGame.fintypeRightMovesOfStateAux {S : Type u} [SetTheory.PGame.State S] (n : ℕ) (s : S) (h : SetTheory.PGame.State.turnBound s ≤ n) : Fintype (SetTheory.PGame.ofStateAux n s h).RightMoves

Equations

• SetTheory.PGame.fintypeRightMovesOfStateAux n s h = Fintype.ofEquiv { t : S // t ∈ SetTheory.PGame.State.r s } (SetTheory.PGame.rightMovesOfStateAux n h).symm

instance SetTheory.PGame.shortOfStateAux {S : Type u} [SetTheory.PGame.State S] (n : ℕ) {s : S} (h : SetTheory.PGame.State.turnBound s ≤ n) : (SetTheory.PGame.ofStateAux n s h).Short

Equations

• One or more equations did not get rendered due to their size.

instance SetTheory.PGame.shortOfState {S : Type u} [SetTheory.PGame.State S] (s : S) : (SetTheory.PGame.ofState s).Short

Equations

• SetTheory.PGame.shortOfState s = id inferInstance

def SetTheory.Game.ofState {S : Type u} [SetTheory.PGame.State S] (s : S) : SetTheory.Game

Construct a combinatorial Game from a state.

Equations

• SetTheory.Game.ofState s = ⟦SetTheory.PGame.ofState s⟧