Define multiplication on `games` (surreal numbers)

Stream: maths

[Apurva Nakade]

Currently the multiplication for pgames is in surreal.lean and it is getting really cumbersome to work with equations involving pgames and equivalences.

Would it be ok to move the definition mul to games.lean and define multiplication for games so that I can define a semiring instance for games and use the ring tactic? It should be pretty trivial to do this now as all the corresponding theorems for pgames are done.

[Scott Morrison]

Absolutely; moving material between files is a fine thing to do. (Somtimes, if it's complicated, it's best to do it as a separate PR, which you can explicitly describe in as a pure refactor, with no change to content, as this is easier to review, and be sure nothing got lost.)

[Scott Morrison]

On the other hand, I'm confused about the maths. I haven't been thinking about this for a while, but I thought game didn't actually form a ring in the first place, and that we needed to pass to numeric games (i.e. surreals) for some part of it.

[Apurva Nakade]

I'll try it out and see if something goes wrong but right now it looks like multiplication is well defined upto equivalences. This is probably false for inverses and definitely false for the order relation.

[Scott Morrison]

By the way, I hadn't seen these before but just stumbled on them: http://www.cs.cmu.edu/afs/cs/academic/class/15859-s05/www/lecture-notes/comb-games-notes.pdf seem to be some very nice notes about combinatorial games, and are perhaps the most-amenable-to-formalisation of sources I've seen.

[Scott Morrison]

They don't have anything to say about multiplication on non-numeric games, however.

[Apurva Nakade]

Awesome, thanks! :D

[Apurva Nakade]

Actually, I was wrong. I thought we had the following lemma in the library but we don't:

theorem mul_congr {w x y z : pgame} (h₁ : w ≈ x) (h₂ : y ≈ z) : w * y ≈ x * z :=
sorry

This is very likely false because of the negative signs that show up in the definition of multiplication.

Oh well

[Apurva Nakade]

Scott Morrison said:

By the way, I hadn't seen these before but just stumbled on them: http://www.cs.cmu.edu/afs/cs/academic/class/15859-s05/www/lecture-notes/comb-games-notes.pdf seem to be some very nice notes about combinatorial games, and are perhaps the most-amenable-to-formalisation of sources I've seen.

Theorem 3.8 in this document gives a proof of "product of two numeric numbers is numeric".
The proof is huge - essentially you need to prove 4 statements simultaneously :( :(
I have been trying to untangle these but it is looking unlikely. This is going to end up really messy.