What to do about PGame

Stream: maths

[Violeta Hernández]

So, it's well-known that PGame isn't the "correct" mathematical notion for games, in the sense that its equality is much stricter and depends on type equality.

[Violeta Hernández]

Now that we finally have docs#SetTheory.PGame.Identical (which means we will soon have IGame), my question is: what will happen to docs#PGame and its API?

[Violeta Hernández]

Is the idea that we port all of the PGame API to IGame and deprecate it? Or is the idea to duplicate everything? Or something in between?

[Violeta Hernández]

@Yuyang Zhao

[Violeta Hernández]

I'm not sure if there's Mathlib precedent for having an auxiliary type you have to do things in first even if it's not mathematically correct

[Violeta Hernández]

Like, there's docs#PSet and docs#ONote, but I don't think either of them have very developed APIs

[Yury G. Kudryashov]

Is PGame useful for encoding combinatorial games (e.g., those that appear in math contests) or not at all?

[Violeta Hernández]

It can be used for that. IGame could also be used for that.

[Violeta Hernández]

But PGame seems strictly less convenient in my view. To give an example that currently exists in Mathlib, we can define docs#SetTheory.PGame.nim perfectly well. But the equality nim 0 = 0 is unprovable, because one game's moves are indexed by PEmpty, while the other are indexed by Ordinal.toType 0. These are two empty types which aren't intensionally equal, and thus can't be proven (or disproven) to be equal.

[Violeta Hernández]

Meanwhile for IGame we could in fact prove nim 0 = 0, as two empty games are always docs#SetTheory.PGame.Identical

[Violeta Hernández]

We could define both PGame.nim and IGame.nim, and I would expect the transfer of results from one to the other to be relatively simple. My question is whether we want to duplicate API like this and to what extent.

[Violeta Hernández]

(And what about the other quotients? Does having IGame.nim warrant a Game.nim as well?)

[Tristan Figueroa-Reid]

Violeta Hernández said:

Is the idea that we port all of the PGame API to IGame and deprecate it? Or is the idea to duplicate everything? Or something in between?

There's some use in the theorems in PGame.lean, but any of the other results in other files that are based off of PGame, other than constructing Game, seem better suited to be constructed to some IGame directly. From looking over PSet and ONote, that seems like the most common way to go. Though, I haven't used lean much, so I'm unaware of any better design pattern for this.

[Violeta Hernández]

Personally the takeaway I get from PSet and ONote is that these auxiliary types are useful for easily constructing definitions and proving their basic properties, whereas the types ZFSet and NONote are meant for public use once the basic API is finished.

[Tristan Figueroa-Reid]

Why wasn't Nim and Surreal built on Game from Basic.lean? I assume the motivation for developing theory on IGame instead of PGame operates under the assumption that PGame/IGame will be the used API, but wouldn't Game be the designated public use API?

[Tristan Figueroa-Reid]

It would be extremely nice if there was, for a lack of a better term, a way to lift the equivalence of definitions.

