Computably short games

We already have a definition of short games at IGame.Short, but it is, regrettably, noncomputable. Here, we provide a computable definition of short games from the ground up, following a similar construction method presented in IGame.lean.

We define FGame and its auxiliary backing type SGame as data, providing data for the left and right moves of a game in the form of an auxiliary SGame type. This makes us capable of performing some basic computations on IGame. Since we would like to use the same standard interface for theorem proving in combinatorial games, we restrict this file only for computability usage and FGame generation. Since some of IGame's basic definitions are computable, these theorems suffice for most of the computability we need.

In general, You should not build any substantial theory based off of this file. The theorems here are intended to check for definitional correctness over theory building.

For Mathlib

instance instDecidableLeftTotalOfForallExists_combinatorialGames {α : Type u_1} {β : Type u_2} (r : α → β → Prop) [H : Decidable (∀ (a : α), ∃ (b : β), r a b)] : Decidable (Relator.LeftTotal r)

Equations

• instDecidableLeftTotalOfForallExists_combinatorialGames r = H

instance instDecidableRightTotalOfForallExists_combinatorialGames {α : Type u_1} {β : Type u_2} (r : α → β → Prop) [H : Decidable (∀ (b : β), ∃ (a : α), r a b)] : Decidable (Relator.RightTotal r)

Equations

• instDecidableRightTotalOfForallExists_combinatorialGames r = H

instance instDecidableBiTotalOfForallOfForallExists_combinatorialGames {α : Type u_1} {β : Type u_2} (r : α → β → Prop) [H₁ : Decidable (∀ (a : α), ∃ (b : β), r a b)] [H : Decidable (∀ (b : β), ∃ (a : α), r a b)] : Decidable (Relator.BiTotal r)

Equations

• instDecidableBiTotalOfForallOfForallExists_combinatorialGames r = inferInstanceAs (Decidable (Relator.LeftTotal r ∧ Relator.RightTotal r))

inductive SGame : Type u

The type of "short pre-games", before we have quotiented by equivalence (identicalSetoid).

This serves the exact purpose that PGame does for IGame. However, unlike PGame's relatively short construction, we must prove some extra definitions for computing on top of SGame.

This could perfectly well have been in Type 0, but we make it universe polymorphic for convenience when building quotient types. However, conversions from computable games to their noncomputable counterparts are squeezed to Type 0.

• mk (m n : ℕ) (f : Fin m → SGame) (g : Fin n → SGame) : SGame

def SGame.LeftMoves : SGame → ℕ

The number of left moves on a SGame.

Equations

• (SGame.mk m n f g).LeftMoves = m

def SGame.RightMoves : SGame → ℕ

The number of right moves on a SGame.

Equations

• (SGame.mk m n f g).RightMoves = n

def SGame.moveLeft (g : SGame) : Fin g.LeftMoves → SGame

Perform a left move.

Equations

• (SGame.mk m n f g).moveLeft = f

def SGame.moveRight (g : SGame) : Fin g.RightMoves → SGame

Perform a right move.

Equations

• (SGame.mk m n f g).moveRight = g

@[simp]

theorem SGame.leftMoves_mk (m n : ℕ) (f : Fin m → SGame) (g : Fin n → SGame) : (mk m n f g).LeftMoves = m

@[simp]

theorem SGame.rightMoves_mk (m n : ℕ) (f : Fin m → SGame) (g : Fin n → SGame) : (mk m n f g).RightMoves = n

@[simp]

theorem SGame.moveLeft_mk (m n : ℕ) (f : Fin m → SGame) (g : Fin n → SGame) : (mk m n f g).moveLeft = f

@[simp]

theorem SGame.moveRight_mk (m n : ℕ) (f : Fin m → SGame) (g : Fin n → SGame) : (mk m n f g).moveRight = g

inductive SGame.IsOption : SGame → SGame → Prop

