Surreal numbers

Stream: maths

[Apurva Nakade]

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]

If you have 0 and 1 (which you found), then you only need + to get the coercion.

[Apurva Nakade]

Oh, I see, so Lean is automatically defining n.succ : pgame as n : pgame + 1 : pgame
This is really efficient! Thanks!

[Kevin Buzzard]

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]

As far as I remember, there isn't a clear proof that pgame.short_add is properly commutative and associative.

[Apurva Nakade]

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]

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]

src#numeric.add

[Yakov Pechersky]

I mean src#pgame.numeric_add

[Yakov Pechersky]

oy indeed

[Yakov Pechersky]

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

from the source :scared:

[Apurva Nakade]

Oh wow! Thank you so much!!
I totally missed this. I'll spend some time trying to understand the proof.

[Scott Morrison]

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]

theorem numeric_nat (n : ℕ) : numeric n :=
begin
  induction n with n ih,
  { exact numeric_zero, },
  { rw nat.succ_eq_add_one,
    apply numeric_add ih numeric_one, },
end
theorem numeric_omega : numeric omega :=
begin
  refine ⟨_, _, _⟩,
  { rintro - ⟨⟩, },
  { rintro ⟨n⟩,
    apply numeric_nat, },
  { rintro ⟨⟩, },
end

[Scott Morrison]

(Spoiler also contains numeric_omega.)

[Apurva Nakade]

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

[Apurva Nakade]

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]

That's exactly what it's doing

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

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

[Apurva Nakade]

Interesting!!

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

[Scott Morrison]

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

Not natural numbers. Anything that is notated by numerical digits

[Apurva Nakade]

Just for the record here's one more solution

Spoiler (numeric_nat numeric_omega)

import set_theory.surreal
open pgame

theorem numeric_nat (n : ℕ) : numeric n :=
begin
induction n with n hn,
apply numeric_zero,
apply numeric_add hn numeric_one,
end

theorem numeric_omega : numeric omega :=
⟨by rintros ⟨ ⟩ ⟨ ⟩, λ i, by simp [numeric_nat i.down] , by simp only [forall_pempty]⟩

#check numeric_nat
#check numeric_omega

I'll try to get it in the library.

[Scott Morrison]

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

[Scott Morrison]

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

[Apurva Nakade]

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]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

docs#nat.cast

[Yakov Pechersky]

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

[Apurva Nakade]

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,

[Kevin Buzzard]

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]

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

[Eric Wieser]

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]

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]

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]

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]

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

[Yakov Pechersky]

You can try using quot.sound and quot.ind instead, which do not try to infer the setoid on their own.

[Apurva Nakade]

Interesting! Thanks,

[Apurva Nakade]

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]

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]

There's no point defining sub there like that, it will use that definition for you automatically.

[Eric Wieser]

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

[Eric Wieser]

Which is more work, but unfolds more nicely

[Eric Wieser]

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

[Apurva Nakade]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Apurva Nakade]

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]

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]

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]

Do we know that the surreals are a field?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Apurva Nakade]

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]

Oh, it's not even proved to be numeric

[Mario Carneiro]

that should be fairly easy

[Mario Carneiro]

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

[Apurva Nakade]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

don't see anything about the other field operations though

[Apurva Nakade]

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

[Apurva Nakade]

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]

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

[Apurva Nakade]

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]

yeah was just about to post that, lol

[Eric Rodriguez]

finish is also good

[Eric Rodriguez]

(although in this case it completely fails)

[Apurva Nakade]

tidy ftw :sunglasses:

[Scott Morrison]

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]

The first step of mindlessly golfing a tidy proof is to add newlines and indentation, so you have a hope. :-)

[Kevin Buzzard]

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]

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]

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]

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]

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]

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

[Apurva Nakade]

Thanks! :)

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

[Apurva Nakade]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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]

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

[Eric Wieser]

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

[Apurva Nakade]

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

[Apurva Nakade]

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]

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]

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]

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

[Scott Morrison]

Meh, not really.

[Apurva Nakade]

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

[Apurva Nakade]

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]

and hope that weak_relabelling implies equiv.

[Apurva Nakade]

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

[Mario Carneiro]

Isn't this just the same as equiv?

[Mario Carneiro]

why not prove equiv directly?

[Mario Carneiro]

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

[Apurva Nakade]

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]

I'm not entirely sure how to do either tbh

[Scott Morrison]

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]

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

[Mario Carneiro]

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]

Awesome, thanks!!

[Apurva Nakade]

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]

do you have the additive group lemmas?

[Mario Carneiro]

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

[Apurva Nakade]

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

[Apurva Nakade]

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

[Mario Carneiro]

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

[Mario Carneiro]

Q: why do you care about pgame?

[Apurva Nakade]

Right now mul is not defined for surreals

[Mario Carneiro]

it respects the quotient, doesn't it?

[Mario Carneiro]

also this lemma doesn't use mul

[Apurva Nakade]

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

[Apurva Nakade]

i meant equiv for pgames

[Mario Carneiro]

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

[Mario Carneiro]

lift mul to surreal

[Apurva Nakade]

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

[Apurva Nakade]

I'll try to prove that directly

[Apurva Nakade]

Thanks!

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Apurva Nakade]

Ah interesting, I think Conway calls them pseudo-numbers

[Apurva Nakade]

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

[Apurva Nakade]

Would it then make sense to change the definition of surreals as a subtype of pseudo-numbers?

[Mario Carneiro]

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

[Apurva Nakade]

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

[Mario Carneiro]

Oops, this already exists

[Mario Carneiro]

that's game

[Apurva Nakade]

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

[Mario Carneiro]

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]

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]

Creating surreal -> game is a more natural thing to do. But I still need to define mul on surreals.

[Apurva Nakade]

I suspect that it should not be too difficult

[Mario Carneiro]

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]

Awesome, thanks so much!

[Yakov Pechersky]

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

[Mario Carneiro]

actually just deleting the letI is enough

[Mario Carneiro]

because this is actually the official setoid on pgame

[Apurva Nakade]

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]

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,

[Mike Shulman]

What is the status of multiplication of surreal numbers in mathlib? In the documentation here I see

The definition of multiplication for surreal numbers is surprisingly difficult and is currently missing in the library...This will make for a fun and challenging project.

but it sounds from the discussion above as though some progress was made? I have a student who might be interested in contributing to this if it is still open.

[Rob Lewis]

@Apurva Nakade ?

[Apurva Nakade]

