Nat → PGame cast, again

Stream: mathlib4

[Violeta Hernández]

Thinking back to this instance. I don't know if we should even have it.

[Violeta Hernández]

docs#SetTheory.PGame.instNatCast

[Violeta Hernández]

The issue is: this doesn't match the usual definition of natural numbers as games through the correspondence n = {0, 1, ..., n - 1 | }

[Violeta Hernández]

We have this definition but for greater generality as docs#Ordinal.toPGame. But that file imports both PGame and Game, so if we define the NatCast there, by that point, we will already have defined NatCast on Game.

[Violeta Hernández]

I guess we could split the file in two. Make it strictly about PGame, then make the Game file import it, and move the results on Game to the end of it.

[Violeta Hernández]

Yeah, I'm also realizing now that we will need this NatCast instance if we want to talk about small games or dyadic numbers.

[Violeta Hernández]

There's another problem though. If we define NatCast like this, we don't have the equalities ↑0 = 0, ↑1 = 1, or ↑(n + 1) = ↑n + 1. The last one is unavoidable, but the other two are certainly annoying.

[Violeta Hernández]

So maybe the actual solution is to move Ordinal.toPGame to the PGame file? And define 0 = toPGame 0 and 1 = toPGame 1.

[Violeta Hernández]

Yeah, I know def-eqs are evil and especially when it comes to types, but it is pretty jarring to talk about (0 : ℕ) and (1 : ℕ) and not being able to just write 0 or 1

[Eric Wieser]

Violeta Hernández said:

The issue is: this doesn't match the usual definition of natural numbers as games through the correspondence n = {0, 1, ..., n - 1 | }

What goes wrong if you define it this way, and then define the Zero/One instances as natCast 0/natCast 1?

[Violeta Hernández]

There's nothing that really goes wrong, it's just that either we end up duplicating this definition later with Ordinal.toPGame, or we have to move Ordinal.toPGame much earlier

[Violeta Hernández]

Well... There is something that might go wrong. The proofs we have of the arithmetical properties are pretty convoluted, and a lot of them simply case on a PGame to avoid having to use the moveLeft / moveRight API.

[Violeta Hernández]

In particular, we got a bunch of proofs that currently use the fact that the left moves of 1 are indexed by PUnit

[Violeta Hernández]

If we did the redefinition in terms of Ordinal.toPGame, the new type of moves would be the much uglier Ordinal.toType 1.

[Violeta Hernández]

This does have a Uniqueinstance, but working with this is in fact somewhat less direct then just using Unit

[Violeta Hernández]

I'm also just a bit skeptical about defining ordinal games before even defining 0 or 1, could we even prove what we want about them?

[Violeta Hernández]

Unless we just made the definition but didn't develop the API for anything other than 0 or 1 till much later

[Violeta Hernández]

There's an alternate solution I just came up with

[Violeta Hernández]

We could define n as {n - 1 | } instead

[Violeta Hernández]

It might even be nicer to work with. The only real reason the {0, 1, ... | } definition is considered canonical is because it generalizes to ordinals, but if we're explicitly talking about natural numbers then we don't really need that

[Mario Carneiro]

why not define Ordinal.toPGame first and then use that to define natCast?

[Mario Carneiro]

But actually, as long as the adding ones definition gives the correct answer I don't see any particular reason not to use it

[Mario Carneiro]

I don't think the defeq of this definition is very important

[Violeta Hernández]

It gives the correct Game, but not the "correct" PGame

[Mario Carneiro]

oh I see, for PGame these are all different

[Mario Carneiro]

in that case, just make definitions for all of them

[Violeta Hernández]

2 = (0 + 1) + 1 = {(0 + 1) + 0, (0 + 0) + 1 | } ≡r { 1, 1 | } instead of the expected { 1 | } or { 0, 1 | }

[Mario Carneiro]

what is that ≡ there?

[Violeta Hernández]

A relabelling

[Mario Carneiro]

I thought relabellings couldn't change values?

[Violeta Hernández]

Yeah, the value of the game is correct, it's just not assembled like one might expect

[Mario Carneiro]

I'm not sure why we should care about this

[Mario Carneiro]

looking at equality or relabelling of PGames seems like the wrong notion

[Violeta Hernández]

Hm, I think we might have n = { n - 1 | } up to identity, actually

[Violeta Hernández]

If so this might not really be an issue

[Mario Carneiro]

what changed?

[Violeta Hernández]

Up to identity, not relabellings

[Violeta Hernández]

...there's a lot of equivalence relations on PGame

[Mario Carneiro]

you just gave a derivation which seems to state otherwise, so I'm asking how that is not the case

[Violeta Hernández]

The identity relation deduplicates elements which are themselves identical, so that { x, x, ..., x | } ≡ { x | }

[Violeta Hernández]