A well-founded relation on SGame. While this goes against minimizing SGame code, this enables well-defined recursion in SGame.

• moveLeft {x : SGame} (n : Fin x.LeftMoves) : (x.moveLeft n).IsOption x
• moveRight {x : SGame} (n : Fin x.RightMoves) : (x.moveRight n).IsOption x

theorem SGame.isOption_wf : WellFounded IsOption

instance SGame.instWellFoundedRelation : WellFoundedRelation SGame

Equations

• SGame.instWellFoundedRelation = { rel := SGame.IsOption, wf := SGame.isOption_wf }

def SGame.tacticSgame_wf : Lean.ParserDescr

Equations

• SGame.tacticSgame_wf = Lean.ParserDescr.node `SGame.tacticSgame_wf 1024 (Lean.ParserDescr.nonReservedSymbol "sgame_wf" false)

instance SGame.instDecidableEq : DecidableEq SGame

Equations

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

def SGame.Identical : SGame → SGame → Prop

The identical relation on short games. See PGame.Identical.

Equations

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

def SGame.«term_≡_» : Lean.TrailingParserDescr

The identical relation on short games. See PGame.Identical.

Equations

• SGame.«term_≡_» = Lean.ParserDescr.trailingNode `SGame.«term_≡_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≡ ") (Lean.ParserDescr.cat `term 51))

theorem SGame.identical_iff {x y : SGame} : x.Identical y ↔ (Relator.BiTotal fun (x1 : Fin x.LeftMoves) (x2 : Fin y.LeftMoves) => (x.moveLeft x1).Identical (y.moveLeft x2)) ∧ Relator.BiTotal fun (x1 : Fin x.RightMoves) (x2 : Fin y.RightMoves) => (x.moveRight x1).Identical (y.moveRight x2)

theorem SGame.Identical.refl (x : SGame) : x.Identical x

theorem SGame.Identical.symm {x y : SGame} : x.Identical y → y.Identical x

theorem SGame.Identical.trans {x y z : SGame} : x.Identical y → y.Identical z → x.Identical z

def SGame.identicalSetoid : Setoid SGame

Identical as a Setoid.

Equations

• SGame.identicalSetoid = { r := SGame.Identical, iseqv := SGame.identicalSetoid._proof_1 }

theorem SGame.Identical.moveLeft {x y : SGame} : x.Identical y → ∀ (i : Fin x.LeftMoves), ∃ (j : Fin y.LeftMoves), (x.moveLeft i).Identical (y.moveLeft j)

If x ≡ y, then a left move of x is identical to some left move of y.

theorem SGame.Identical.moveLeft_symm {x y : SGame} : x.Identical y → ∀ (i : Fin y.LeftMoves), ∃ (j : Fin x.LeftMoves), (x.moveLeft j).Identical (y.moveLeft i)

If x ≡ y, then a left move of y is identical to some left move of x.

theorem SGame.Identical.moveRight {x y : SGame} : x.Identical y → ∀ (i : Fin x.RightMoves), ∃ (j : Fin y.RightMoves), (x.moveRight i).Identical (y.moveRight j)

If x ≡ y, then a right move of x is identical to some right move of y.

theorem SGame.Identical.moveRight_symm {x y : SGame} : x.Identical y → ∀ (i : Fin y.RightMoves), ∃ (j : Fin x.RightMoves), (x.moveRight j).Identical (y.moveRight i)

If x ≡ y, then a right move of y is identical to some right move of x.

@[irreducible]

instance SGame.Identical.instDecidable (a b : SGame) : Decidable (a.Identical b)

Equations

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

Game moves

def FGame : Type u

Short games up to identity.

FGame uses the set-theoretic notion of equality on short games, similarly to how IGame is defined on top of PGame.

Here, we have the distinct advantage of being able to use finsets as our backing left and right sets over IGame's small sets.

Equations

• FGame = Quotient SGame.identicalSetoid