For example, with the recent PR for removing options (https://github.com/leanprover-community/mathlib4/pull/20170), it would be great if instead of having to copy over the definition, you can say IGame.removeLeft is the same as PGame.removeLeft with = being defined as the equivalence relation for IGame.

[Mitchell Lee]

It is not true that removing a left option from a PGame removes the corresponding left option from the corresponding IGame. Also, if it were true, it would be a theorem that needs to be proved.

[Tristan Figueroa-Reid]

Yes, lift was a terrible word to use there. You are right - it isn't true.

[Tristan Figueroa-Reid]

Also, since removeLeft/Right takes in an argument for a type, a rewrite like that would not work. My bad.

[Mitchell Lee]

Maybe I'm missing something important, but the decision to build up the theory on PGame rather than IGame strikes me as similar to the decision to define a basis of a vector space as an indexed family of vectors rather than as a set of vectors. In other words, I don't see how it should meaningfully affect the theory.

[Mitchell Lee]

With that said, building up the theory on IGame does have one significant upside, which is that identity is now literally an equality (=), so it can be used with rw and simp.

[Tristan Figueroa-Reid]

Mitchell Lee said:

Maybe I'm missing something important, but the decision to build up the theory on PGame rather than IGame strikes me as similar to the decision to define a basis of a vector space as an indexed family of vectors rather than as a set of vectors. In other words, I don't see how it should meaningfully affect the theory.

I believe the original PGame construction was because it was much more convenient to construct a Game if one could say that Game was PGame quotient with the equivalence relation built on top of Equiv rather than building Game directly.

Plus, PGame, as we discussed earlier, is not standard in combinatorial game theory literature:

Violeta Hernández said:

So, it's well-known that PGame isn't the "correct" mathematical notion for games, in the sense that its equality is much stricter and depends on type equality.

[Tristan Figueroa-Reid]

*The point of that message was to say that PGame's construction was most likely not a purposeful decision as a good idea to have, but rather a decision that was necessary or helpful to develop Game. I believe the comments over Game both old and new hint to such a reason.

[Tristan Figueroa-Reid]

Though, PGame is still useful outside of constructing Game: i.e. PGame.Shortis computable while a IGame.Short or Game.Short wouldn't be, so any State game would have to be able to instantiate PGame.Short.

[Violeta Hernández]

Tristan Figueroa-Reid said:

Why wasn't Nim and Surreal built on Game from Basic.lean? I assume the motivation for developing theory on IGame instead of PGame operates under the assumption that PGame/IGame will be the used API, but wouldn't Game be the designated public use API?

As for nim, the correct generality for any concrete game (i.e. a game with a fixed set of left and right moves) is IGame. Once that drops, we can rework the file around it.

As for surreal numbers, that's just a different choice of quotients. A lot of the proof of the well-definedness of surreal multiplication makes use of game arithmetic, so there's a real argument for Game being the correct structure, though someone would have to do the replacement and check.

[Violeta Hernández]

With how much IGame keeps coming up, I think we should work on getting it into Mathlib ASAP. How should we go about doing that?

My idea is, we create a new IGame file (to stop bloating the PGame file) and slowly port over functionality. If there's any definitions (like option removal) that only really make sense for IGame rather than PGame, we can take them out/deprecate them.

[Violeta Hernández]

A lot of the stuff on the PGame are really order lemmas that work on any preorder. We won't have to port any of that, as we can just generalize it instead. (I'm already currently working on that)

[Tristan Figueroa-Reid]

Violeta Hernández said:

With how much IGame keeps coming up, I think we should work on getting it into Mathlib ASAP. How should we go about doing that?

My idea is, we create a new IGame file (to stop bloating the PGame file) and slowly port over functionality. If there's any definitions (like option removal) that only really make sense for IGame rather than PGame, we can take them out/deprecate them.

I can try working on it. I'll make a base IGame definition PR first, then we can discuss potential deprecations.

[Tristan Figueroa-Reid]

Also, Relabelling still is planned to be deprecated, right?

[Violeta Hernández]

I don't see any reason for keeping it around.

[Tristan Figueroa-Reid]

Violeta Hernández said:

I don't see any reason for keeping it around.

Alright. I was just wondering to ensure that the new theorems I produced for Identical don't rely on Relabelling.

[Tristan Figueroa-Reid]

Though, I do see a single use for Relabelling: One could probably show that if x is PGame.Short and x ≡r y, then y is Short, which was mentioned in the original Combinatorial Game Theory pull request: that theorem would be useful for computability. If we document why we prefer Identical over Relabelling, it seems safe to keep Relabelling around and not deprecate it.

[Yuyang Zhao]

There is already PR #14760 for IGame. Maybe it doesn't actually need #7162, but at least it needs to merge #5901 first.

[Tristan Figueroa-Reid]

Yuyang Zhao said:

There is already PR #14760 for IGame. Maybe it doesn't actually need #7162, but at least it needs to merge #5901 first.

Right! Did #5901 go stale?

[Yuyang Zhao]

No one has approved this PR until now. @Violeta Hernández Do I need to split #5901 further?

[Tristan Figueroa-Reid]

Also, #5901 conflicts with https://github.com/leanprover-community/mathlib4/pull/20149/files, though I believe the theorems related to that are simpler in #5901 than currently.

[Violeta Hernández]

