Sylver coinage and ConcreteGame

Stream: combinatorial-games

[Junyan Xu]

I've defined the concrete impartial game of Sylver coinage here, shown it always terminates, solved a few simple positions, and listed Hutchings' theorem and corollaries as to-dos. I made a definition of P-position just for Sylver coinage, but it would work for any well-founded impartial game described by a relation / transition graph. Maybe this could inspire more work around ConcreteGame; for example, it might be more convenient if relLeft : α → α → Prop is replaced by LeftMoves : α → Type _ and moveLeft (a : α) : LeftMoves a → α.

[Violeta Hernández]

I'd be glad to help you port this over to our repo.

[Violeta Hernández]

The idea behind ConcreteGame is that it represents the directed graph of all possible states in a game.

[Violeta Hernández]

In the case of Sylver coinage, the type would be sets of named numbers, and the relation would be between s and insert a s when a is a valid new number to name.

[Violeta Hernández]

What would the benefit of LeftMoves and moveLeft be as you define them? I admit the use of dependent types makes me somewhat skeptical. PGame was awful to work with because of them.

[Violeta Hernández]

simp and aesop generally work much better at proving relations between sets than they do at proving relations between indexed families (especially when the index types aren't even def-eq!)

[Junyan Xu]

I mean that in this case it's more convenient if the moves are indexed by a subtype of Nat; I wrote two lemmas that quantifies over such moves, and introducing Left/RightMoves would allow you to state these lemmas as general API.

[Violeta Hernández]

Why can't these lemmas be general API as is?

[Violeta Hernández]

I prefer them much more to the dependently typed versions.

[Violeta Hernández]

The issue is, if you have two games that are prop-eq but not def-eq (a very common occurrence), then the same is true for the types indexing the moves of said games. Which means you have to introduce casts and heqs everywhere. Which sucks.

[Violeta Hernández]

That was the issue back when docs#PGame was still a part of the library, and in fact removing that type was the whole reason we made our own repo in the first place!

[Violeta Hernández]

I'm currently in the process of splitting ConcreteGame into a loopy and a well-founded counterpart. Once that's done we can add the Sylver coinage code.

[Junyan Xu]

I'd suggest that you include the type α in the structure ConcreteGame. For example for Sylver coinage it seems pointless to introduce a type synonym for Finset Nat in order to put a ConcreteGame instance on it. This will also make it clear that you shouldn't consider prop-eq between games because they include prop-eq between types. But a suitable quotient of ConcreteGame will be identifiable with IGame/LGame.

I think we should focus on usability and API for concrete games when developing ConcreteGame. The way humans play concrete games is to make moves that transition between states, rather than consider all possible states and check which ones have moves from the current state. We would like to quantify over moves rather than states. With the current definition you can make a constructor that collapses LeftMoves/moveLeft into relLeft (btw it should be RelLeft), and build APIs around the constructor, but it would be easier if you just build LeftMoves/moveLeft into the definition. (It might be better to allow an arbitrary type of labels instead of just Bool (left/right); we may build "ConcreteZFSet" with a single label and the von Neumann ordinal of a Lean Ordinal will simply be any representative well-ordered type of the Ordinal.)

[Violeta Hernández]

I'd suggest that you include the type α in the structure ConcreteGame.

How would this look for sylver coinage? What type would the instance exist on, if not on (an alias for) the type of states?

The way humans play concrete games is to make moves that transition between states, rather than consider all possible states and check which ones have moves from the current state.

This is true, and you can do this through the IGame.leftMoves / IGame.rightMoves functions, as you can for any other game.

(It might be better to allow an arbitrary type of labels instead of just Bool (left/right); we may build "ConcreteZFSet" with a single label and the von Neumann ordinal of a Lean Ordinal will simply be any representative well-ordered type of the Ordinal.)

I think the "correct" way to define ZFSet.{u} would be as the initial algebra of the functor fun α ↦ {x : Set α // Small.{u} x}. The two argument version of this is what we did for IGame, which has the benefit that we can also build the final co-algebra, which happens to be the type of loopy games LGame. I don't know if this can actually be implemented into Mathlib though, since as I understand it there are people who're very invested in keeping ZFSet and its constructors computable.

[Violeta Hernández]

(the final coalgebra corresponding to the ZFSet functor would give Aczel's non-well-founded set theory)

[Violeta Hernández]

This will also make it clear that you shouldn't consider prop-eq between games because they include prop-eq between types. But a suitable quotient of ConcreteGame will be identifiable with IGame/LGame.

I think there might be a misunderstanding. Prop-eq between games is fine and commonplace ever since we ditched docs#PGame for IGame. In our current setup even basic equations like x = {leftMoves x | rightMoves x} are not definitional. But since all the API is about sets rather than types of moves, there is no problem whatsoever.

Also, there isn't a type of ConcreteGames. The idea behind ConcreteGame is that you should be able to define an IGame (or really, an LGame) from its game graph. You're still ultimately working with IGame when you do this, rather than a new type of games.

[Violeta Hernández]

@Junyan Xu I've thought about this some more. Following LGame.corec, it makes sense to redefine ConcreteGame to use functions leftMoves : a -> Set a and rightMoves : a -> Set a rather than relations.

[Violeta Hernández]

After all, the function ConcreteGame.toLGame is nothing more than a call to LGame.corec!

[Violeta Hernández]

I agree that in the case of Sylver coinage it makes more sense to think of the options of a move as being indexed by a natural number, rather than a set of lists. I don't think we need dependent types to address this, though. We can define Sylver.cons in the obvious way, and prove that options of toIGame l look like toIGame (cons a l).

[Violeta Hernández]

On the topic of ConcreteGame. We currently have IGame.Poset and IGame.Domineering living in the IGame namespace. I don't like that as a pattern - we could conceivably define loopy versions of these games, or others in the future.

[Violeta Hernández]

What do you think about moving them to the ConcreteGame namespace?

[Violeta Hernández]

I've opened this PR: https://github.com/vihdzp/combinatorial-games/pull/174

[Junyan Xu]

I think the current ConcreteGame should be called GameGraph instead, and the actual ConcreteGame should take types Left/RightMoves as I suggested above. PR#174 doesn't really change the definition (it's defeq up to reordering). You can see the definition of PosetRel and relLeft/Right in Domineering all include an existential quantifier, and what they quantify over are exactly the moves. With the Outcome development, it would be nice to replace ∀ y ∈ x.leftMoves, by ∀ y : x.LeftMoves in user-facing API.
I also don't see the point of introducing a type synonym def Domineering := Finset (ℤ × ℤ) and def Poset (α : Type*) [Preorder α] := Set α with the to/ofDomineering/to/ofPoset auxiliary functions, which can be avoided if the type Finset (ℤ × ℤ)/Set α is included as a field of ConcreteGame. I might submit my version of PR#174 at some point. My version of Sylver coinage would be something like

structure ConcreteImpartialGame : Type (u + 1) where
  States : Type u -- maybe call it `Pos` instead
  Moves : States → Bool → Type u -- maybe allow a different universe
  move (s : States) {b : Bool} : Moves s b → States

def SylverCoinage : ConcreteImpartialGame.{0} where
  States := Set ℕ
  Moves s _b := {n : ℕ // n ∉ Ideal.span s ∧ n ≠ 1}
  move s _b n := insert n.1 s

[Violeta Hernández]

Again, I'm very heavily against this dependent type design. We've had trouble with this in the past with PGame. I'd rather not have to go through that again.

[Violeta Hernández]

Working with sets has done us wonders. Aesop in particular has had a lot of opportunity to shine, solving goals that were 30 lines or more in the old development.

[Violeta Hernández]

Also, ConcreteGame isn't supposed to be a structure. We're not really interested in the type of concrete games (or game graphs, if you prefer to call them that); rather, the class is supposed to function as a shortcut to build IGames and FGames in "realistic" scenarios.

[Aaron Liu]

I think this should be a structure rather than a class

[Violeta Hernández]

The type of game graphs is just FGame with worse equality. We don't need it.

[Aaron Liu]

docs#UniformSpace.Core is also just a shortcut to building uniform spaces but it's also a structure

[Aaron Liu]

This should not be a class

[Violeta Hernández]

Oh, I think I see what you mean now.

[Violeta Hernández]

I guess using a structure rather than a class would obviate the need for type aliases.

[Aaron Liu]

Not sure about bundling the type though

[Violeta Hernández]

Yeah, I agree with using a structure. I was just confused about what the motivation was.

[Violeta Hernández]

I don't agree with having a type of moves for every state. I think this is a really bad idea which has already failed us before.

[Violeta Hernández]

Aaron Liu said:

Not sure about bundling the type though

What's the alternative? Taking the type as an argument?

[Violeta Hernández]

Yeah, that does make more sense to me.

[Violeta Hernández]

Just to make sure. The idea would be to make functions, say, IGame.domineering, or IGame.sylver, instead of using ConcreteGame.toIGame for everything, right?

[Aaron Liu]

oh you can play sylver coinage on any noetherian semiring

[Aaron Liu]

or I guess any noetherian semimodule over any semiring

[Violeta Hernández]

Well presumably you can play it in any semiring, it just doesn't always terminate

[Aaron Liu]

yeah

[Junyan Xu]

oh you can play sylver coinage on any noetherian semiring

Great comment! Golfed wellFounded_rel accordingly.

[Junyan Xu]

Again, I'm very heavily against this dependent type design. We've had trouble with this in the past with PGame. I'd rather not have to go through that again.
Working with sets has done us wonders. Aesop in particular has had a lot of opportunity to shine, solving goals that were 30 lines or more in the old development.

Probably there's some misunderstanding; I'm not asking you to change the definition of IGame or LGame or forbid you to work with sets. Even without changing the definition of ConcreteGame, we still have to provide a constructor for game graphs starting from types of moves and functions from moves to positions, and I'm just suggesting wrapping the inputs of the constructor into a structure. You take the ranges of the functions from moves to positions when you pass from concrete games to game graphs, and you'll continue to use sets and relations and aesop once you're in the world of game graphs.

We're not going to work with equalities in ConcreteGame or GameGraph, but it would be an interesting problem to define an equivalence relation on GameGraphs with a starting position such that GameGraph.toLGame identifies the quotient with LGame.

[Violeta Hernández]

Well, if the idea is to state results on LGame and IGame in the set form, then what's the advantage of using the dependent types in ConcreteGame?

[Violeta Hernández]

The whole concept of building a game from its graph is what the corecursor on LGame is doing. I don't see a reason to not just copy down that design.

[Junyan Xu]

I'm not concerned with building a game from its graph, I'm concerned with building a graph from the moves. You can't use the same type for all positions, because available moves depend on the position. In the case of Sylver coinage, the type of moves is {n : ℕ // n ∉ Ideal.span s ∧ n ≠ 1} which depends on s (more precisely the predicate defining the subtype depends on s even though the ambient type ℕ doesn't).

[Violeta Hernández]

Again, I'd rather we just write down the sets of left and right options explicitly.

[Violeta Hernández]

We then could (and should) add a simp lemma that "for all left options x of a Sylver coinage position, P x" is equivalent to "for every natural number not in the span, P n"

[Violeta Hernández]

(I hope I'm not coming off as too harsh. I'd like to hear someone else's opinion on this DTT design.)

[Junyan Xu]

Instead of writing that lemma only for Sylver coinage, I'd write a generic lemma that also applies to e.g. poset games and domineering. Maybe another simp lemma for the case that the type of moves is a subtype.

[Violeta Hernández]

I don't think there's really a generic lemma here. The best way to write down left/right options of a game depends heavily on how that game is defined

[Violeta Hernández]

Compare e.g. forall_leftMoves_neg, forall_leftMoves_add, and forall_leftMoves_mul.

[Junyan Xu]

You're saying that the type of moves may have multiple constructors so one forall over the type might break into a conjunction of foralls. This is a valid concern and occurs in concrete games like chess where you first choose a piece to move and then which square to move to (depending on the piece). I think the single constructor case still applies to a lot of games, but I agree maybe we should name it SingleConstructorCore rather than ConcreteGame.

[Junyan Xu]

or I guess any noetherian semimodule over any semiring

It seems possible to unify this with poset games under the following general setting: given a type T and a closure operator on it, we construct the game with positions Set T, and the moves available at a position s : Set T are elements of T not contained in the closure of s. For poset games we take the upper closure of s while for Sylver coinage we take the subsemimodule spanned by s.

[Violeta Hernández]

Junyan Xu said:

You're saying that the type of moves may have multiple constructors so one forall over the type might break into a conjunction of foralls.

More generally than that, there are usually "nice" ways to index moves in forall/exist, and instead of using the "every position has a type of moves" idea, we can simply use lemmas of this type to achieve the same ease of use.

[Violeta Hernández]

Junyan Xu said:

or I guess any noetherian semimodule over any semiring

It seems possible to unify this with poset games under the following general setting: given a type T and a closure operator on it, we construct the game with positions Set T, and the moves available at a position s : Set T are elements of T not contained in the closure of s. For poset games we take the upper closure of s while for Sylver coinage we take the subsemimodule spanned by s.

That's an interesting idea. Does "closure operator" just mean any function a -> Set a? Or is there some more specific condition? And can we state a general termination condition, that translates to being a WQO in the poset case, and to being noetherian in the Sylver coinage case?

[Aaron Liu]

docs#ClosureOperator

[Aaron Liu]

it's the reflector for a reflective subcategory of a preorder α viewed as a thin category

[Violeta Hernández]

I don't know what those words mean :frown:

[Violeta Hernández]

But I can understand "function with similar order properties to the closure operator of a topological space"

[Violeta Hernández]

Wait. Say we have a game that can sometimes be loopy/infinite but which can sometimes be well-founded. Under suitable assumptions, Sylver coinage and poset games are examples of this.

If we make concrete games a class, this isn't an issue. We can make the well-founded class extend the loopy class, which makes toIGame and toLGame both available under the suitable typeclass assumptions.

If we make them a structure, doesn't that mean we have to choose one of two structures (the loopy or the well-founded one) to state our results?

[Violeta Hernández]

A solution would be to, for every game, choose whether we're going to treat it as an IGame or an LGame. That feels like a weird decision. e.g. poset games are better studied in the well-founded case. But does that mean that we shouldn't allow for the loopy case? Or does that mean that we'd have to create two structures ConcreteIGame.Poset and ConcreteLGame.Poset just to state the results?

[Violeta Hernández]

(though thinking about it. Maybe the idea is that you use the structures to define the toIGame and toLGame functions, and then never make reference to the structure again?)

[Aaron Liu]

I think the idea is to prove theorems about the class

[Aaron Liu]

or not the class but the type that holds your stuff

[Aaron Liu]

hmmmm should ConcreteGame be a class after all?

[Violeta Hernández]

I like that the structure approach gets rid of the need for type aliases.

[Aaron Liu]

It feels similar to proving theorems about a type like docs#WithTop which gains more properties as the base type gains properties (preorder -> partial order -> semilattice -> lattice -> ...)

[Aaron Liu]

but in this case there is only one property, which is well-foundedness

[Violeta Hernández]

Maybe we should fully Lean into the idea of having these types as mere auxiliaries.

[Violeta Hernández]

You define your structures representing your games. You use those to define the maps into IGame and/or LGame. Maybe you're able to prove some properties like Impartial and Dicotic more easily. But after that, you don't touch the concrete classes anymore.

[Violeta Hernández]

Under that philosophy it's not really an issue to have redundancy in ConcreteIGame / ConcreteLGame. You're not using these to state the public API anyways.

[Aaron Liu]

sure that works?

[Aaron Liu]

yeah that works

[Violeta Hernández]

@Junyan Xu what do you think about that design?

[Junyan Xu]

I think ConcreteGame (GameGraph) need not bundle the well-founded condition; you can have a ConcreteGame.toLGame constructor and also .toIGame given a [IsWellFounded IsOption] argument (in fact you only need Acc IsOption startPosition).
It might be beneficial to introduce HasLeft/RightMoves typeclasses of which IGame, LGame and the positions in any ConcreteGame could all be instances. Then you can define IsOption/Subposition and IsLeft/RightWin/Loss/Draw uniformly for all three. Otherwise you may want to state all results using ConcreteGame since it's the most general.

[Junyan Xu]

And can we state a general termination condition, that translates to being a WQO in the poset case, and to being noetherian in the Sylver coinage case?

I think the termination condition is the ascending chain condition on closed subsets.

[Aaron Liu]

Equivalently, every closed subset is finitely generated (the closure of a finite set)

[Junyan Xu]

In order to show the union of a chain of a closed sets is closed, you need that every element in the closure of a set is in the closure of some finite subset, which is satisfied by poset games (every element is in the closure of a single element) and Sylver coinage, but not for e.g. topological closure. (This goes inside the argument that every closed set is f.g. ⇒ WellFoundedGT on closed sets)

[Aaron Liu]

Junyan Xu said:

In order to show the union of a chain of a closed sets is closed, you need that every element in the closure of a set is in the closure of some finite subset, which is satisfied by poset games (every element is in the closure of a single element) and Sylver coinage, but not for e.g. topological closure. (This goes inside the argument that every closed set is f.g. ⇒ WellFoundedGT on closed sets)

What do you mean? Can you explain?

[Junyan Xu]

The prime spectrum of Z with the Zariski topology is an example of a topological space failing ACC on closed subsets (it's closed subsets are finite subsets of the complement of the zero ideal and the whole space), but every closed subset is the closure of a finite subset (since the whole space is the closure of the generic point (the zero ideal)).
(Gemini came up with an equivalent example by constructing a topology on Nat adjoining a point.)

Spaces satisfying ACC on closed subsets are called Artinian in some online posts, but it might be better to call them co-Noetherian, since they have nothing to do with Artinian rings.

[Aaron Liu]

oh I see where I went wrong

[Aaron Liu]

yeah that makes sense

[Aaron Liu]

yeah since it doesn't preserve filtered colimits

[Junyan Xu]

https://mathoverflow.net/questions/93276/a-game-on-noetherian-rings is apparently exactly the generalization of Sylver coinage to rings, also played under the misere convention (by requiring choosing a non-unit).

[Violeta Hernández]

This paper is linked in the answers, might be an interesting thing to work towards formalizing.
https://arxiv.org/abs/1205.2884

[Junyan Xu]

One issue of unifying poset games and Sylver coinage is that the positions in poset games are represented as sets of playable moves (in particular they're complements of closed sets), while in Sylver coinage they're usually represented as sets of played moves (contained in the closed sets of non-playable moves). If we want to unify both we'll need to change one of them ...

[Violeta Hernández]

It seems much more natural to do the former. If after two sequences of moves you have the same options, it doesn't make much sense to distinguish them.

[Violeta Hernández]

(In fact, by extensionality, these games would be equal)

[Junyan Xu]

Yeah, two sets with the same closure describe equivalent positions in Sylver coinage, so equal when passed to IGame/LGame. However, note that the number of played moves is always finite, but the number of playble moves is often infinite, so of course you see positions always described as sets of played moves in the literature.

[Violeta Hernández]

I think that's just a matter of how we write the theorems. If f is the function returning the playable moves from a set of played moves, we can prove that the left moves of f s look like f (insert n s) for n such that (...)

[Junyan Xu]

It seems much more natural to do the former.

IMO the latter (Sylver coinage's convention) is more natural because the position changes are just $s\mapsto s\cup\{a\}$ (and playable moves are $\overline{s}^c$). While with the former (poset game's convention), the position changes come with double negation $s\rightsquigarrow\overline{s^c\cup\{a\}}^c$, even though the playable are simply $s$. (Here $s$ denotes the set representing the position and overline denotes closure). Admittedly in the special case of poset games the position changes boil down to the simpler $s\rightsquigarrow s\setminus\overline{\{a\}}$, and if you play them on a finite poset the positions are finite under both conventions, but the latter convention still likely gives shorter description of the positions.

[Violeta Hernández]

Hmm. Yeah, that double negation is annoying.

[Violeta Hernández]

I guess we could do the former, and prove a lemma that if $\overline s = \overline t$ then the games are equal.

[Aaron Liu]

Can't we just use the closure of the played moves to describe the position?

[Aaron Liu]

Since equal closures means equal games

[Violeta Hernández]

How would that work?

[Aaron Liu]

wdym?

[Violeta Hernández]

Surely requiring toIGame to take an argument IsClosed s is more annoying than to just make it take the closure internally.

[Aaron Liu]

oh yeah just don't do that

[Aaron Liu]

make it return junk values

[Aaron Liu]

none of the math for calculating the moves actually requires your set be closed

[Aaron Liu]

but every move will take you to a closed position since you take the closure

[Violeta Hernández]

So from a position s the moves are to the closures of positions in ${\overline s}^c$, is that what you're saying?

[Aaron Liu]

maybe I'm misunderstanding what this closure thing is

[Violeta Hernández]

I've just been thinking about it like it's a topological space

[Aaron Liu]

I've been thinking of it like docs#Subgroup.closure or docs#Ideal.span or docs#upperClosure or docs#IntermediateField.adjoin

[Violeta Hernández]

Aaron Liu said:

make it return junk values

Surely the junk value for s can just be the actual value for its closure?

[Aaron Liu]

but what does this closure operater represent again?

[Aaron Liu]

I have forgotten

[Violeta Hernández]

The closure basically represents the moves you've exhausted

[Violeta Hernández]

In the poset game it's the upper closure of your set

[Violeta Hernández]

In Sylver coinage it's the span of your set

[Violeta Hernández]

You can't choose positions in there

[Aaron Liu]

oh ok

[Aaron Liu]

so how do you plan to take this closure operator

[Violeta Hernández]

Wdym by "take it"?

[Aaron Liu]

like as an argument

[Violeta Hernández]

We can define a function ClosureIGame f s taking a closure operation f and a position s

[Aaron Liu]

to your game building function

[Violeta Hernández]

Then we can define poset games, Sylver coinage, etc. in terms of this

[Aaron Liu]

is f just a function? will I have to pass around the proof that it's a closure operator?

[Violeta Hernández]

docs#ClosureOperator is a structure

[Aaron Liu]

can we use docs#LowerAdjoint instead?

[Aaron Liu]

I noticed it in the same file

[Aaron Liu]

hmmm actually maybe not since it doesn't

[Aaron Liu]

ok yeah I have no idea

[Aaron Liu]

oh we have docs#GaloisInsertion

[Aaron Liu]

yknow what it actually doesn't matter to me how we represent the moves

[Aaron Liu]

anything that works is fine

[Violeta Hernández]

@Junyan Xu I've completely redone #174, making ConcreteGame into a single structure. This is definitely much cleaner! No need for type aliases all over the place anymore.

[Violeta Hernández]

I do have a certain design question

[Violeta Hernández]

Where should we put stuff like the poset to IGame function, or the domineering to IGame function?

[Violeta Hernández]

Or more broadly, the material about these functions.

[Violeta Hernández]

It feels weird to put the stuff about PosetRel in the root namespace. But it also feels weird putting it in IGame - what if we ever want to define a loopy poset game? And it also feels weird putting it in LGame.

[Violeta Hernández]

What do you think about this:

• Put all the "preliminary" material about a given game in a namespace inside the ConcreteGame namespace, e.g. ConcreteGame.Poset for preliminaries on poset games, ConcreteGame.Domineering for preliminaries on domineering.
• Put results on IGame/LGame/whatever of these games in the appropriate namespace, e.g. IGame.poset_univ_fuzzy_zero

[Junyan Xu]

I think I'd put everything under the ConcreteGame.<NameOfGame> namespace. Results about the corresponding abstract games might be distinguished by subscripts ᵢ ₗ if IGame/LGame is too cumbersome to type.

[Violeta Hernández]

I don't know how I feel about the subscript idea, but I guess we could define e.g. ConcreteGame.Poset.toIGame and ConcreteGame.Poset.toLGame and just write toIGame / toLGame in theorems.

[Violeta Hernández]

So, now that ConcreteGame has been refactored (twice), how should we use it to formalize this?

[Violeta Hernández]

I imagine ClosureGame would be the concrete game, which takes a closure operator f on Set a, where moves s = (insert . s) '' (f s)^C

[Violeta Hernández]

Making an LGame from this is simple enough. But how would we state the well-foundedness condition?

[Violeta Hernández]

I think it'd have to be a case by case basis

[Violeta Hernández]

Well, before I do anything of the sort, there are a few more changes I want to do with ConcreteGame, so that the API fits Yuyang Zhao's refactor better: #210

[Violeta Hernández]

Though thinking about this a bit more... Would defining closureGame really gain us anything?

[Violeta Hernández]

Sure, both games are a special case of that, but is there anything whatsoever we can say about closureGame in the general case?

[Violeta Hernández]

@Junyan Xu

[Junyan Xu]

Sorry I've been busy lately. I wouldn't have the time to refactor posetGame using closureGame, and it probably is the easiest to add Sylver coinage directly rather than going through closureGame. Sylver coinage is removed from #27743 for now. However there's an issue about dependencies between projects downstream of mathlib that I communicated with Johan Commelin in private message:

There are some open conjectures around Sylver coinage which I intend to PR to the formal conjectures repo. If the definition of Sylver coinage isn't in mathlib but only in combinatorial-games, then I think I either need to copy the code over to the formal conjectures repo, or else make combinatorial-games a dependency of formal conjectures (I'm not sure they'd accept this dependency).

[Violeta Hernández]

There are more conjectures about combinatorial games we could potentially add. One of them currently exists as a proof_wanted, being the inequality:

proof_wanted birthday_mul_le (x y : Surreal) : (x * y).birthday ≤ x.birthday * y.birthday

I do think it probably makes sense to keep the repositories separate, though. The CGT repo is a bit volatile in its current state. We haven't yet had to seriously consider having downstream dependents.

[Violeta Hernández]

I think the best thing is probably to re-define Sylver coinage as a game using machinery other than IGame (i.e. copy over the code you had about P-positions and such).

[Violeta Hernández]

Junyan Xu said:

I wouldn't have the time to refactor posetGame using closureGame

I can do that, if that's what we want to do. My question is rather whether there are any benefits to doing so. Are there any theorems about either poset games or Sylver coinage that generalize to that setting? Or at the very least, is the construction of either game made simpler by establishing this common groundwork first?

[Violeta Hernández]

I'd really like to have an answer to this. It's blocking work on both Sylver coinage and poset games.

[Violeta Hernández]

I guess I could just try implementing ClosureGame and see how that goes

[Violeta Hernández]

Ok yeah there are certainly a few nontrivial results we'd otherwise have to prove twice

[Violeta Hernández]

One that immediately comes to mind is "the positions accessible from the empty set are finite sets"

[Violeta Hernández]

There's also this:

instance (f : ClosureOperator (Set α)) [WellFoundedGT (Subtype f.IsClosed)] :
    IsWellFounded _ (closureGame f).IsOption := by
  sorry

[Violeta Hernández]

On a somewhat unrelated note, I realize that ConcreteGame isn't a very informative name

[Violeta Hernández]

What do you think about renaming it to GameGraph or even just Graph?

[Violeta Hernández]

Isn't it a bit weird that we have

theorem toLGame_congr (h : f s = f t) :
    (closureGame f).toLGame s = (closureGame f).toLGame t := by
  sorry

Why not just define the states of closureGame as f.Closeds?

[Junyan Xu]

sounds reasonable to me

[Aaron Liu]

Violeta Hernández said:

Isn't it a bit weird that we have

theorem toLGame_congr (h : f s = f t) :
    (closureGame f).toLGame s = (closureGame f).toLGame t := by
  sorry

Why not just define the states of closureGame as f.Closeds?

That's what I said

[Violeta Hernández]

Just realized something cool: WellQuasiOrderedLE a -> WellFoundedLT (UpperSet a)

[Aaron Liu]

what's the LT on UpperSet

[Violeta Hernández]

the wrong one

[Aaron Liu]

which one is that

[Violeta Hernández]

Opposite of subset

[Aaron Liu]

oh well yeah that's literally one of the definitions