# Zulip Chat Archive

## Stream: maths

### Topic: Surreal numbers

#### Apurva Nakade (Apr 12 2021 at 16:17):

Hi,

I'm trying to play around with some surreal numbers in Lean and am looking at the TODO's in the library.

The first TODO says to construct a proof of `numeric n`

which is a term of type `pgame n \to Prop`

where `n : \nat`

.

Amazingly, Lean is able to coerce `n : \nat`

to `n : pgame`

. I searched the code for a definition of this coercion but only found `pgame.has_zero`

and `pgame.has_one`

. How is this coercion happening?

Thanks,

#### Johan Commelin (Apr 12 2021 at 16:18):

If you have `0`

and `1`

(which you found), then you only need `+`

to get the coercion.

#### Apurva Nakade (Apr 12 2021 at 16:20):

Oh, I see, so Lean is automatically defining `n.succ : pgame`

as `n : pgame + 1 : pgame`

This is really efficient! Thanks!

#### Kevin Buzzard (Apr 12 2021 at 21:27):

I think that actually it *defines* `bit0 n : pgame`

to be `(n : pgame) + (n : pgame)`

and `bit1 n : pgame`

to be `(bit0 n : pgame) + (1 : pgame)`

which could in theory be different ;-)

#### Yakov Pechersky (Apr 12 2021 at 21:33):

As far as I remember, there isn't a clear proof that `pgame.short_add`

is properly commutative and associative.

#### Apurva Nakade (Apr 12 2021 at 22:26):

I tried just hacking my way through to see what the definitions look like for some small cases and the definition becomes unrecognizable at `n=2`

.

```
import set_theory.surreal
open pgame
theorem numeric_zero' : numeric 0 :=
begin
split,
repeat {simp},
end
theorem numeric_one' : numeric 1 :=
begin
split,
repeat {simp},
apply numeric_zero',
end
theorem numeric_two' : numeric 2 :=
begin
split,
-- goal is unrecognizable
end
theorem numeric_nat (n : ℕ) : numeric n :=
begin
-- don't even know how to start
end
```

How does one work with this kind of definition? My guess is to first prove things about `numeric n`

and show that it can be rewritten in a simplified form but I'm having trouble just unfolding the definition of add.

#### Apurva Nakade (Apr 12 2021 at 22:28):

For example, in "math", I believe 2 is simply {1|} (and possibly few other numbers in the left and right sets) but I'm not able to see how `numeric 2`

reduces to this.

#### Yakov Pechersky (Apr 12 2021 at 22:29):

#### Yakov Pechersky (Apr 12 2021 at 22:30):

I mean src#pgame.numeric_add

#### Yakov Pechersky (Apr 12 2021 at 22:30):

`oy`

indeed

#### Yakov Pechersky (Apr 12 2021 at 22:31):

```
-- TODO prove
-- theorem numeric_nat (n : ℕ) : numeric n := sorry
```

from the source :scared:

#### Apurva Nakade (Apr 12 2021 at 22:33):

Oh wow! Thank you so much!!

I totally missed this. I'll spend some time trying to understand the proof.

#### Scott Morrison (Apr 12 2021 at 23:07):

The proof of `numeric_nat`

follows in just a few lines from `numeric_zero`

, `numeric_one`

, and `numeric_add`

, just by inducting on `n`

. I'm not sure why it wasn't done previously.

#### Scott Morrison (Apr 12 2021 at 23:15):

#### Scott Morrison (Apr 12 2021 at 23:15):

(Spoiler also contains `numeric_omega`

.)

#### Apurva Nakade (Apr 12 2021 at 23:26):

Thanks! I thought so too. I had missed this `numeric_add`

lemma.

#### Apurva Nakade (Apr 12 2021 at 23:27):

Kevin Buzzard said:

I think that actually it

defines`bit0 n : pgame`

to be`(n : pgame) + (n : pgame)`

and`bit1 n : pgame`

to be`(bit0 n : pgame) + (1 : pgame)`

which could in theory be different ;-)

What does `bit0`

mean mathematically? It seems to be doubling the number but that can't be right :o

#### Yakov Pechersky (Apr 12 2021 at 23:29):

That's exactly what it's doing

#### Yakov Pechersky (Apr 12 2021 at 23:30):

You can imagine the binary encoding of a number like 13 : 1101. In Lean, it would be:

```
set_option pp.numerals false
#check 13 -- bit1 (bit0 (bit1 has_one.one)) : ℕ
```

#### Yakov Pechersky (Apr 12 2021 at 23:30):

which, read from left to right, is exactly `1 0 1 1`

#### Yakov Pechersky (Apr 12 2021 at 23:31):

It's just a more efficient encoding than the unary `13 = 1 + 1 + ... + 1`

#### Apurva Nakade (Apr 12 2021 at 23:35):

Interesting!!

So internally natural numbers are computed using "binary" induction and not "unary" induction. Nice!

#### Scott Morrison (Apr 12 2021 at 23:42):

(I'll leave my spoiler tag above starred, and perhaps PR it one day, but if you get there first that would be great! :-)

#### Yakov Pechersky (Apr 13 2021 at 00:02):

Not natural numbers. Anything that is notated by numerical digits

#### Apurva Nakade (Apr 13 2021 at 14:13):

Just for the record here's one more solution

Spoiler (numeric_nat numeric_omega)

I'll try to get it in the library.

#### Scott Morrison (Apr 13 2021 at 14:25):

Looks good, PR away. (Indenting inside `begin ... end`

blocks! :-)

#### Scott Morrison (Apr 13 2021 at 14:26):

(Also, in spoiler tags, you can put another ````lean`

block inside to get formatting.

#### Apurva Nakade (Apr 13 2021 at 15:10):

Done. I'll also try to clear the other TODO's in the file.

Would it be a good idea to add some lemmas about simplifying surreal numbers coming from natural numbers, like `n \equiv {n - 1 | } `

? and the "simplicity rule"?

#### Yakov Pechersky (Apr 13 2021 at 15:15):

Since surreal has instances for has_zero, has_one, and has_add, nats can automatically be cast to surreal

#### Yakov Pechersky (Apr 13 2021 at 15:16):

You might want to prove commutativity of the addition defined on surreal.

#### Yakov Pechersky (Apr 13 2021 at 15:16):

#### Yakov Pechersky (Apr 13 2021 at 15:18):

docs#nat.cast_add is the proof, basically, for the question you asked

#### Apurva Nakade (Apr 15 2021 at 15:10):

I'm slowly working on proving properties about the addition of surreal numbers.

Is there a nicer way to write the following code:

```
import set_theory.surreal
namespace surreal
theorem zero_add : ∀ x : surreal, 0 + x = x :=
begin
rintros ⟨x, ox⟩,
apply quotient.sound,
apply pgame.zero_add_equiv,
end
theorem add_zero : ∀ x : surreal, x + 0 = x :=
begin
rintros ⟨x, ox⟩,
apply quotient.sound,
apply pgame.add_zero_equiv,
end
instance : add_monoid surreal :=
{ add := add,
add_assoc := add_assoc,
zero := 0,
zero_add := zero_add,
add_zero := add_zero }
end surreal
```

Weirdly I'm not able to merge the two `apply`

s.

Thanks,

#### Kevin Buzzard (Apr 15 2021 at 15:12):

First change `apply`

to refine:

```
theorem zero_add : ∀ x : surreal, 0 + x = x :=
begin
rintros ⟨x, ox⟩,
refine quotient.sound _,
refine pgame.zero_add_equiv _,
end
```

and then it's easy:

```
theorem zero_add : ∀ x : surreal, 0 + x = x :=
begin
rintros ⟨x, ox⟩,
exact quotient.sound (pgame.zero_add_equiv _),
end
```

#### Apurva Nakade (Apr 15 2021 at 15:14):

Oh I see, I was missing that `_`

at the end.

Thanks!

#### Eric Wieser (Apr 15 2021 at 15:22):

You might find that

```
theorem zero_add : ∀ x : surreal, 0 + x = x :=
begin
rintros ⟨x, ox⟩,
exact quotient.sound (pgame.zero_add_equiv _),
end
```

golfs further to

```
theorem zero_add : ∀ x : surreal, 0 + x = x
| ⟨x, ox⟩ := quotient.sound (pgame.zero_add_equiv _)
```

#### Eric Wieser (Apr 15 2021 at 15:30):

This works too:

```
section
-- otherwise the elaborator gets in our way
local attribute [elab_with_expected_type] quotient.ind
instance : add_monoid surreal :=
{ add := add,
add_assoc := add_assoc,
zero := 0,
zero_add := quotient.ind $ λ a, quotient.sound $ pgame.zero_add_equiv _,
add_zero := quotient.ind $ λ a, quotient.sound $ pgame.add_zero_equiv _ }
end
```

#### Apurva Nakade (Apr 15 2021 at 15:39):

Thanks, I was trying something like `λ ⟨x, ox⟩, ...`

but that did not work.

I guess Lean is better at pattern matching `| ⟨x, ox⟩ := ...`

.

#### Apurva Nakade (Apr 15 2021 at 15:41):

Eric Wieser said:

You might find that

`theorem zero_add : ∀ x : surreal, 0 + x = x := begin rintros ⟨x, ox⟩, exact quotient.sound (pgame.zero_add_equiv _), end`

golfs further to

`theorem zero_add : ∀ x : surreal, 0 + x = x | ⟨x, ox⟩ := quotient.sound (pgame.zero_add_equiv _)`

I just tried this one out and Lean is throwing a type mismatch error for `quotient.sound`

#### Apurva Nakade (Apr 15 2021 at 15:42):

I'm guessing it is not able to infer the setoid type.

#### Yakov Pechersky (Apr 15 2021 at 15:43):

You can try using `quot.sound`

and `quot.ind`

instead, which do not try to infer the setoid on their own.

#### Apurva Nakade (Apr 15 2021 at 15:44):

Interesting! Thanks,

#### Apurva Nakade (Apr 19 2021 at 16:56):

Here's a construction of `ordered_add_comm_group`

instance for surreal numbers:

```
import set_theory.surreal
open pgame
namespace surreal
def neg : surreal → surreal :=
surreal.lift (λ x ox, ⟦⟨-x, pgame.numeric_neg ox⟩⟧) (λ _ _ _ _ a, quotient.sound (pgame.neg_congr a))
instance : ordered_add_comm_group surreal :=
{ add := surreal.add,
add_assoc := surreal.add_assoc,
zero := 0,
zero_add := by { rintros ⟨x, ox⟩, exact quotient.sound (pgame.zero_add_equiv _) },
add_zero := by { rintros ⟨x, ox⟩, exact quotient.sound (pgame.add_zero_equiv _) },
neg := surreal.neg,
sub := λ x y, x + surreal.neg y,
sub_eq_add_neg := by try_refl_tac,
add_left_neg := by { rintros ⟨x, ox⟩, exact quotient.sound pgame.add_left_neg_equiv },
add_comm := by { rintros ⟨x, ox⟩ ⟨y, oy⟩, exact quotient.sound pgame.add_comm_equiv },
le := surreal.le,
lt := surreal.lt,
le_refl := by { rintros ⟨x, ox⟩, refl },
le_trans := by { rintros ⟨x, ox⟩ ⟨y, oy⟩ ⟨z, oz⟩, exact pgame.le_trans },
lt_iff_le_not_le := by { rintros ⟨x, ox⟩ ⟨y, oy⟩, exact pgame.lt_iff_le_not_le ox oy },
le_antisymm := by { rintros ⟨x, ox⟩ ⟨y, oy⟩ h₁ h₂, exact quotient.sound ⟨h₁, h₂⟩ },
add_le_add_left := by { rintros ⟨x, ox⟩ ⟨y, oy⟩ hx ⟨z, oz⟩, exact pgame.add_le_add_left hx } }
end surreal
```

Is there any way I can improve the code?

#### Apurva Nakade (Apr 19 2021 at 17:05):

The next TODO in the surreal.lean file is the construction of a homomorphism `surreal → game`

but I don't know what `game`

is.

So, I'm instead thinking of constructing the "dyadic rationals" as surreal numbers.

#### Eric Wieser (Apr 19 2021 at 17:13):

There's no point defining `sub`

there like that, it will use that definition for you automatically.

#### Eric Wieser (Apr 19 2021 at 17:14):

However, it might be worth doing if you defined it as `⟦⟨x-y, pgame.numeric_sub ox oy⟩⟧`

instead

#### Eric Wieser (Apr 19 2021 at 17:14):

Which is more work, but unfolds more nicely

#### Eric Wieser (Apr 19 2021 at 17:16):

I'd recommend you make a PR with what you have anyway

#### Apurva Nakade (Apr 19 2021 at 17:27):

Thanks! Will push this to mathlib soon.

I also didn't like just using the `sub`

definition from some instance in the library but I couldn't figure out how to get Lean to infer it automatically.

#### Mario Carneiro (Apr 19 2021 at 17:29):

Regarding dyadic rationals, I think a good intermediate step is to define and prove the basic properties of the `midpoint`

function, which I think is the main driver behind the dyadic rational construction

#### Mario Carneiro (Apr 19 2021 at 17:30):

(maybe there are conditions on the inputs, I forget the details)

#### Mario Carneiro (Apr 19 2021 at 17:31):

It's awfully convenient to have `x - y = x + -y`

be defeq. I wouldn't redefine it unless it expands to something crazy with the default definition

#### Apurva Nakade (Apr 19 2021 at 19:42):

Mario Carneiro said:

Regarding dyadic rationals, I think a good intermediate step is to define and prove the basic properties of the

`midpoint`

function, which I think is the main driver behind the dyadic rational construction

Do you have a specific property in mind? I think it is true that $1/2^{n+1} = \{ 0 | 1/2^n \}$. More generally, $(x + y)/2 = \{ x | y \}$ works when $x$ and $y$ are *adjacent numbers created on the same day*.

I can try and figure out what this might look like formally.

#### Mario Carneiro (Apr 19 2021 at 21:15):

Right, that latter property is the one I'm talking about. You have to prove that that number is in fact $m:=(x+y)/2$, for example by proving that $m+m=x+y$

#### Mario Carneiro (Apr 19 2021 at 21:15):

"created on the same day" also sounds a bit finicky

#### Mario Carneiro (Apr 19 2021 at 21:16):

Is it possible to say anything interesting about $\{x\mid y\}$ when $x$ and $y$ are just random surreals?

#### Mario Carneiro (Apr 19 2021 at 21:17):

Also, you said "more generally" but the first statement doesn't follow from the second since 0 is born on day 0

#### Apurva Nakade (Apr 19 2021 at 21:53):

Oh right, 0 isn't born on the same day!

I'll take a look at Conway and try to work out the exact mathematical statement.

#### Apurva Nakade (Apr 19 2021 at 22:01):

So I believe the correct mathematical statement is this: if $\dots, x_{-i}, x_{-i + 1}, \dots, x_{-1}, x_0 = 0, x_1, \dots, x_i \dots$ are the numbers created *by* day $n$ then the $\{ x_i | x_{i + 1} \}$ is the midpoint of $x_i$ and $x_{i+1}$. But this fails for arbitrary $\{x_i | x_j \}$.

#### Apurva Nakade (Apr 19 2021 at 22:03):

On shortcut is to just prove that $\{0 | 1/2^n \} + \{0 | 1/2 ^ n \} = 1/2^{n-1}$. And define $m / 2^n$ as $1/2^n + \dots + 1/2^n$. This will not require the concept of "days".

#### Mario Carneiro (Apr 19 2021 at 22:06):

Do we know that the surreals are a field?

#### Mario Carneiro (Apr 19 2021 at 22:06):

I'm guessing no, but if not then a lot of shortcuts like that won't work

#### Mario Carneiro (Apr 19 2021 at 22:07):

Also, what's the proof sketch? The lean version of the definition is pretty different from the set theory definition

#### Apurva Nakade (Apr 19 2021 at 22:09):

There is a definition of inverse in the library for pgames: https://github.com/leanprover-community/mathlib/blob/0dfac6ebc9cbb286afb013ccfd7c7478a11ba1e5/src/set_theory/surreal.lean#L106

It might be possible to define the field instance for surreal using this.

#### Mario Carneiro (Apr 19 2021 at 22:13):

Oh, it's not even proved to be numeric

#### Mario Carneiro (Apr 19 2021 at 22:13):

that should be fairly easy

#### Mario Carneiro (Apr 19 2021 at 22:14):

I lifted those definitions straight off wikipedia. I don't think they came with proofs attached

#### Apurva Nakade (Apr 19 2021 at 22:15):

Oh cool, let me try this out first then. Thanks!

#### Mario Carneiro (Apr 19 2021 at 22:16):

Looking at those expressions, I think commutativity of addition and the other ring axioms should be "straightforward"

#### Mario Carneiro (Apr 19 2021 at 22:24):

I think the correct statement regarding midpoints is that if you have a surreal number $x=\{L\mid R\}$ such that $\sup L < \inf R$ (let's say they are real numbers, and in the easy case the max/min are attained), then $x=(\sup L+\inf R)/2$

#### Mario Carneiro (Apr 19 2021 at 22:26):

Oh no that's not right, $\{2\mid 5\}=3$ is mentioned on wikipedia

#### Mario Carneiro (Apr 19 2021 at 22:39):

Oh, `pgame`

already has `add_comm`

proved, it just needs to be packed up

#### Mario Carneiro (Apr 19 2021 at 22:39):

don't see anything about the other field operations though

#### Apurva Nakade (Apr 20 2021 at 14:51):

Right, I'll work on proving things about `mul`

first.

#### Apurva Nakade (Apr 21 2021 at 23:34):

I spent hours (unsuccessfully) trying to prove `x * 0 = 0 `

for `pgame`

s by hand only to discover this:

```
import set_theory.surreal
universes u
namespace pgame
def mul_zero_relabelling :
Π (x : pgame.{u}), relabelling (x * 0) 0
:= by {rintros ⟨⟩, tidy}
end pgame
```

This is insane! How is `tidy`

so powerful? Is this a valid proof? It almost feels like I'm cheating somehow.

#### Alex J. Best (Apr 21 2021 at 23:35):

If you run `tidy?`

instead, it will tell you what tactics it did.

#### Apurva Nakade (Apr 21 2021 at 23:38):

This is the suggestion:

```
fsplit, work_on_goal 0 { dsimp at *, fsplit, work_on_goal 0 { intros ᾰ, cases ᾰ, work_on_goal 0 { cases ᾰ, cases ᾰ_snd }, cases ᾰ, cases ᾰ_snd }, work_on_goal 0 { intros ᾰ, cases ᾰ }, work_on_goal 0 { intros x, cases x, work_on_goal 0 { cases x, cases x_snd }, cases x, cases x_snd }, intros x, cases x }, work_on_goal 0 { dsimp at *, fsplit, work_on_goal 0 { intros ᾰ, cases ᾰ, work_on_goal 0 { cases ᾰ, cases ᾰ_snd }, cases ᾰ, cases ᾰ_snd }, work_on_goal 0 { intros ᾰ, cases ᾰ }, work_on_goal 0 { intros x, cases x, work_on_goal 0 { cases x, cases x_snd }, cases x, cases x_snd }, intros x, cases x }, work_on_goal 0 { intros i, cases i, work_on_goal 0 { cases i, cases i_snd }, cases i, cases i_snd }, intros j, cases j
```

:dizzy:

#### Eric Rodriguez (Apr 21 2021 at 23:38):

yeah was just about to post that, lol

#### Eric Rodriguez (Apr 21 2021 at 23:38):

`finish`

is also good

#### Eric Rodriguez (Apr 21 2021 at 23:39):

(although in this case it completely fails)

#### Apurva Nakade (Apr 21 2021 at 23:42):

`tidy`

ftw :sunglasses:

#### Scott Morrison (Apr 22 2021 at 00:24):

Even though that's a fairly large tactic script coming out of `tidy`

, I would bet it's straightforward to hand-edit down to something much smaller, even before you understand what it is doing. Very often it runs `cases`

unnecessarily (or "too early"), and this is a large part of why it is slow. Also very often it calls `dsimp`

unnecessarily.

#### Scott Morrison (Apr 22 2021 at 00:26):

The first step of mindlessly golfing a `tidy`

proof is to add newlines and indentation, so you have a hope. :-)

#### Kevin Buzzard (Apr 22 2021 at 06:28):

It looks to me like for the most part it's taking terms apart, with a bit of `simp`

thrown in. If it's slow to run you might want to replace with the output of `tidy?`

and then start aggressively using `rintro`

and `rcases`

.

Yeah I've seen both `tidy`

and `nlinarith`

do things they should never be able to do

#### Apurva Nakade (Apr 23 2021 at 15:33):

I did manage to simplify it quite a bit, and in the process discovered `rintros?`

:

```
import set_theory.surreal
open pgame
namespace pgame
/-- `x * 0` has exactly the same moves as `0`. -/
theorem mul_zero_relabelling : Π (x : pgame), relabelling (x * 0) 0
| (mk xl xr xL xR) :=
⟨by fsplit; rintro (⟨_, ⟨⟩⟩ | ⟨_, ⟨⟩⟩),
by fsplit; rintro (⟨_, ⟨⟩⟩ | ⟨_, ⟨⟩⟩),
by rintro (⟨_, ⟨⟩⟩ | ⟨_, ⟨⟩⟩),
by rintro ⟨⟩⟩
/-- `0 * x` has exactly the same moves as `0`. -/
theorem zero_mul_relabelling : Π (x : pgame), relabelling (0 * x) 0
| (mk xl xr xL xR) :=
⟨by fsplit; rintro (⟨⟨⟩, _⟩ | ⟨⟨⟩, _⟩),
by fsplit; rintro (⟨⟨⟩, _⟩ | ⟨⟨⟩, _⟩),
by rintro (⟨⟨⟩,_⟩ | ⟨⟨⟩,_⟩),
by rintro ⟨⟩⟩
end pgame
```

#### Apurva Nakade (Apr 25 2021 at 16:55):

I'm trying to prove basic properties about the multiplication of surreal numbers.

I have several proofs written out completely but all of the need the following lemmas, which I'm having trouble proving:

```
import set_theory.surreal
open pgame
def neg_congr_relabelling {x y : pgame}
(h₁ : x.relabelling y) : (-x).relabelling (-y) :=
sorry
def add_congr_relabelling {w x y z : pgame}
(h₁ : w.relabelling x) (h₂ : y.relabelling z) : (w + y).relabelling (x + z) :=
sorry
```

I can try induction on the various variables but that seems like the wrong way to prove these.

Morally, these should be defined recursively but I'm not accustomed to writing recursion in Lean.

Any suggestions?

Thanks,

#### Mario Carneiro (Apr 25 2021 at 17:08):

Here's a proof for the first one. The recursion pattern is borrowed from `relabelling.symm`

```
def neg_congr_relabelling : ∀ {x y : pgame}, x.relabelling y → (-x).relabelling (-y)
| (mk xl xr xL xR) (mk yl yr yL yR) ⟨L_equiv, R_equiv, L_relabelling, R_relabelling⟩ :=
⟨R_equiv, L_equiv,
λ i, neg_congr_relabelling (by simpa using R_relabelling (R_equiv i)),
λ i, neg_congr_relabelling (by simpa using L_relabelling (L_equiv.symm i))⟩
```

#### Apurva Nakade (Apr 26 2021 at 13:52):

Thanks!

I've managed to get a proof for `surreal.mul_comm`

```
import set_theory.surreal
open pgame
namespace pgame
/-- An explicit description of the moves for Left in `x * y`. -/
def left_moves_mul {x y : pgame} : (x * y).left_moves
≃ x.left_moves × y.left_moves ⊕ x.right_moves × y.right_moves :=
by { cases x, cases y, refl, }
/-- An explicit description of the moves for Right in `x * y`. -/
def right_moves_mul {x y : pgame} : (x * y).right_moves
≃ x.left_moves × y.right_moves ⊕ x.right_moves × y.left_moves :=
by { cases x, cases y, refl, }
@[simp] lemma mk_mul_move_left_inl {xl xr yl yr} {xL xR yL yR} {i j} :
(mk xl xr xL xR * mk yl yr yL yR).move_left (sum.inl (i,j))
= (mk xl xr xL xR).move_left i * (mk yl yr yL yR)
+ (mk xl xr xL xR) * (mk yl yr yL yR).move_left j
- (mk xl xr xL xR).move_left i * (mk yl yr yL yR).move_left j
:= rfl
@[simp] lemma mul_move_left_inl {x y : pgame} {i j} :
(x * y).move_left ((@left_moves_mul x y).symm (sum.inl (i,j)))
= x.move_left i * y + x * y.move_left j - x.move_left i * y.move_left j
:= by {cases x, cases y, refl}
@[simp] lemma mk_mul_move_left_inr {xl xr yl yr} {xL xR yL yR} {i j} :
(mk xl xr xL xR * mk yl yr yL yR).move_left (sum.inr (i,j))
= (mk xl xr xL xR).move_right i * (mk yl yr yL yR)
+ (mk xl xr xL xR) * (mk yl yr yL yR).move_right j
- (mk xl xr xL xR).move_right i * (mk yl yr yL yR).move_right j
:= rfl
@[simp] lemma mul_move_left_inr {x y : pgame} {i j} :
(x * y).move_left ((@left_moves_mul x y).symm (sum.inr (i,j)))
= x.move_right i * y + x * y.move_right j - x.move_right i * y.move_right j
:= by {cases x, cases y, refl}
@[simp] lemma mk_mul_move_right_inl {xl xr yl yr} {xL xR yL yR} {i j} :
(mk xl xr xL xR * mk yl yr yL yR).move_right (sum.inl (i,j))
= (mk xl xr xL xR).move_left i * (mk yl yr yL yR)
+ (mk xl xr xL xR) * (mk yl yr yL yR).move_right j
- (mk xl xr xL xR).move_left i * (mk yl yr yL yR).move_right j
:= rfl
@[simp] lemma mul_move_right_inl {x y : pgame} {i j} :
(x * y).move_right ((@right_moves_mul x y).symm (sum.inr (i, j)))
= x.move_right i * y + x * y.move_left j - x.move_right i * y.move_left j
:= by {cases x, cases y, refl}
@[simp] lemma mk_mul_move_right_inr {xl xr yl yr} {xL xR yL yR} {i j} :
(mk xl xr xL xR * mk yl yr yL yR).move_right (sum.inr (i,j))
= (mk xl xr xL xR).move_right i * (mk yl yr yL yR)
+ (mk xl xr xL xR) * (mk yl yr yL yR).move_left j
- (mk xl xr xL xR).move_right i * (mk yl yr yL yR).move_left j
:= rfl
@[simp] lemma mul_move_right_inr {x y : pgame} {i j} :
(x * y).move_right ((@right_moves_mul x y).symm (sum.inr (i,j)))
= x.move_right i * y + x * y.move_left j - x.move_right i * y.move_left j
:= by {cases x, cases y, refl}
/-- If `w` has the same moves as `x` and `y` has the same moves as `z`,
then `w + y` has the same moves as `x + z`. -/
def add_congr_relabelling : ∀ {w x y z : pgame},
w.relabelling x → y.relabelling z → (w + y).relabelling (x + z)
| (mk wl wr wL wR) (mk xl xr xL xR) (mk yl yr yL yR) (mk zl zr zL zR)
⟨L_equiv₁, R_equiv₁, L_relabelling₁, R_relabelling₁⟩
⟨L_equiv₂, R_equiv₂, L_relabelling₂, R_relabelling₂⟩ :=
begin
refine ⟨_,_,_,_⟩,
{ fsplit, -- left moves
{ rintro (i|j),
{ exact sum.inl (L_equiv₁ i) },
{ exact sum.inr (L_equiv₂ j) }},
{ rintro (i|j),
{ exact sum.inl (L_equiv₁.symm i) },
{ exact sum.inr (L_equiv₂.symm j) }},
{ rintro (_|_); simp only [equiv.symm_apply_apply] },
{ rintro (_|_); simp only [equiv.apply_symm_apply] }},
{ fsplit, -- right moves
{ rintro (i|j),
{ exact sum.inl (R_equiv₁ i) },
{ exact sum.inr (R_equiv₂ j) }},
{ rintro (i|j),
{ exact sum.inl (R_equiv₁.symm i) },
{ exact sum.inr (R_equiv₂.symm j) }},
{ rintro (_|_); simp only [equiv.symm_apply_apply] },
{ rintro (_|_); simp only [equiv.apply_symm_apply] }},
{ rintro (i|j), -- move left
{ exact add_congr_relabelling
(L_relabelling₁ i)
(⟨L_equiv₂, R_equiv₂, L_relabelling₂, R_relabelling₂⟩) },
{ exact add_congr_relabelling
(⟨L_equiv₁, R_equiv₁, L_relabelling₁, R_relabelling₁⟩)
(L_relabelling₂ j) }},
{ rintro (i|j), -- move right
{ exact add_congr_relabelling
(R_relabelling₁ i)
(⟨L_equiv₂, R_equiv₂, L_relabelling₂, R_relabelling₂⟩) },
{ exact add_congr_relabelling
(⟨L_equiv₁, R_equiv₁, L_relabelling₁, R_relabelling₁⟩)
(R_relabelling₂ j) }},
end
using_well_founded { dec_tac := pgame_wf_tac }
/-- If `x` has the same moves as `y`, then `-x` has the sames moves as `-y`. -/
def neg_congr_relabelling : ∀ {x y : pgame}, x.relabelling y → (-x).relabelling (-y)
| (mk xl xr xL xR) (mk yl yr yL yR) ⟨L_equiv, R_equiv, L_relabelling, R_relabelling⟩ :=
⟨R_equiv, L_equiv,
λ i, neg_congr_relabelling (by simpa using R_relabelling (R_equiv i)),
λ i, neg_congr_relabelling (by simpa using L_relabelling (L_equiv.symm i))⟩
/-- If `w` has the same moves as `x` and `y` has the same moves as `z`,
then `w - y` has the same moves as `x - z`. -/
theorem sub_congr_relabelling {w x y z : pgame}
(h₁ : w.relabelling x) (h₂ : y.relabelling z) : (w - y).relabelling (x - z) :=
add_congr_relabelling h₁ (neg_congr_relabelling h₂)
/-- If `a` has the same moves as `x`, `b` has the same moves as `y`,
and `c` has the same moves as `z`, then `a + b - c` has the same moves as `y + x - z`. -/
lemma add_sub_comm {a b c x y z : pgame}
(h₁ : a.relabelling x) (h₂ : b.relabelling y) (h₃ : c.relabelling z) :
(a + b - c).relabelling (y + x - z) :=
sub_congr_relabelling
(relabelling.trans
(add_comm_relabelling a b)
(add_congr_relabelling h₂ h₁)) h₃
/-- `x * y` has exactly the same moves as `y * x`. -/
theorem mul_comm_relabelling (x y : pgame) : (x * y).relabelling (y * x):=
begin
induction x with xl xr xL xR I1 I2 generalizing y,
induction y with yl yr yL yR J1 J2,
refine ⟨_,_,_,_⟩,
{ fsplit; rintro (⟨i, j⟩ | ⟨i, j⟩);
exact sum.inl (j,i) <|> exact sum.inr (j,i) <|> refl },
{ fsplit; rintro (⟨i, j⟩ | ⟨i, j⟩);
exact sum.inl (j,i) <|> exact sum.inr (j,i) <|> refl },
{ rintro (⟨i, j⟩ | ⟨i, j⟩),
{ exact add_sub_comm (I1 i (mk yl yr yL yR)) (J1 j) (I1 i (yL j)) },
{ exact add_sub_comm (I2 i (mk yl yr yL yR)) (J2 j) (I2 i (yR j)) }},
{ rintro (⟨i, j⟩ | ⟨i, j⟩),
{ exact add_sub_comm (I2 j (mk yl yr yL yR)) (J1 i) (I2 j (yL i)) },
{ exact add_sub_comm (I1 j (mk yl yr yL yR)) (J2 i) (I1 j (yR i)) }}
end
/-- `x * y` is equivalent to `y * x`. -/
theorem mul_comm_equiv (x y : pgame) : (x * y).equiv (y * x) :=
equiv_of_relabelling (mul_comm_relabelling x y)
/-- `x * 0` has exactly the same moves as `0`. -/
theorem mul_zero_relabelling : Π (x : pgame), relabelling (x * 0) 0
| (mk xl xr xL xR) :=
⟨by fsplit; rintro (⟨_,⟨⟩⟩ | ⟨_,⟨⟩⟩),
by fsplit; rintro (⟨_,⟨⟩⟩ | ⟨_,⟨⟩⟩),
by rintro (⟨_,⟨⟩⟩ | ⟨_,⟨⟩⟩),
by rintro ⟨⟩⟩
/-- `x * 0` is equivalent to `0`. -/
theorem mul_zero_equiv (x : pgame) : (x * 0).equiv 0 :=
equiv_of_relabelling (mul_zero_relabelling x)
/-- `0 * x` has exactly the same moves as `0`. -/
theorem zero_mul_relabelling : Π (x : pgame), relabelling (0 * x) 0
| (mk xl xr xL xR) :=
⟨by fsplit; rintro (⟨⟨⟩,_⟩ | ⟨⟨⟩,_⟩),
by fsplit; rintro (⟨⟨⟩,_⟩ | ⟨⟨⟩,_⟩),
by rintro (⟨⟨⟩,_⟩ | ⟨⟨⟩,_⟩),
by rintro ⟨⟩⟩
/-- `0 * x` is equivalent to `0`. -/
theorem zero_mul_equiv (x : pgame) : (0 * x).equiv 0 :=
equiv_of_relabelling (zero_mul_relabelling x)
end pgame
```

#### Kevin Buzzard (Apr 26 2021 at 13:56):

That is some very elegant-looking code! I hope you're PR'ing this stuff!

#### Apurva Nakade (Apr 26 2021 at 14:00):

Thanks! :)

I'll try to optimize the code a bit and PR it away.

#### Apurva Nakade (Apr 26 2021 at 14:01):

Would you recommend opening up a single PR for the entire thing?

#### Eric Wieser (Apr 26 2021 at 14:03):

If by "entire thing" you mean that medium-length code block above, definitely

#### Eric Wieser (Apr 26 2021 at 14:03):

if you mean "Everything you intend to do on surreal numbers after that" too, then probably not!

#### Eric Wieser (Apr 26 2021 at 14:04):

It's tempting to rename `equiv_of_relabelling`

to `relabelling.equiv`

, and then you can probably just remove the `zero_mul_equiv`

etc lemmas as they become `(zero_mul_relabelling x).equiv`

#### Apurva Nakade (Apr 26 2021 at 14:07):

Great, I'll do that.

There are quite a few other `_equiv`

lemmas in pgame and surreal that are like that. Will need to change that as well.

#### Eric Wieser (Apr 26 2021 at 14:21):

That might make sense to do as a standalone "chore" or "refactor" PR

#### Eric Wieser (Apr 26 2021 at 14:21):

If you're looking for an excuse to split your PR in two :)

#### Apurva Nakade (Apr 26 2021 at 15:11):

It should be fine. Those theorems are never used anywhere :P

#### Apurva Nakade (Apr 27 2021 at 04:33):

Eric Wieser said:

It's tempting to rename

`equiv_of_relabelling`

to`relabelling.equiv`

, and then you can probably just remove the`zero_mul_equiv`

etc lemmas as they become`(zero_mul_relabelling x).equiv`

This is turning out to be more complicated than I first thought. I'll follow your suggestion of opening a separate PR for refactoring.

#### Apurva Nakade (Apr 28 2021 at 18:30):

TIL: For pgames, it turns out that `a*(b+c)`

is not a relabelling of `a*b + a*c`

. You get a term `x - x`

on one side and `0`

on the other.

#### Scott Morrison (Apr 28 2021 at 23:23):

Given multiplication only really works on surreals, not on games, you expect it to break at some point. But it's nice to know this is where it starts, I didn't know that at all!

#### Eric Wieser (Apr 28 2021 at 23:36):

Is it worth PRing the statement that no such relabeling exists?

#### Scott Morrison (Apr 28 2021 at 23:44):

Meh, not really.

#### Apurva Nakade (Apr 29 2021 at 00:49):

I too discovered this completely accidentally. Just the number of terms on the two sides do not agree.

#### Apurva Nakade (Apr 29 2021 at 00:49):

My current hope is to define the following:

```
inductive weak_relabelling : pgame.{u} → pgame.{u} → Type (u+1)
| mk : Π {x y : pgame} (L : x.left_moves ≃ y.left_moves) (R : x.right_moves ≃ y.right_moves),
(∀ (i : x.left_moves), (x.move_left i).equiv (y.move_left (L i))) →
(∀ (j : y.right_moves), (x.move_right (R.symm j)).equiv (y.move_right j)) →
weak_relabelling x y
```

#### Apurva Nakade (Apr 29 2021 at 00:50):

and hope that `weak_relabelling`

implies `equiv`

.

#### Apurva Nakade (Apr 29 2021 at 00:51):

I think this should provide `mul_comm_weak_relabelling`

for pgames too, not just surreals.

#### Mario Carneiro (Apr 29 2021 at 01:54):

Isn't this just the same as `equiv`

?

#### Mario Carneiro (Apr 29 2021 at 01:55):

why not prove `equiv`

directly?

#### Mario Carneiro (Apr 29 2021 at 01:55):

(specifically, rather than a new inductive that should be a lemma about `equiv`

)

#### Apurva Nakade (Apr 29 2021 at 02:45):

For `equiv`

we'll need to show that `a*(b+c) \le a*b + a*c`

and `a*b + a*c \le a*(b+c)`

.

#### Apurva Nakade (Apr 29 2021 at 02:45):

I'm not entirely sure how to do either tbh

#### Scott Morrison (Apr 29 2021 at 03:55):

Mario is suggesting that you prove

```
lemma foo {x y : pgame} (L : x.left_moves ≃ y.left_moves) (R : x.right_moves ≃ y.right_moves),
(∀ (i : x.left_moves), (x.move_left i).equiv (y.move_left (L i))) →
(∀ (j : y.right_moves), (x.move_right (R.symm j)).equiv (y.move_right j)),
x.equiv y
```

#### Apurva Nakade (Apr 29 2021 at 05:01):

I see, so instead of an inductive type do a lemma. Sounds good!

#### Mario Carneiro (Apr 29 2021 at 05:02):

By the way, if you are wondering how to prove the lemma, note that this is exactly the inductive step in the proof of `equiv_of_relabelling`

#### Apurva Nakade (Apr 29 2021 at 05:05):

Awesome, thanks!!

#### Apurva Nakade (Apr 30 2021 at 15:45):

Any suggestions for proving this:

```
import set_theory.pgame
local infix ` ≈ ` := pgame.equiv
lemma aux {a b c d e : pgame} : (a + b) + (c + d) - (e + b) ≈ a + c - e + d :=
sorry
```

?

This is the last lemma I need for proving `left_distrib_equiv`

.

#### Mario Carneiro (Apr 30 2021 at 15:46):

do you have the additive group lemmas?

#### Mario Carneiro (Apr 30 2021 at 15:47):

you shouldn't need to resort to relabellings all the time

#### Apurva Nakade (Apr 30 2021 at 15:59):

I'm having trouble because the `equiv`

instead of `=`

.

#### Apurva Nakade (Apr 30 2021 at 16:00):

There is an instance of `add_comm_group`

for `surreal`

but nothing for `pgames`

.

#### Mario Carneiro (Apr 30 2021 at 16:00):

If only there were a quotient you could use...

#### Mario Carneiro (Apr 30 2021 at 16:00):

Q: why do you care about pgame?

#### Apurva Nakade (Apr 30 2021 at 16:01):

Right now `mul`

is not defined for `surreals`

#### Mario Carneiro (Apr 30 2021 at 16:02):

it respects the quotient, doesn't it?

#### Mario Carneiro (Apr 30 2021 at 16:02):

also this lemma doesn't use mul

#### Apurva Nakade (Apr 30 2021 at 16:03):

Ah, I need this as an intermediate step for proving `a * (b + c) = a * b + a * c`

#### Apurva Nakade (Apr 30 2021 at 16:03):

i meant equiv for pgames

#### Mario Carneiro (Apr 30 2021 at 16:03):

I am saying, forget about pgames except as an implementation detail of surreal

#### Mario Carneiro (Apr 30 2021 at 16:04):

lift mul to surreal

#### Apurva Nakade (Apr 30 2021 at 16:04):

Yeah, there is a missing piece `numeric_mul`

for descending `mul`

to `surreal`

#### Apurva Nakade (Apr 30 2021 at 16:04):

I'll try to prove that directly

#### Apurva Nakade (Apr 30 2021 at 16:04):

Thanks!

#### Mario Carneiro (Apr 30 2021 at 16:05):

There may be a use for the quotient of pgame by equiv, without the numeric part

#### Mario Carneiro (Apr 30 2021 at 16:05):

that would be the easiest way to prove the theorem you mention

#### Mario Carneiro (Apr 30 2021 at 16:06):

I'm not sure what the benefit of restricting to numeric is, I guess some laws don't hold

#### Apurva Nakade (Apr 30 2021 at 16:06):

Ah interesting, I think Conway calls them pseudo-numbers

#### Apurva Nakade (Apr 30 2021 at 16:07):

Yeah, I can totally do that and all the proofs will simplify a lot!

#### Apurva Nakade (Apr 30 2021 at 16:08):

Would it then make sense to change the definition of `surreals`

as a subtype of `pseudo-numbers`

?

#### Mario Carneiro (Apr 30 2021 at 16:08):

ah, `pgame.star`

is a witness to the failure of partial ordering

#### Apurva Nakade (Apr 30 2021 at 16:09):

Right, they have the ring structure but not the order or field structures

#### Mario Carneiro (Apr 30 2021 at 16:14):

Oops, this already exists

#### Mario Carneiro (Apr 30 2021 at 16:14):

that's `game`

#### Apurva Nakade (Apr 30 2021 at 16:21):

Great, I'll check that out and figure out how to connect it back to surreal numbers.

#### Mario Carneiro (Apr 30 2021 at 16:22):

Actually there is a complication, because I think that `pgame.numeric`

does not respect the equivalence relation. You can take as the subtype the assertion that some pgame in the equivalence class is numeric, but then functions that are lifted have to sometimes be evaluated on non-numeric pgames

#### Mario Carneiro (Apr 30 2021 at 16:23):

Alternatively, you can just leave the definition as is and construct an injection `surreal -> game`

so that you can prove theorems about surreal by injecting them into `game`

#### Apurva Nakade (Apr 30 2021 at 16:34):

Creating `surreal -> game`

is a more natural thing to do. But I still need to define `mul`

on surreals.

#### Apurva Nakade (Apr 30 2021 at 16:35):

I suspect that it should not be too difficult

#### Mario Carneiro (Apr 30 2021 at 16:35):

Here is a proof of your lemma using `game`

```
import set_theory.game tactic.abel
local infix ` ≈ ` := pgame.equiv
lemma aux {a b c d e : pgame} : (a + b) + (c + d) - (e + b) ≈ a + c - e + d :=
begin
letI := pgame.setoid,
apply @quotient.exact pgame,
change (⟦a⟧ + ⟦b⟧ + (⟦c⟧ + ⟦d⟧) - (⟦e⟧ + ⟦b⟧) : game) = ⟦a⟧ + ⟦c⟧ + -⟦e⟧ + ⟦d⟧,
abel,
end
```

#### Apurva Nakade (Apr 30 2021 at 16:36):

Awesome, thanks so much!

#### Yakov Pechersky (Apr 30 2021 at 16:38):

No need for `letI`

, just `apply @quotient.exact' pgame`

#### Mario Carneiro (Apr 30 2021 at 16:39):

actually just deleting the letI is enough

#### Mario Carneiro (Apr 30 2021 at 16:39):

because this is actually the official setoid on pgame

#### Apurva Nakade (Apr 30 2021 at 16:42):

This trick of jumping to `games`

looks really useful. I can probably use it to simplify a lot of other nasty proofs in `surreal.lean`

.

#### Apurva Nakade (May 01 2021 at 05:19):

When I added `import set_theory.game`

to `surreal.lean`

I started getting type mismatch errors.

For example here : https://github.com/leanprover-community/mathlib/blob/6b6366b351f3e3c242e620aa0c39a4dc1eca8c10/src/set_theory/surreal.lean#L408 (on branch surreal_mul_distrib)

I am getting the following error:

```
type mismatch at application
has_add.add w
term
w
has type
pgame : Type (u+1)
but is expected to have type
game : Type (?+1)
state:
w x y z : pgame,
ow : w.numeric,
ox : x.numeric,
oy : y.numeric,
oz : z.numeric,
ix : x.left_moves,
hix : w ≤ x.move_left ix,
iz : z.left_moves,
hiz : y ≤ z.move_left iz
⊢ w + y ≤ x.move_left ix + z
```

Lean is interpreting `has_add.add`

as the addition of `game`

s instead of `pgame`

s.

The `\le`

also broke in a few places but I was able to fix it using `pgame.le_refl`

.

Any suggestions on how to resolve this? Thanks,

Last updated: May 18 2021 at 08:14 UTC