We don't currently have identity in Mathlib, but it's been discussed a lot and there's an open PR that introduces it

[Mario Carneiro]

does that relation subsume relabelling?

[Violeta Hernández]

Yeah, the idea is to remove relabellings after it's introduced

[Violeta Hernández]

Relabellings are not really the correct notion to talk about games being the same

[Mario Carneiro]

is that different from the equivalence relation used by Game?

[Violeta Hernández]

Yes, the equivalence relation used by Game is just the antisymmetrization relation

[Violeta Hernández]

Games with entirely different movesets can still work out to be equivalent (under the antisymmetrization relation)

[Mario Carneiro]

oh so {0, 1 | } is not identity-related to {1 | }

[Mario Carneiro]

IMO the adding ones definition looks the most canonical to me

[Mario Carneiro]

people have seen it in many other settings, it doesn't need explication

[Violeta Hernández]

It feels a bit too needlessly complicated IMO. I tried making API for its left moves a while back but got stuck because the left moves of a natural n aren't equal to other naturals.

[Violeta Hernández]

I get that strict equality should be avoided, but talking about e.g. the left moves of a left move is currently basically impossible in the current API otherwise

[Violeta Hernández]

IGame (games up to identity) would make this situation better, but it still would be nice to just have moveLeft n = n - 1 as a characterizing equality, or something of the sort

[Violeta Hernández]

Instead of having n - 1 copies of games that are only identical to n - 1 as left moves

[Violeta Hernández]

Compare to Ordinal.toPGame, which does satisfy ∃ a < o, (Ordinal.toPGame o).moveLeft i = Ordinal.toPGame a as a strict equality

[Mario Carneiro]

why do you need to talk about left moves directly? That seems very internal-detail

[Violeta Hernández]

They're games! Talking about their moves is most of what we do

[Mario Carneiro]

would it be possible to have an induction principle which allows manipulating them up to identity?

[Violeta Hernández]

Hm, how would that look like?

[Mario Carneiro]

you get to specify the type you want to be the left/right moves, and as long as these types are identity-related to what you want, then you get a value identity-related to the result

[Mario Carneiro]

it's not really clear to me how you actually use this left move function though so it's hard to suggest something formal

[Mario Carneiro]

Violeta Hernández said:

They're games! Talking about their moves is most of what we do

Why is it not sufficient to just know that the left moves is some function with some domain? When making constructions you don't generally need to introspect more than that, and equality of types is evil(TM)

[Violeta Hernández]

So basically, a mechanism to cast the indexing types of a PGame to other congruent types?

[Violeta Hernández]

I agree we shouldn't be talking about the domain of the moveLeft function, but talking about its range is quite important.

[Mario Carneiro]

bounds on its range maybe, the exact values I'm not so sure

[Violeta Hernández]

Bounds on its range is certainly too weak, then we couldn't define stuff like birthdays

[Violeta Hernández]

Those require some knowledge about the structure of games. Again, IGame is what we'd ideally be using, but for now we're stuck with PGame

[Mario Carneiro]

isn't the birthday just the height of the recursion?

[Violeta Hernández]

Yeah, but different equivalent Games can have very different heights

[Violeta Hernández]

For instance { }, or { -1 | 1 }, or { -ω₁ | ω₁ } all have very different heights but are equivalent to 0

[Violeta Hernández]

Maybe the real solution to the original NatCast conundrum is to just wait until IGame drops, refactor all that needs to be, and then see how we proceed.

[Violeta Hernández]

To clarify my point, structural equivalence of games is a mathematically useful notion. But both relabellings and strict equality are stronger than this, and thus not very mathematical.

[Kim Morrison]

(I don't really have time to be drawn back into this, but I'll throw out there that relabellings are not useful for thinking about the general theory, but very helpful to have on hand once you want to analyze a particular game --- which is very much a part of studying combinatorial games a la Conway!)

[Tristan Figueroa-Reid]

Kim Morrison said:

(I don't really have time to be drawn back into this, but I'll throw out there that relabellings are not useful for thinking about the general theory, but very helpful to have on hand once you want to analyze a particular game --- which is very much a part of studying combinatorial games a la Conway!)

Wouldn't that be the purpose of Identical? (I was curious about deprecating Relabellings from a comment brought about in #20088.)Relabellings would only be useful if x ≡r y was equivalent to / implied x = y, but I would be astonished if that was the case. Otherwise, Identical is the more useful definition when trying to analyze a particular game, as it doesn't preserve the type-theoretic notions that this formalization has, as @Violeta Hernández mentioned.

[Tristan Figueroa-Reid]

I can see Relabellings as a tool only for faster proofs for identicalness in specific cases.

[Violeta Hernández]

I agree with you. And really, the functionality given by relabellings can be imitated by the identical relation. We should be able to create a constructor for identicalness given two equivalences mapping games to identical games.