addition of surreals

Stream: general

[Scott Morrison]

@Mario Carneiro,

I have a question about your definition of addition for surreal numbers. My student @Isabel Longbottom has been
trying to use it when working on combinatorial games, and we'd really like to have a siplification lemma
that spells out addition in a more familiar form. We'd like to be able to prove the following lemma:

@[simp] lemma add_def {xl xr xL xR yl yr yL yR} :
  add (mk xl xr xL xR) (mk yl yr yL yR) =
    mk (xl ⊕ yl) (xr ⊕ yr)
    (λ xy, sum.cases_on xy (λ x : xl, add (xL x) (mk yl yr yL yR))
                           (λ y : yl, add (mk xl xr xL xR) (yL y)))
    (λ xy, sum.cases_on xy (λ x : xr, add (xR x) (mk yl yr yL yR))
                           (λ y : yr, add (mk xl xr xL xR) (yR y))) := sorry

immediately after the definition of add (say at l. 189 of surreal.lean).

Is it reasonably to want this? How does one prove such a lemma? Neither of us have had much luck...

[Mario Carneiro]

It should be rfl if you got it right

[Mario Carneiro]

Or if I got it right... The definition is wrong. Use this instead

def add (x y : pSurreal) : pSurreal :=
begin
  induction x with xl xr xL xR IHxl IHxr generalizing y,
  induction y with yl yr yL yR IHyl IHyr,
  have y := mk yl yr yL yR,
  refine ⟨xl ⊕ yl, xr ⊕ yr, sum.rec _ _, sum.rec _ _⟩,
  { exact λ i, IHxl i y },
  { exact λ i, IHyl i },
  { exact λ i, IHxr i y },
  { exact λ i, IHyr i }
end

instance : has_add pSurreal := ⟨add⟩

@[simp] lemma add_def {xl xr xL xR yl yr yL yR} :
    mk xl xr xL xR + mk yl yr yL yR =
    mk (xl ⊕ yl) (xr ⊕ yr)
    (λ xy, sum.cases_on xy (λ x : xl, xL x + mk yl yr yL yR)
                           (λ y : yl, mk xl xr xL xR + yL y))
    (λ xy, sum.cases_on xy (λ x : xr, xR x + mk yl yr yL yR)
                           (λ y : yr, mk xl xr xL xR + yR y)) := rfl

[Mario Carneiro]

By the way, I diagnosed this by adding some names for the intermediate functions and proving the equation lemmas for them, then using congr on the target lemma to see what went wrong

def add2
  {xl xr} (xL : xl → pSurreal) (xR : xr → pSurreal)
  (IHxl : xl → pSurreal) (IHxr : xr → pSurreal)
  {yl yr} (yL : yl → pSurreal) (yR : yr → pSurreal)
  (IHyl : yl → pSurreal) (IHyr : yr → pSurreal) : pSurreal :=
⟨xl ⊕ yl, xr ⊕ yr,
  λ xy, sum.cases_on xy (λ i, IHxl i) (λ i, IHyl i),
  λ xy, sum.cases_on xy (λ i, IHxr i) (λ i, IHyr i)⟩

def add1 {xl xr} (xL : xl → pSurreal) (xR : xr → pSurreal)
  (IHxl : xl → pSurreal) (IHxr : xr → pSurreal) (y : pSurreal) : pSurreal :=
begin
  induction y with yl yr yL yR IHyl IHyr,
  refine ⟨xl ⊕ yl, xr ⊕ yr, λ xy, sum.cases_on xy _ _, λ xy, sum.cases_on xy _ _⟩,
  { exact λ i, IHxl i },
  { exact λ i, IHyl i },
  { exact λ i, IHxr i },
  { exact λ i, IHyr i }
end

/-- The sum of `x = {xL | xR}` and `y = {yL | yR}` is `{xL + y, x + yL | xR + y, x + yR}`. -/
def add (x y : pSurreal) : pSurreal :=
begin
  induction x with xl xr xL xR IHxl IHxr,
  induction y with yl yr yL yR IHyl IHyr,
  refine ⟨xl ⊕ yl, xr ⊕ yr, sum.rec _ _, sum.rec _ _⟩,
  { exact λ i, IHxl i },
  { exact λ i, IHyl i },
  { exact λ i, IHxr i },
  { exact λ i, IHyr i }
end

instance : has_add pSurreal := ⟨add⟩

lemma add_def2 {xl xr xL xR IHxl IHxr yl yr yL yR} :
  @add1 xl xr xL xR IHxl IHxr (mk yl yr yL yR) =
  add2 xL xR IHxl IHxr yL yR
    (λ i, add1 xL xR IHxl IHxr (yL i))
    (λ i, add1 xL xR IHxl IHxr (yR i)) := rfl

lemma add_def1 {xl xr xL xR y} :
  mk xl xr xL xR + y = add1 xL xR (λ i, xL i + y) (λ i, xR i + y) y := rfl

@[simp] lemma add_def {xl xr xL xR yl yr yL yR} :
    mk xl xr xL xR + mk yl yr yL yR =
    mk (xl ⊕ yl) (xr ⊕ yr)
    (λ xy, sum.cases_on xy (λ x : xl, xL x + mk yl yr yL yR)
                           (λ y : yl, mk xl xr xL xR + yL y))
    (λ xy, sum.cases_on xy (λ x : xr, xR x + mk yl yr yL yR)
                           (λ y : yr, mk xl xr xL xR + yR y)) :=
begin
  rw [add_def1, add_def2, add2],
  congr; funext; congr; funext j, dsimp, rw add_def1,
end

[Mario Carneiro]

@Scott Morrison Actually, if you really want a nice equation lemma for this, I recommend the following:

def addL {xl xr yl yr} (xL : xl → pSurreal) (xR yL yR) (xy : xl ⊕ yl) : pSurreal :=
sum.cases_on xy (λ i, xL i + mk yl yr yL yR) (λ i, mk xl xr xL xR + yL i)

@[simp] lemma addL_inl {xl xr yl yr} (xL xR yL yR) (i : xl) :
  @addL xl xr yl yr xL xR yL yR (sum.inl i) = xL i + mk yl yr yL yR := rfl

@[simp] lemma addL_inr {xl xr yl yr} (xL xR yL yR) (i : yl) :
  @addL xl xr yl yr xL xR yL yR (sum.inr i) = mk xl xr xL xR + yL i := rfl

def addR {xl xr yl yr} (xL) (xR : xr → pSurreal) (yL yR) (xy : xr ⊕ yr) : pSurreal :=
sum.cases_on xy (λ i, xR i + mk yl yr yL yR) (λ i, mk xl xr xL xR + yR i)

@[simp] lemma addR_inl {xl xr yl yr} (xL xR yL yR) (i : xr) :
  @addR xl xr yl yr xL xR yL yR (sum.inl i) = xR i + mk yl yr yL yR := rfl

@[simp] lemma addR_inr {xl xr yl yr} (xL xR yL yR) (i : yr) :
  @addR xl xr yl yr xL xR yL yR (sum.inr i) = mk xl xr xL xR + yR i := rfl

@[simp] lemma add_def {xl xr xL xR yl yr yL yR} :
  mk xl xr xL xR + mk yl yr yL yR =
  mk (xl ⊕ yl) (xr ⊕ yr) (addL xL xR yL yR) (addR xL xR yL yR) := rfl

[Floris van Doorn]

Oh sorry, I made a mistake when reviewing your PR, I thought these definitions were definitionally equal. My bad!