Surreal inverses and division

Stream: mathlib4

[Ted Hwa]

After correcting the definition of surreal inverses (discussed in this thread), I have proven that the definition indeed gives a multiplicative inverse, and defined a LinearOrderedField structure on Surreal. The PR is #14498

[Kevin Buzzard]

Yikes it's huge! Usually PRs, especially from new contributors, are encouraged to be more like 150 lines, although at first glance the code looks pretty good -- thanks! Is there any way you can PR some preliminaries separately? Another issue is that there are not that many people who are able to review PRs in this area.

[Eric Wieser]

I think putting up the whole thing at once like this is still good - it's just not the final step to getting it reviewed. What it does mean is that when people ask about how the pieces are used, you can point at the big PR for examples, and they can suggest how to change it to avoid the need for those pieces at all if necessary

[Ted Hwa]

I can break each file's changes into a separate PR, but the main proof in the Division file is still long. The PR #14463 to fix the formula was intended to be able a small change leading up to this PR. But in the discussion on the other thread, there was disagreement on whether it should be separated or incorporated into this PR.

Another issue is that there are not that many people who are able to review PRs in this area.

Any suggestions on what to do about that? I acknowledge this is a somewhat niche area of mathematics.

[Kim Morrison]

Perhaps ping previous contributors to these files (although likely Mario and I won't have time to review)?

[Eric Wieser]

I think the key difference with #14463 is that it changes the definition. PRs that add lemmas about existing definitions are much easier to review, because theorems can't be wrong in the same way

[Ted Hwa]

Tagging contributors for the multiplication proof : @Violeta Hernández @Junyan Xu

[Eric Wieser]

One easy first split might be the insertLeft definition and the lemmas about it.

[Eric Wieser]

(where it might be reasonable to add insertRight at the same time, if others agree)

[Yaël Dillies]

Instead of saying "This PR incorporates #14463", you should write "- [ ] depends on: #14463" in the PR description

[Eric Wieser]

Yael, previous discussion was that people were uncomfortable merging that PR without the proof the change was correct being in the same one

[Yaël Dillies]

Ah sorry I thought this uncomfortability was cleared by the later PR containing the proof

[Eric Wieser]

Maybe it now has been

[Ted Hwa]

The first split out PR is #14517 for insertLeft and insertRight

[Ted Hwa]

Here are the PR's split out so far:

#14517 - the insertLeft and insertRight lemmas (already mentioned above), which has been reviewed by @Eric Wieser for code style (thank you!), but he would like someone with more knowledge in the area to check it for any obvious missing lemmas.

#14463 - corrects the definition of inverse. In the other thread, there now seems to be some agreement that this change is now acceptable because we have a proof that it is correct. But it hasn't gotten any reviews by anyone yet.

#14600 - a few simple lemmas about Surreal numbers needed in the proof. It's actually a continuation of a previous PR #14278 which @Eric Wieser reviewed but then I closed because we weren't sure about whether they should be simp lemmas or not. I removed all the simp in the new PR. (When I tried to reopen the old PR, github wouldn't let me - I think I messed something up by doing a rebase then force push. Anyway it was easier to just open a new PR.)

If anyone can review these PRs that would be appreciated.

[Violeta Hernández]

#14517 seems fine to me, though I'm quite a bit rusted with Lean

[Violeta Hernández]

Same goes for #14600

[Violeta Hernández]

Can't really comment on #14463, I haven't worked with surreal division at all :frown:

[Ted Hwa]

Thank you @Violeta Hernández ! I'm not sure, if you need to / have permissions to approve the PRs on github? If not, can someone else approve based on the above comments?

[Violeta Hernández]

No, my approval is really just an informal one

[Kim Morrison]

I left some naming comments on #14517.

[Kim Morrison]

I left comments on #14600.

[Kim Morrison]

@Violeta Hernández , it may be helpful to look at my comments to see the type of things it is helpful to catch in review. :-)

[Eric Wieser]

I pushed a few golfs to #14517

[Kim Morrison]

Nice!

[Ted Hwa]