Hi @Mike Shulman , I gave up on trying to prove that product of numbers is a number because the proofs got too long and my local machine could not handle them! I don't think anyone is working on this right now. It should make for a nice project but the theorems in Conway's book are not enough and one would need to come up with smart ways to simplify the proof.

[Apurva Nakade]

Once you have this, the later proofs would simplify greatly, especially the theorems in docs#surreal.dyadic so it would be amazing if your students can make it work.

[Apurva Nakade]

Theorem 3.8 here is the one I tried formalizing.

[Mike Shulman]

Thanks!

[Michael Stoll]

Hi, as it happens, I was sending an email to Mario Carneiro just today with essentially the same question that @Mike Shulman asked: I also have a student who would be interested in working on this for her Master's thesis.
Since I am responsible for the proof of Theorem 3.8 in the paper linked to by @Apurva Nakade (even though I did this quite some time ago), I would hope that I can provide enough help to my student to get the proof (or a variant of it) formalized.
On the other hand, I would not want to sort of "steal" the topic from @Mike Shulman , who asked before me. So I'm not sure how to proceed from here...

[Mike Shulman]

I will PM you.

[Violeta Hernández]

Hi, I'm working on this!

[Violeta Hernández]

I believe to have found a way to complete the proof of multiplication well definedness in a way that is actually nice to work with

[Violeta Hernández]

I'm only like 80% sure that this works

[Violeta Hernández]

The precise statement you prove is this 370964201478553600.png

[Violeta Hernández]

And the way you prove this is by proving that for any game g, if x + y + z is a relabelling of g, then that statement is true

[Violeta Hernández]

You induct on g using the subsequent relation

[Violeta Hernández]

I'll try actually writing the proof down later today or tomorrow, wish me luck!

[Violeta Hernández]

Oh, and this works since you just get the inductive hypothesis with subsequent and reordered arguments, which means that the sum ends up a relabelling of some subsequent game

[Violeta Hernández]

Update: the exact induction I posted doesn't work, but I got something pretty similar that seems very promising. I'll be posting my progress on the surreal_mul branch.

[Eric Wieser]

(branch#surreal_mul)

[Violeta Hernández]

Great news everyone! I believe I finally nailed the induction hypothesis

[Violeta Hernández]

I've updated the branch

[Violeta Hernández]

If we prove mul_args.result, the result follows

[Violeta Hernández]

And that itself can be proven by well foundedness on the relation I defined on that type

[Violeta Hernández]

I'll continue sketching the proof in the following days

[Violeta Hernández]

I've run into a problem I did not expect to run into

[Violeta Hernández]

I think mathlib may have the wrong definition of < on games?

[Violeta Hernández]

ONAG doesn't seem to define <, but it does define ≰, which is already really weird, given that in mathlib, x < y is equivalent to ¬ y ≤ x

[Violeta Hernández]

This other PDF I found does define <, but it defines x < y as x ≤ y ∧ ¬ y ≤ x

[Violeta Hernández]

Which is the definition that would hold if < came from a partial_order, but mathlib makes it clear that those two definitions conflict?

[Violeta Hernández]

So, what's the deal here? Was the choice of defining x < y as ¬ y ≤ x intentional?

[Violeta Hernández]

Or was it some accident we've perpetrated that has somehow not broken anything yet?

[Reid Barton]

Violeta Hernández said:

given that in mathlib, x < y is equivalent to ¬ y ≤ x

Are you talking about game in particular?

[Violeta Hernández]

Oh yeah, I should have mentioned that

[Violeta Hernández]

I'm talking about both pgame and game

[Violeta Hernández]

Yeah, there is something very wrong

[Violeta Hernández]

Every source I've looked says that 0 < G means that Left can enforce a win in G no matter who starts

[Violeta Hernández]

And analogously for G < 0

[Violeta Hernández]

This conflicts directly with pgame.star_lt_zero

[Reid Barton]

It looks intentional for sure but I agree it seems strange.

[Violeta Hernández]

This seems to go all the way back to https://github.com/leanprover-community/mathlib/commit/b41277c70937d8cd46639bbef674e656e8e397dd

[Violeta Hernández]

@Scott Morrison what's your justification for this?

[Reid Barton]

I would even go so far as to say it is wrong, given that the module docstring says the theory is based on ONAG.

[Violeta Hernández]

Yeah, I'm increasingly convinced that this is flat out wrong

[Violeta Hernández]

My theory is this: the easiest way to define ≤ was to define both it and its negation simultaneously via Conway induction, and it was decided that the negation was going to be called < for convenience

[Scott Morrison]

I think this predates me: the stuff on pgame was adapted from existing material on surreal, and I just followed how that had been done. (I think? I'm very open to the possibility I misremember things, and did things badly wrong. :-)

[Scott Morrison]

Is the fix just to rename < on pgame to ≰?

[Scott Morrison]

I'm not sure anything is "wrong", just a terribly misleading symbol is being used. :-)

[Violeta Hernández]

Well, it's not just that

[Violeta Hernández]

If we're going to do that, we're also going to have to rename a bunch of theorems, refactor others, etc.

[Violeta Hernández]

And we're also going to have to add the correct API for the correct <

[Violeta Hernández]

By the way, I dug a bit deeper and I found https://github.com/leanprover-community/mathlib/commit/901178e2084d7d4a97bc2ddef68135eb124aa130

[Violeta Hernández]

So it seems like this goes back to @Mario Carneiro

[Reid Barton]

I guess the definition of < was generalized from surreal (where it is correct) to game (where it is not)

[Scott Morrison]

I don't understand though when you say "it's not just that", however: isn't the only problem that we should have used a different symbol than <? After replacing the symbols and appropriately updating declaration names, there's no discrepancy from ONAG, right?

[Scott Morrison]

And nothing currently in pgame.lean has anything to say about "the real <" used in other references?

[Violeta Hernández]

What I mean is, even if there's not really any maths to fix (Lean won't let us prove false things, that's kind of the point), there's a lot of API that needs to be tweaked

[Scott Morrison]

(Sorry, above I suggested we just need to replace all the use of < with ≰, but that's obviously literally wrong, because the order of arguments needs to flip.)

[Scott Morrison]

But yes, I agree this is worth fixing.

[Violeta Hernández]

I'll get to this in a few hours

[Yaël Dillies]

Ah! So game really ought to be a preorder, just as literally anything else in the library. I was really confused so as to why < on games ought to escape the rule.

[Violeta Hernández]

In fact, a partial_order

[Violeta Hernández]

And what's more, an ordered_add_comm_group

[Junyan Xu]

image.png
image.png
Here are the notations from Winning Ways (p.29, p.32, 2nd edition)

The same notations are on ONAG (1976), p.73, p.78:
image.png

[Junyan Xu]

So < should be ⧏ (⧏)
Vertical bar beside right triangle: ⧐
Unicode hexadecimal: 0x29d0
Left triangle beside vertical bar: ⧏
Unicode hexadecimal: 0x29cf
In block: Miscellaneous Mathematical Symbols-B

[Junyan Xu]

Violeta Hernández said:

In fact, a partial_order

Didn't you just claim game isn't a partial_order? (I think it is.)

[Yaël Dillies]

Precisely. Currently game is not a partial order when you use docs#game.has_lt. The question is whether we should make docs#game.partial_order an instance and use the < from there.

[Michael Stoll]

I had raised precisely this point (that < on games in mathlib is not compatible with < as defined by Conway &Co) in private communication with @Mario Carneiro a while ago. I'd be strongly in favor of changing the mathlib definition to be compatible with the literature.

[Mario Carneiro]

The notation is used on wikipedia; I believe this is where I got it from

[Mario Carneiro]

not on games, on surreals

[Michael Stoll]

BTW, it was mostly me who developed the proof of Theorem 3.8 in Schleicher-Stoll (trying to make Conway's somewhat vague arguments precise).
It is nice to see that this proof apparently can be formalized (and simplified in the process)!

[Michael Stoll]

Mario Carneiro said:

not on games, on surreals

This is the point: On surreals, < and <| are the same, since numbers are never fuzzy to each other.

[Michael Stoll]

But for games, there is the possibility that two games are incomparable ("fuzzy").

[Mario Carneiro]

I believe that the definition currently called < is important and plays a central role in the theory, but it is not obvious to me that this relation corresponds to < or <| and it would be good to have some literature evidence of such

[Michael Stoll]

By docs#game.not_le, for games, the current definition implies that x < y is the same as ¬y ≤ x.
However (as was pointed out in this thread above), ONAG defines x <| y as ¬y ≤ x(on page 78) and x < y as x ≤ y ∧ ¬y ≤ x. (BTW, Conway defines < the same way for (surreal) numbers (on page 4), but it eventually turns out that ≤ defines a linear order on numbers.)

[Yaël Dillies]

Oooh, this is why the literature on games was so confusing to me. I never realized that x <| y just meant ¬ y ≤ x.

[Michael Stoll]

(One motivation for Dierk Schleicher and myself to write our paper was that we felt that the order (first numbers, then games) in ONAG has the logic backwards, beacuse numbers are really special games...)

[Yaël Dillies]

Should we even define <|? game is a partial order among many others and I can't justify the fact that it gets to have a symbol that would make sense everywhere else but isn't used.

[Mario Carneiro]

The mutually recursive definition of <| and <= gives them equal status, even though they are provably negations of each other

[Mario Carneiro]

I think that is an argument that they should exist as definitions; for the notation I don't have much of an opinion

[Michael Stoll]

It may make sense to also define ||, to have all four possibilities and their combinations...

[Yaël Dillies]

Sure, but do we want to use <| after bootstrapping ≤? is your argument that we should do this because (≤)ᶜ doesn't have the recursive properties of <|? (but do we use those recursive properties anywhere?)

[Mario Carneiro]

note that <| is actually taken IIRC for some silly definition on option that is never used

[Johan Commelin]

But there is
Junyan Xu said:

So < should be ⧏ (⧏)
Vertical bar beside right triangle: ⧐
Unicode hexadecimal: 0x29d0
Left triangle beside vertical bar: ⧏
Unicode hexadecimal: 0x29cf
In block: Miscellaneous Mathematical Symbols-B

[Mario Carneiro]

https://github.com/leanprover-community/lean/blob/f722a688012753f6adbd57e3df7499d498d82945/library/init/data/option/basic.lean#L42-L43 <-- someone should PR remove these

[Johan Commelin]

Never used in mathlib, afaict

[Mario Carneiro]

I saw someone use lhoare once but it's just get_or_else with reversed argument order

[Mario Carneiro]

In any case I think these surreal/game notations would be localized so the option definitions don't matter

[Eric Wieser]

What does lhoare stand for?

[Eric Wieser]

Could also use ≰ (not less than or equal, U+2270, ≰) as notation, although my font makes a meal of it

[Johan Commelin]

Presumably "left/right operator" in Hoare logic or something like that (https://en.wikipedia.org/wiki/Hoare_logic)

[Michael Stoll]

Yaël Dillies said:

Sure, but do we want to use <| after bootstrapping ≤? is your argument that we should do this because (≤)ᶜ doesn't have the recursive properties of <|? (but do we use those recursive properties anywhere?)

⧏ (and ⧐) are used in various statements and proofs in ONAG, so they would be useful to have if we want to stay close to the standard reference.

[Yaël Dillies]

If we end up really using this as a separate definition/symbol, it should

• be available from has_le, instead of being specialized to game
• have a suggestive notation, to make it clear that it's just the negation of ≤

[Yaël Dillies]

After all, we do have docs#ne as a separate definition with notation ≠.

[Yaël Dillies]

It seems to me that the main argument for having a separate definition instead of just separate notation is that it allows dot notation.

[Mario Carneiro]

Eric Wieser said:

What does lhoare stand for?

like Johan I believe the names come from "left/right + [Tony] Hoare", but these are not operators I recognize from hoare logic

[Mario Carneiro]

unfortunately the originating commit doesn't give any clue as to the origin or intent behind the definitions

[Kevin Buzzard]

Mario Carneiro said:

https://github.com/leanprover-community/lean/blob/f722a688012753f6adbd57e3df7499d498d82945/library/init/data/option/basic.lean#L42-L43 <-- someone should PR remove these

You CS people can have them, we want fancy unicode for games, not ASCII art.

[Violeta Hernández]

@Michael Stoll the simplification I had found relied on a property that was true for mathlib < but not actually correct for the true <

[Violeta Hernández]

So other than restate depth in terms of birthdays and merge P2 with P4, it's almost the same argument

[Violeta Hernández]

I personally prefer the not less or equal symbol here, I find it much more straightforward (and I believe this is what Conway uses in ONAG)

[Violeta Hernández]

That said I'm not convinced that it's worth having as a separate relation, rather than just writing down \neg x \le y

[Violeta Hernández]

I also agree with Yaël that if we're going to make it a separate relation, it shouldn't be localized to games

[Violeta Hernández]

I imagine many of the theorems for \notle in games are still true on preorders

[Michael Stoll]

Violeta Hernández said:

So other than restate depth in terms of birthdays and merge P2 with P4, it's almost the same argument

OK, thanks for the clarification. The main thing is that the proof is correct (which I have to admit I was only 99% certain about).

[Violeta Hernández]

I wonder how useful it is to have these lemmas on ¬ x ≤ y

[Violeta Hernández]

@[simp] theorem mk_le_mk {xl xr xL xR yl yr yL yR} :
  (⟨xl, xr, xL, xR⟩ : pgame) ≤ ⟨yl, yr, yL, yR⟩ ↔
  (∀ i, ¬ mk yl yr yL yR ≤ xL i) ∧
  (∀ j, ¬ yR j ≤ mk xl xr xL xR) :=
sorry

@[simp] theorem mk_not_le_mk {xl xr xL xR yl yr yL yR} :
  ¬ mk yl yr yL yR ≤ mk xl xr xL xR ↔
  (∃ i, mk xl xr xL xR ≤ yL i) ∨
  (∃ j, xR j ≤ mk yl yr yL yR) :=
sorry

[Violeta Hernández]

They were previously lemmas on < which made sense to have, but now?

[Mario Carneiro]

those kind of lemmas will not play as well with simp

[Violeta Hernández]

Hmm, you're right

[Violeta Hernández]

I'm wondering if we should have the former at all

[Mario Carneiro]

?

[Violeta Hernández]

*latter

[Mario Carneiro]

Those are the definition of <= and <|, of course we want them

[Mario Carneiro]

and they make good simp lemmas too

[Violeta Hernández]

That's only assuming that we actually have notation for <|, and I'm skeptical of this being a good idea

[Mario Carneiro]

if there was no such notation it would still be exactly as written, just without the notation

[Violeta Hernández]

True, but surely it would be easier to just use mk_le_mk and, if needed, push_neg?

[Violeta Hernández]

What's more, this isn't even the form that push_neg gives for the lemma

[Violeta Hernández]

@[simp] theorem mk_not_le_mk {xl xr xL xR yl yr yL yR} :
  ¬ mk yl yr yL yR ≤ mk xl xr xL xR ↔
  (∀ i, ¬ mk xl xr xL xR ≤ yL i) →
  (∃ j, xR j ≤ mk yl yr yL yR) :=
by { rw mk_le_mk, push_neg, refl }

[Mario Carneiro]

That's not a good form at all

[Mario Carneiro]

I'm not a fan of gratuitous push_neg. These kind of theorems don't really need LEM and the proofs are shorter that way too

[Mario Carneiro]

I know most people don't care but I occasionally clean up LEM usage in fundamental logic lemmas where possible

[Mario Carneiro]

The negations here just confuse the tactics by making one variation look "more complex" than the other, leading to lots of symmetry breaking

[Violeta Hernández]

That might be a case for actually having a \notle relation on games

[Mario Carneiro]

I have a slight preference for x <| y over y \notle x because it puts the variables in the right order

[Mario Carneiro]

...in fact I think it has to be in that order for the recursive definition to work

[Mario Carneiro]

because (x <| y, x <= y) is what is defined by recursion

[Violeta Hernández]

Right

[Violeta Hernández]

Still, what kind of annoys me is that we'd be dealing with a really basic relation and have almost no API for it

[Mario Carneiro]

why no API?

[Violeta Hernández]

I mean, that thing I mentioned earlier, that most of the basic results on <| should in fact be basic results of \notle on preorders

[Violeta Hernández]

I'm not quite sure how we could leverage this

[Mario Carneiro]

We don't have a typeclass for converse-le-preorders so I wouldn't worry about it

[Violeta Hernández]

Also, another question

[Violeta Hernández]

How should the lemmas about <| be called?

[Mario Carneiro]

lf = less-fuzzy?

[Violeta Hernández]

I like that

[Violeta Hernández]

...no, I don't know, I still kinda agree with Yaël that it's silly to define this new symbol for games and nothing else, despite it making sense on any preorder

[Mario Carneiro]

Sure, that's a potential refactor to consider once there is more than 1 example

[Mario Carneiro]

it would be quite a lot of work and lf would not be nearly as good a name

[Violeta Hernández]

Mario Carneiro said:

The mutually recursive definition of <| and <= gives them equal status, even though they are provably negations of each other

I don't agree with this. I think that our simultaneous definition of these symbols is more of an inductive hack. If we really wanted to, we could have defined ≤ using the standard ZFC definition and just prove that the relation on pairs where entries can be swapped as long as at least one entry decreases is well-founded

[Violeta Hernández]

It's just easier not to do that

[Mario Carneiro]

I disagree, I would say that x <| y and ~(y <= x) are not intensionally equal in the same way that a + b and b + a are not intensionally equal

[Mario Carneiro]

it is a theorem, proven by induction, that they coincide

[Mario Carneiro]

The refactor I am talking about for preorder would be to add another field notle and a proof x \notle y <-> ~(x <= y), to be able to change the defeq of the notle relation beyond the default one

[Violeta Hernández]

Why would it need to be a field of preorder? We don't do this for \ge

[Mario Carneiro]

because it is changing the defeq

[Violeta Hernández]

This would be pretty easy to circumvent though

[Mario Carneiro]

We could do it for ge as well, if we had more than 0 examples where we want the defeqs to differ

[Violeta Hernández]

def le_not_ge : Π (x y : pgame), Prop × Prop
| (mk xl xr xL xR) (mk yl yr yL yR) :=
  -- the orderings of the clauses here are carefully chosen so that
  --   and.left/or.inl refer to moves by Left, and
  --   and.right/or.inr refer to moves by Right.
((∀ i : xl, (le_not_ge (xL i) ⟨yl, yr, yL, yR⟩).2) ∧
  (∀ j : yr, (le_not_ge ⟨xl, xr, xL, xR⟩ (yR j)).2),
(∃ i : yl, (le_not_ge ⟨xl, xr, xL, xR⟩ (yL i)).1) ∨
  (∃ j : xr, (le_not_ge (xR j) ⟨yl, yr, yL, yR⟩).1))
using_well_founded { dec_tac := pgame_wf_tac }

instance : has_le pgame := ⟨λ x y, (le_not_ge x y).1⟩
instance : has_lt pgame := ⟨λ x y, x ≤ y ∧ ¬ y ≤ x⟩

-- We need a few auxiliary theorems before proving that `(le_not_ge x y).2 ↔ ¬ y ≤ x`.

private theorem mk_le_mk_aux {xl xr xL xR yl yr yL yR} :
  mk xl xr xL xR ≤ mk yl yr yL yR ↔
  (∀ i, (le_not_ge (xL i) (mk yl yr yL yR)).2) ∧
  (∀ j, (le_not_ge (mk xl xr xL xR) (yR j)).2) :=
show (le_not_ge _ _).1 ↔ _, by rw le_not_ge

private theorem mk_not_le_mk_aux {xl xr xL xR yl yr yL yR} :
  (le_not_ge (mk xl xr xL xR) (mk yl yr yL yR)).2 ↔
  (∃ i, mk xl xr xL xR ≤ yL i) ∨
  (∃ j, xR j ≤ mk yl yr yL yR) :=
show (le_not_ge _ _).2 ↔ _, by { rw le_not_ge, refl }

private theorem le_not_ge_iff_aux {x y : pgame} :
  (x ≤ y ↔ ¬ (le_not_ge y x).2) ∧ ((le_not_ge x y).2 ↔ ¬ y ≤ x) :=
begin
  induction x with xl xr xL xR IHxl IHxr generalizing y,
  induction y with yl yr yL yR IHyl IHyr,
  simp only [mk_le_mk_aux, mk_not_le_mk_aux,
    not_and_distrib, not_or_distrib, not_forall, not_exists,
    and_comm, or_comm, IHxl, IHxr, IHyl, IHyr, iff_self, and_self]
end

private theorem le_not_ge_iff {x y : pgame} : (le_not_ge x y).2 ↔ ¬ y ≤ x :=
le_not_ge_iff_aux.2

@[simp] theorem mk_le_mk {xl xr xL xR yl yr yL yR} :
  mk xl xr xL xR ≤ mk yl yr yL yR ↔
  (∀ i, ¬ mk yl yr yL yR ≤ xL i) ∧
  (∀ j, ¬ yR j ≤ mk xl xr xL xR) :=
by simp_rw [mk_le_mk_aux, le_not_ge_iff]

theorem mk_not_le_mk {xl xr xL xR yl yr yL yR} :
  ¬ mk yl yr yL yR ≤ mk xl xr xL xR ↔
  (∃ i, mk xl xr xL xR ≤ yL i) ∨
  (∃ j, xR j ≤ ⟨yl, yr, yL, yR⟩) :=
by rw [←le_not_ge_iff, mk_not_le_mk_aux]

[Violeta Hernández]

Once you have those last two theorems, there's not really a need to invoke le_not_ge ever again

[Violeta Hernández]

So I don't think it's worth adding a new field to preorder for this

[Mario Carneiro]

I don't either

[Mario Carneiro]

I think that pgame specifically should have a notle definition

[Violeta Hernández]

Hmm... I think I'll take your compromise

[Violeta Hernández]

If there's ever another instance where we want this separate \notle definition, then we can take whatever theorems about it we prove here, and generalize those to preorders

[Violeta Hernández]

Until then, I'll just make it a definition on pgame specifically

[Mario Carneiro]

using the le_not_ge_iff lemma you can pretty easily eliminate <| in any theorem statements if you don't want to see it

[Violeta Hernández]

Oh and one last thing, what symbol are we going to use then?

[Mario Carneiro]

and pretty much the only theorems of interest for these converse-le-preorders are cyclic permutations of le_trans

[Violeta Hernández]

We could use <| or ⧏ or ◁

[Mario Carneiro]

I think Kevin wants to veto <|

[Violeta Hernández]

I'm not a fan either

[Violeta Hernández]

If we want to stick as closely as possible to Conway, we should be using ⧏

[Violeta Hernández]

(it looks kinda cramped in my font, though)

[Mario Carneiro]

lgtm

[Mario Carneiro]

it lines up in my lean font, it's a bit short on zulip

[Violeta Hernández]

Alright then

[Violeta Hernández]

I'll get refactoring

[Violeta Hernández]

If we're just going to change < to ⧏, then not that many things should be different by the end of this

[Violeta Hernández]

Oh, one last thing!

[Violeta Hernández]

The < error seems to have propagated to one other file

[Violeta Hernández]

winner.lean

[Mario Carneiro]

what error?

[Violeta Hernández]

image.png

[Violeta Hernández]

These two should just be 0 < G and G < 0 respectively

[Violeta Hernández]

And to me it seems like it isn't worth having a separate definition for that?

[Mario Carneiro]

The new definition of lt is this already, right?

[Mario Carneiro]

x < y <-> x <| y /\ x <= y

[Mario Carneiro]

if so I agree this doesn't need separate definition, we don't have pos on preorders

[Violeta Hernández]

Alright then

[Violeta Hernández]

For the moment I'll just replace < with ⧏ in those files, but I'll probably refactor those afterwards

[Mario Carneiro]

it might be worth stuffing the documentation about "left wins" and "right wins" in terms of positive and negative somewhere though, that's not very obvious

[Violeta Hernández]

Ah, this is a more technical issue, but how do you define a new symbol in Lean?

[Violeta Hernández]

I tried

local infix ` ⧏ ` := λ x y, (le_lf x y).2

and it tells me something about a missing precedence command

[Mario Carneiro]

put a :50 or something after the backticks

[Mario Carneiro]

it should probably line up with the numbers from #print <

[Violeta Hernández]

There goes, thanks!

[Violeta Hernández]

Should I also introduce ⧐ with a simp lemma x ⧐ y ↔ y ⧏ x or is that not worth it?

[Mario Carneiro]

let's do our best to pretend gt doesn't exist

[Violeta Hernández]

Yeah, I don't think it's worth it either

[Violeta Hernández]

Just to be sure,

@[simp] theorem not_le {x y : pgame} : ¬ x ≤ y ↔ y ⧏ x := not_le_lf.1
@[simp] theorem not_lf {x y : pgame} : ¬ x ⧏ y ↔ y ≤ x := not_le_lf.2

both of these should be simp, right?

[Violeta Hernández]

https://leanprover-community.github.io/mathlib_docs/set_theory/game/pgame.html#pgame.right_response

[Violeta Hernández]

Do we really need this? Seems pretty useless to me

[Violeta Hernández]

I guess it's a way to prove that x ≤ 0 actually means that Right wins as the second player?

[Mario Carneiro]

I don't see any obvious way to do so, it's more or less true by definition

[Violeta Hernández]

Yeah, that's my thought too

[Violeta Hernández]

There's currently a covariant_class_swap_add_lt instance on pgame

[Violeta Hernández]

Would it be worth it changing it into a covariant_class_swap_add_lf instance? I don't know if there's any API for covariant relations other than < or ≤

[Yaël Dillies]

No there is not.

[Violeta Hernández]

Could that API exist in the future, though? Surely it would just be a matter of not enforcing has_lt or has_le in those theorems

[Violeta Hernández]

In fact, I'll in some form need the covariantness of \lf to prove that of <

[Violeta Hernández]

Since < is equivalent to \le and \lf

[Violeta Hernández]

Maybe it could be a theorem instead of an instance for now?

[Yaël Dillies]

Yes, there's no point in making an instance to use it exactly once.

[Violeta Hernández]

I mean, it would be nice to have auto-generated add_lf_add and all those other lemmas, but I guess I can prove them myself for now

[Violeta Hernández]

Question

[Violeta Hernández]

How can I use ⧏ for both pgame and game?

[Violeta Hernández]

Having a local infix is only letting me define it once

[Yaël Dillies]

Are you sure? You can overload notation.

[Mario Carneiro]

not local notation

[Mario Carneiro]

I would just not import the notation or use a subscript

[Violeta Hernández]

I feel like this whole file should just go
https://leanprover-community.github.io/mathlib_docs/set_theory/game/winner.html

[Violeta Hernández]

The main definitions are literally just <, >, ||, and ≈

[Violeta Hernández]

We really do not need new names for these relations

[Violeta Hernández]

I know that it's very bad practice to do more than one big thing in a PR, but if I could just delete that file right now, it would make my lt refactor a smidge easier

[Scott Morrison]

I have no attachment to it. Presumably it is still a leaf node? We may want to have a meta discussion, separated from this subject matter, about removing old leaf nodes.

[Violeta Hernández]

A single other file depends on it

[Violeta Hernández]

nim.lean

[Scott Morrison]

Sorry. I think for this refactor you've got to bring it along.

[Violeta Hernández]

:(

[Scott Morrison]

Or propose it first.

[Violeta Hernández]

It doesn't make sense to kill it without the refactor

[Violeta Hernández]

Violeta Hernández said:

The main definitions are literally just <, >, ||, and ≈

This is only true with the correct definitions of < and >

[Mario Carneiro]

for this PR it should not be hard to replace them with left_wins G := 0 < G etc and give one line proofs of all the theorems. This will make the deletion an easy sell

[Scott Morrison]

Oh, I see. Okay, let's nuke it.

[Mario Carneiro]

in particular, if they aren't one line proofs then you might be missing an API theorem

[Scott Morrison]

Although mario's suggestion is probably even better. :-)

[Violeta Hernández]

I am currently missing the || relation

[Violeta Hernández]

I don't know if I should define it now that I defined ⧏, or if that should come in a subsequent PR

[Mario Carneiro]

I think it makes sense to add, if only to have a place to hang all these winner/loser docs

[Yaël Dillies]

Yeah Fox won't be mad if you remove this file. The point was Sprague-Grundy. If you can keep Spraguuuuuuuue-Grundy compiling, cool.

[Violeta Hernández]

As a matter of fact, I got the entire file to one line proofs

[Violeta Hernández]

Often more like 20 character proofs, haha

[Junyan Xu]

Parallel to: ∥
Unicode hexadecimal: 0x2225
In block: Mathematical Operators

Double vertical line: ‖
Unicode hexadecimal: 0x2016
In block: General Punctuation

Musical symbol double barline: 𝄁
Unicode hexadecimal: 0x1d101
In block: Musical Symbols

The second looks best on my machine in VSCode. (I'm using https://shapecatcher.com/)

wow the first is slanted on my phone but vertical on laptop!

[Violeta Hernández]

I feel like the first one might be the one we want? It's the mathematical operator after all

[Mario Carneiro]

the first one is used in mathlib already, for vector norm

[Mario Carneiro]

...and the second one means fintype cardinality apparently

[Mario Carneiro]

probably it's fine to reuse the symbol

[Mario Carneiro]

actually you should not reuse the vector norm symbol, it's not localized (it's a notation typeclass)

[Mario Carneiro]

what about a symbol like )( ?

[Junyan Xu]

I don't think the second one (‖) is declared as a notation? Here indeed it's used to refer to cardinality, but that's definitely not standard.

[Mario Carneiro]

it's declared as a local notation in several files

[Mario Carneiro]

https://github.com/leanprover-community/mathlib/blob/0038a0436f689d37fd3ad00d69d617c338ae6028/src/data/fintype/card_embedding.lean#L17

[Violeta Hernández]

https://github.com/leanprover-community/mathlib/pull/13963

[Scott Morrison]

I've got to say, I don't like the characterisation that we've had the incorrect definition. We've had a perfectly correct definition for a notion that usually has different notation. (And worse, that in some references the notation we used meant something else, although this was not the case for the cited reference.)

I absolutely agree it warrants fixing, but 1) I'm a bit annoyed as I feel like I'm being told my work on pgame was "wrong" (I agree the way I did things was ... not great), and 2) people may decide to misleadingly point at this as an example of a formalised library getting a definition wrong, and both of those are easily avoidable, I hope.

[Damiano Testa]

In support of Scott's comment, as an outsider to the topic, I was puzzled at the beginning about what it meant that a definition was "wrong". It took me a while to realize that it meant that it did not align with some other arbitrary choice of definition whose notation looked the same.

[Violeta Hernández]

I'd say it's worse than that, I couldn't find any source with the previous definition

[Violeta Hernández]

Though perhaps it might be better to say, we used one symbol when we should have used another

[Scott Morrison]

What do you mean? The previous definition is exactly ⧏, but with the symbol < instead of ⧏.

[Scott Morrison]

e.g. it exactly matches the definition in ONAG, using the symbol < for his ≰.

[Violeta Hernández]

Yeah, that

[Violeta Hernández]

We used the wrong symbol, and thought we were deducing results about one symbol when in reality we were deducing results about the other

[Scott Morrison]

(Sorry, maybe I'm just having a bad day. :-) I'm very glad this is fixed now: certainly your PR is a massive improvement and I'm embarrassed to have not understood this myself earlier.)

[Kevin Buzzard]

Re notation: the reason I'm anti <| is that specifically within the mathematician community people have said to me how much easier lean code is to read than code in other provers, and this seems like a perfect place to reinforce this: "oh look they use exactly the same symbol as in the literature".

[Violeta Hernández]

Oh don't worry, I didn't understand this either until I spoke with someone that did know about this and they kept telling me how I was wrong about my inequalities

[Violeta Hernández]

I've learned a lot about games with this refactor

[Junyan Xu]

@Michael Stoll @Violeta Hernández
Good news! Surreals now form a linear_ordered_comm_ring without sorry!

[Violeta Hernández]

Woooo!

[Violeta Hernández]

I'm unfortunately spread thin by finals at the moment, so I don't know when I'll have time to review this thoroughly. Might be until Wednesday...

[Junyan Xu]

I'm puzzled by the module docstring saying "the surreals form a complete ordered field". I don't think they form a docs#conditionally_complete_linear_order, because for any increasing sequence with an upper bound, the surreal number with the sequence as left options and the upper bound as the unique right option is still an upper bound but smaller than the given upper bound, so there's no least upper bound. Git traces back to #1274 by @Scott Morrison.

[Eric Rodriguez]

All complete ordered fields are isomorphic to R, no?

[Damiano Testa]

Archimedean?

[Yaël Dillies]

#3292

[Yaël Dillies]

(I'm working on it, the head PR is currently #14307)

[Eric Rodriguez]

It doesn't seem to require it from the sources I see, I guess completeness implies archimedean

[Eric Rodriguez]

(with order, ofc, else p-adics are a counterexample)

[Patrick Stevens]

Yes - see https://mathoverflow.net/questions/362991/who-first-characterized-the-real-numbers-as-the-unique-complete-ordered-field; to paraphrase, if not Archimedean then the set of naturals is bounded above so has a least upper bound; but any upper bound of the natural numbers is not a least upper bound because you can subtract 1 from it.

[Violeta Hernández]

I think there's the possibility that this is a complete ordered field on a technicality, just like the ordinals are a lattice on a technicality

[Violeta Hernández]

i.e. every small (read ZFC) set of surreals has an infimum and supremum

[Violeta Hernández]

Even then, unless I misunderstand something, that docstring shouldn't be there

[Damiano Testa]

Ah yes, Archimedean is implied by the rest of the hypotheses: thanks for the link!

[Kevin Buzzard]

The surreals are most certainly not archimedean. The confusion is imprecision in the language -- "complete" can mean more than one thing. Wikipedia says something about the issue.

[Stuart Presnell]

As discussed here: https://leanprover-community.github.io/archive/stream/116395-maths/topic/reals.20are.20unique.20complete.20ordered.20field.html#131161921

[Patrick Stevens]

As a tenuously-related aside which I'm only making because I can never resist the opportunity to plug this paper, Real Analysis In Reverse (https://arxiv.org/pdf/1204.4483.pdf) uses the surreals (or more precisely those with birthday less than $\omega_1$) to prove that "nested bounded closed intervals have nonempty intersection" does not imply "Dedekind complete" in the presence of the other ordered field axioms. It also warns that "It’s easy for students to appeal to the Archimedean Property without realizing they are doing so, especially because concrete examples of non-Archimedean ordered fields are unfamiliar to them."

[Mario Carneiro]

Violeta Hernández said:

I think there's the possibility that this is a complete ordered field on a technicality, just like the ordinals are a lattice on a technicality

Surreals are not a complete ordered field on a technicality, namely that they aren't a set and a field is a set

[Mario Carneiro]

If you are in a setting (like lean) where the totality of surreals can be discussed, then they are a field but not they are still not complete because there are (proper) subclasses of the surreals which have no supremum

[Mario Carneiro]

it is only if you allow the field itself to be proper but not the subsets considered in the definition of Inf that they appear "complete"

[Mario Carneiro]

Similarly, the ordinals are a lattice but not a complete lattice unless you bastardize the definition in some way

[Junyan Xu]

it is only if you allow the field itself to be proper but not the subsets considered in the definition of Inf that they appear "complete"

ordinal and cardinal are (large) complete linear orders in this sense; the instances docs#ordinal.conditionally_complete_linear_order_bot and docs#cardinal.conditionally_complete_linear_order_bot say that any (possibly large) subsets with an upper bound has a least upper bound, and separately we know that any small subset has an upper bound.

In surreals, any small subset still has an upper bound (just take all elements of the subset as left options), but my argument above shows it has a least upper bound iff it has a maximal element, so surreals aren't even a docs#conditionally_complete_linear_order.

[Junyan Xu]

This conditional completeness looks the same as Dedekind completeness in Wikipedia.

[Junyan Xu]

I am undetermined whether surreals still can be complete in the uniform space sense (it hasn't become my second nature to unpack definitions via filters), but I feel it's not (even without uniqueness, as in the mathlib definition docs#complete_space).

[Violeta Hernández]

A good example of a set without a supremum in surreals is the naturals

[Violeta Hernández]

If x is an upper bound, so is x - 1

[Junyan Xu]

Yeah, and my argument gives {0,1,2, ... | x} is also an upper bound: it's a surreal because all left options are smaller than the unique right option x, because 0,1,2,... is strictly increasing, so an upper bound must be a strict upper bound (with < instead of ≤; same holds for any subset without maximal element). And any surreal is greater than all its left options, so it's an upper bound. Any surreal is less than all its right options, so it's smaller than x.

[Junyan Xu]

{0,1,2, ... | x} might be exactly equal to x - 1 ... No, not necessarily.

[Damiano Testa]

This discussion has clarified a lot of uneasiness that I always had about which common assumptions characterise the reals up to order isomorphism! I'm also happy that Archimedean plays a role in this and that "complete" also has several meanings!

[Kevin Buzzard]

An example "one level down" of the size issue which Mario was flagging would be that if you only believed in finite sets, but could imagine the rationals existed as some kind of "class" (each element in it can be described using finite sets, and you don't attempt to describe all the elements of Q at once in your language but use predicates instead) then Q is "complete" for you because every nonempty subset of Q is finite in your world and hence has a least upper bound.

[Junyan Xu]

It seems well-known that the surreals contain gaps, so morally they shouldn't be complete in any sense, and indeed it's also not complete as a uniform space (Cauchy completeness, with uniform structure from the topological group structure with the order topology). This is stated in the abstract of https://arxiv.org/abs/1307.7392v3, and p.18 onwards shows any Cauchy sequence indexed by the class of all ordinals either converge to a surreal or to a Type Ia gap. The mathlib definition docs#complete_space requires that every Cauchy filter converges to some surreal, which is equivalent to that every Cauchy net (possibly indexed by a proper class) converges, so surreals aren't a complete_space by the mathlib definition.

However, if we restrict to Cauchy nets indexed by sets, these do converge, because they are all eventually constant! For any net f that is not eventually constant and i an element of the indexing set, {|f j - f k|}_{j,k ≥ i} contains a positive surreal ε_i, and the surreal ε = {0 | ε_i for all i in indexing set} is positive and smaller than all ε_i, i.e. for any i, there are some j, k ≥ i such that |f j - f k| > ε_i > ε, so f is not Cauchy. Therefore, we can say the surreals are "small-complete" in the uniform space sense (similar to the "conditional" completeness of ordinals and cardinals, and reminiscent of small-completeness in category theory.

[Violeta Hernández]

Alright, I've got some time to spare!

[Violeta Hernández]

First question, what's up with mul_option? Seems like a very ad-hoc definition and its lemmas are even worse

[Violeta Hernández]

Another complaint I want to get out of the way quickly: I don't think we should borrow the notation from the paper so literally. For someone just reading through mathlib, it's going to seem very out of place that we use P1, P2, and P4 as the names of our prepositions (instead of P3 for the last one), and thm8 isn't going to make any sense either.

[Violeta Hernández]

Oh wait, you do use P3 too, nevermind then

[Violeta Hernández]

Minor remark, I don't think you use abel in the hydra file

[Violeta Hernández]

I'll PR the minor and uncontroversial changes from that file now, so that the final diff is smaller

[Violeta Hernández]

Reading through more of the PR, I think I see what purpose mul_option plays. I guess it can stay, but it should either be made into a private, auxiliary definition, or if it has any potential of being useful outside of the surreal multiplication proof, it should have a good docstring explaining how that is

[Violeta Hernández]

I think the left_moves_mul_iff and right_moves_mul_iff lemmas should be made into induction principles rather than equivalences, kind of how I did on #14345. Also, it would be nice if the theorem names made reference to the fact you're working with games and not pre-games.

[Violeta Hernández]

I don't think there's a need for le_of_forall_lt. The lemmas le_of_forall_lf and lt.lf should get you there much more easily.

[Violeta Hernández]

I wonder if is_option_neg would be better stated as : is_option (-x) (-y) ↔ is_option x y. What's the general strategy for these lemmas on negations where you can write it both ways? Surely the rest of mathlib has some tips here

[Violeta Hernández]

I think your proposal of making numeric into a set should be its own separate PR. I'll give you the chance to do it, unless you want me to do it for you

[Violeta Hernández]

Minor typo: "because we needs show P1, P2..."

[Junyan Xu]

Thanks for taking a look! I just pushed further cleanup including docstring for mul_option. I'll address other comments later tonight if you haven't figured them out by then.

[Violeta Hernández]

I was just about to say, the rest of the PR looks very very clean. It's amazing you managed to organize such a complicated statement in such a clean way!

[Junyan Xu]

Another complaint I want to get out of the way quickly: I don't think we should borrow the notation from the paper so literally. For someone just reading through mathlib, it's going to seem very out of place that we use P1, P2, and P4 as the names of our prepositions (instead of P3 for the last one), and thm8 isn't going to make any sense either.

With a detailed section docstring, I guess this should be okay? When working on a hard proof, you don't want to write very long names that are fully descriptive. Enclosing these lemmas/defs not supposed to be used elsewhere in a arcane namespace is enough to prevent clashing with these short names. Final results ready for consumption are extracted to the numeric namespace, like mul_pos (basically P3), mul_congr_left (P2), and mul (P1).

I don't think there's a need for le_of_forall_lt. The lemmas le_of_forall_lf and lt.lf should get you there much more easily.

docs#le_of_forall_lt already exists and takes the extraneous numeric hypotheses, so I'm just removing those hypotheses and move it to game/pgame.

I wonder if is_option_neg would be better stated as : is_option (-x) (-y) ↔ is_option x y.

It seems it's easier to use this way. You might experiment with the other way and see what it takes to fix everything. When making decisions about forms of lemmas (e.g. whether to take quotient into game or not, e.g. in P2), I chose the form that makes the most proofs the shortest.

I think your proposal of making numeric into a set should be its own separate PR. I'll give you the chance to do it, unless you want me to do it for you

It's already done in this branch. If uncontroversial (I assume), might just go into mathlib with the same PR.

Regarding mul_option, it would be easier to show left/right_moves_mul_iff if we first prove the lemmas that the left options of the second kind/right options of both kinds are equivalent to (possibly negation of) mul_options.

[Violeta Hernández]

Alright, you've sold me on the P1 and such names, after all these are just auxiliary constructions

[Violeta Hernández]

I still think thm8 is a bad namespace name

[Violeta Hernández]

Why not something more descriptive like surreal_mul? Not like we're going to use this namespace much anyways

[Violeta Hernández]

As for le_of_forall_lt, I remember why I added it now. It makes working with surreals a tad easier. The lemma can and should stay, I'll move and golf it later today

[Violeta Hernández]

I do still think numeric turning into a set should be a separate PR, since it has a very different aim and scope to the rest of this

[Violeta Hernández]

And for mul_option, can you describe what the idea is? Want to make sure we're on the same track here

[Junyan Xu]

mul_option is what makes the main idea (of exploiting symmetry) possible; because all left/right options of the surreal product are of the same form, whenever we want to prove a statement about those options, we can do it uniformly, by applying the same lemma. For example, the proof of P1 consists of four applications of mul_option_lt, the proof of P2 consists of four applications of mul_option_lt_mul_of_equiv, and the proof of P4 also requires four statements of the form mul_options_lt_mul.
I envision that mul_option might also be used to golf some existing proofs.

Will be back in 1.5-2 hours.

[Junyan Xu]

Alright I've renamed thm8 to surreal_mul ... and opened #14585 from branch#surreal_set (it also does some other stuff now).

[Violeta Hernández]

I'll attempt to redefine mul in terms of mul_option, see if that makes anything simpler

[Violeta Hernández]

I imagine we'll have to unfold it to prove all the basic theorems, but it simplifies the surreal multiplication proof, then it should be a net gain

[Violeta Hernández]

By the way, I've taken many of the todos and improvements in your branch and PR'd them separately