def FGame.mk (x : SGame) : FGame

The quotient map from SGame into FGame.

Equations

• FGame.mk x = ⟦x⟧

theorem FGame.mk_eq_mk {x y : SGame} : mk x = mk y ↔ x.Identical y

theorem FGame.mk_eq {x y : SGame} : x.Identical y → mk x = mk y

Alias of the reverse direction of FGame.mk_eq_mk.

theorem SGame.Identical.mk_eq {x y : SGame} : x.Identical y → FGame.mk x = FGame.mk y

Alias of the reverse direction of FGame.mk_eq_mk.

---

Alias of the reverse direction of FGame.mk_eq_mk.

theorem FGame.ind {motive : FGame → Prop} (H : ∀ (y : SGame), motive (mk y)) (x : FGame) : motive x

instance FGame.instDecidableEq : DecidableEq FGame

Equations

• FGame.instDecidableEq = Quotient.decidableEq

noncomputable def FGame.out (x : FGame) : SGame

Choose an element of the equivalence class using the axiom of choice.

Equations

• x.out = Quotient.out x

@[simp]

theorem FGame.out_eq (x : FGame) : mk x.out = x

def FGame.leftMoves : FGame → Finset FGame

The finset of left moves of the game.

Equations

• FGame.leftMoves = Quotient.lift (fun (x : SGame) => Finset.image (fun (y : Fin x.LeftMoves) => FGame.mk (x.moveLeft y)) Finset.univ) FGame.leftMoves._proof_1

def FGame.rightMoves : FGame → Finset FGame

The finset of right moves of the game.

Equations

• FGame.rightMoves = Quotient.lift (fun (x : SGame) => Finset.image (fun (y : Fin x.RightMoves) => FGame.mk (x.moveRight y)) Finset.univ) FGame.rightMoves._proof_1

@[simp]

theorem FGame.leftMoves_mk (x : SGame) : (mk x).leftMoves = Finset.image (mk ∘ x.moveLeft) Finset.univ

@[simp]

theorem FGame.rightMoves_mk (x : SGame) : (mk x).rightMoves = Finset.image (mk ∘ x.moveRight) Finset.univ

theorem FGame.ext {x y : FGame} (hl : x.leftMoves = y.leftMoves) (hr : x.rightMoves = y.rightMoves) : x = y

theorem FGame.ext_iff {x y : FGame} : x = y ↔ x.leftMoves = y.leftMoves ∧ x.rightMoves = y.rightMoves

def FGame.IsOption (x y : FGame) : Prop

IsOption x y means that x is either a left or a right move for y.

Equations

• x.IsOption y = (x ∈ y.leftMoves ∨ x ∈ y.rightMoves)

theorem FGame.IsOption.of_mem_leftMoves {x y : FGame} : x ∈ y.leftMoves → x.IsOption y

theorem FGame.IsOption.of_mem_rightMoves {x y : FGame} : x ∈ y.rightMoves → x.IsOption y

theorem FGame.isOption_wf : WellFounded IsOption

instance FGame.instIsWellFoundedIsOption : IsWellFounded FGame IsOption

theorem FGame.IsOption.irrefl (x : FGame) : ¬x.IsOption x

theorem FGame.self_notMem_leftMoves (x : FGame) : x ∉ x.leftMoves

theorem FGame.self_notMem_rightMoves (x : FGame) : x ∉ x.rightMoves

def FGame.ofLists (s t : List FGame) : FGame

Construct a FGame from its left and right lists. This is an auxiliary definition used to define the more general FGame.ofFinsets.

Equations

• FGame.ofLists s t = Quotient.finLiftOn₂ s.get t.get (fun (i : Fin s.length → SGame) (j : Fin t.length → SGame) => FGame.mk (SGame.mk s.length t.length i j)) ⋯

@[simp]

theorem FGame.leftMoves_ofLists {s t : List FGame} : (ofLists s t).leftMoves = s.toFinset

@[simp]

theorem FGame.rightMoves_ofLists {s t : List FGame} : (ofLists s t).rightMoves = t.toFinset

def FGame.ofFinsets (s t : Finset FGame) : FGame

Construct a FGame from its left and right finsets.

This is given notation {s | t}ꟳ, where the superscript F is to disambiguate from set builder notation, and from the analogous constructors on other game types.

Equations

• {s | t}ꟳ = Quotient.liftOn₂ s.val t.val FGame.ofLists FGame.ofFinsets._proof_1

def FGame.«term{_|_}ꟳ» : Lean.ParserDescr

Construct a FGame from its left and right finsets.

This is given notation {s | t}ꟳ, where the superscript F is to disambiguate from set builder notation, and from the analogous constructors on other game types.

Conventions for notations in identifiers:

• The recommended spelling of {· | ·}ꟳ in identifiers is ofFinsets.

Equations

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

@[simp]

theorem FGame.leftMoves_ofFinsets {s t : Finset FGame} : {s | t}ꟳ.leftMoves = s

@[simp]

theorem FGame.rightMoves_ofFinsets {s t : Finset FGame} : {s | t}ꟳ.rightMoves = t

def FGame.Subposition : FGame → FGame → Prop

A (proper) subposition is any game in the transitive closure of IsOption.

Equations

• FGame.Subposition = Relation.TransGen FGame.IsOption

theorem FGame.Subposition.of_mem_leftMoves {x y : FGame} (h : x ∈ y.leftMoves) : x.Subposition y

theorem FGame.Subposition.of_mem_rightMoves {x y : FGame} (h : x ∈ y.rightMoves) : x.Subposition y

theorem FGame.Subposition.trans {x y z : FGame} (h₁ : x.Subposition y) (h₂ : y.Subposition z) : x.Subposition z

instance FGame.instIsTransSubposition : IsTrans FGame Subposition

instance FGame.instIsWellFoundedSubposition : IsWellFounded FGame Subposition

instance FGame.instWellFoundedRelation : WellFoundedRelation FGame

Equations

• FGame.instWellFoundedRelation = { rel := FGame.Subposition, wf := ⋯ }

def FGame.tacticFgame_wf : Lean.ParserDescr

Discharges proof obligations of the form ⊢ Subposition .. arising in termination proofs of definitions using well-founded recursion on FGame.

Equations

• FGame.tacticFgame_wf = Lean.ParserDescr.node `FGame.tacticFgame_wf 1024 (Lean.ParserDescr.nonReservedSymbol "fgame_wf" false)

Basic games

instance FGame.instZero : Zero FGame

The game 0 = {∅ | ∅}ꟳ.

Equations

• FGame.instZero = { zero := {∅ | ∅}ꟳ }

theorem FGame.zero_def : 0 = {∅ | ∅}ꟳ

@[simp]

theorem FGame.leftMoves_zero : leftMoves 0 = ∅

@[simp]

theorem FGame.rightMoves_zero : rightMoves 0 = ∅

instance FGame.instOne : One FGame

The game 1 = {{0} | ∅}ꟳ.

Equations

• FGame.instOne = { one := {{0} | ∅}ꟳ }

theorem FGame.one_def : 1 = {{0} | ∅}ꟳ

@[simp]

theorem FGame.leftMoves_one : leftMoves 1 = {0}

@[simp]

theorem FGame.rightMoves_one : rightMoves 1 = ∅

Repr

unsafe instance FGame.instRepr : Repr FGame

The Repr of FGame. We confine inputs to {0} to make universe determinism easy on #eval, and we prefer our notation of games {{a, b, c}|{d, e, f}} over the usual flattened out one {a, b, c|d, e, f} to match with the IGame builder syntax.

Equations

• FGame.instRepr = { reprPrec := fun (g : FGame) (x : ℕ) => FGame.instRepr_aux✝ g }