formalizing topology games in a library depending on mathlib

Stream: new members

[Steven Clontz]

I'm interested in starting to formalize my research in my own Lean library depending on mathlib. The plan is to start with the theory of selection games but starting from scratch is proving to be harder than working on mathlib itself. I was able to use https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency to set up https://github.com/StevenClontz/formalized-selection-games but I would love some hints/guidance on the "right" way to start modeling a new mathematical object in Lean. (Note that selection games do not terminate after finitely-many rounds so I cannot build on top of games in the sense of Conway.)

[Daniel Weber]

Could you explain the definition of a selection game, and some operations you often do with them? I can't understand it from the Wikipedia article

[Steven Clontz]

Sure thing. A selection game $G_1(\mathcal A,\mathcal B)$ is played as follows for any sets $\mathcal A,\mathcal B$:

• During round $n\in\mathbb N$, P1 chooses some $A_n\in\mathcal A$.
• Then, P2 chooses some $b_n\in A_n$.

So a playthrough of the game is a sequence $A_0,b_0,A_1,b_1,\dots$. We say P2 wins this game if the set $\{b_n:n\in\mathbb N\}\in\mathcal B$; otherwise P1 wins.

Example of use: The W-space property which lays properly between first-countable and sequential is equivalent to P1 having a winning strategy in the game $G_1(\mathcal T_x,\neg\Gamma_x)$ at each point $x$ of the space, where $\mathcal T_x$ is the set of (open) neighborhoods of $x$, and $\neg\Gamma_x$ is the set of ranges of sequences that do not converge to $x$. And first-countability is equivalent to P1 having a winning predetermined strategy (a strategy that ignores the selections of P2).

My ham-fisted attempt to model this is at https://github.com/StevenClontz/formalized-selection-games/blob/main/SelectionGames/Basic.lean :

import Mathlib.Data.Set.Defs
import Mathlib.Data.Set.Operations
open Set Function

variable {X : Type}

structure SGame (X) where
  A : Set (Set X)
  B : Set (Set X)

structure SGame.Play (g : SGame X) where
  Moves₁ : ℕ → Set X
  Moves₂ : ℕ → X
  Legal₁ : ∀ n, Moves₁ n ∈ g.A
  Legal₂ : ∀ n, Moves₂ n ∈ Moves₁ n

def SGame.OneWins (g : SGame X) (p : g.Play) : Prop :=
  range p.Moves₂ ∈ g.B

def SGame.TwoWins (g : SGame X) (p : g.Play) : Prop :=
  ¬ g.OneWins p

structure SGame.OnePre (g : SGame X) where
  Moves : ℕ → Set X
  Legal : ∀ n, Moves n ∈ g.A

def SGame.Principle (g : SGame X) : Prop :=
  ∀ σ : g.OnePre, ∃ p : g.Play, p.Moves₁ = σ.Moves ∧ g.TwoWins p

[Sven Manthe]

I'm sorry for the self-advertisement, but since your selection games are a particular case of Gale-Stewart games, you might be interested in https://leanprover.zulipchat.com/#narrow/channel/113486-announce/topic/Borel.20determinacy (although the theorem does not apply in most cases).

[Steven Clontz]

While the theorem doesn't apply to this work directly, I certainly could implement a selection game as a Gale-Stewart game, or in any case, use that GitHub as hints for my own work. Thank you for sharing!