Zulip Chat Archive

Stream: maths

Topic: Surreal numbers


view this post on Zulip 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,

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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 ;-)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Apr 12 2021 at 22:29):

src#numeric.add

view this post on Zulip Yakov Pechersky (Apr 12 2021 at 22:30):

I mean src#pgame.numeric_add

view this post on Zulip Yakov Pechersky (Apr 12 2021 at 22:30):

oy indeed

view this post on Zulip Yakov Pechersky (Apr 12 2021 at 22:31):

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

from the source :scared:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Apr 12 2021 at 23:15):

view this post on Zulip Scott Morrison (Apr 12 2021 at 23:15):

(Spoiler also contains numeric_omega.)

view this post on Zulip Apurva Nakade (Apr 12 2021 at 23:26):

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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Apr 12 2021 at 23:29):

That's exactly what it's doing

view this post on Zulip 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)) : ℕ

view this post on Zulip Yakov Pechersky (Apr 12 2021 at 23:30):

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

view this post on Zulip Yakov Pechersky (Apr 12 2021 at 23:31):

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

view this post on Zulip Apurva Nakade (Apr 12 2021 at 23:35):

Interesting!!

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

view this post on Zulip 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! :-)

view this post on Zulip Yakov Pechersky (Apr 13 2021 at 00:02):

Not natural numbers. Anything that is notated by numerical digits

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Apr 13 2021 at 14:25):

Looks good, PR away. (Indenting inside begin ... end blocks! :-)

view this post on Zulip Scott Morrison (Apr 13 2021 at 14:26):

