feat(set_theory/game/rgame): pre-games up to relabelling

[vihdzp]

---

• depends on: [Merged by Bors] - refactor(set_theory/game/*): Fix bad notation < on (pre-)games #13963

This is only a basic development. A complete development will require some missing lemmas about relabellings and multiplication, which are blocked by #13651.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - refactor(set_theory/game/*): Fix bad notation < on (pre-)games #13963
  By Dependent Issues (🤖). Happy coding!

[alreadydone]

I'm afraid I don't quite see the point of this PR. Is there any particular application in mind? If we want to recover the "identity" (as opposed to equality) relation in ONAG, the equivalence relation should look like pSet.equiv. This weaker condition already ensures substitutability as summand and as option, under both the normal and misere play conventions. (However, If we restrict to games with no duplicate options at every level, the weaker condition would be equivalent to the current definition (existence of bijections).)

If your objective is to rewrite in inequalities easily, then casting to rgame doesn't seem easier than casting straight into game, where the same inequalities and more equalities hold. I wonder if rw_mod_cast could accommodate this use case; the paper says it's not restricted to injective casts. If the casting approach works well then we may not need #13611.

[vihdzp]

Yes, the idea is to recover the identity relation. It is true that relabellings aren't exactly this, since you can have duplicate options, but they're close enough that pretty much the same theorems work.

Games up to relabelling have a few extra algebraic properties that pre-games don't have, i.e. they're an add_comm_monoid. I think these results are of standalone interest, since they're the results we'd be proving about pgame if we weren't working within type theory.

[vihdzp]

Actually, there is one extra thing about rgame that makes it useful on its own: it allows us to naturally talk about relabelled options.

For instance, suppose we want do Conway induction on a + b + c. If we prove that the theorem follows from b, c.move_left i, and a, then tough luck, since b + (c.move_left i) + a isn't an option of a + b + c. It is however a relabelling of an option of a + b + c, which means that Conway induction should still apply. rgame gives us a convenient framework to state this.

If they weren't so far back the dependency chain, the proofs of well-foundedness for le and trans_le could benefit from something like this (note that they can be restated as Conway induction on the sum of their arguments). I wasn't able to state the proof of well-definedness for surreals in terms of this, but I still believe this might come in handy at a later point.

[vihdzp]

On further thought, I agree that it would be best to define a quotient by extensionality rather than just relabelling. I can then prove that relabelling x y implies extensional x y or however we call it.

[vihdzp]

I'll keep thinking about what the best way to go about doing this is. Since there's a bunch of other refactors I want to do first, I'll close this PR for the moment.