Game relations

Stream: maths

[Violeta Hernández]

Combinatorial games are a preorder. To my knowledge, they're the only ordered structure in Mathlib, where the ordering is a main object of study, that is not also a partial order.

This has given rise to some unorthodox notation. I'm particularly interested in bringing up docs#SetTheory.PGame.LF and docs#SetTheory.PGame.Fuzzy

[Violeta Hernández]

x ⧏ y is the same thing as ¬ y ≤ x, while x ‖ y is just the incomparable relation.

[Violeta Hernández]

The former had historical reason for existing, as it had to be defined through simultaneous induction alongside the ≤ relation. But this hasn't been the case ever since we defined docs#Sym2.GameAdd.

[Violeta Hernández]

I propose we refactor it out.

[Violeta Hernández]

As for ‖, I think we should create IncompRel for a general partial order (if it doesn't already exist under another name) and make it scoped notation for that.

[Violeta Hernández]

@Yaël Dillies

[Daniel Weber]

Violeta Hernández said:

I propose we refactor it out.

I think the notation should remain, and perhaps even the definition, just as an abbrev

[Violeta Hernández]

I don't think the less or fuzzy relation on games is any better behaved in games than in any other preorders or partial orders

[Violeta Hernández]

From experience, it's common to talk about fuzzy games, but this less or fuzzy relation seems much rarer

[Violeta Hernández]

I've only seen it used by Conway

[Violeta Hernández]

Besides this, we have a lot of order lemmas throughout Mathlib stated in terms of "not ≤", and having a notation for this would just make it harder to find them

[Daniel Weber]

Alright

[Violeta Hernández]

Oh yeah and if we're going to deprecate LF, we can recover Yaël's keybind \lf for ⌊

[Violeta Hernández]

I remember them complaining about this :stuck_out_tongue:

[Violeta Hernández]

Adding to this. We could also deprecate docs#SetTheory.PGame.Equiv and instead make it local notation for docs#AntisymmRel

[Violeta Hernández]

These three changes combined will probably cut the length of the PGame file in half

[Violeta Hernández]

Unrelated question, but why does AntisymmRel take in a relation argument? Is there any situation where we want to use it with a relation that isn't ≤?

[Violeta Hernández]

Oh and also

[Violeta Hernández]

@Yaël Dillies Do you remember if I ever made an IncompRel PR back in Mathlib3? I couldn't find it but I'm pretty sure I did

[Violeta Hernández]

If not it shouldn't be hard to make one from scratch

[Violeta Hernández]

(deleted)

[Junyan Xu]

Dug out from my inbox: https://github.com/leanprover-community/mathlib3/pull/15168

[Violeta Hernández]

Another question: would it make sense to create notations for AntisymmRel and IncompRel? Typing both of them out explicitly is quite annoying when we can just write ≤ or <

[Violeta Hernández]

It might be silly, but I'm thinking we could use ⋚ for AntisymmRel. Of course, if there's any other established notation it'd be better to just use that.

[Violeta Hernández]

We currently use ≈ for Equiv, but this clashes with the Setoid.r symbol.

[Violeta Hernández]

For IncompRel we can just reuse ‖, I think. We can make it a scoped notation so it doesn't clash with norms.

[Junyan Xu]

previous proposals

[Violeta Hernández]

Oh that explains why this all felt familiar

[Violeta Hernández]

I'm currently proposing to make this notation more general, rather than just keeping it for games. I can't imagine they're the only partial order for which we care about these relations.

[Violeta Hernández]

Forgot to link to #19554

[Violeta Hernández]

This PR introduces the ⋚ notation for AntisymmRel. It'd be great to hear opinions on whether this is the best notation possible, or whether we should scope it, etc.

[Violeta Hernández]

I've opened #19588 to keep track of order refactors to the PGame file

[Ted Hwa]

Violeta Hernández said:

I've only seen it used by Conway

It is pretty commonly used in CGT. For example, it is used in Lessons in Play as well as Siegel's Combinatorial Game Theory.

I hope we at least retain the notation as an abbrev, as suggested by @Daniel Weber

[Ted Hwa]

I find results like the following more intuitive when stated with the ⧏ notation:
x ⧏ y and y ≤ z implies x ⧏ z

It looks like a sort of transitive property, or in terms of games, "the sum of a winning game and a losing game is a winning game".

[Ted Hwa]

Violeta Hernández said:

Besides this, we have a lot of order lemmas throughout Mathlib stated in terms of "not ≤", and having a notation for this would just make it harder to find them

Would using an abbrev allow Lean to "see through" the notation and use the order lemmas stated in terms of "not ≤" ? If not, is there some other mechanism that would allow it? It would be great to be able to use the standard CGT notation ⧏ without having to restate lemmas.

[Violeta Hernández]

Ted Hwa said:

I find results like the following more intuitive when stated with the ⧏ notation:
x ⧏ y and y ≤ z implies x ⧏ z

It looks like a sort of transitive property, or in terms of games, "the sum of a winning game and a losing game is a winning game".

Conversely, I find it's easier to find proofs for these results when stated in terms of ≤. For instance, this is just fun hzx => hyx (hyz.trans hzx).

[Violeta Hernández]

I definitely think it'd be suboptimal to prove PGame.lf_of_lf_of_le when we could prove not_le_of_not_le_of_le for general preorders

[Violeta Hernández]

Ted Hwa said:

Would using an abbrev allow Lean to "see through" the notation and use the order lemmas stated in terms of "not ≤" ? If not, is there some other mechanism that would allow it? It would be great to be able to use the standard CGT notation ⧏ without having to restate lemmas.

Using abbrev is definitely not the answer since it won't work in rw (and setting the simp normal form of not LE to LF seems very questionable to me). We could just keep this as a notation, but I feel like it'd just make things less intuitive for everyone else who isn't super familiar with CGT.

[Violeta Hernández]

Frankly even I, having some familiarity with CGT, find Conway's conventions perplexing. For the longest time I assumed being "fuzzy" or "confused" with 0 implied being at some sort of infinitesimal distance. Just using the term "incomparable" would have gotten things across better.

[Violeta Hernández]

If the goal of Mathlib is interoperability, we should be speaking in the language of preorders rather than the dialect of games.

[Junyan Xu]

Ted Hwa said:

I find results like the following more intuitive when stated with the ⧏ notation:
x ⧏ y and y ≤ z implies x ⧏ z

It looks like a sort of transitive property, or in terms of games, "the sum of a winning game and a losing game is a winning game".

This isn't quite right? I think it means: if a player wins moving first in A (= y - x), and wins moving second in B (= z - y), then they wins moving first in A + B (= z - x). It's weird to call B a losing game because the player may also win when moving first in B (i.e. if B > 0).

[Ted Hwa]

Junyan Xu said:

Ted Hwa said:

I find results like the following more intuitive when stated with the ⧏ notation:
x ⧏ y and y ≤ z implies x ⧏ z

It looks like a sort of transitive property, or in terms of games, "the sum of a winning game and a losing game is a winning game".

This isn't quite right? I think it means: if a player wins moving first in A (= y - x), and wins moving second in B (= z - y), then they wins moving first in A + B (= z - x). It's weird to call B a losing game because the player may also win when moving first in B (i.e. if B > 0).

Yes, you are right. I was really thinking of impartial games when I said "winning game" and "losing game". It should be "wins moving first" and "wins moving second" for general games.

[Junyan Xu]

Impartial games are either = or ‖, and the < case never happens, so you probably won't use the symbols ⧏ and ≤ for them :)

[Ted Hwa]

Junyan Xu said:

Impartial games are either = or ‖, and the < case never ‖, and the < case never happens, so you probably won't use the symbols ⧏ and ≤ for them :)

Yes, I know. For impartial games, the sum of two losing games is a losing game, and the sum of a winning game and a losing game is a winning game. It's just the way I remind myself of the general results for ⧏ and ≤ - the impartial "losing game" becomes ≤ and the impartial "winning game" corresponds to ⧏.

[Ted Hwa]

To get back to the original topic of the thread - I still like the idea of keeping the CGT standard notation ⧏. Maybe you could leave the notation in PGame rather than Mathlib.Order if you feel it's too nonstandard outside of CGT. I did this little experiement with the notation. Maybe it's too naive, but it seems to work okay.

Another nice thing about ⧏ is that we have suitable Trans instances defined so that calc sequences with ⧏and ≤ work correctly.

[Violeta Hernández]

Eh, sure. We can keep it as notation. But most if not all of the API that currently exists for it should exist in the generality of ≤ for preorders instead.

[Violeta Hernández]

Ted Hwa said:

Another nice thing about ⧏ is that we have suitable Trans instances defined so that calc sequences with ⧏and ≤ work correctly.

Do we even do this as of right now?

[Violeta Hernández]

Also, I'm curious, would registering a Trans ≤ (≥)^C (≥)^C instance have the same effect?