Thank you @Kim Morrison and @Eric Wieser for the reviews! I have made the suggested changes.

[Ted Hwa]

When I resolved a merge conflict for the big PR #14498, suddenly the CI is failing with this error:

error: ././././Mathlib/SetTheory/Surreal/Division.lean:261:5: unknown tactic

The tactic on that line is ring_nf. What happened?

[Ted Hwa]

Ok when I did import Mathlib.Tactic.Ring.RingNF then it worked. It must have been getting pulled in transitively before.

[Ted Hwa]

I updated #14498 with the above merged PRs (thank you @Kim Morrison !). However, I am unable to figure out how to fix this error:

error: ././././Mathlib/SetTheory/Surreal/Division.lean:811:47: application type mismatch
  Sum.inr ()
argument
  ()
has type
  Unit : Type
but is expected to have type
  PUnit.{u_1 + 1} : Type u_1

It seems to be because insertLeft was changed to use Sum.elim instead of match. When I revert to the old definition using match, then everything works. I'm not sure how to fix this apparent universe issue. I tried replacing () by PUnit.unit and it is accepted, but then the subsequent simp does not simplify anymore (it refuses to apply the simp lemma mul_moveLeft_inl).

Is there a way to fix this or should I revert to the old definition using match ?

Old definition (uses match):

def insertLeft (x x' : PGame.{u}) : PGame :=
  match x with
  | mk xl xr xL xR => mk (xl ⊕ PUnit) xr (fun i' =>
      match i' with
      | .inl i => xL i
      | .inr () => x'
    ) xR

New definition (uses Sum.elim):

def insertLeft (x x' : PGame.{u}) : PGame :=
  match x with
  | mk xl xr xL xR => mk (xl ⊕ PUnit) xr (Sum.elim xL fun _ => x') xR

[Eric Wieser]

The () notation only would for PUnit.{0} (edit: pushed a fix to use Unit instead of PUnit)

[Eric Wieser]

My initial reaction to this is that the problem wouldn't exist if you used Option instead of ⊕ PUnit!

[Kim Morrison]

Not at a computer, but I'd be trying to work out why simp isn't applying that lemma.

[Eric Wieser]

My guess would be that you first need to apply a lemma about Sum.elim

[Ted Hwa]

I got it to work. I just needed to add Sum.elim_inr to the list of simp only lemmas at the end. There was no problem with mul_moveLeft_inl. I must have misread the infoview when I said that. Sorry for wasting everyone's time on this.

[Kim Morrison]

No problem. We're all learning!

[Eric Wieser]

In your defense the infoview got pretty cluttered mid-proof there. I wonder if we should have syntax highlighting / bracket matching there to help?

[Ted Hwa]

I think I may have gotten confused by the "Expected type" section in the infoview (I don't really understand what that is). When the context is long and there are several goals and the "Expected type" section shows up, it is easy to scroll too far (looking through the goals) and end up in the "Expected type" section thinking that is a goal, since it looks very similar. Then probably I tried a simp and saw nothing changed, so I concluded that the simp didn't work but actually I was looking at the "Expected type" which did not change.

[Kevin Buzzard]

This is why it's not a good idea to have several goals :-) The moment there's more than one goal you want to use \. to get yourself into the situation where instead you have multiple "threads" each with one goal. Then you can use sorry to close all the goals which are around other than the one you're working on, and then if you add an _ you can be sure that any "expected type* errors will correspond to the unique error in your code.

[Ted Hwa]

I learned that field_simp doesn't actually need a field, and can work when dividing by units in a commutative ring. This simplified the proof a lot since throughout the proof, we are trying to prove we have a field and from the inductive hypothesis, certain elements are already known to be units. Previously I was doing a lot of manipulations by hand.

[Violeta Hernández]

Hi! I've spent the past week revisiting all of these game files and I think I've got a hang of the API once again

[Violeta Hernández]

(deleted)

[Violeta Hernández]

I think it might be a good idea to make a preliminary PR containing only the stuff about normalization. That's the easy prerequisites to the complex calculations, in some sense.

[Violeta Hernández]

I opened #15779, which should hopefully simplify this step a bit