(Also, in spoiler tags, you can put another ```lean block inside to get formatting.

view this post on Zulip 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"?

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Apr 13 2021 at 15:16):

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

view this post on Zulip Yakov Pechersky (Apr 13 2021 at 15:16):

docs#nat.cast

view this post on Zulip Yakov Pechersky (Apr 13 2021 at 15:18):

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

view this post on Zulip 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 applys.

Thanks,

view this post on Zulip 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

view this post on Zulip Apurva Nakade (Apr 15 2021 at 15:14):

Oh I see, I was missing that _ at the end.
Thanks!

view this post on Zulip 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 _)

view this post on Zulip 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

view this post on Zulip 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⟩ := ....

view this post on Zulip 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

view this post on Zulip Apurva Nakade (Apr 15 2021 at 15:42):

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

view this post on Zulip 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.

view this post on Zulip Apurva Nakade (Apr 15 2021 at 15:44):

Interesting! Thanks,

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Apr 19 2021 at 17:14):

Which is more work, but unfolds more nicely

view this post on Zulip Eric Wieser (Apr 19 2021 at 17:16):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 19 2021 at 17:30):

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

view this post on Zulip 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

view this post on Zulip 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/2n+1={01/2n} 1/2^{n+1} = \{ 0 | 1/2^n \} . More generally, (x+y)/2={xy} (x + y)/2 = \{ x | y \} works when xx and yy are adjacent numbers created on the same day.

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

view this post on Zulip 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)/2m:=(x+y)/2, for example by proving that m+m=x+ym+m=x+y

view this post on Zulip Mario Carneiro (Apr 19 2021 at 21:15):

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

view this post on Zulip Mario Carneiro (Apr 19 2021 at 21:16):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Apurva Nakade (Apr 19 2021 at 22:01):

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

view this post on Zulip Apurva Nakade (Apr 19 2021 at 22:03):

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

view this post on Zulip Mario Carneiro (Apr 19 2021 at 22:06):

Do we know that the surreals are a field?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 19 2021 at 22:13):

Oh, it's not even proved to be numeric

view this post on Zulip Mario Carneiro (Apr 19 2021 at 22:13):

that should be fairly easy

view this post on Zulip Mario Carneiro (Apr 19 2021 at 22:14):

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

view this post on Zulip Apurva Nakade (Apr 19 2021 at 22:15):

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

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (Apr 19 2021 at 22:24):

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

view this post on Zulip Mario Carneiro (Apr 19 2021 at 22:26):

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

view this post on Zulip Mario Carneiro (Apr 19 2021 at 22:39):

Oh, pgame already has add_comm proved, it just needs to be packed up

view this post on Zulip Mario Carneiro (Apr 19 2021 at 22:39):

don't see anything about the other field operations though

view this post on Zulip Apurva Nakade (Apr 20 2021 at 14:51):

Right, I'll work on proving things about mul first.

view this post on Zulip 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.

view this post on Zulip Alex J. Best (Apr 21 2021 at 23:35):

If you run tidy? instead, it will tell you what tactics it did.

view this post on Zulip 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:

view this post on Zulip Eric Rodriguez (Apr 21 2021 at 23:38):

yeah was just about to post that, lol

view this post on Zulip Eric Rodriguez (Apr 21 2021 at 23:38):

finish is also good

view this post on Zulip Eric Rodriguez (Apr 21 2021 at 23:39):

(although in this case it completely fails)

view this post on Zulip Apurva Nakade (Apr 21 2021 at 23:42):

tidy ftw :sunglasses:

view this post on Zulip 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.

view this post on Zulip 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. :-)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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,

view this post on Zulip 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))⟩

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 13:56):

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

view this post on Zulip Apurva Nakade (Apr 26 2021 at 14:00):

Thanks! :)

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

view this post on Zulip Apurva Nakade (Apr 26 2021 at 14:01):

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

view this post on Zulip Eric Wieser (Apr 26 2021 at 14:03):

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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Apr 26 2021 at 14:21):

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

view this post on Zulip Eric Wieser (Apr 26 2021 at 14:21):

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

view this post on Zulip Apurva Nakade (Apr 26 2021 at 15:11):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Eric Wieser (Apr 28 2021 at 23:36):

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

view this post on Zulip Scott Morrison (Apr 28 2021 at 23:44):

Meh, not really.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Apurva Nakade (Apr 29 2021 at 00:50):

and hope that weak_relabelling implies equiv.

view this post on Zulip Apurva Nakade (Apr 29 2021 at 00:51):

I think this should provide mul_comm_weak_relabelling for pgames too, not just surreals.

view this post on Zulip Mario Carneiro (Apr 29 2021 at 01:54):

Isn't this just the same as equiv?

view this post on Zulip Mario Carneiro (Apr 29 2021 at 01:55):

why not prove equiv directly?

view this post on Zulip Mario Carneiro (Apr 29 2021 at 01:55):

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

view this post on Zulip 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).

view this post on Zulip Apurva Nakade (Apr 29 2021 at 02:45):

I'm not entirely sure how to do either tbh

view this post on Zulip 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

view this post on Zulip Apurva Nakade (Apr 29 2021 at 05:01):

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

view this post on Zulip 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

view this post on Zulip Apurva Nakade (Apr 29 2021 at 05:05):

Awesome, thanks!!

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 30 2021 at 15:46):

do you have the additive group lemmas?

view this post on Zulip Mario Carneiro (Apr 30 2021 at 15:47):

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

view this post on Zulip Apurva Nakade (Apr 30 2021 at 15:59):

I'm having trouble because the equiv instead of =.

view this post on Zulip Apurva Nakade (Apr 30 2021 at 16:00):

There is an instance of add_comm_group for surreal but nothing for pgames.

view this post on Zulip Mario Carneiro (Apr 30 2021 at 16:00):

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

view this post on Zulip Mario Carneiro (Apr 30 2021 at 16:00):

Q: why do you care about pgame?

view this post on Zulip Apurva Nakade (Apr 30 2021 at 16:01):

Right now mul is not defined for surreals

view this post on Zulip Mario Carneiro (Apr 30 2021 at 16:02):

it respects the quotient, doesn't it?

view this post on Zulip Mario Carneiro (Apr 30 2021 at 16:02):

also this lemma doesn't use mul

view this post on Zulip 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

view this post on Zulip Apurva Nakade (Apr 30 2021 at 16:03):

i meant equiv for pgames

view this post on Zulip Mario Carneiro (Apr 30 2021 at 16:03):

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

view this post on Zulip Mario Carneiro (Apr 30 2021 at 16:04):

lift mul to surreal

view this post on Zulip Apurva Nakade (Apr 30 2021 at 16:04):

Yeah, there is a missing piece numeric_mul for descending mul to surreal

view this post on Zulip Apurva Nakade (Apr 30 2021 at 16:04):

I'll try to prove that directly

view this post on Zulip Apurva Nakade (Apr 30 2021 at 16:04):

Thanks!

view this post on Zulip Mario Carneiro (Apr 30 2021 at 16:05):

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

view this post on Zulip Mario Carneiro (Apr 30 2021 at 16:05):

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

view this post on Zulip 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

view this post on Zulip Apurva Nakade (Apr 30 2021 at 16:06):

Ah interesting, I think Conway calls them pseudo-numbers

view this post on Zulip Apurva Nakade (Apr 30 2021 at 16:07):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 30 2021 at 16:08):

ah, pgame.star is a witness to the failure of partial ordering

view this post on Zulip Apurva Nakade (Apr 30 2021 at 16:09):

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

view this post on Zulip Mario Carneiro (Apr 30 2021 at 16:14):

Oops, this already exists

view this post on Zulip Mario Carneiro (Apr 30 2021 at 16:14):

that's game

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Apurva Nakade (Apr 30 2021 at 16:35):

I suspect that it should not be too difficult

view this post on Zulip 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

view this post on Zulip Apurva Nakade (Apr 30 2021 at 16:36):

Awesome, thanks so much!

view this post on Zulip Yakov Pechersky (Apr 30 2021 at 16:38):

No need for letI, just apply @quotient.exact' pgame

view this post on Zulip Mario Carneiro (Apr 30 2021 at 16:39):

actually just deleting the letI is enough

view this post on Zulip Mario Carneiro (Apr 30 2021 at 16:39):

because this is actually the official setoid on pgame

view this post on Zulip 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.

view this post on Zulip 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 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