Tristan Figueroa-Reid said:

Though, I do see a single use for Relabelling: One could probably show that if x is PGame.Short and x ≡r y, then y is Short, which was mentioned in the original Combinatorial Game Theory pull request: that theorem would be useful for computability. If we document why we prefer Identical over Relabelling, it seems safe to keep Relabelling around and not deprecate it.

I'm not convinced. Again, the issue is that Relabelling is exposing an implementation detail within type theory that wouldn't arise in a set theoretic treatment of games.

Here's another idea: why not create a separate structure for short games? Something like ShortGame or whatnot, whose constructors are families indexed by a Fintype. We can then define the conversion from this type into PGame and such, and show the comparison operations are all decidable.

Alternatively... Is computability ever going to be an actual concern? Even basic games are very difficult to compare using only the naive definitions. If I'm not mistaken, the size of the game tree for n * n grows superexponentially.

[Mitchell Lee]

I don't see any reason it shouldn't already be possible to do computations with a short IGame, provided that SetTheory.IGame.Short is data rather than merely a proposition. (Specifically, it would be the data of a short PGame that is in the identity class defined by the IGame.)

[Tristan Figueroa-Reid]

Mitchell Lee said:

I don't see any reason it shouldn't already be possible to do computations with a short IGame, provided that SetTheory.IGame.Short is data rather than merely a proposition. (Specifically, it would be the data of a short PGame that is in the identity class defined by the IGame.)

Right! That does definitely make Relabelling superficial then.

[Violeta Hernández]

Yuyang Zhao said:

No one has approved this PR until now. Violeta Hernández Do I need to split #5901 further?

I'll do another pass-through :smile:

[Violeta Hernández]

Tristan Figueroa-Reid said:

It would be extremely nice if there was, for a lack of a better term, a way to lift the equivalence of definitions.

For example, with the recent PR for removing options (https://github.com/leanprover-community/mathlib4/pull/20170), it would be great if instead of having to copy over the definition, you can say IGame.removeLeft is the same as PGame.removeLeft with = being defined as the equivalence relation for IGame.

We do have that, in the form of Quotient.lift. If you can prove that x ≈ y → f x = f y, then you can define a function g on the quotient such that g ⟦x⟧ = f x definitionally. And usually after that point, a lot of the API trivially carries over.

The issue is that by defining the option removal function as you are, this property is false.

[Violeta Hernández]

Violeta Hernández said:

Yuyang Zhao said:

No one has approved this PR until now. Violeta Hernández Do I need to split #5901 further?

I'll do another pass-through :smile:

Sorry for the delay! Left a review earlier today.

[Violeta Hernández]

Relating to all of this. Since IGame will serve as a second quotient on PGame, we won't be able to use quotient notation on both. And I think the approach that makes most sense is to use quotient notation on neither.

[Violeta Hernández]

That is, instead of writing [[x]], we'd write Game.mk or IGame.mk. What do you think?

[Violeta Hernández]

A corollary of this is that we wouldn't be able to use ≈ as notation for Setoid.r either. We could instead make it local notation for AntisymmRel.

[Violeta Hernández]

When that happens, should we replace equiv by antisymmRel in theorem names, or do we keep it as is?

[Violeta Hernández]

@Tristan Figueroa-Reid

[Tristan Figueroa-Reid]

I would put a quotient on IGame, as I think IGame would be used much more than Game.

[Violeta Hernández]

I think both are pretty important quotients. Even though IGame is what we talk about most, passing to Game is a very useful tool to prove inequalities.

[Violeta Hernández]

(also, I understand that global setoid notation is getting phased out anyways)

[Tristan Figueroa-Reid]

Violeta Hernández said:

(also, I understand that global setoid notation is getting phased out anyways)

Oh! Interesting!

[Aaron Liu]

I want to hear more about this too: why?

[Violeta Hernández]

Well, this is hearsay from @Eric Wieser in another thread

[Tristan Figueroa-Reid]

Violeta Hernández said:

I think both are pretty important quotients. Even though IGame is what we talk about most, passing to Game is a very useful tool to prove inequalities.

Right - I forgot about that. It makes sense to remove quotient notation fully, then :+1: