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: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):

(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.

docs#nat.cast

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,
end

theorem add_zero : ∀ x : surreal, x + 0 = x :=
begin
rintros ⟨x, ox⟩,
apply quotient.sound,
end

zero := 0,

end surreal


Weirdly I'm not able to merge the two applys.

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 _,
end


and then it's easy:

theorem zero_add : ∀ x : surreal, 0 + x = x :=
begin
rintros ⟨x, ox⟩,
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⟩,
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

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⟩,
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))

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,
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₂⟩ },

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 pgames 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
(L_relabelling₁ i)
(⟨L_equiv₂, R_equiv₂, L_relabelling₂, R_relabelling₂⟩) },
(⟨L_equiv₁, R_equiv₁, L_relabelling₁, R_relabelling₁⟩)
(L_relabelling₂ j) }},
{ rintro (i|j), -- move right
(R_relabelling₁ i)
(⟨L_equiv₂, R_equiv₂, L_relabelling₂, R_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) :=

/-- 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

/-- 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?

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

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):

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
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 games instead of pgames.
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