Well-founded recursion for pgames

Stream: maths

[Apurva Nakade]

I've been stuck on a big proof for surreal numbers for quite some time now.

I'm trying to prove a complicated theorem f(x, y) for {x y : pgames} by recursion.
I end up having to use statements like f(x - xL i, yL j), f(xL k, yR l - y), etc in the proof where xL _ are the left moves of x and xR _ are the right moves of x and similarly for y. Note that the "depth" always increases and there are no terms of the form f(x - xL i, y) so mathematically the recursion is fine.

Lean is unable to prove well-founded recursion for this. I tried doing a trace and it seems to be that the terms of the form x - xL i are throwing it off.

I'm not sure if I can come up with a mwe for this. I can post my big messy proof here.

Any suggestions on how to prove that this kind of recursion is well-founded?

[Scott Morrison]

You might have to post. Sometimes if you're really suffering with a well-founded recursion, it can be helpful to work out how to instead do a inductive proof on nat itself. (e.g. introduce a complexity measure, and hypotheses that explicitly control your arguments in terms of it). If nothing else sometimes it's helpful as a paper-proof step, to make sure you're really doing a sensible induction.

[Mario Carneiro]

Usually surreal numbers require a much higher order induction than nat though

[Scott Morrison]

From the looks of the terms you mention, no lexicographic ordering on the arguments is going to help you, so you're certainly going to have to introduce by hand a different complexity measure, whether you do it with using_well_founded, or by induction on nat

[Scott Morrison]

Ah, good point.

[Mario Carneiro]

probably you can do it using a surreal number or ordinal as the measure though

[Scott Morrison]

I suspect though @Apurva Nakade might be talking about Theorem 3.8 of http://www.cs.cmu.edu/afs/cs/academic/class/15859-s05/www/lecture-notes/comb-games-notes.pdf, which claims to work by induction on a tuple of natural numbers.

[Apurva Nakade]

I'll clean up the code a bit and post it soon.

Yes, I'm trying to prove a weaker version of Theorem 3.8 from those notes. The theorem as it is in the notes is too hard to code. They prove inequalities involving sums of products, which is insane!

In those notes they define a "depth" which I think in Conway's terms might be "day" on which the numbers are born. I think I might need to prove some well_foundedness in terms of "depth". Tbh I've been using the tactic blindly and don't understand well_foundedness much. Is there any reference for this? Or some existing theorems about well_foundedness in mathlib?

[Apurva Nakade]

Here's the code

import set_theory.surreal

namespace pgame
open pgame

-- some lemmas first
theorem numeric_sub {x y : pgame} (ox : numeric x) (oy : numeric y) : numeric (x - y) :=
numeric_add ox (numeric_neg oy)

theorem zero_le₁ {x : pgame} : 0 ≤ x ↔
  (∀ j : x.right_moves, 0 < x.move_right j) :=
by { rw le_def_lt, exact ⟨λ ⟨hl, hr⟩ j, hr j, λ hr, ⟨by rintro ⟨ ⟩, hr⟩⟩ }

theorem le_zero₁ {x : pgame} : x ≤ 0 ↔
  (∀ i : x.left_moves, x.move_left i < 0) :=
by { rw le_def_lt, exact ⟨λ ⟨hl, hr⟩ i, hl i, λ hl, ⟨hl, by rintro ⟨ ⟩⟩⟩ }

theorem zero_lt₁ {x : pgame} : 0 < x ↔
  (∃ i : x.left_moves, 0 ≤ x.move_left i) :=
by {rw lt_def_le, dsimp, simp[forall_pempty] }

theorem lt_zero₁ {x : pgame} : x < 0 ↔
  (∃ j : x.right_moves, x.move_right j ≤ 0) :=
by {rw lt_def_le, dsimp, simp[forall_pempty] }

-- missing trans rules for pgames
@[trans] theorem lt_of_lt_of_equiv' {x y z : pgame} (h₁ : x < y) (h₂ : y ≈ z) : x < z := lt_of_lt_of_le h₁ h₂.1
@[trans] theorem le_of_le_of_equiv' {x y z : pgame} (h₁ : x ≤ y) (h₂ : y ≈ z) : x ≤ z := le_trans h₁ h₂.1
@[trans] theorem lt_of_equiv_of_lt' {x y z : pgame} (h₁ : x ≈ y) (h₂ : y < z) : x < z := lt_of_le_of_lt h₁.1 h₂
@[trans] theorem le_of_equiv_of_le' {x y z : pgame} (h₁ : x ≈ y) (h₂ : y ≤ z) : x ≤ z := le_trans h₁.1 h₂

--problem will well-founded recursion :(

set_option trace.solve_by_elim true

theorem foobar : Π {x y : pgame},
(x.numeric → y.numeric → 0 < x → 0 < y → 0 < x * y) ∧
(x.numeric → y.numeric → 0 ≤ x → 0 ≤ y → 0 ≤ x * y)
| (mk xl xr xL xR) (mk yl yr yL yR) :=
begin
  let x := mk xl xr xL xR,
  let y := mk yl yr yL yR,
  split,
  { intros ox oy pos_x pos_y,
    have nonneg_x : 0 ≤ x, from le_of_lt numeric_zero ox pos_x,
    have nonneg_y : 0 ≤ y, from le_of_lt numeric_zero oy pos_y,
    obtain ⟨i, hi⟩ := zero_lt₁.1 pos_x,
    obtain ⟨j, hj⟩ := zero_lt₁.1 pos_y,
    rw zero_lt₁,
    use sum.inl (i, j),
    calc 0 ≤ yL j * (x - xL i)
           : foobar.2 (oy.2.1 j) (numeric_sub ox (ox.2.1 i))
            hj ((@le_iff_sub_nonneg (xL i) x).1 (le_of_lt (ox.2.1 i) ox (ox.move_left_lt i)))
       ... ≈ (x - xL i) * yL j
           : mul_comm_equiv _ _
       ... ≈ 0 + (x - xL i) * yL j
           : (zero_add_equiv _).symm
       ... ≤ xL i * y + (x - xL i) * yL j
           : add_le_add_right $ foobar.2 (ox.2.1 i) oy hi nonneg_y
       ... ≈ xL i * y + x * yL j - xL i * yL j
           : by { apply @quotient.exact pgame, simp, abel } },
  { intros ox oy nonneg_x nonneg_y,
    have hx' := zero_le₁.1 nonneg_x, dsimp at hx',
    have hy' := zero_le₁.1 nonneg_y, dsimp at hy',
    rw zero_le₁,
    rintros (⟨i, j⟩ | ⟨i, j⟩),
    { by_cases h : 0 ≤ xL i,
      { calc 0 ≤ xL i * y : foobar.2 (ox.2.1 i) oy h nonneg_y
      ... ≈ xL i * y + 0 : (add_zero_equiv _).symm
      ... < xL i * y + (x - xL i) * yR j
          : add_lt_add_left $ foobar.1 (numeric_sub ox (ox.2.1 i)) (oy.2.2 j)
                                (lt_iff_sub_pos.1 (ox.move_left_lt i)) (hy' j)
      ... ≈ xL i * y + x * yR j - xL i * yR j
          : by { apply @quotient.exact pgame, simp, abel } },
      { rw not_le at h,
        calc 0  ≤ x * yR j
                : foobar.2 ox (oy.2.2 j) nonneg_x (le_of_lt numeric_zero (oy.2.2 j) (hy' j))
          ... ≈ x * yR j + 0 : (add_zero_equiv _).symm
          ... < x * yR j + (0 - xL i) * (yR j - y)
                : add_lt_add_left $ foobar.1 (numeric_sub numeric_zero (ox.2.1 i))
                                       (numeric_sub (oy.2.2 j) oy)
                                       (lt_iff_sub_pos.1 h)
                                       (lt_iff_sub_pos.1 (oy.lt_move_right j))
          ... ≈ xL i * y + x * yR j - xL i * yR j
              : by { apply @quotient.exact pgame, simp, abel } } },
  {
    by_cases h : 0 ≤ yL j,
    {calc 0 < xR i * (y - yL j)
            : foobar.1 (ox.2.2 i) (numeric_sub oy (oy.2.1 j)) (hx' i) (lt_iff_sub_pos.1 (oy.move_left_lt j))
     ... ≈ 0 + xR i * (y - yL j) : (zero_add_equiv _).symm
     ... ≤ x * yL j + xR i * (y - yL j)
         : add_le_add_right $ foobar.2 ox (oy.2.1 j) nonneg_x h
     ... ≈ xR i * y + x * yL j - xR i * yL j : by { apply @quotient.exact pgame, simp, abel } },
    {rw not_le at h,
    calc 0
         < (xR i - x) * (0 - yL j)
         : foobar.1 (numeric_sub (ox.2.2 i) ox) (numeric_sub numeric_zero (oy.2.1 j))
           (lt_iff_sub_pos.1 (ox.lt_move_right i))
           (lt_iff_sub_pos.1 h)
      ... ≈ 0 + (xR i - x) * (0 - yL j)
          : (zero_add_equiv _).symm
      ... ≤ xR i * y + (xR i - x) * (0 - yL j)
          : add_le_add_right $ foobar.2 (ox.2.2 i) oy
                                  (le_of_lt numeric_zero (ox.2.2 i) (hx' i)) nonneg_y
      ... ≈ xR i * y + x * yL j - xR i * yL j : by { apply @quotient.exact pgame, simp, abel } } } },
end
using_well_founded { dec_tac := pgame_wf_tac }

end pgame

[Apurva Nakade]

The notes prove the following instead by expanding everything out

theorem foo {x y w z : pgame} : x.numeric → y.numeric → w.numeric → z.numeric →
(x < w) → (y < z) →
(x * z + w * y < x * y + w * z) := sorry

but we can transfer all the variables to one side and reduce the theorem to mul_pos. Because le and lt are defined in terms of each other, we end up having to prove the two theorems simultaneously.

[Apurva Nakade]

(deleted)

[Apurva Nakade]

Mario Carneiro said:

probably you can do it using a surreal number or ordinal as the measure though

How would one go about doing this? I think any connection between pgame and ordinal would be great. Does there exist a map pgame \to ordinals?

[Mario Carneiro]

import set_theory.game
import set_theory.ordinal_arithmetic

namespace pgame

noncomputable def {u} bday : pgame.{u} → ordinal.{u}
| (mk xl xr xL xR) := ordinal.sup.{u u} $
  sum.elim (λ i, (xL i).bday.succ) (λ i, (xR i).bday.succ)

end pgame

[Apurva Nakade]

Great, thanks! I should be able to prove that bday behaves well under arithmetic operations of pgames.

Given such a functor, how does one prove something is well_founded? Mathematically, I want to say that any descending chain of ordinals is finite but I dunno how this is encoded into well_founded in lean.

[Apurva Nakade]

(deleted)

[Mario Carneiro]

there is an instance already saying that ordinals are well ordered by <

[Mario Carneiro]

So you would use something like inv_image (<) bday and typeclass inference knows that this relation has a well founded instance

[Apurva Nakade]

Awesome, thanks again! I'll try this out.

[Kevin Buzzard]

Re foo -- can you deduce it from (z-y)*(w-x)>0? I have this vague memory that there are problems with distributivity though...

[Apurva Nakade]

Yeah, this is exactly what i'm trying to prove. Distributivity is fine as we've already shown all the ring properties for pgames up to equivalence.

theorem mul_pos {x y w z : pgame} : x.numeric → y.numeric → w.numeric → z.numeric →
(0 < w - x) → (0 < z - y) →
0 < (w  - x)(z  -  y) := sorry

You can't prove the above theorem by itself as < is defined in terms of \le so you end up having to prove both simultaneously.

[Kevin Buzzard]

I am asking whether it's easier to prove a>0 and b>0 and a,b numeric implies ab>0 (two variables not four), but I don't know anything about this stuff.

[Apurva Nakade]

Yups, this is the theorem I'm currently trying:

theorem foobar : Π {x y : pgame},
(x.numeric → y.numeric → 0 < x → 0 < y → 0 < x * y) ∧
(x.numeric → y.numeric → 0 ≤ x → 0 ≤ y → 0 ≤ x * y)

[Apurva Nakade]

Really hoping to make the well-founded recursion problem go away for this.

[Kevin Buzzard]

so what happens when you just try doing this by induction on birthday?

[Kevin Buzzard]

That's how Conway would do it, right?

[Apurva Nakade]

I haven't tried it yet. But hopefully it works after that.

Yes! That's my thought too, just need to set it up.
Need to prove a few lemmas about birthday first. I think this might take some time...

[Kevin Buzzard]

Conway seems to give an argument in his proof of Theorem 8(iii) on p19 of ONAG

[Kevin Buzzard]

and, as you originally suggested, he proved x>0 and y>0 implies xy>0 from this more general statement you were originally considering.

[Apurva Nakade]

I looking at his proofs, he is proving the theorem with 4 variables directly :scared:
There are lots of WALOGs and "... can be deduced from ..." in there.

[Apurva Nakade]

One very basic question: ordinal has a preorder instance. From this, how do I extract ordinal.le_trans? I tried the following but it did not quite work

import set_theory.game
import set_theory.ordinal_arithmetic

noncomputable instance temp : preorder ordinal := by apply_instance

#check temp.le_trans           -- unknown identifier
#check ordinal.le_trans       -- unknown identifier

[Eric Wieser]

#check @le_trans ordinal _  -- ∀ {a b c : ordinal}, a ≤ b → b ≤ c → a ≤ c

[Eric Wieser]

Although #check temp.le_trans works for me?

[Apurva Nakade]

Oh, I've open pgame at the start, I should add that to the mwe

[Apurva Nakade]

import set_theory.game
import set_theory.ordinal_arithmetic

open pgame
namespace pgame

noncomputable instance temp : preorder ordinal := by apply_instance

#check temp.le_trans           -- unknown identifier
#check ordinal.le_trans       -- unknown identifier

end pgame

[Eric Wieser]

#check pgame.temp.le_trans

[Eric Wieser]

Named instances are only accessible via their fully-qualified name; instance is roughly short for @[instance] protected def

[Apurva Nakade]

Oh, wow!

[Apurva Nakade]

Thanks, this worked!

[Apurva Nakade]

Ah, I see

[Eric Wieser]

Although it's unlikely you actually need to specify which le_trans you want here anyway

[Apurva Nakade]

There's also the le_trans coming from pgame

[Eric Wieser]

_root_.le_trans will avoid that ambiguity

[Apurva Nakade]

Great, this worked perfectly, thanks!

[Apurva Nakade]

Is there any way to use _root_.le_trans in calc mode?

[Eric Wieser]

local attribute [-trans] pgame.le_trans?

[Eric Wieser]

(deleted)

[Apurva Nakade]

I'm getting 300:1: cannot remove attribute [trans]
I tried putting it inside a section and namespace still the same error.

[Eric Wieser]

Then instead, remove the @[trans] from pgame.le_trans and add local attribute [trans] pgame.le_trans only where you need it

[Apurva Nakade]

This will be too complicated. pgame.le_trans is used in almost every single proof :(

[Eric Wieser]

Sure, but you can add the attribute locally at the top of the section

[Apurva Nakade]

Ah I see, cool, I'll try it out. Will need to shuffle the current proofs around a bit.

[Apurva Nakade]

Apurva Nakade said:

I've been stuck on a big proof for surreal numbers for quite some time now.

I'm trying to prove a complicated theorem f(x, y) for {x y : pgames} by recursion.
I end up having to use statements like f(x - xL i, yL j), f(xL k, yR l - y), etc in the proof where xL _ are the left moves of x and xR _ are the right moves of x and similarly for y. Note that the "depth" always increases and there are no terms of the form f(x - xL i, y) so mathematically the recursion is fine.

Lean is unable to prove well-founded recursion for this. I tried doing a trace and it seems to be that the terms of the form x - xL i are throwing it off.

I'm not sure if I can come up with a mwe for this. I can post my big messy proof here.

Any suggestions on how to prove that this kind of recursion is well-founded?

I think this recursion is not well-founded. It could happen that (x - xL i).bday > x.bday (for example, x = n and xL i = -1.

I dunno how to prove numeric_mul anymore :(
The math proofs I've seen require you to prove things like

theorem foo {x y w z : pgame} : x.numeric → y.numeric → w.numeric → z.numeric →
(x < w) → (y < z) →
(x * z + w * y < x * y + w * z) := sorry

But the LHS and RHS of these inequalities will have 16 terms so we'll end up having to prove 32 inequalities!
Most texts simply wave their hands and say that we'll do one case and the rest are similar, I'm not sure if this is actually true.

Dunno how to proceed from here.

[Apurva Nakade]

Moreover, you cannot even prove (x < w) → (y < z) →(x * z + w * y < x * y + w * z) by itself. Instead you simultaneously have to mul_congr!

[Eric Wieser]

Mario Carneiro said:

import set_theory.game
import set_theory.ordinal_arithmetic

namespace pgame

noncomputable def {u} bday : pgame.{u} → ordinal.{u}
| (mk xl xr xL xR) := ordinal.sup.{u u} $
  sum.elim (λ i, (xL i).bday.succ) (λ i, (xR i).bday.succ)

end pgame

This is now in mathlib as docs#pgame.birthday

[Eric Wieser]

Although the definition is now instead:

noncomputable def birthday : pgame.{u} → ordinal.{u}
| ⟨xl, xr, xL, xR⟩ :=
    max (ordinal.lsub.{u u} $ λ i, birthday (xL i)) (ordinal.lsub.{u u} $ λ i, birthday (xR i))

I assume the difference isn't important? Or do you think your formulation is more convenient @Mario Carneiro than @Violeta Hernández's

[Mario Carneiro]

no, I imagine that will work out basically the same

[Violeta Hernández]

The supremum of a set of successors is definitionally what lsub is

[Violeta Hernández]

Oh I hadn't noticed that this thread was for the exact thing I've been struggling with for the past week

[Violeta Hernández]

But yeah, as for the surreal multiplication proof

[Violeta Hernández]

It can be proven by a very specific induction on birthdays

[Violeta Hernández]

https://github.com/leanprover-community/mathlib/blob/6d7ead9ed67cf7ce04fe63829f7388b9b521e05b/src/set_theory/surreal/basic.lean#L318

[Violeta Hernández]

This is basically the Schleicher proof, except that I figured out you could use birthdays instead of "depth", and also that P2 and P4 could be merged into a single statement

[Violeta Hernández]

The induction, despite being quite complex, relies on a single nontrivial statement on birthdays, which is birthday x < birthday y → birthday (z + x) < birthday (z + y)

[Violeta Hernández]

This can be proven easily from birthday x ≤ birthday y → birthday (z + x) ≤ birthday (z + y), which can be done by unfolding the definition of birthday (x + y) into the maximum of four lsubs and proving each less-equal by the induction hypothesis

[Violeta Hernández]

The only reason I haven't done this yet is that I'm waiting for #13611 to pass, which makes working with addition much less painful

[Violeta Hernández]

If anyone wants to help fill the proof up, it would be greatly appreciated

[Violeta Hernández]

The calculations themselves are basically the same as those in the Schleicher PDF

[Violeta Hernández]

Two updates!

[Violeta Hernández]

First, most of the proof has now been written down

[Violeta Hernández]

Second, I found another simplification of the argument in the PDF

[Violeta Hernández]

Turns out that you don't actually need P1 to conclude P4

[Violeta Hernández]

Schleicher invokes P1 to conclude (xy)^L < xy and xy < (xy)^R, but these inequalities hold for all games, not just numeric games

[Violeta Hernández]

What might not hold is (xy)^L < (xy)^R, which fortunately isn't used

[Violeta Hernández]

So you can in fact prove the following statement: for any x₁, x₂, y, the following hold simultaneously:

• if x₁ = x₂, then x₁ * y is numeric.
• If x₁ ≈ x₂, then x₁ * y ≈ x₂ * y.
• If x₁ < x₂, then,
• • For any left option yL, x₂ * yL + x₁ * y < x₁ * yL + x₂ * y.
• • For any left option yR, x₂ * y + x₁ * yR < x₁ * y + x₂ * yR.

[Violeta Hernández]

And you can prove this by bare Conway induction on x₁ + x₂ + y + y

[Violeta Hernández]

(this wasn't possible before due to that single application of P1)

[Violeta Hernández]

Checking the induction hypothesis pretty much amounts to verifying a bunch of goals similar to "yL + yR + x1 + x2 is subsequent to x1 + x2 + y + y up to relabelling"

[Violeta Hernández]

If the arguments we're in the correct order, this could be done via solve_by_elim

[Violeta Hernández]

And, if addition were commutative, we could use abel for this

[Violeta Hernández]

Unfortunately we run into the issue of relabellings

[Violeta Hernández]

So I'm thinking, perhaps we should have a type of pregames quotiented by relabelling?

[Yaël Dillies]

How is that different from game?

[Violeta Hernández]

game is a much stronger quotient

[Violeta Hernández]

It quotients by antisymmetry

[Violeta Hernández]

So for instance, the empty pregame { | } and the pregame { 1 | -1 } are equal as games but they're not relabellings of one another

[Violeta Hernández]

Conversely, the empty pregame with move types pempty and the empty pregame with move types fin 0 are relabellings but can't be proven equal

[Violeta Hernández]

And as mentioned, another annoying consequence is that x + y is not always equal to y + x, even though they're relabellings

[Yaël Dillies]

Is x + 0 a relabelling of x?

[Violeta Hernández]

Indeed

[Yaël Dillies]

But a * (b + c) is not a relabelling of a * b + a * c?

[Violeta Hernández]

It also is

[Violeta Hernández]

Pre-games up to relabelling are an abelian monoid with commutative and distributive multiplication

[Yaël Dillies]

What's the strongest you can prove about your relabeled_pgames?

[Violeta Hernández]

They don't have additive nor multiplicative inverses though

[Violeta Hernández]

They don't have a partial order (neither do games), but they have all covariant instances for addition (as do pre-games)

[Violeta Hernández]

Oh and addition and multiplication are also associative

[Yaël Dillies]

That sounds good enough to want another type.

[Violeta Hernández]

Glad you agree

[Violeta Hernández]

What I'm wondering is nomenclature

[Yaël Dillies]

I would go for something short, like rgame.

[Violeta Hernández]

I like that

[Yaël Dillies]

Btw, if you're interested in another refactor, you can redefine game as antisymmetrization (≤) pgame.

[Violeta Hernández]

That might be nice

[Violeta Hernández]

I'll look into that

[Violeta Hernández]

Oh wait

[Violeta Hernández]

Turns out rgame isn't as strong as I thought

[Violeta Hernández]

You can define multiplication, and it satisfies x * 0 = 0, x * 1 = 1, x * y = y * x, and (-x) * y = x * (-y) = -(x * y)

[Violeta Hernández]

But unfortunately it isn't distributive nor associative

[Violeta Hernández]

That said, these properties should still make it much easier to deal with multiplication in games

[Violeta Hernández]

Since you can convert inequalities about game to inequalities about rgame and then use these laws via rw

[Violeta Hernández]

What I don't know is what structure these form

[Violeta Hernández]

I think it's just a unital magma? lol

[Eric Rodriguez]

mul_zero_one_class and has_distrib_neg ;b

[Eric Rodriguez]

old-school names are for old-school people

[Eric Rodriguez]

oh wait, is that distrib_neg? or sth else

[Violeta Hernández]

Oh cool

[Violeta Hernández]

It's good to know that there's names for these in mathlib

[Kevin Buzzard]

I sometimes feel like we just made them to make fun of the people who study hierarchies of algebraic structures

[Junyan Xu]

I wonder if people have thought about defining pgame as the type of types (of positions) equipped with two relations L and R (moves) such that the union of both relations is well-founded, together with the starting position. Seems closer to the definition in ONAG than the current inductive type definition, and would be easier to extend to loopy games by dropping the well-founded condition. Moreover, you should be able to get rid of all the relabelling stuff.(maybe not)
image.png

[Michael Stoll]

I tried something like this (it was my first attempt to work in Lean, so don't be too critical...).

import tactic

namespace games

-- We really would like to do the following:

-- inductive Game : Type
-- | make : set Game → set Game → Game

-- but Lean complains of missing "positivity"...

-- so we have to do it in a more pedestrian way.

-- Define the type of (Conway) games.
constant Game : Type

-- Each game has a set of left and a set of right options,
-- which are themselves games.
constants L_opts R_opts : Game → set Game

-- We can construct a game from its left and right options.
noncomputable constant make : set Game → set Game → Game

notation `[` G1 `|` G2 `]` := make G1 G2

-- The following state that these two operations are inverses.
@[simp] axiom make_LR (G : Game) : make (L_opts G) (R_opts G) = G
@[simp] axiom make_L (GL : set Game) (GR : set Game) : L_opts (make GL GR) = GL
@[simp] axiom make_R (GL : set Game) (GR : set Game) : R_opts (make GL GR) = GR

-- A simple consequence is that it suffices to check equality
-- of the left and right options to conclude that two games are the same.
theorem eq_LR (G1 G2 : Game) : G1 = G2 ↔ L_opts G1 = L_opts G2 ∧ R_opts G1 = R_opts G2 :=
begin
  split,
    tauto,
  intro hyp,
  rw [← make_LR G1, ← make_LR G2], cases hyp with h1 h2,
  rw [h1, h2],
end

-- For applications in proofs, this implication is useful.
theorem eq_of_eq_LR (G1 G2 : Game) : L_opts G1 = L_opts G2 ∧ R_opts G1 = R_opts G2 → G1 = G2 :=
begin
  rw eq_LR, tauto,
end

-- We define the notion of "option" of a game.
def is_option (G' : Game) (G : Game) : Prop :=
  G' ∈ L_opts G ∨ G' ∈ R_opts G

-- We note that the elements of `L_opts G` and of `R_opts G` are options of `G`.
lemma L_is_option (G : Game) (GL : Game) : GL ∈ L_opts G → is_option GL G :=
begin
  intro h, rw is_option, left, assumption,
end

lemma R_is_option (G : Game) (GR : Game) : GR ∈ R_opts G → is_option GR G :=
begin
  intro h, rw is_option, right, assumption,
end

--------------------------------------------------------------------
-- The induction principle
--------------------------------------------------------------------

-- This is the "descending game condition":
-- the relation "is option of" is well-founded.
axiom DGC : well_founded is_option

-- This gives us Conway induction for statements involving a single game.
theorem Conway_ind_opt (P : Game → Prop) (hyp : ∀ G : Game, (∀ G', is_option G' G →  P G') → P G) : ∀ G : Game, P G :=
begin
  apply DGC.fix hyp,
end

-- A variant that inducts explicitly on the left and right options.
theorem Conway_ind_LR (P : Game → Prop) (hyp : ∀ G : Game, ((∀ GL ∈ L_opts G, P GL) ∧ (∀ GR ∈ R_opts G, P GR)) → P G) : ∀ G : Game, P G :=
begin
  apply Conway_ind_opt,
  intros G hyp1,
  apply hyp G,
  split,
    intros GL GLG,
    apply hyp1 GL,
    rw is_option, left, assumption,
  intros GR GRG,
  apply hyp1 GR,
  rw is_option, right, assumption,
end


-- Now repeat for pairs of games, when we replace one or both of them by an option.
def is_option_2 (GG1 : Game × Game) (GG : Game × Game) : Prop :=
  (GG1.fst = GG.fst ∧ is_option GG1.snd GG.snd)
   ∨ (is_option GG1.fst GG.fst ∧ GG1.snd = GG.snd)
   ∨ (is_option GG1.fst GG.fst ∧ is_option GG1.snd GG.snd)

def L_opts1_is_option_2 (GL : Game) (GG : Game × Game) : GL ∈ L_opts GG.fst → is_option_2 (GL, GG.snd) GG :=
begin
  intro hyp, unfold is_option_2, right, left, simp, apply L_is_option, assumption,
end

def R_opts1_is_option_2 (GR : Game) (GG : Game × Game) : GR ∈ R_opts GG.fst → is_option_2 (GR, GG.snd) GG :=
begin
  intro hyp, unfold is_option_2, right, left, simp, apply R_is_option, assumption,
end

def L_opts2_is_option_2 (GL : Game) (GG : Game × Game) : GL ∈ L_opts GG.snd → is_option_2 (GG.fst, GL) GG :=
begin
  intro hyp, unfold is_option_2, left, simp, apply L_is_option, assumption,
end

def R_opts2_is_option_2 (GR : Game) (GG : Game × Game) : GR ∈ R_opts GG.snd → is_option_2 (GG.fst, GR) GG :=
begin
  intro hyp, unfold is_option_2, left, simp, apply R_is_option, assumption,
end

-- Note that this is a subrelation of the lexicographic product.
lemma is_option_2_sub_lex : subrelation is_option_2 (prod.lex is_option is_option) :=
begin
  unfold subrelation,
  intros GG1 GG2 hyp, refine (prod.lex_def is_option is_option).mpr _,
  unfold is_option_2 at hyp, tauto,
end

-- Then we can use existing machinery to deduce that this is well-founded.
lemma DGC_2 : well_founded is_option_2 :=
begin
  apply subrelation.wf is_option_2_sub_lex _,
  apply prod.lex_wf DGC DGC,
end

-- ... and derive the induction principle.
theorem Conway_ind_opt_2 (P : Game × Game → Prop) (hyp : ∀ G : Game × Game, (∀ GG, is_option_2 GG G →  P GG) → P G) : ∀ G : Game × Game, P G :=
begin
  apply DGC_2.fix hyp,
end

 (etc.)

It was not clear to me, however, how to show in Lean that a structure exists that satisfies the axioms.

[Junyan Xu]

I'll take a closer look at your code when I have more time. Here's an attempt I started last night, where I constructed a game from the smaller games after left/right moves, but am yet to prove well-foundedness. Negation of a game is obtained by switching L and R, and sum of two games have pos defined to be the product of the two pos; I've yet to think about multiplication (of surreals). (corrected to add the starting position in structure pgame.)

import tactic

universes u v

structure pgame :=
(pos : Type u)
(L R : pos → pos → Prop)
(wf : well_founded $ λ x y, L x y ∨ R x y)
(start : pos)

namespace pgame
open sum

/- special case of sigma.lex -/
inductive sigma_disjoint {α : Type u} {T : α → Type v}
  (r : Π a, T a → T a → Prop) : (Σ a, T a) → (Σ a, T a) → Prop
| mk : ∀ a x y, r a x y → sigma_disjoint ⟨a,x⟩ ⟨a,y⟩

/-- construct a game from left/right options -/
def of_L_R {α β : Type u} (L : α → pgame.{u}) (R : β → pgame.{u}) : pgame.{u} :=
{ pos := ((Σ a, (L a).pos) ⊕ Σ b, (R b).pos) ⊕ unit,
  start := inr (),
  L := λ x y, match x, y with
    | inl (inl ⟨a, p⟩), inr _ := p = (L a).start
    | inl (inl p₁), inl (inl p₂) := sigma_disjoint (λ a, (L a).L) p₁ p₂
    | inl (inr p₁), inl (inr p₂) := sigma_disjoint (λ b, (R b).L) p₁ p₂
    | _, _ := false
    end,
  R := λ x y, match x, y with
    | inl (inr ⟨b, p⟩), inr _ := p = (R b).start
    | inl (inl p₁), inl (inl p₂) := sigma_disjoint (λ a, (L a).R) p₁ p₂
    | inl (inr p₁), inl (inr p₂) := sigma_disjoint (λ b, (R b).R) p₁ p₂
    | _, _ := false
    end,
  wf := ⟨λ p, begin
    sorry,
  end ⟩}

def neg (g : pgame.{u}) : pgame.{u} :=
{ pos := g.pos,
  L := g.R,
  R := g.L,
  wf := by { convert g.wf, ext, exact or.comm },
  start := g.start }

inductive game_sum_rel {α β : Type u} (r₁ : α → α → Prop) (r₂ : β → β → Prop) :
  α × β → α × β → Prop
| fst : ∀ a a' b, r₁ a a' → game_sum_rel (a,b) (a',b)
| snd : ∀ a b b', r₂ b b' → game_sum_rel (a,b) (a,b')

def add (g₁ : pgame.{u}) (g₂ : pgame.{u}) : pgame.{u} :=
{ pos := g₁.pos × g₂.pos,
  L := game_sum_rel g₁.L g₂.L,
  R := game_sum_rel g₁.R g₂.R,
  wf := sorry,
  start := (g₁.start, g₂.start) }

end pgame

[Michael Stoll]

Here is another snippet from my attempt:

-- Define the four simplest games.
noncomputable def G0 : Game := [ {} | {} ]
noncomputable def G1 : Game := [ {G0} | {} ]
noncomputable def Gn1 : Game := [ {} | {G0} ]
noncomputable def Gstar : Game := [ {G0} | {G0} ]

-- Note that `Game` is inhabited.
noncomputable instance Game_inhabited : inhabited Game := ⟨ G0 ⟩

-- Define negation of games.
-- We use well-founded recursion for that.
-- Ideally, we want to have
--   `make {f GR (R_is_option G GR h) GR | h : GR ∈ R_opts G} {f GL ... | GL ∈ L_opts G}` ,
-- but `{f x | x ...}` is not legal set syntax.

-- This describes the recursive construction:
-- we assume that `f G'` gives `-G'` for the options `G'` of `G` and construct `-G` out of these values.
noncomputable def neg_help (G : Game) (f : Π G1, is_option G1 G → Game) : Game :=
  make {GNL : Game | ∃ (GR : Game) (h : GR ∈ R_opts G), GNL = f GR (R_is_option G GR h)}
            {GNR : Game | ∃ (GL : Game) (h : GL ∈ L_opts G), GNR = f GL (L_is_option G GL h)}
-- Now apply the fixed point operator for the recursion.
noncomputable def neg (G :Game) : Game :=
  DGC.fix neg_help G

--noncomputable instance Game_has_neg : has_neg Game := ⟨ neg ⟩

notation `-` G := neg G

-- The following basically establish rewrite rules.
@[simp] lemma L_opts_of_neg (G : Game) : L_opts (-G) = {GRN : Game | ∃ GR ∈ (R_opts G), GRN = -GR} :=
begin
  unfold neg, rw DGC.fix_eq, unfold neg_help, simp,
end

@[simp] lemma R_opts_of_neg (G : Game) : R_opts (-G) = {GLN : Game | ∃ GL ∈ (L_opts G), GLN = -GL} :=
begin
  unfold neg, rw DGC.fix_eq, unfold neg_help, simp,
end

-- Show that `-(-G) = G`.
@[simp] theorem neg_neg (G : Game) : -(-G) = G :=
begin
  revert G,
  -- We use Conway induction for this.
  have ind := Conway_ind_opt (λ G, -(-G) = G), simp at ind,
  apply ind,
  intros G hyp,
  -- It is sufficient to show that the sets of left/right options agree.
  rw eq_LR, split,
    simp, refine set.ext _, intro G1, simp, split,
      intro hyp1, cases hyp1 with GLN hyp1, cases hyp1 with hyp1 hyp2, cases hyp1 with GL hyp1,
      cases hyp1 with hyp11 hyp12,
      have h := hyp GL (L_is_option G GL hyp11),
      rw [hyp2, hyp12, h],
      assumption,
    intro h1, have h := hyp G1 (L_is_option G G1 h1),
    use -G1,
    split,
      use G1, split, assumption, refl,
    rw h,

    simp, refine set.ext _, intro G1, simp, split,
      intro hyp1, cases hyp1 with GRN hyp1, cases hyp1 with hyp1 hyp2, cases hyp1 with GR hyp1,
      cases hyp1 with hyp11 hyp12,
      have h := hyp GR (R_is_option G GR hyp11),
      rw [hyp2, hyp12, h],
      assumption,
    intro h1, have h := hyp G1 (R_is_option G G1 h1),
    use -G1,
    split,
      use G1, split, assumption, refl,
    rw h,
end

-- We get the fact that negation is injective.
lemma neg_inj (G1 G2 : Game) : -G1 = -G2 → G1 = G2 :=
begin
  intro hyp,
  rw ← (neg_neg G1), rw ← (neg_neg G2), rw hyp,
end

-- Also, `G₁ = -G₂` implies `G₂ = -G₁`.
lemma neg_swap (G₁ G₂ : Game) : G₁ = -G₂ → G₂ = -G₁ :=
begin
  intro h, rw ← neg_neg G₂, apply eq.symm, rw h,
end

-- Some simple statements on the simplest games and negation.
lemma G0_neg : -G0 = G0 :=
begin
  rw (eq_LR (-G0) G0), unfold G0, simp,
end

lemma G1_neg : -G1 = Gn1 :=
begin
  rw (eq_LR (-G1) Gn1), unfold Gn1, unfold G1, simp, apply G0_neg,
end

lemma Gstar_neg : -Gstar = Gstar :=
begin
  rw (eq_LR (-Gstar) Gstar), unfold Gstar, simp, apply G0_neg,
end

-- Now we do addition.
-- To use Conway induction on pairs of games,
-- we need to work with the product type.
noncomputable def add_help (GG : Game × Game) (f : Π (GG1 : Game × Game), is_option_2 GG1 GG → Game) : Game :=
  make {GAL : Game | (∃ (GL : Game) (h : GL ∈ L_opts GG.fst), GAL = f (GL, GG.snd) (L_opts1_is_option_2 GL GG h))
                          ∨ (∃ (GL : Game) (h : GL ∈ L_opts GG.snd), GAL = f (GG.fst, GL) (L_opts2_is_option_2 GL GG h))}
       {GAR : Game | (∃ (GR : Game) (h : GR ∈ R_opts GG.fst), GAR = f (GR, GG.snd) (R_opts1_is_option_2 GR GG h))
                          ∨ (∃ (GR : Game) (h : GR ∈ R_opts GG.snd), GAR = f (GG.fst, GR) (R_opts2_is_option_2 GR GG h))}

noncomputable def add_pair (GG : Game × Game) : Game :=
  DGC_2.fix add_help GG

-- Translate  `Game × Game → Game`  into  `Game → Game → Game` .
noncomputable def add (G1 G2 : Game) : Game :=  add_pair (G1, G2)

--noncomputable Game_has_add : has_add Game := ⟨ add ⟩

notation G1 ` + ` G2 := add G1 G2

-- Lemmas that can be used for simplification.
@[simp] lemma L_opts_of_add (G1 G2 : Game) : L_opts (G1 + G2) =
  {GAL : Game | (∃ (GL : Game) (h : GL ∈ L_opts G1), GAL = GL + G2)
                ∨ (∃ (GL : Game) (h : GL ∈ L_opts G2), GAL = G1 + GL)} :=
begin
  unfold add, unfold add_pair, rw DGC_2.fix_eq, unfold add_help, simp,
end

@[simp] lemma R_opts_of_add (G1 G2 : Game) : R_opts (G1 + G2) =
  {GAR : Game | (∃ (GR : Game) (h : GR ∈ R_opts G1), GAR = GR + G2)
                ∨ (∃ (GR : Game) (h : GR ∈ R_opts G2), GAR = G1 + GR)} :=
begin
  unfold add, unfold add_pair, rw DGC_2.fix_eq, unfold add_help, simp,
end

example : G0 + G0 = G0 :=
begin
  rw eq_LR, unfold G0, simp,
end

(then I go on to prove facts on addition).
The proofs can probably be considerably simplified...

[Violeta Hernández]

I don't believe defining games in terms of sets of games works in type theory

[Violeta Hernández]

Otherwise you could define a game whose left set is the set of all games

[Violeta Hernández]

And that's an absurd

[Violeta Hernández]

Mathlib already has pre-games, and it defines them via type indexed families of pre-games

[Violeta Hernández]

Crucially the indexing types must belong to universe u, while the type of pre-games is in universe u+1, which avoids the contradiction

[Violeta Hernández]

This has the annoyance that pre-games with equal left and right sets of games can still be different if the indexing types or the indexing itself are different, but I'm currently defining tbe quotient of pre-games by extensionality to overcome this

[Mario Carneiro]

In surreals you have an equivalence of recursive equivalence like "forall a, exists b, A_left a <= B_left b" to deal with this, and pSet has something similar - src#pSet.equiv

[Violeta Hernández]

Pre-games already have a notion of a relabelling

[Mario Carneiro]

I assume relabelling is a bit too strict of an equivalence for games though

[Violeta Hernández]

And existence of a relabelling almost corresponds to ZFC equality of pre-games

[Violeta Hernández]

Not quite because it assumes that you have multisets instead of sets

[Violeta Hernández]

Of course, it's too strict for games

[Violeta Hernández]

That's a quotient by antisymmetry

[Violeta Hernández]

Not just structural equality

[Mario Carneiro]

for pSet it's also not quite relabeling, because it needs to be relabeling where after the relabeling the elements are equivalent

[Mario Carneiro]

or maybe that's part of relabeling

[Mario Carneiro]

I suppose pre-games don't have any quotient on them?

[Mario Carneiro]

that's what makes them pre-games

[Michael Stoll]

Violeta Hernández said:

I don't believe defining games in terms of sets of games works in type theory

That's the problem I had; this is why I resorted to axioms and constants to describe the set-up in a way that was as close as possible to Conway's definition.
Note that I wrote this code before I was aware that combinatorial games are present in mathlib. (And before I had any experience with Lean to speak of.)

[Mario Carneiro]

Regarding @Junyan Xu 's point about loopy games, I believe the correct approach is to use a coinductive type instead of an inductive type but otherwise with the same definition. Because we would want to consider the A -> A and B -> B and A -> B -> A all be equivalent loopy games (there is only one infinite line of play)

[Violeta Hernández]

Junyan Xu said:

Moreover, you should be able to get rid of all the relabelling stuff.(maybe not)
image.png

I don't think that would get rid of the relabelling stuff. If you have a type of positions, then it stands that you can have two games that are exactly the same except they use a different type.

[Mario Carneiro]

@Michael Stoll using sets of games leads to the same paradoxes in set theory too. Well-foundedness is an essential component, and I believe Conway uses an informal description of transfinite induction in ONAG

[Mario Carneiro]

using inductive types is by far the easiest way to do this and get the right answer in CIC

[Violeta Hernández]

Doesn't set theory circumvent this by having games be a proper class?

[Michael Stoll]

In a way, Conway defines games as sets with two kinds of elements.

[Michael Stoll]

And well-foundedness is sort of built-in ("... all games arise in this way"); alternatively, it is equivalent to the induction principle for games.

[Michael Stoll]

If one wants to build the theory within set theory, then the games are not a set, but a proper class (which is not a problem).

[Junyan Xu]

An element of set α in Lean is actually a predicate, which may be an actual set or a proper class, if α is in a higher universe; for example when α is pgame.{u} : Type (u+1), s : set α is small (an "actual set" in Type u) if subtype s is equipotent to some type in Type u, and a proper class otherwise.

Conway defines games/numbers like how you define the von Neumann universe or constructible universe in set theory, implicitly using transfinite induction; at each step you can only use games/numbers you already constructed. In Lean, this smallness is guaranteed by using indexing types in Type u for left and right options.

The point of my new definition is: if we have to use indexing types, why not use a single indexing type for all positions? It also makes some definitions simpler, e.g. negation, and impartial games would simply be those with L=R.

I don't think we need force isomorphic games be equal using coinductive types or something like Aczel's anti-foundation axiom; there are many different types of games as you can see in Winning Ways and it's easy to find coincidences where the games are CGT equivalent or even the game graphs are the same, but they don't have to be the same pgame; it would be enough to prove by induction that you can substitute one with the other without changing the CGT value (equivalence class) of the whole game.

[Mario Carneiro]

Describing what it means for a game to be well founded is approximately as complicated as defining pgame in the first place though

[Mario Carneiro]

you basically have to say that a game has a pgame that surjects onto it in a certain sense

[Mario Carneiro]

I think that your general concept of game-graphs are useful but distinct from either the inductive or coinductive concept of pgame

[Mario Carneiro]

You need the coinductive analogue of game to provide the values of loopy games and game-graphs

[Junyan Xu]

Mario Carneiro said:

Describing what it means for a game to be well founded is approximately as complicated as defining pgame in the first place though

Is this complicated, or problematic, or you mean something else?

universes u v

structure pgame :=
(pos : Type u)
(L R : pos → pos → Prop) /- L x y means x is a option at position y for left -/
(wf : well_founded $ λ x y, L x y ∨ R x y)
(start : pos)

[Mario Carneiro]

src#pgame

[Mario Carneiro]

I think it's more complicated

[Mario Carneiro]

the fact that you can't pattern match on it and have to carry start around seems like it will make proofs harder

[Mario Carneiro]

for graphs you usually don't designate a start vertex in the structure itself

[Mario Carneiro]

Also, you might not want to assume the whole type is well founded, only the elements under start

[Mario Carneiro]

that is acc (λ x y, L x y ∨ R x y) start

[Junyan Xu]

You can remove unreachable elements and get an equivalent game.

[Mario Carneiro]

sure, but those kinds of arguments are messy in lean

[Junyan Xu]

I'll definitely try to replicate current development in mathlib to see how easy my definition is to work with.

[Junyan Xu]

You may try the two sorrys in my code posted above, I won't get to them until 6pm (~3 hours later).

[Junyan Xu]

I think docs#well_founded.well_founded_iff_has_min and docs#set.well_founded_on_iff_no_descending_seq will be handy. (The second uses dependent choice but mathlib is fine with it.)

[Violeta Hernández]

I find that Lean generally makes it so that it's harder to use that characterization of well foundedness

[Violeta Hernández]

Usually, if everything is setup right, you can do bare induction and get what you want more easily

[Violeta Hernández]

This is just my opinion though

[Junyan Xu]

I've defined ≤ and showed it's reflexive using the new definition and I'll call it a day; more to come!
https://gist.github.com/alreadydone/cdf39674c4bec9a8f298e43024771621

[Violeta Hernández]

Are you planning for this to replace the current definition in mathlib? Or is this just a side thing?

[Violeta Hernández]

What you're doing seems nice but I feel like refactoring pgame with this would be a ton of work with little (if any) benefit

[Junyan Xu]

I believe my definition is the most natural when dealing with concrete games (that are described by which moves are possible at each position) and loopy games, and realizing addition as juxtaposition of games is really nice. Currently it's in exploration phase, and if the mathlib definition turns out to be superior for some purposes we may work on providing some glues between the two.

[Violeta Hernández]

How would multiplication work? Don't you need well foundedness to define that?

[Violeta Hernández]

Which wouldn't quite work on loopy games

[Junyan Xu]

Yeah, I don't think multiplication is well-behaved even for well-founded games (and there are at least two definitions of ≤ as the loopy games slides show, and there is the misère play convention (first player without move wins) where there isn't a nice notion of ≤). Multiplication won't respect equivalence unless restricted to surreals. I expect of_L_R in my earlier post will be required to define multiplication. I haven't thought about surreals much, but I have done some computations in On₂, the (algebraically closed, etc.) field of characteristic two formed by all ordinals by considering them as impartial games, where multiplication is defined like in the surreal case. I think Winning Ways also defined multiplication for more general games that's well-behaved under certain conditions, but I have to look them up.

[Scott Morrison]

I think it would be fine to have an alternative definition in parallel, if there is appropriate glue.

[Reid Barton]

docs#pgame.state already looks pretty similar

[Scott Morrison]

I'd forgotten about that one, even though the domineering example I built uses it.

[Scott Morrison]

For lots of concrete games the turn bound is easy and convenient, and in practice how you might be proving well-foundedness anyway.

[Scott Morrison]

I think it would be great to have more actual concrete games! Hex, dots-and-boxes, and go would all be lovely (some amount of fitting square pegs in round holes to treat these all as Conway style games, but they could be described other ways, too).

[Kevin Buzzard]

My paper on dots and boxes describes how at a professional level it has little to do with combinatorial game theory, but strings and coins (:= dots and boxes with the normal play rule rather than "most boxes is the winner") would be lovely :-)

[Junyan Xu]

Update: I've shown game is a ordered_add_comm_group under the new definition within 374 lines: https://gist.github.com/alreadydone/cdf39674c4bec9a8f298e43024771621

[Junyan Xu]

Updates: I have been able to show the well-foundedness of the game constructed from left/right options (formerly called of_L_R and now simply called of); see the end of https://gist.github.com/alreadydone/93e25ccda07b0c9c1ef2b40efedf3339. However, at the same time I came up with an explicit construction of a type of positions for the product of two games (has anyone written about it before?) and plan to use it instead of of:

instance : has_mul pgame :=
{ mul := λ g₁ g₂,
  { pos := tree3 (bool × g₁.pos × g₂.pos),
    /- could also potentially be `multiset (bool × g₁.pos × g₂.pos)`; each element
       of the multiset is seen as an expression of the form +x*y or -x*y, where x is a position in g₁ and y a position in g₂. -/
    L := closure (mul_rel tt g₁.L g₂.L ∪ mul_rel ff g₁.L g₂.R ∪
                  mul_rel ff g₁.R g₂.L ∪ mul_rel tt g₁.R g₂.R),
    R := closure (mul_rel ff g₁.L g₂.L ∪ mul_rel tt g₁.L g₂.R ∪
                  mul_rel tt g₁.R g₂.L ∪ mul_rel ff g₁.R g₂.R),
    wf := sorry,
    start := (tt, g₁.start, g₂.start) } }

See the beginning of the gist above for the full code.

I like the symmetric form of the definition of L and R fields. It works for surreal multiplication, but presumably not for multiplying a positive game with an arbitrary game, which I'll worry about later. (I'm currently experimenting with jux : (fin 3 → tree3) → tree3 instead of jux : tree3 → tree3 → tree3 → tree3.)

To fill in the sorry above, I basically need to prove the termination of a version of the hydra game; basically, the options of the product of two games are each a sum of three products, that is to say if you cut a head of the hydra, it grows back three heads at some lower levels ("less than" the original product w.r.t. the < relation that is the transitive closure of (sgn, xL/xR, y), (sgn, x, yL/yR) < (sgn', x, y)). I realized I need some form of Kőnig's lemma and Googled with the keywords "Kőnig hydra", and this MO problem came up. After browsing the answers, I found that @Peter LeFanu Lumsdaine 's approach seems simpler than setting up the stage to apply Kőnig's lemma, so that's what I'm gonna formalize now. The statement is as below (with multiset instead of list); it doesn't seem to show up when defining multiplication via Conway induction as done in mathlib.

import data.multiset.basic

variables {α : Type*} [decidable_eq α] (r : α → α → Prop)

/-- Cut one head `a` of a hydra `s`, and it grows back an arbitrary finite number of
  heads at "lower levels" than the head cut. -/
inductive cut_rel : multiset α → multiset α → Prop
| cut {s t : multiset α} (a ∈ s) : (∀ a' ∈ t, r a' a) → cut_rel (s.erase a + t) s

theorem well_founded.cut_rel (hr : well_founded r) : well_founded (cut_rel r) := sorry

Since the line count is growing large, I'll probably split this project into multiple files and create a folder (like set_theory/game_new) in mathlib to contain it and create a branch on github. If people find it easier to work with this new definition, we may continue to add materials to that folder and gradually deprecate the old one.

[Violeta Hernández]

I'm still really iffy on this. The way I see it, your approach has the following pros and cons:

Pros:

• Allows a natural extension to loopy games.

Cons:

• The induction arguments become considerably harder.
• Much worse definitional equalities (since you force a game and all subsequent moves to be part of the same graph).
• The notion of "relabellings" becomes much more complicated.
• The refactor would take a large amount of work, and to me it's not even clear that everything would work out nicely.
• This deviates from Conway's approach even more radically than our current approach (and supposedly, that's what we're trying to formalize).

Call it force of habit, but I'd rather stick to what we have unless there's other substantial reasons to switch, or unless there's a substantial theory on loopy games that we can formalize using your definition.

[Violeta Hernández]

To give a basic example of something that would break in a way that's hard to fix: ordinal.to_pgame. Currently, a lot of the results about it induct on the ordinal, which is possible because left moves of o.to_pgame are exactly a.to_pgame for a < o. With your definition, this wouldn't be the case, so you'd need to consider relabellings in pretty much all of the proofs.

[Violeta Hernández]

Pretty much this same reasoning extends to nim.

[Junyan Xu]

set_theory.game.ordinal is a short file. Would it convince you it's a viable approach if I reproduce the results therein? Your "relabelling" is basically my iso, which I showed preserves Rlose (i.e. 0 ≤ g) in map_iso_Rlose_iff, and use it in the following lemmas to show commutativity, associativity, etc. I later defined a structure iso which is quite simple:

structure iso (g g' : pgame) :=
(pos : g.pos ≃ g'.pos)
(L : inv_image g'.L pos = g.L)
(R : inv_image g'.R pos = g.R)

I'm puzzled by your comment that "induction arguments become considerably harder" and "much worse definitional equalities". Can you elaborate and maybe give an example in my code, or have I not got to the point where they'll be problematic? My experience has been that induction/recursion becomes unnecessary in many places with my approach. It's a one-off thing to prove well-foundedness in various constructions, and I wouldn't call them hard except for multiplication. Contrary to your comment, I think one advantage of my approach is that addition, negation, multiplication, and impartial games now have totally non-inductive definitions (is_numeric can also be defined by quantifying over all positions using the inductively defined Lwin); when defining Rlose/Lwin, I used induction on positions instead of games.

I agree it's a deviation from Conway's approach but I'd argue using indexing types for left/right options is also a deviation, and necessitates relabelling which makes things inelegant (though using a ordinal-indexed union of games born by birthday x would be more inelegant). As I said before, the initial motivation of my definition is : "if we have to use indexing types, why not use a single one?" In general, I think we should choose what works best (like the filter approach to topology, or is_localization in mathlib), which can only be found out through experimentation. It would be great if more people like you are interested to join the effort. I think I currently have all the essential results in game.pgame and game.basic except for mul and inv, and those are my ongoing work. My plan is to gradually work through all files under game and surreal, which seem to contain everything about CGT in mathlib and don't seem that massive, though I think I probably don't have the energy to complete a refactor without other people's interest and help. So I think it's a sensible approach to add another folder, so people can choose whichever approach that suits their purpose when they develop CGT and/or contribute to mathlib. I'd like to keep the same pgame, game etc. namespace (which shouldn't be a problem if you don't import files from both development), but I expect some linters may complain.

[Junyan Xu]

For ordinals or nimbers, we can actually realize them simply as different starting positions in the "same" game, with all ordinals in the universe as positions, L = (<), and R = (<) for nimbers and empty for ordinals; just the start needs to be changed to the ordinal. This is at the expense of elevating the game from pgame.{u} to pgame.{u+1} though. The larger ordinals are unreachable in the game, but this is the flexibility offered by my approach and not a bug (e.g. the extraneous positions also occur in my definition of multiplication).

[Scott Morrison]

I would be interested in seeing a concrete game translated to this formalism, too, e.g. domineering.

[Mario Carneiro]

I think that this approach makes more sense without the wffield

[Mario Carneiro]

The fact that you have to universe-bump is a pretty fundamental difference

[Scott Morrison]

You only have to universe bump if you want to fit all ordinals in, don't you? There'll be some u-small ordinals trick otherwise?

[Junyan Xu]

The current approach uses o.out.α (invokes choice) which seems to be the only option to lower the universe.

[Mario Carneiro]

note that ordinal is rampantly choice-assuming. It would need a very significant rewrite in order to make it not need choice and many theorems would not hold

[Mario Carneiro]

It's usually possible to avoid using o.out but there isn't much gain to be had in doing so because choice already appears ten times in the dependencies

[Mario Carneiro]

Note that the definition of to_pgame is actually computable; the reason for the noncomputable! is because one of the auxiliary definitions lean creates is unexpectedly noncomputable and it causes a weird error message

[Mario Carneiro]

Here's a definition that avoids noncomputable!

[Mario Carneiro]

/-- Converts a well order into the corresponding pre-game. -/
def well_order_to_pgame {α : Type u} [has_well_founded α] : α → pgame.{u}
| a := ⟨{x // has_well_founded.r x a}, pempty,
  λ y, have _, from y.2, well_order_to_pgame y.1, pempty.elim⟩
using_well_founded { dec_tac := tactic.assumption }

/-- Converts an ordinal into the corresponding pre-game. -/
def to_pgame (o : ordinal.{u}) : pgame.{u} :=
⟨o.out.α, pempty, well_order_to_pgame, pempty.elim⟩

[David Wärn]

Note that you can define loopy games in the same style as docs#pgame by writing a coinductive definition instead of an inductive one. Here's a sketch:

import data.pfunctor.univariate.M
import set_theory.game.pgame

universe u

def loopy_game : Type (u+1) := pfunctor.M ⟨Type u × Type u, λ p, ulift.{u+1} (p.fst ⊕ p.snd)⟩

def pgame.loopy_game : pgame.{u} → loopy_game.{u} :=
pfunctor.M.corec $ λ G, ⟨(G.left_moves, G.right_moves),
                          λ p, sum.elim G.move_left G.move_right p.down⟩

namespace loopy_game

variable (G : loopy_game.{u})

def left_moves : Type u := G.head.fst
def right_moves : Type u := G.head.snd
def move_left (x : left_moves G) : loopy_game := G.children (ulift.up (sum.inl x))
def move_right (y : right_moves G) : loopy_game := G.children (ulift.up (sum.inr y))

inductive is_wf : loopy_game.{u} → Prop
| sup {G : loopy_game} :
  (∀ x : G.left_moves, is_wf (G.move_left x)) →
  (∀ y : G.right_moves, is_wf (G.move_right y)) →
  is_wf G

def is_wf.pgame (h : is_wf G) : pgame := h.rec $ λ _ _ _ ls rs, pgame.mk _ _ ls rs

end loopy_game

Probably you could go further and show that pgame is equivalent to the subtype of well-founded loopy games in this language

The code above essentially defines loopy_game to be a terminal coalgebra for a certain polynomial functor. Junyan's definition instead looks at the type of all (well-founded) pointed coalgebras. This makes a lot of sense if we want to construct explicit elements of loopy_game -- normally we define elements of a coinductive type by corecursion, i.e. by constructing explicit coalgebras. (Actually this is analogous to how we deal with bisimulation in mathlib: instead of defining an indexed coinductive prop of bisimulations, we take a bisimulation to be some coalgebra for the same functor.)

I think it's not clear which of these two approaches to loopy games is the best, but for well-founded games I don't understand what the problem with docs#pgame is (other than it being difficult to construct concrete games, but this problem seems to be solved by docs#pgame.state)

[Junyan Xu]

Thanks but I'm yet to read more about pfunctor and coinduction. From my limited understanding about bisimulation, it seems to be a better and more general notion of strong equivalence between games than relabelling. Here strong equivalence means it guarantees substitutability (in sums and as options) in any (loopy or wf) game under both the normal and misere play convention. (If you want to see more theory about loopy and misere games, there are whole chapters in Aaron Siegel's Combinatorial Game Theory.

As evidence of better defeq with my approach, see lines 135-137: neg_zero and neg_neg are propositional equalities in mathlib; with my approach the former is defeq in Lean 3, and the latter (I think) is defeq in Lean 4 due to structure eta being defeq. neg_add is only true up to relabelling in mathlib; with my approach it's also defeq (which is "abused" in add_le_add_iff_Rlose, for example).

[Violeta Hernández]

A bunch of equalities in pgame might become def-eq in Lean 4, but I'm unsure to what extent that will help.

[Violeta Hernández]

It's very interesting that you're able to avoid induction in many circumstances. It's also interesting that you get better definitional equalities in these basic definitions. That speaks to some mathematical elegance in your approach. That said, there are a lot of induction proofs scattered throughout, some quite hard and involved, and I'm still not convinced that your approach can avoid all of them. And there's still the problem of definitional equalities in inductively defined families of games like ordinal.to_pgame and nim.

I very strongly disagree with your approach of bumping the universe of ordinal.to_pgame. This sort of universe bumping can lead to very hard to solve problems later down the line. I'm interested in seeing how the ordinal.lean file would work with your approach without said universe bumping.

I could help with your new definition, but I've yet to see benefits large enough to justify all the work that would be needed for this refactoring. If you only want loopy games, then the coinductive approach seems to be by far the smoothest alternative given the current state of the library.

[Violeta Hernández]

I really don't want to come off as mean, because I can imagine that you've been working for hours on this, and I don't want to give the impression that said work is worthless or uninteresting. I'd just like to more carefully evaluate what's better for mathlib in the short and long run.

[Violeta Hernández]

Also, I'm quite biased given my recent heavy involvement on the mathlib pgame code base. So I'd like to hear opinions from others too.

[Violeta Hernández]

After this < refactor, there's another pretty big refactor I want to do

[Violeta Hernández]

We currently have a lot of congr lemmas for the different relations, and even then, proving inequalities is a total hassle

[Violeta Hernández]

This could be made way easier if we defined game earlier

[Violeta Hernández]

Then, to prove an inequality on pgame, we could simply change it into the def-eq inequality on game, and use a few rws

[Junyan Xu]

My latest thoughts: although I can provide an explicit model for the positions in the multiplication of two games, it doesn't seem to simplify any proofs, unlike in the addition case, so I probably won't open a PR for this approach in the near future. I will continue to explore the approach for concrete games, loopy games, and ordinals, when I have the leisure. I have yet to understand the coinductive approach to loopy games; for example, how would I construct a loopy_game from my pos, L, R and vice versa?

I might soon PR some work related to well-foundedness that has arisen from this endeavour, including the termination of the hydra game, which provides one way to show the well-foundedness of the induction for properties of surreal multiplication in the notes of Schleicher--Stoll; namely, if you consider the arguments of P1(x,y), P2(x1,x2,y) and P4(x,y1,y2) as multisets {x,y}, {x1,x2,y}, and {x,y1,y2}, then each of P1, P2, P4 is deduced from P1, P2, P4 with smaller argument multisets under the cut_expand relation. The proof of termination is actually pretty elegant using acc; interestingly it uses the add_rel for game addition.

def cut_expand {α : Type*} [decidable_eq α]
  (r : α → α → Prop) (s' s : multiset α) : Prop :=
∃ (t : multiset α) (a ∈ s), (∀ a' ∈ t, r a' a) ∧ s' = s.erase a + t

[Violeta Hernández]

If your cut_expand approach works, that would be super elegant

[Violeta Hernández]

Well, it might be a bit inconvenient to set up, since P1, P2, P4 are meant to have a fixed amount of arguments

[Violeta Hernández]

So you might need to induct on a generic multiset s and make the inductive hypotheses "if {x, y} is less than s then P1, ..."

[Violeta Hernández]

On the topic of relabellings and extensionality

[Violeta Hernández]

I wonder if relabellings are even useful to begin with

[Violeta Hernández]

Just from reading the definition of docs#pSet.equiv, it seems like the same amount of work to prove two games are relabellings and to prove they're extensionally equal

[Violeta Hernández]

If this is the case, then surely we don't need relabellings at all?

[Violeta Hernández]

On an unrelated note, I hadn't ever noticed just how similar pgame and pSet are

[Violeta Hernández]

pSet can very well be called the unary version of pgame

[Violeta Hernández]

Which I guess is to be expected, ZFC games are constructed almost the same way as ZFC sets, just twice

[Violeta Hernández]

I'm going to try to get rid of relabelling in favor of identical, which actually describes extensionality

[Violeta Hernández]

If proofs become no more complicated than they were before, then to me that suggests that there's no need for relabelling at all

[Violeta Hernández]

This is my idea:

/--
`identical x y` says that `x` and `y` are extensionally the same game. Specifically, for every move
in `x` there's an inductively `identical` move for `y`, and viceversa. Compare to `pSet.equiv`.

In ZFC, identical games would indeed be the same games.
-/
inductive identical : pgame.{u} → pgame.{u} → Type (u+1)
| mk : Π {x y : pgame} (Lxy : x.left_moves → y.left_moves) (Lyx : y.left_moves → x.left_moves)
         (Rxy : x.right_moves → y.right_moves) (Ryx : y.right_moves → x.right_moves),
         (∀ i, identical (x.move_left i) (y.move_left (Lxy i))) →
         (∀ i, identical (y.move_left i) (x.move_left (Lyx i))) →
         (∀ j, identical (x.move_right j) (y.move_right (Rxy j))) →
         (∀ j, identical (y.move_right j) (x.move_right (Ryx j))) →
       identical x y

[Mario Carneiro]

isn't that the game equivalence relation?

[Mario Carneiro]

game is to pgame as Set is to pSet

[Mario Carneiro]

(the similarity is not a coincidence, pgame was mostly a copy-paste-paste job)

[Junyan Xu]

isn't that the game equivalence relation?

Certainly not. g + -g, which can be arbitrarily complicated, is equivalent to 0 in game

[Junyan Xu]

pSet can very well be called the unary version of pgame
Which I guess is to be expected, ZFC games are constructed almost the same way as ZFC sets, just twice

Yes, that's why I drew a parallel between Conway's construction of games and the von Neumann universe. The axiom of regularity/foundation says the von Neumann universe contains all the sets.

[Junyan Xu]

pSet.equiv is a Prop though, are you sure you want to keep the data in identical?

[Mario Carneiro]

it's also defined by recursion not induction

[Mario Carneiro]

I think this is the difference between docs#function.bijective and docs#equiv; I wouldn't be surprised if both notions are useful

[Junyan Xu]

Then, to prove an inequality on pgame, we could simply change it into the def-eq inequality on game, and use a few rws

As mentioned in #13925, I wonder whether this would be a nice application of the norm_cast (specifically rw_mod_cast) tactic. If that's the case, I think @Mario Carneiro can probably provide some guidance on how to write an "extension" or something for that tactic to apply to pgames.

[Mario Carneiro]

I don't think you need to write an extension or anything; you just mark the relevant theorems with the @[norm_cast] attribute

[Violeta Hernández]

What exactly is restricted supposed to mean?

[Violeta Hernández]

My new definition of identical really resembles it

[Violeta Hernández]

But I don't quite understand the docstring

[Violeta Hernández]

Also, is ≡ in use in mathlib? I want to use that for identical

[Junyan Xu]

It means what the docstring says: x has no more left moves and no less right moves than y. If you have fewer moves you are more likely to lose, so it implies x ≤ y: x is worse or equal for left than y.
It's different from your definition because the maps are single sided: (L : x.left_moves → y.left_moves), not the other way around, (R : y.right_moves → x.right_moves), not the other way around.

[Junyan Xu]

From my reading of the paper, to utilize rw_mod_cast for pgame, it seems we need to do the following:

• Introduce a has_coe instance from pgame to game (seems necessary).
• write the move lemmas and mark them with @[norm_cast]: the quotient map (the cast) pgame → game respects add/neg/sub/zero
• write and mark the elim lemmas: < ≤ ⧏ are preserved by the cast, plus ↑a = ↑b ↔ a ≈ b
• squash lemmas should only be necessary when we have the casts pgame → pgame-mod-identical → game (maybe also for {x // x.numeric} → surreal → game and {x // x.numeric} → pgame → game?)

[Violeta Hernández]

I proved that x ≡ y implies restricted x y (and of course, restricted y x)

[Violeta Hernández]

I wonder if the converse is true?

[Violeta Hernández]

That is, restricted x y and restricted y x imply x ≡ y

[Violeta Hernández]

I have just produced one of the goofiest proofs ever

/-- If `w` is identical to `x` and `y` is identical to `z`, then `w + y` is identical to `x + z`. -/
theorem identical.add_congr : ∀ {w x y z : pgame.{u}}, w ≡ x → y ≡ z → w + y ≡ x + z
| ⟨wl, wr, wL, wR⟩ ⟨xl, xr, xL, xR⟩ ⟨yl, yr, yL, yR⟩ ⟨zl, zr, zL, zR⟩
  ⟨Lwx, Lxw, Rwx, Rxw, HLwx, HLxw, HRwx, HRxw⟩ ⟨Lyz, Lzy, Ryz, Rzy, HLyz, HLzy, HRyz, HRzy⟩ :=
begin
  let Hwx : ⟨wl, wr, wL, wR⟩ ≡ ⟨xl, xr, xL, xR⟩ := ⟨Lwx, Lxw, Rwx, Rxw, HLwx, HLxw, HRwx, HRxw⟩,
  let Hyz : ⟨yl, yr, yL, yR⟩ ≡ ⟨zl, zr, zL, zR⟩ := ⟨Lyz, Lzy, Ryz, Rzy, HLyz, HLzy, HRyz, HRzy⟩,
  fsplit;
  rintro (i | i),
  { exact sum.inl (Lwx i) },
  { exact sum.inr (Lyz i) },
  { exact sum.inl (Lxw i) },
  { exact sum.inr (Lzy i) },
  { exact sum.inl (Rwx i) },
  { exact sum.inr (Ryz i) },
  { exact sum.inl (Rxw i) },
  { exact sum.inr (Rzy i) },
  all_goals {dsimp},
  { exact (HLwx i).add_congr Hyz },
  { exact Hwx.add_congr (HLyz i) },
  { exact (HLxw i).add_congr Hyz },
  { exact Hwx.add_congr (HLzy i) },
  { exact (HRwx i).add_congr Hyz },
  { exact Hwx.add_congr (HRyz i) },
  { exact (HRxw i).add_congr Hyz },
  { exact Hwx.add_congr (HRzy i) }
end
using_well_founded { dec_tac := pgame_wf_tac }

[Violeta Hernández]

This is the only proof so far that has been somewhat longer than the previous proof about relabelling, and even then, I'd argue this proof is clearer than the original one

[Violeta Hernández]

(btw, I reordered some arguments in identical which made some proofs quite easier)

[Violeta Hernández]

Yeah, I think I was right! Proving that things are identical is pretty much as easy / hard as proving they're relabellings

[Violeta Hernández]

And in fact, I was even able to golf a bunch of proofs

[Junyan Xu]

Violeta Hernández said:

That is, restricted x y and restricted y x imply x ≡ y

It seems x = {1,0| }, y = {1| } is a counterexample.

[Violeta Hernández]

Hmm... it seems like there is one theorem in mathlib that is no longer true with identical but was with relabelling

[Violeta Hernández]

docs#pgame.short_of_relabelling

[Violeta Hernández]

This isn't currently used anywhere, though

[Violeta Hernández]

What should be done here?

[Violeta Hernández]

I do think that there's little case in keeping relabelling around if we're going to have identical... but maybe there's some case

[Violeta Hernández]

Violeta Hernández said:

This isn't currently used anywhere, though

Oh, it's actually used somewhere

[Violeta Hernández]

Hmm

[Violeta Hernández]

Being a relabelling is a strictly stronger notion than being identical, so maybe what we should have is a theorem showing one implies the other

[Violeta Hernández]

Would be nice to have another symbol for the relabelling relation

[Violeta Hernández]

Maybe ≡r?

[Scott Morrison]

Is it used to show domineering is a short game? I forget.

[Violeta Hernández]

It's used in some theorems about short games, yeah

[Violeta Hernández]

I guess that for those, it's important to provide an actual bijection between moves

[Mario Carneiro]

One way to recover that theorem is to define something like "essentially short" which means that from each position there are a finite number of equivalence classes up to identical

[Mario Carneiro]

note that a game is essentially short iff it is identical to a short game, and if you take that as the definition then the theorem becomes almost tautologically true

[Violeta Hernández]

I think the question we should be asking is: should something like {0, 0, 0, ... | }with infinitely many zeros be short?

[Mario Carneiro]

it is essentially short by my definition

[Violeta Hernández]

This would probably break all of the computability on short games, though

[Mario Carneiro]

how so

[Mario Carneiro]

especially if essentially short came with an actual finset of equivalence class representatives

[Mario Carneiro]

actually make that a list or multiset, there is no point in distinctness here

[Violeta Hernández]

Hmm, that might work

[Violeta Hernández]

So, to be clear, we do want to replace relabelling by identical, right?

[Mario Carneiro]

I don't see why not have both, but making identical be the load bearing one seems good to me

[Violeta Hernández]

...yeah, actually, it might be a better idea to just have both

[Violeta Hernández]

I do think we would need to mix them in the API, though

[Violeta Hernández]

When possible, have identical in the hypotheses, and relabelling in the conclusions

[Mario Carneiro]

well one implies the other so that seems fine

[Violeta Hernández]

I now have another problem

[Violeta Hernández]

I attempted to make relabelling into a Prop

[Kevin Buzzard]

When making API for nnreal it's certainly handy to have a \ne 0 in the hypotheses and 0 < a in the conclusions because of dot notation and docs#has_lt.lt.ne' , one could play the same trick here

[Violeta Hernández]

Which to me makes a lot of sense: relabelling should be an equivalence relation, and it's not like we ever use the data

[Violeta Hernández]

...except, we actually do use the data

[Violeta Hernández]

docs#pgame.short_of_relabelling

[Mario Carneiro]

you said something about computability? I think we do use the data

[Violeta Hernández]

There's no way to avoid this, is there? Unless we were to make short games noncomputable

[Mario Carneiro]

certainly if identical is data and you have identical_of_relabelling you will need the data

[Violeta Hernández]

I didn't mean for identical to be data either

[Mario Carneiro]

like I said earlier this is like equiv vs bijective

[Mario Carneiro]

guess which one sees more use in mathlib?

[Violeta Hernández]

I don't think this is quite the same situation

[Violeta Hernández]

Under normal circumstances, we really don't have any use for the data in a relabelling

[Violeta Hernández]

We can't "apply" a relabelling like we can an equivalence

[Mario Carneiro]

why not?

[Mario Carneiro]

you can take a strategy for one game and make a strategy for the other, or other things like that

[Violeta Hernández]

That's just the relabelling itself

[Violeta Hernández]

You're not applying it to anything

[Violeta Hernández]

You might suppose you can apply a relabelling between a and b to a subsequent game of a, but even if this is possible we have no API whatsoever for this

[Mario Carneiro]

if you have a play sequence on one game you can apply it to get a play sequence on the other

[Mario Carneiro]

I think just about any data "about" a game can be remapped across the relabelling

[Mario Carneiro]

so it really does look like equiv to me

[Violeta Hernández]

Hmm... you're right

[Violeta Hernández]

We currently have no API for this at all, but it's certainly something that could at some point be worked on

[Mario Carneiro]

that all mostly applies to identical as well

[Violeta Hernández]

Alright, I see why this should be data

[Violeta Hernández]

Before trying to do any of the identical stuff, I've opened #14155 to add the ≡rnotation for relabellings and clean up some proofs

[Violeta Hernández]

I should probably outline what I'm getting at with all this

[Violeta Hernández]

The idea is to first define this identical relation. Then, we define the quotient of games by this relation and prove that negation, addition, and multiplication (?) can be lifted to this quotient. This should save us from the pain of congr lemmas when proving identities or relabellings.

[Violeta Hernández]

Note that game can't do this, as the relabelling relation doesn't lift to it

[Violeta Hernández]

Hmmm... wait. If I really want to do this, then I actually need to define two quotients, one for relabelings and one for identical games

[Violeta Hernández]

This feels excessive and redundant, but it also seems like the easiest way to work with these two relations

[Junyan Xu]

Violeta Hernández said:

So you might need to induct on a generic multiset s and make the inductive hypotheses "if {x, y} is less than s then P1, ..."

I'm currently using your mul_args:

def cut_expand {α : Type*} [decidable_eq α] (r : α → α → Prop) (s' s : multiset α) : Prop :=
∃ (t : multiset α) (a ∈ s), (∀ a' ∈ t, r a' a) ∧ s' = s.erase a + t

inductive mul_args : Type (u+1)
| P1 (x y : pgame.{u}) : mul_args
| P24 (x₁ x₂ y : pgame.{u}) : mul_args

def to_multiset : mul_args → multiset pgame
| (mul_args.P1 x y) := {x, y}
| (mul_args.P24 x₁ x₂ y) := {x₁, x₂, y}

def hyp : mul_args → Prop
| (mul_args.P1 x y) := numeric x → numeric y → numeric (x * y)
| (mul_args.P24 x₁ x₂ y) := numeric x₁ → numeric x₂ → numeric y → P24 x₁ x₂ y

def ces := by classical; exact inv_image (cut_expand subsequent) to_multiset

theorem P1_of_P24 (x y : pgame) (ih : ∀ a', ces a' (mul_args.P1 x y) → hyp a')
  (hx : x.numeric) (hy : y.numeric) : (x * y).numeric := sorry

seems to be working fine!

[Violeta Hernández]

That's pretty amazing

[Violeta Hernández]

Do you have a proof sketch for the hydra game ending?

[Violeta Hernández]

I think that warrants its own separate PR

[Violeta Hernández]

And I'd be glad to help if possible

[Junyan Xu]

This is a full proof in under 100 lines.

[Violeta Hernández]

Yeah, I believe this is an interesting enough result to maybe even have its own file

[Violeta Hernández]

Obviously the PR wouldn't be stated in terms of games, though

[Violeta Hernández]

Note: the proof of le_trans could be stated in terms of this, though I don't think it's large enough that this would be able to golf it

[Junyan Xu]

Since it's just 100 lines I think it could go to the end of https://leanprover-community.github.io/mathlib_docs/logic/relation.html instead of having its own file.

I'd like to PR it, but maybe I'll wait until I fill in more details in the Theorem 3.8 proof to convince that this well-foundedness result is the only thing left to make the proof work.

[Violeta Hernández]

Wait, you're working on that independently?

[Junyan Xu]

I have looked at your code

[Junyan Xu]

but instead of doing it in one stretch I try to extract lemmas that apply to multiple cases

[Violeta Hernández]

That's what I've attempted too, but all of these lemmas seem to depend on the same induction hypotheses

[Junyan Xu]

your surreal_mul branch hasn't been updated for almost 2 weeks, is there any new progress? I see that you are busy with other PRs.

I think I really just started to write code about Theorem 3.8 today, after the < correction was merged. I've shown one of the four cases of P1 follows from the induction hypothesis, and is now hoping the same lemmas that solved this case would also solve the other cases.

[Violeta Hernández]

I just merged with master :P

[Violeta Hernández]

Yeah, I've been busy with other PRs

[Violeta Hernández]

I wanted a certain lemma on birthdays, which necessitated a certain lemma on ordinals, and that led me down a rabbit hole of fixing some glaring holes in that API

[Violeta Hernández]

I still haven't even added that darned lemma

[Violeta Hernández]

But it wouldn't be necessary with your new approach

[Violeta Hernández]

I'll see if I can continue work on the proof within the next few days

[Violeta Hernández]

And you know, the sheer work you've put into your new framework for games is starting to convince me that it might be worth it, but I have no idea how I would pitch this to everyone else

[Violeta Hernández]

Still a bit worried about e.g. the ordinal and nim API though

[Junyan Xu]

Violeta Hernández said:

I wanted a certain lemma on birthdays, which necessitated a certain lemma on ordinals, and that led me down a rabbit hole of fixing some glaring holes in that API

I find it strange to see the birthday (x + y) stuff in your code. Why not express it in terms of birthday x and birthday y? Seems that (x + y) doesn't appear in the options of the product of two games?

[Violeta Hernández]

As far as I know (and I don't know that many things) there isn't any nice form for the birthday of the sum of two games

[Violeta Hernández]

(deleted)

[Violeta Hernández]

However, this value does have the property that it decreases when you replace either game by a subsequent one

[Violeta Hernández]

Further, if the birthday of y is less than the birthday of z, the birthday of x + y is less than the birthday of x + z

[Kevin Buzzard]

I think that's now called something like covariant_class (+) (<) or something

[Violeta Hernández]

We don't have any named relation for "the birthday of x is less than the birthday of y" though

[Violeta Hernández]

I don't think we need it either

[Violeta Hernández]

Violeta Hernández said:

Further, if the birthday of y is less than the birthday of z, the birthday of x + y is less than the birthday of x + z

Note, I'm only 99% sure of this

[Violeta Hernández]

I wanted to prove it in Lean, but for that I needed a lemma lsub_sum, which would be a consequence of sup_sum, which would be a consequence of csup_sum, which I had no idea where to put because conditionally_complete_lattice.lean and complete_lattice.lean are very different files despite most of the same theorems being true... you get my point

[Violeta Hernández]

Predictably, this lf refactor broke what I had of the surreal multiplication proof

[Violeta Hernández]

I'll try to fix it later today

[Mario Carneiro]

Violeta Hernández said:

Violeta Hernández said:

Further, if the birthday of y is less than the birthday of z, the birthday of x + y is less than the birthday of x + z

Note, I'm only 99% sure of this

That sounds false, at least with strict less than

[Mario Carneiro]

I think if the birthday of x is large then it will dominate and the birthday of x + y will be the same as x or maybe one more

[Mario Carneiro]

(at least, I am taking it as analogous to the claim that rank y < rank z -> rank (x ⊔ y) < rank (x ⊔ z) in zfc)

[Mario Carneiro]

Oh no wait I remember now, this is the natural sum operation on ordinals

[Mario Carneiro]

which we don't have any API for

[Mario Carneiro]

That is, I claim that birthday (x + y) = birthday x # birthday y

[Violeta Hernández]

Let me sketch a proof of that claim:

We first prove that birthday y ≤ birthday z → birthday (x + y) ≤ birthday (x + z) by Conway induction. Separate each birthday as the max of four lsubs. By the inductive hypotheses, these are less-or-equal respectively.

Then, if birthday y < birthday z, there exists some optionz' of z with birthday y ≤ birthday z', so that birthday (x + y) ≤ birthday (x + z') < birthday (x + z).

[Violeta Hernández]

Mario Carneiro said:

Oh no wait I remember now, this is the natural sum operation on ordinals

Nice! Yet another thing I can do with ordinals!

[Mario Carneiro]

And yes, I believe that y < z -> x # y < x # z

[Mario Carneiro]

the theory of natural sum/product is pretty darn similar to the theory of birthdays of surreals though, it might not be worth the rephrasing

[Mario Carneiro]

there is one novelty you get with the ordinal formulation though, which is the concrete definition of natural sum given by lining up the cantor normal forms and adding things pointwise

[Violeta Hernández]

Whoa, that works?

[Violeta Hernández]

That's really cool

[Violeta Hernández]

We don't need to "rephrase" ordinal birthdays in terms of the natural sum and product. But we could define the natural sum and product on ordinals, prove all the necessary theorems, then simply transfer them to surreal birthdays

[Mario Carneiro]

yup, it's mentioned at the end of that wikipedia section

[Mario Carneiro]

The easiest way to prove it probably goes via the observation that the natural sum is the greatest order type of a total order extending the disjoint union of types with order types x and y respectively. It is easy to see that the pointwise sum of cantor orderings is a way to order that disjoint union: you take all the A stuff and then all the B stuff in each coordinate, which proves that the cantor formula is <= x # y. For the reverse I think you can use ordinal induction, although it looks messy

[Violeta Hernández]

I think we'll need quite a lot more API for Cantor normal forms to get this to work

[Violeta Hernández]

It's not immediate to fix my progress on the multiplication proof

[Violeta Hernández]

I had taken a few shortcuts that just don't work anymore

[Violeta Hernández]

Which leads to the question of whether I was actually simplifying the proof by using lf instead of lt, or if my approach was flawed and I just hadn't realized it

[Violeta Hernández]

I'm going to have to go over the proof again with what I now know and evaluate this, and I am currently too tired to do so

[Violeta Hernández]

So maybe tomorrow

[Violeta Hernández]

On an unrelated note

[Violeta Hernández]

We have a consensus on \<| and \lf being useful shortcuts, right?

[Violeta Hernández]

I lied, I'm looking at the proof right now :P

[Violeta Hernández]

image.png This right here is an iff, if z₁ and z₂ are numeric

[Violeta Hernández]

This is an immediate consequence of le_def_lt, the numeric counterpart to le_def_lf (which I have already PR'd)

[Violeta Hernández]

I wonder, can we get away with the if direction without assuming that these are numeric?

[Violeta Hernández]

It isn't really a problem, this dependency still satisfies the hydra relation, but it's a dependency I hadn't accounted for before

[Junyan Xu]

pgame.le_def_lf doesn't assume numeric, and we are proving lt, which implies lf unconditionally, so I don't see any additional dependency.

[Violeta Hernández]

Oh, you're right

[Violeta Hernández]

So, it seems like we can prove P2 by using a weaker form of P4 using lf instead of lt

[Violeta Hernández]

Here's the question: can we perhaps do the rest of the proof from this weaker P4'?

[Violeta Hernández]

If so then we've found a way to simplify the argument

[Violeta Hernández]

I'm a bit skeptical of this working though, since add_lf_add isn't actually true

[Violeta Hernández]

Hmm... in fact, this would have doomed my proof if I hadn't realized we had lt and lf swapped

[Violeta Hernández]

Alright, I got the proof working again... or rather, what I had written of it

[Violeta Hernández]

There's little missing now, other than the proof of well-foundedness

[Violeta Hernández]

I think I can finish the skeleton tonight

[Violeta Hernández]

Yeah actually no

[Violeta Hernández]

I am way past my bedtime and I only finished one of eight (?) remaining cases

[Violeta Hernández]

I got this as the output of abel

[Violeta Hernández]

image.png

[Violeta Hernández]

Note that ⟦x₁R jx₁ * mk yl yr yL yR⟧ appears on both sides of the inequality

[Violeta Hernández]

Is there some easy way to make abel realize this and cancel them out? Or some other tactic that does the job better?

[Violeta Hernández]

Note: the original expression was even more complicated, and abel did successfully cancel out one of two pairs of common terms

[Yaël Dillies]

"cancelling out" means "applying a monotonicity lemma", so I think it's out of scope for abel.

[Violeta Hernández]

Is there any other tactic that can deal with this?

[Violeta Hernández]

For full context: here's my hypothesis and my goal image.png

[Violeta Hernández]

x₁ is def-eq to mk x₁l x₁r x₁L xᵣ btw, same goes for x₂

[Violeta Hernández]

Actually, there might be some syntactic equality troubles that prevent a single tactic from closing the goal, but simplifying H₃ enough that I can just use one or two rw add_comm and exact would be amazing

[Reid Barton]

Use some lemma to rewrite H3 to the form 0 < _ and then try abel?

[Yaël Dillies]

tactic#monotonicity

[Violeta Hernández]

You mean mono?

[Violeta Hernández]

mono at H₃ doesn't seem to work

[Violeta Hernández]

Reid Barton said:

Use some lemma to rewrite H3 to the form 0 < _ and then try abel?

This might work, maybe apply_rules could do this?

[Violeta Hernández]

I have proven four out of eight goals in the very last stretch of the skeleton of the proof!

[Violeta Hernández]

The skeleton will be ready really soon

[Violeta Hernández]

(today in messages that are funnier without context)

[Violeta Hernández]

Six out of eight!

[Violeta Hernández]

Eight out of eight!!!!!!

[Violeta Hernández]

Alright, the skeleton of the proof is done

[Violeta Hernández]

This is almost 300 lines of code for a single proof (which I presume is some sort of mathlib record?)

[Violeta Hernández]

There's definitely room for golfing though

[Violeta Hernández]

@Junyan Xu

[Violeta Hernández]

I tried to make the induction step easier to prove by deduplicating applications of the induction hypothesis

[Violeta Hernández]

Even then, there are a whopping 36 applications we need to prove well-founded

[Violeta Hernández]

I'm going through each of them and verifying they satisfy the cut_expand relation

[Violeta Hernández]

Not formally, yet

[Violeta Hernández]

Actually, the cut_expand relation is a wee bit too weak

[Violeta Hernández]

It seems like we need its transitive closure

[Violeta Hernández]

Fortunately I proved not too long ago that the transitive closure of a well-founded relation is well-founded

[Violeta Hernández]

Now, here's the kicker

[Violeta Hernández]

What's a succint way to prove two multisets satisfy the cut_expand relation?

[Violeta Hernández]

image.png If we provide t, are the other proofs rfl?

[Junyan Xu]

It's great that you finished the proof! I'll hopefully PR my part tonight. I'll probably change s' = s.erase a + t to s' + {a} = s + t in cut_expand, as it avoids decidable_eq and it's probably easier to show concrete multisets satisfy the relation with + instead of erase.

And I think I'll also define an inductive relation on mul_args that is a subrelation of inv_image (trans_gen $ cut_expand is_option) (so well-founded and we can have the has_well_founded instance on mul_args) and covers all cases we need, and then we can define a wf tactic that use solve_by_elim with the constructors of the relation to fulfill the wf obligations.

[Junyan Xu]

Violeta Hernández said:

What's a succint way to prove two multisets satisfy the cut_expand relation?

The docs for fin_casesappears like that it could solve these, but actually not.

[Junyan Xu]

The most systematic way I can think of now is to use add_singleton to expand it to sum of singletons, then use commutativity, associativity etc. (Notice that {a,b,c} is something like ({a}.cons b).cons c under the hood.)

[Violeta Hernández]

Junyan Xu said:

And I think I'll also define an inductive relation on mul_args that is a subrelation of inv_image (trans_gen $ cut_expand is_option) (so well-founded and we can have the has_well_founded instance on mul_args) and covers all cases we need, and then we can define a wf tactic that use solve_by_elim with the constructors of the relation to fulfill the wf obligations.

Already on it:

instance : has_lt mul_args :=
⟨inv_image (relation.trans_gen $ cut_expand subsequent) to_multiset⟩

instance : has_well_founded mul_args :=
{ r := (<),
  wf := inv_image.wf _ (cut_expand.wf wf_subsequent).trans_gen }

[Violeta Hernández]

I'm writing down the sorries for the well-foundedness proofs

[Violeta Hernández]

There! I've sorried all 36 of them

[Violeta Hernández]

And they should all be true

[Violeta Hernández]

How does your new definition for cut_expand look like?

[Violeta Hernández]

I want to try some things out with it

[Violeta Hernández]

I presume it's this?

def cut_expand (r : α → α → Prop) (s s' : multiset α) : Prop :=
∃ (t : multiset α) (a ∈ s), (∀ a' ∈ t, r a' a) ∧ s' + {a} = s + t

example : cut_expand (<) ({0, 1, 3} : multiset ℕ) ({0, 1, 2, 2, 2, 2} : multiset ℕ) :=
begin
  refine ⟨{2, 2, 2, 2}, 3, _, λ a h, _, _⟩,
  { dec_trivial },
  { fin_cases h;
    dec_trivial },
  { dec_trivial }
end

[Junyan Xu]

Interesting, changing erase to + makes it decidable and fin_cases applicable?

[Violeta Hernández]

At least for naturals

[Junyan Xu]

Oh yes, pgame doesn't have decidable_eq

[Violeta Hernández]

Is there any way to prove goals like x₁ ∈ {x₁, x₂, x₃} easily without decidable_eq?

[Violeta Hernández]

Or god forbid, something like this image.png

[Violeta Hernández]

I've started filling out the sorries

[Violeta Hernández]

The one that I'm going to leave open is the one for cut_expand.wf

[Violeta Hernández]

That's all yours

[Junyan Xu]

Violeta Hernández said:

Is there any way to prove goals like x₁ ∈ {x₁, x₂, x₃} easily without decidable_eq?

Maybe simp only [multiset.mem_cons] then use rfl with some or.inl, or.inr.

Violeta Hernández said:

Or god forbid, something like this image.png

maybe simp only [<- multiset.singleton_add], abel

[Violeta Hernández]

I filled in some simple lemmas for P1 x' y' < P1 x y, we're already down to 26 sorries

[Junyan Xu]

Actually I want to remove the a ∈ s condition, which is unnecessary for irreflexive relation r.

[Violeta Hernández]

Every well-founded relation is irreflexive

[Violeta Hernández]

So yeah, you should remove that

[Violeta Hernández]

I'm having a bit of trouble

[Violeta Hernández]

Not with the proofs themselves

[Violeta Hernández]

But rather, giving names to like 10 auxiliary lemmas for that relation is not really working out haha

[Junyan Xu]

Junyan Xu said:

maybe simp only [<- multiset.singleton_add], abel

Just need an additional rw multiset.has_insert to make it work:

import data.multiset.basic

example : ({1,2} : multiset ℕ) + {2,3,5} = {2,3,5,1,2} :=
begin
  rw multiset.has_insert,
  simp only [← multiset.singleton_add], abel,
end

[Junyan Xu]

However it's still cumbersome. Maybe wrap it into a single local tactic? I think Lean can't come up with t (=s' + {a} - s) automatically because multiset.has_sub uses decidable_eq.

[Violeta Hernández]

On second thought, I'm not sure this will help

[Violeta Hernández]

I've been able to produce relatively short proofs for the theorems I've needed, without relying on things like these

[Junyan Xu]

I think if you adopt my approach and define (<) on mul_args as an inductive relation, then you can replace the ~10 auxiliary lemmas with ~10 constructors; you can prove it's a subrelation of the inv_image in a single lemma, and use subrelation.wf to show it's well-founded. And here's a way to name the constructors systematically; for example, the constructor that produces mul_args.P1 y x₂L < mul_args.P24 x₁ x₂ y may be named eyo₂, meaning that the first argument is equal to y and the second is an option of x₂. Similarly, the constructor that produces mul_args.P24 yL yR x < mul_args.P1 x y may be named oyoyex.

[Junyan Xu]

#14190

[Violeta Hernández]

I decided against defining < on mul_args directly, instead opting to define a relation on multisets themselves. That way, I'm able to directly apply lemmas like {x, y} = {y, x}without having to use change or unfold

[Violeta Hernández]

But yeah, your approach still works

[Violeta Hernández]

There's some auxiliary lemmas on cut_expand I'll still need, but I'll PR those after your PR is merged

[Violeta Hernández]

I just realized

[Violeta Hernández]

I think you can prove equality of multisets like {x₁, x₂, x₃} = {x₂, x₂, x₁, x₃} by ext, tauto

[Mario Carneiro]

ext, simp should also work

[Scott Morrison]

I've always held that if ext, simp fails to prove a "these things are the same because they are made out of the same ingredients" goal, then you are obligated to go write the missing @[ext] and @[simp] lemmas before proceeding!

[Yaël Dillies]

In that case I'm not sure this holds, because there can be arbitrarily many or_comm required to prove the goal.

[Violeta Hernández]

We got \lf, \<|, and \fuzzy added to vscode-lean!

[Yaël Dillies]

Did you add them to the other extensions as well?

[Violeta Hernández]

Uhhhhh no

[Violeta Hernández]

I probably should do that

[Violeta Hernández]

What other extensions are there?

[Julian Berman]

(I pull in changes every so often to neovim, so I pulled yours in already. There's emacs too but I think Sebastian does the same every so often. Probably some day we'll have a shared location that doesn't involve copy pasting, but for now I think you're good)

[Yaël Dillies]

There's also @Arthur Paulino's Chrome extension

[Eric Wieser]

I only just learnt to use \lf and \rf to type ⌊ and ⌋ :(

[Yaël Dillies]

Aaah, no that was one of my favorite shortcuts :sad:

[Eric Wieser]

What does "lf" stand for in the pgame world?

[Yaël Dillies]

"less than or fuzzy to"

[Eric Wieser]

ltf might be a reasonable compromise then, although I don't remember what the rules are for resolving ambiguity of abbreviations

[Eric Wieser]

Maybe adding \floor for ⌊$CURSOR⌋ is a better solution anyway

[Ruben Van de Velde]

Or both?

[Eric Wieser]

It would be great if we could move the management of these aliases to within mathlib itself

[Eric Wieser]

But that's probably a conversation for a new thread

[Violeta Hernández]

I decided to go ahead and PR natural addition: #14291

[Violeta Hernández]

This is relevant to games in two ways (that I know of!)

[Violeta Hernández]

a.to_pgame + b.to_pgame ≈ (of_nat_ordinal (to_nat_ordinal a + to_nat_ordinal b)).to_pgame

[Violeta Hernández]

(i.e. natural addition is the addition on ordinal games)

[Violeta Hernández]

And birthday (a + b) = of_nat_ordinal (to_nat_ordinal (birthday a) + to_nat_ordinal (birthday b))

[Violeta Hernández]

This of and to notation totally sucks, but natural addition and multiplication have a ton of algebraic properties, so it was worth making into a type alias so that we could provide all the appropriate instances

[Eric Rodriguez]

maybe add some notation for of/to? localised maybe?

[Violeta Hernández]

Any suggestions?

[Violeta Hernández]

I'm guessing such a notation would look something like ᵒᵈ and friends

[Scott Morrison]

Or just put them in a namespace so by opening the namespace you can just write to and from? I think this might be too specialized to warrant notation.

[Violeta Hernández]

That's clever

[Violeta Hernández]

to_nat_ordinal and of_nat_ordinal are both already in a nat_ordinal namespace. Should I just rename them to to and of?

[Junyan Xu]

Wikipedia uses the notations ⊕ and ⊗ which I think are standard. The ⊕ notation is also common for Nim sum / xor, and nim sum/product also have tons of algebraic properties (forming an algebraically closed field On₂, see Lieven le Bruyn's blog posts), but we may use ⊕₂ ⊗₂ to signify both their binary nature and their similarity to natural sum/product.

By the way, well partial orders is spelt docs#set.is_pwo in mathlib, and it would be nice to connect them to natural sums/products as explained in the first Wikipedia page.

[Violeta Hernández]

⊕ is definitely a no-go, since it's used for type sums

[Violeta Hernández]

Also, the decision to make a new type in order to use + and * was quite intentional. These natural operations have a lot of algebraic structure to them, and we'd be missing out on tons of instances if we just made them operations on ordinal itself

[Violeta Hernández]

They're commutative, associative, preserve order, are cancellative, and distributive

[Violeta Hernández]

And they have the usual 0 and 1 from ordinals

[Junyan Xu]

Ok yes, a lot of nice properties seem impossible to state without the had_add has_mul instances, and those would conflict with the original ones, so a type synonym seems necessary.

[Violeta Hernández]

In an ideal world we'd have group (+) instead of add_group and such, but this isn't that world :sob:

[Junyan Xu]

Maybe what we want is a ⊗ b = of_nat_ordinal (to_nat_ordinal a * to_nat_ordinal b) and the alike.

Here's how people solve the notation conflict with type sum in biproducts ("direct sum") in the categorical setting; in concrete categories its underlying type is usually exactly the type sum. I wonder if it makes sense and easy to make the ⊕ notation localized.

By the way, anyone knows why lf and equiv are displayed in the docs instead of their notations?

[Eric Wieser]

It's because the notation is local

[Violeta Hernández]

Notations still give you syntactic equality, right? If so, that's definitely the right approach

[Violeta Hernández]

Still, I wouldn't use ⊕, since that's also used for nimber addition

[Junyan Xu]

Wikipedia also suggests the # ⨳ notations.

[Violeta Hernández]

Yeah, I'd rather go with that

[Violeta Hernández]

# could potentially clash with the notation for cardinality, but I find it unlikely we'll ever involve the two at the same time

[Violeta Hernández]

Hmm... actually, I'm not so sure about the local notation anymore

[Violeta Hernández]

Because, the theorems about nat_ordinal are most naturally stated in terms of nat_ordinal, of course

[Violeta Hernández]

But the # notation requires us to state our theorems as theorems about ordinal instead

[Mario Carneiro]

Violeta Hernández said:

# could potentially clash with the notation for cardinality, but I find it unlikely we'll ever involve the two at the same time

umm... cardinal and ordinal are very often used together

[Violeta Hernández]

Hmm.... true

[Mario Carneiro]

I think it doesn't need a symbol beyond what it gets via nat_ordinal

[Mario Carneiro]

a.nadd b / a.nmul b?

[Junyan Xu]

If a b are nat_ordinal then these are just a + b a * b.

[Mario Carneiro]

I mean for the ordinal ops

[Junyan Xu]

Oh yes

[Mario Carneiro]

nat_ordinal would wrap those ops and give them notation

[Junyan Xu]

Yes nadd nmul look short enough. Though I just looked into Unicode just for fun:

The official name for ⨳ ⨳ is "smash product", and in the same block there are also ⩩ ⩩ and ⩨ ⩨, but ⌗ ⌗ is in a different block (0x2317, Miscellaneous Technical). This vertical version looks better than the slanted # #, and also avoids conflict.
There is also
Vai syllable pu: ꖛ ꖛ
Unicode hexadecimal: 0xa59b
In block: Vai (a language in Liberia and Sierra Leone)

[Violeta Hernández]

I'm worried that by wrapping around + and *, we either

• lose a lot of flexibility due to not having typeclasses
• have to prove a lot of lemmas twice

[Mario Carneiro]

? nat_ordinal would have typeclasses

[Mario Carneiro]

you could use nat_ordinal to prove theorems about nadd and nmul by wrapping, but I don't think there will be a huge number of such lemmas

[Violeta Hernández]

Yeah, but we wouldn't have, say nadd_assoc or nadd_comm, or nadd_lt_nadd_left, ... unless we went ahead and wrote every single one of them out

[Mario Carneiro]

you will definitely have nadd_assoc and nadd_comm

[Mario Carneiro]

because you have to prove those

[Violeta Hernández]

My point is that we have those for + on nat_ordinal rather than for nadd

[Violeta Hernández]

I guess it's not that much boilerplate we'd need to add, but still

[Mario Carneiro]

you will have them on nat_ordinal by wrapping nadd_assoc

[Mario Carneiro]

calling the operation + doesn't magically prove it is commutative and associative

[Mario Carneiro]

there are some "theorems for free" but that is not one of them

[Mario Carneiro]

like nadd_left_assoc, okay you might want to defer to group lemmas (although the proof is so trivial it might be more work to prove by reflecting to nat_ordinal than directly)

[Violeta Hernández]

No, I rather mean

[Violeta Hernández]

If we were to wrap around + by using nadd, we'd need to prove a bunch of boilerplate like

theorem nadd_comm : ∀ a b, nadd a b = nadd b a := @add_comm nat_ordinal _
theorem nadd_assoc : ∀ a b c, (nadd a b).nadd c = nadd a (nadd b c) := @add_assoc nat_ordinal _

and so on

[Violeta Hernández]

But I guess it's not that much boilerplate anyways

[Mario Carneiro]

I'm saying that those lemmas would have substantive proofs

[Violeta Hernández]

Sure, they'd have the proofs from nat_ordinal

[Mario Carneiro]

and they would be referenced in the instance : add_comm_group nat_ordinal

[Violeta Hernández]

Oh yeah, I'm aware of that

[Junyan Xu]

It seems another occasion where we'd like to norm_cast into nat_ordinal when we want to prove something about nat sum/prod, in order for instances on nat_ordinal to fire. Maybe just a little bit of boilerplate would make that work? I haven't tried it with pgame->game.

[Mario Carneiro]

Personally I think nat_ordinal and nadd will not get much use beyond the few pgame lemmas you are working on right now

[Mario Carneiro]

they are pretty much only ever brought up in connection with surreals / combinatorial games

[Mario Carneiro]

which is why I think having a couple definitions and no notation is fine

[Violeta Hernández]

I went ahead and defined nadd on ordinal. As expected, there were a lot of boilerplate lemmas to transfer over, though they're almost all def-eq so that's no issue. I think this is a good price to pay for much simpler notation.

https://github.com/leanprover-community/mathlib/pull/14291/commits/f5c5e1e710c92089b88f7f329626f45959785b97

[Violeta Hernández]

And yeah, I guess that what I'm ultimately doing is pretty niche. But that doesn't mean we can't make it look pretty!

[Mario Carneiro]

It looks like nat_ordinal has a ton of boilerplate going in the opposite direction

[Mario Carneiro]

my suggesion is to steal the definition of nat_ordinal.add and paste it in ordinal.nadd

[Mario Carneiro]

and then prove ordinal.nadd_assoc directly

[Mario Carneiro]

and then nat_ordinal will only be boilerplate lemmas

[Violeta Hernández]

I don't think this will entirely work out, since a few of the boilerplate lemmas (the nadd_lt_nadd ones) are generated from the covariant and contravariant instances

[Violeta Hernández]

So at the very least, those have to be proven in nat_ordinal first

[Mario Carneiro]

Aren't those instances true on ordinal too?

[Violeta Hernández]

Not all of them, and even if they were, they wouldn't be on the same operation!

[Mario Carneiro]

of course, s/+/nadd/

[Mario Carneiro]

and if they aren't instances, just call them nadd_lt_nadd

[Violeta Hernández]

The instances automatically generate the iff and cancel lemmas though

[Violeta Hernández]

If I proved these theorems on ordinal first, I'd need to manually prove those lemmas

[Mario Carneiro]

which instance are you talking about specifically?

[Mario Carneiro]

all the ones I see apply to ordinal too

[Violeta Hernández]

I'm talking about add_covariant_class_lt and the seven other similar ones

[Mario Carneiro]

instance add_covariant_class_lt :
  covariant_class ordinal.{u} ordinal.{u} nadd (<) :=

et al

[Violeta Hernández]

Unfortunately, those instances don't have support for any operations other than +,*, or their swapped counterparts (and relations other than < and ≤)

[Violeta Hernández]

So doing this wouldn't autogenerate the lemmas

[Violeta Hernández]

In fact, it wouldn't even give us access to the add_lt_add_left and such lemmas

[Violeta Hernández]

Since they require a has_add instance specifically

[Mario Carneiro]

do you want rel_iff_cov?

[Mario Carneiro]

poking around in the relevant files I see several generic lemmas, they have generic names of course

[Mario Carneiro]

I think if the instances are expressible they should definitely be stated on ordinal, possibly in addition to nat_ordinal

[Violeta Hernández]

My understanding is that there's little to no support for these custom covariant and contravariant classes

[Violeta Hernández]

It's the reason I didn't implement them for lf on pgame

[Violeta Hernández]

Maybe someone else can confirm

[Mario Carneiro]

I'm wondering what kind of nontrivial thing you are even getting out of these classes. We have it stated in a bunch of different ways that x < y -> f x < f y implies f is injective and strictly increasing and iff-preserves lt and le

[Mario Carneiro]

but not having the lemmas doesn't seem like a good reason to not have the instances

[Mario Carneiro]

theorem nadd_lt_nadd_left : ∀ {b c} (h : b < c) a, a ♯ b < a ♯ c :=
@add_lt_add_left nat_ordinal _ _ _
theorem lt_of_nadd_lt_nadd_left : ∀ {a b c}, a ♯ b < a ♯ c → b < c :=
@lt_of_add_lt_add_left nat_ordinal _ _ _
theorem nadd_lt_nadd_iff_left : ∀ a {b c}, a ♯ b < a ♯ c ↔ b < c :=
@add_lt_add_iff_left nat_ordinal _ _ _ _

We don't need all three of these, the last one is plenty

[Violeta Hernández]

Well, we get all three almost for free on nat_ordinal

[Mario Carneiro]

I know, but we get all three for free just from nadd_lt_nadd_iff_left

[Mario Carneiro]

in fact, you could probably prove the first two even shorter by using the last one

[Mario Carneiro]

but I would just drop them, we try to discourage the one way version of iff lemmas unless they are really heavily used

[Mario Carneiro]

it's more compositional that way

[Violeta Hernández]

The way I see it, if we're going to write down boilerplate, we might as well be thorough

[Violeta Hernández]

I wouldn't mourn the loss of the one-sided theorems though

[Mario Carneiro]

well it's a lot less boilerplate if you do it the other way around (I contest)

[Mario Carneiro]

like nat_ordinal.blsub doesn't need to exist at all

[Mario Carneiro]

also ditto on what eric said, instead of a + b ≤ of_nat_ordinal (to_nat_ordinal a + to_nat_ordinal b) you should use only one of the two functions at a time, to_nat_ordinal (a + b) ≤ to_nat_ordinal a + to_nat_ordinal b

[Eric Wieser]

The advantage of having it is that for n : nat_ordinal, n.blsub doesn't resolve to something with a messy type

[Mario Carneiro]

I don't think you should ever need to write n.blsub

[Mario Carneiro]

if all the substantive proof is over ordinal and nadd then the only thing that nat_ordinal needs to do is lift the ring ops

[Violeta Hernández]

nat_ordinal.blsub was actually Eric's suggestion, haha

[Violeta Hernández]

It really only makes things easier to look at

[Violeta Hernández]

I could remove it and save a few rewrites

[Mario Carneiro]

I'm saying that blsub of a nat_ordinal is not a thing that should be happening

[Mario Carneiro]

regardless of how it is written

[Eric Wieser]

From a mathematical perspective, you mean?

[Mario Carneiro]

yes

[Mario Carneiro]

it's used inside the definition of nat_ordinal.add but if that is defined directly on ordinal then I think you won't ever need it elsewhere

[Violeta Hernández]

Surely from a mathematical perspective, nat_ordinal wouldn't need to exist?

[Violeta Hernández]

It only exists because Lean doesn't allow us to define more than one addition for a type

[Violeta Hernández]

Mathematicians have no issue with that

[Mario Carneiro]

sure, so do your best to not use it at all and see how far you can get

[Mario Carneiro]

(that's not sarcasm)

[Mario Carneiro]

I can believe that there are some theorems that currently are only stated for plus-like things so you need to transfer stuff to nat_ordinal, but just use it to get the theorem and then go back to ordinal to finish the proof

[Mario Carneiro]

(and don't forget that you can switch between nat_ordinal and ordinal namespaces multiple times)

[Eric Rodriguez]

I just realised, another option is to make notation that does all the casting stuff for you, and then you should be able to do many rws and stuff as if the notation was a real +/*

[Violeta Hernández]

I think I get your point: we have nat_ordinal for the instances, and nothing more, right?

[Violeta Hernández]

I like that design better

[Violeta Hernández]

It should avoid most if not all of the annoying casting we currently have

[Violeta Hernández]

And if we ever need some theorem that's available through an instance on nat_ordinal, we can simply def-eq cast it

[Violeta Hernández]

What precedences should I set for ♯ and ⨳?

[Violeta Hernández]

I'm still not using the latter, but still

[Mario Carneiro]

For this application, it makes sense to make them the same as + and * respectively

[Violeta Hernández]

And what would those precedences be?

[Violeta Hernández]

I don't know where to find them

[Violeta Hernández]

By the way, I did the refactor Mario suggested, and the lemmas look much nicer!

[Mario Carneiro]

#print +

[Mario Carneiro]

I think it is 65

[Violeta Hernández]

Currently having a go at defining natural multiplication and I'm already at a roadblock with distributivity

[Violeta Hernández]

image.png Other than a stupidly long rw chain, how can I prove this?

[Violeta Hernández]

(note that the terms a' ⨳ b' and a ⨳ b' in this cancel out, giving the result)

[Violeta Hernández]

I could cast this into a (huge) expression in nat_ordinal, but afaik there's no tactic that can finish the goal even then

[Mario Carneiro]

A calc block is probably the clearest way

[Mario Carneiro]

you should be able to normalize it using simp [comm, left_comm, assoc]

[Violeta Hernández]

Is there any way I can normalize it, while specifying the order of the terms?

[Violeta Hernández]

That would be extremely useful if possible

[Mario Carneiro]

one hack is to choose fortuitous variable names

[Mario Carneiro]

otherwise, you are probably better off using rw [left_comm] to bring something to the front

[Violeta Hernández]

docs#left_comm

[Violeta Hernández]

This?

[Mario Carneiro]

nadd_left_comm probably

[Violeta Hernández]

Oh, I see!

[Violeta Hernández]

Once you simp [assoc] you can use nadd_left_comm to move terms as you will

[Violeta Hernández]

Clever!

[Violeta Hernández]

I did it! I managed to prove this!

[Violeta Hernández]

And it only took like 10 rws!

[Damiano Testa]

On a just vaguely related note: if you had actual has_add.add, the proposed tactic move_add gives you the option of specifying which terms in a sum should be first/last at will. You can also of course pass the full permutation, if you so wish!

I'm simply bringing this up since it is the second time that I see a place where move_add would have been wanted "in the wild". Also, adding support for operations other than + would be fairly easy.

[Mario Carneiro]

you would still need to know that the new operation is comm/assoc

[Damiano Testa]

Yes, you would need the analogues of add_assoc, add_comm and add_left_comm.

[Damiano Testa]

These are the three "external" inputs to the tactic, everything else is moving exprs around.

[Violeta Hernández]

Damiano Testa said:

I'm simply bringing this up since it is the second time that I see a place where move_add would have been wanted "in the wild". Also, adding support for operations other than + would be fairly easy.

Make that a third! I would have benefited a lot from that in the surreal multiplication proof

[Violeta Hernández]

I have some huge rw blocks over there too

[Damiano Testa]

Ok, I'll leave the current PR as is, since it has already gone through some revisions. But I will add a second PR allowing "custom" operations.

I was thinking of just + and * support, but I might try to see if I can get a "generic" tactic that takes also an operation as input. It might be tricky to specify the comm/assoc lemmas to use in this case, though.

[Violeta Hernández]

We wouldn't need this if there were some easy way to convert a lemma on ordinal and natural operations to the corresponding one on nat_ordinal

[Violeta Hernández]

I've heard people say norm_cast could help but I don't really know how that works

[Damiano Testa]

I do not know neither the maths, nor the mathlib side of this story, so I'll leave this to someone else!

My naïve view is that norm_cast would take care of dealing with seen and unseen coercions and uniformize everything. Thus, if there were a coe between nat_ordinal and pgames (or games, I really don't know), then norm_cast could convert expressions where one appear into expressions where the other appears.

[Damiano Testa]

I think that you might have to tag the relevant lemmas with a norm_cast attribute, but this is something that I have never done and might be wrong about.

[Violeta Hernández]

I managed to prove the basic properties of natural multiplication and wow were they painful

[Violeta Hernández]

At least now I'm almost sure I have the correct definition

[Violeta Hernández]

I had to extrapolate a bit since every source I looked at just gave the Cantor form definition instead of the recursive one

[Violeta Hernández]

@Junyan Xu hydra PR got merged! I got a bit distracted as of late with the whole natural operations schtick, but I'll PR some auxiliary lemmas on cut_expand shortly and hopefully finish the proof with them

[Junyan Xu]

A few days ago I experimented with the idea of exploiting symmetry to reduce the number of cases in the surreal multiplication proof; e.g. there are 2x2x3=12 cases to show P1 (that x*y is numeric), but I can almost reduce it to just 3 cases using P24_neg, P24_neg', and docs#pgame.quot_mul_neg, docs#pgame.quot_mul_comm etc. (The 3 cases are used to show left_lt_right, and lines 566-581 use left_lt_right to show all 2x2=4 cases. Line 582 onwards are old proofs.) It seems the < and > cases could also follow from one another. However, using symmetry introduces additional obligations to prove identities and handle induction hypotheses (?), so I'm not sure the proofs will end up shorter. I only thought carefully about proving P1, but I expect to exploit symmetry when proving P2 and P4, you'd still apply the symmetries to P2 and P4 instead of P1.

The code is obviously very disorganized so I wouldn't be surprised if it ends up being unhelpful ... However
I am at a conference and don't expect to be able to work on this in the next few days, and since you are getting back to this, I decided to push it in the hope that it could be somewhat inspirational.

[Violeta Hernández]

(deleted)

[Violeta Hernández]

By the way, as for a tactic to solve numeric obligations

[Violeta Hernández]

You can often use solve_by_elim [numeric.move_left, numeric.move_right]

[Violeta Hernández]

I'm wondering

[Violeta Hernández]

Given that the order relations on games are much, much nicer to work with than those on games, should we have a simp lemma converting between them? Or is that dangerous?

[Violeta Hernández]

And if making it a simp lemma isn't the best idea, could it be made norm_cast? I don't know how that works really

[Violeta Hernández]

At the very least we should have the lemmas for rewriting

[Eric Rodriguez]

Violeta Hernández said:

Given that the order relations on games are much, much nicer to work with than those on games, should we have a simp lemma converting between them? Or is that dangerous?

one of these should be pgames and I guess it's the first one

[Violeta Hernández]

Oh sorry

[Violeta Hernández]

It's the second one

[Eric Rodriguez]

lost the 5050 ;b

[Violeta Hernández]

@Junyan Xu I have some time to look into this again

[Violeta Hernández]

What's the general idea in your simplification? I'm having a bit of a hard time following it

[Violeta Hernández]

I agree with some of your ideas, like separating P1 and such into definitions and proving comm lemmas and the like. This should make the proof shorter and easier to follow.

[Violeta Hernández]

I do disagree with various of your ideas here. mul_args should have only two constructors. That way, you get a stronger induction hypothesis for less work (instead of trying to prove that P1 implies both P2 and P4 for the same set of values).

[Violeta Hernández]

Further, defining an ad-hoc relation on mul_args and proving it well founded wouldn't really lead to less work, since we'd still have to prove exactly the same things we're currently proving to prove that it's a subrelation of cut_expand.

[Violeta Hernández]

And totally disagree on defining move_left on {x // numeric x}. There's absolutely no reason we should be working directly with these subtypes. Just separate x and numeric x.

[Violeta Hernández]

Btw I PR'd the lemmas to cast inequalities from pgame to game, and the lemma that relabellings preserve being numeric

[Violeta Hernández]

Oh and also, I don't think that tactic to prove games numeric would be all that useful, since almost always you just apply numeric.move_left and numeric.move_right once or twice

[Junyan Xu]

Violeta Hernández said:

And totally disagree on defining move_left on {x // numeric x}. There's absolutely no reason we should be working directly with these subtypes. Just separate x and numeric x.

Those are just some random ideas that are not necessarily good. However it seems nice to change numeric from a predicate to set, which allows us to write x : numeric through coercion instead of x : {x // numeric x}: https://github.com/leanprover-community/mathlib/compare/surreal_set?expand=1#diff-cfb19983c79209e00ac093e670e2db956ca48e00238011a5854479250cbaec67L58

I am back from the conference and can probably flesh out and clean up more of my plan in branch#surreal_mul_symm this weekend; I'll keep you posted.

[Violeta Hernández]

Would that still allow for dot notation? If so that might be a good idea

[Violeta Hernández]

From your code it seems like the answer is yes

[Violeta Hernández]

Yeah, this looks like a good idea

[Junyan Xu]

I've finished the proof of P1 with my symmetry approach at https://github.com/leanprover-community/mathlib/compare/surreal_mul_symm'?expand=1#diff-cfb19983c79209e00ac093e670e2db956ca48e00238011a5854479250cbaec67R318
I'll leave P2 and P4 to tomorrow.

[Violeta Hernández]

Oh nice! I haven't been nearly as free as I thought I'd be, but I'll check your code thoroughly as soon as I can

[Violeta Hernández]

Should the type equality lemmas like x.left_moves = y be simp?

[Violeta Hernández]

I've been told previously that they shouldn't be, but it seems like all over the code this decision has already been taken as a "yes"

[Violeta Hernández]

Consider for instance docs#pgame.zero_left_moves or docs#pgame.one_left_moves or docs#pgame.pow_half_left_moves

[Violeta Hernández]

Moreover, zero_left_moves is actually used a few times in some dsimps

[Violeta Hernández]

The rationale I got for not making them simp is that type equality is finicky and that this could break things. But surely simp will just not work in those instances?

[Violeta Hernández]

Moreover, there's a few simp lemmas on types like pempty and punit that aren't available on general empty / unique types

[Violeta Hernández]

Like ∀ x : pempty, p x and (∀ x : punit, p x) ↔ p punit.star

[Violeta Hernández]

Well, I guess something that should be done anyways is generalizing forall_pempty and exists_pempty to empty types

[Junyan Xu]

I made an attempt to redefine pSet and pgame such that they have the correct notion of equality (namely "identity") out of the box, where type equality is replaced by set equality, but Lean does not accept it:

import data.set.basic
universe u

structure indexed_set (α : Type u) : Type u := (I : Sort u) (f : I → α)

instance (α : Type u) : setoid (indexed_set α) :=
{ r := λ s₁ s₂, set.range s₁.f = set.range s₂.f,
  iseqv := ⟨λ _, rfl, λ _ _, eq.symm, λ _ _ _, eq.trans⟩ }

inductive pSet : Type u
| mk (s : quotient $ indexed_set.setoid pSet) : pSet

inductive pgame : Type u
| mk (L R : quotient $ indexed_set.setoid pgame) : pgame
/-inductive type being declared can only be nested
inside the parameters of other inductive types -/

I then immediately found this thread confirming that quotient is forbidden, so we're out of luck.

[Junyan Xu]

It seems to me that allowing quotient won't lead to paradoxes that arise when allowing set, but am not sure whether there are other technical problems.

Personally, I am fine with making type equalities simp lemmas in the situation of pgames.

[Junyan Xu]

But, the philosophy is that we care about the underlying set and not the indexing type, so maybe this and the right/existential versions are more benign lemmas:

lemma left_moves_induction {xl xr xL xR} (P : pgame → Prop) :
  (∀ x : (mk xl xr xL xR).left_moves, P $ move_left _ x) ↔ (∀ x : xl, P $ xL x) := iff.rfl

[Violeta Hernández]

Sure, but those won't fire whenever the game in question isn't reducible

[Violeta Hernández]

Also, there's a few rare situations in which we do care about the types, though granted, they arise only because of our specific design. That's when we're proving equalities (not equivalences or relabellings) between pre-games.

[Violeta Hernández]

Or when we're showing that the move sets for some game are empty or unique

[Violeta Hernández]

Most of the time you can just use pempty.is_empty or punit.unique for these proofs, but if the definition is irreducible, then you need to do some type rewriting

[Violeta Hernández]

Something like that happens in the ordinal.lean file

[Junyan Xu]

Whether the type is reducible, you should be able to do apply (left_moves_induction _).2.

[Violeta Hernández]

That wouldn't work either

[Violeta Hernández]

I'm talking about games that aren't definitionally equal to anything of the form mk xl xr xL xR

[Junyan Xu]

I'm talking about games that aren't definitionally equal to anything of the form mk xl xr xL xR

For example?

[Junyan Xu]

The simp lemmas you want are for explicit pgames, right? The examples you gave were zero, one, and pow_half n. And mk is the only constructor...

[Violeta Hernández]

ordinal.to_pgame

[Violeta Hernández]

Since it's defined via the equation compiler, you need to use rw to_pgame to prove the equality with mk _ _ _ _

[Violeta Hernández]

Which is definitely odd, but that's how it goes

[Violeta Hernández]

Another example might be a pre-game retrieved from an exists

[Violeta Hernández]

It's not going to be def-eq to any specific mk _ _ _ _

[Violeta Hernández]

Although of course you can case on it

[Junyan Xu]

Another example might be a pre-game retrieved from an exists

I don't think you can simp its moves though because you don't know what they are ...

[Junyan Xu]

For ordinal.to_pgame, yes if you #print it you see it's well_founded.fix under the hood:

def ordinal.to_pgame._main._pack : Π (_x : ordinal), (λ (_x : ordinal), pgame) _x :=
λ (_x : ordinal),
  has_well_founded.wf.fix
    (λ (_x : ordinal),
       id_rhs ((Π (_y : ordinal), has_well_founded.r _y _x → pgame) → pgame)
         (λ (_F : Π (_y : ordinal), has_well_founded.r _y _x → pgame),
            mk (quotient.out _x).α pempty
              (λ (x : (quotient.out _x).α), let hwf : typein has_lt.lt x < _x := _ in _F (typein has_lt.lt x) hwf)
              pempty.elim))
    _x

[Junyan Xu]

But in this case to_pgame_left_moves etc. aren't defeq, so they won't fire with dsimp and rewriting by them will cause problems, right? Seems a situation where induction principles would be more useful.

[Junyan Xu]

Would this be more convenient?

lemma to_pgame_move_left (o : ordinal) :
  set.range o.to_pgame.move_left = set.range (λ x : o.out.α, (typein (<) x).to_pgame) :=
by { rw [to_pgame], refl }

together with lemmas:

import data.set.basic

variables {α : Type*} {I₁ I₂ : Sort*} (f₁ : I₁ → α) (f₂ : I₂ → α)

lemma range_eq_iff_forall_exists :
  set.range f₁ = set.range f₂ ↔ (∀ i₁, ∃ i₂, f₂ i₂ = f₁ i₁) ∧ (∀ i₂, ∃ i₁, f₁ i₁ = f₂ i₂) :=
⟨λ h, ⟨λ i₁, h.subst (set.mem_range_self i₁), λ i₂, h.substr (set.mem_range_self i₂)⟩,
 λ h, set.ext $ λ x, ⟨λ ⟨i₁, hx⟩, hx ▸ h.1 i₁, λ ⟨i₂, hx⟩, hx ▸ h.2 i₂⟩⟩

lemma range_eq_iff_forall_iff :
  set.range f₁ = set.range f₂ ↔ ∀ (P : α → Prop), (∀ i, P $ f₁ i) ↔ (∀ i, P $ f₂ i) :=
begin
  split,
  { intros h P, iterate 2 { rw ← set.forall_range_iff }, rw h },
  { intros h, ext x, split; revert x; rw set.forall_range_iff; intro i,
    exacts [(h $ set.range f₂).2 (λ i, ⟨i, rfl⟩) i, (h $ set.range f₁).1 (λ i, ⟨i, rfl⟩) i] },
end

lemma range_eq_iff_exists_iff :
  set.range f₁ = set.range f₂ ↔ ∀ (P : α → Prop), (∃ i, P $ f₁ i) ↔ (∃ i, P $ f₂ i) :=
begin
  simp_rw [← not_forall_not, not_iff_not], rw range_eq_iff_forall_iff f₁ f₂, split,
  { exact λ h P, h (λ x, ¬P x) },
  { intros h P, convert h (λ x, ¬P x); simp_rw not_not },
end

[Violeta Hernández]

More convenient than what? I think the current API works pretty well already

[Violeta Hernández]

to_left_moves_to_pgame together with its small API are really all you need

[Junyan Xu]

My point is that in general when the pgame is defined recursively and not defeq to some mk, you may prove an equality between set.range and automatically unlock the forall/exists lemmas.

More generally, if you want to change the indexing type, you may show one of the four conditions and automatically get the other three.

It doesn't seem to me that the APIs around ordinal.to_pgame are completely satisfactory; I think we should strive to eliminate heq lemmas if possible.

[Violeta Hernández]

That approach certainly works, though I still prefer the current one. Building the equivalence between set.Iio o and o.to_pgame.left_moves just makes it really convenient to build a given move, or to reason about an arbitrary one.

[Violeta Hernández]

There is a heq lemma, but it's used only once and never again. If we wanted to, we could make it private and it wouldn't break anything. The API doesn't really depend on it.

[Violeta Hernández]

Moreover, the current aprroach allows you to explicitly build a move that leads to a certain position, instead of just declaring it exists

[Violeta Hernández]

This pattern of building equivalences between left/right moves of games and simpler types is one I've replicated throughout the whole game API, and it's worked very well

[Junyan Xu]

I think my approach still allows you to build move if desired; it only forgets the equivalence (or weaker correspondences) that goes between the two indexing types, but still remembers the two indexing functions. For example, with this

example (o : ordinal) :
  set.range o.to_pgame.move_left = set.range (λ x : set.Iio o, to_pgame x) :=
begin
  symmetry, rw to_pgame, convert function.surjective.range_comp (enum_iso_out o).surjective _,
  ext, congr, exact subtype.ext_iff.1 ((enum_iso_out o).symm_apply_apply x).symm,
end

you can choose to build the move using o.to_pgame.move_left or using to_pgame.

[Violeta Hernández]

What I mean is, say you want a move i such that (to_pgame 2).move_left i = to_pgame 1. With your approach, you need to show to_pgame 1 ∈ set.range (λ x : set.Iio 2, to_pgame x) (which is pretty easy, granted), then rewrite into to_pgame 1 ∈ set.range o.to_pgame.move_left, and that still only tells you that there exists some move with the property you want. You need to use cases to actually retrieve the move.

If you're building data, you'll instead need to call classical.some.

With my approach, you can explicitly build said move as to_left_moves_to_pgame ⟨1, one_lt_two⟩, and simp will do the rest.

[Violeta Hernández]

docs#ordinal.to_pgame_lf is a very good example of this in action.

[Junyan Xu]

With my approach the proof for to_pgame_lf would be:

lemma range_move_left_eq_range_to_pgame (o : ordinal) :
  set.range o.to_pgame.move_left = set.range (λ x : set.Iio o, to_pgame x) :=
sorry /- see earlier post -/

lemma range_eq_iff_forall_iff {α : Type*} {I₁ I₂ : Sort*} (f₁ : I₁ → α) (f₂ : I₂ → α) :
  set.range f₁ = set.range f₂ ↔ ∀ (P : α → Prop), (∀ i, P $ f₁ i) ↔ (∀ i, P $ f₂ i) :=
sorry /- see earlier post -/

theorem to_pgame_lf {a b : ordinal} (h : a < b) : a.to_pgame ⧏ b.to_pgame :=
((range_eq_iff_forall_iff _ _).1 (range_move_left_eq_range_to_pgame b) (function.swap lf _)).1 move_left_lf ⟨a, h⟩

[Violeta Hernández]

Yeah, I feel like my approach is simpler both conceptually and in terms of the final code

[Violeta Hernández]

Seems odd having to use a clever induction principle for something like this

[Violeta Hernández]

Especially when the pencil and paper proof of this theorem is just "since a < b, there's a left move from b.to_pgame to a.to_pgame, Q.E.D"

[Junyan Xu]

The following might everything more convenient and will make simp lemmas like docs#pgame.zero_left_moves obsolete, but may need a large refactor: namely, for each concrete pgame, register two instances has_left_moves and has_right_moves; for example, for ordinal.to_pgamewe register the instance has_left_moves (o.to_pgame) which holds the data of an indexing type set.Iio o (which lies in a higher universe but is more convenient), the indexing function λ x, to_pgame x, and a proof that the range of the indexing function is equal to the range of x.move_left. For the theorems that mentions left_moves and move_left, make a version that takes an additional typeclass argument has_left_moves x, and use the indexing type as left_moves and the indexing function as move_left instead; the new version would be proved from the old using my range_eq_iff_forall_iff and range_eq_iff_exists_iff. This way, I think we can forget about left_moves and always directly work with the desired indexing function.

[Violeta Hernández]

I'm going to oppose this on grounds that it's just too clever

[Violeta Hernández]

I've worked with large and rapidly changing codebases before, and being too clever is what ultimately led to their downfall

[Violeta Hernández]

And really, I don't want to forget about the concrete types. They're a quirk of our design choices, sure, but they're quirks that make sense and are convenient within type theory, which is what we're working with.

[Junyan Xu]

Well, I'm just trying my best to address your original question about simp lemmas, but it seems you are not open enough to new ideas :( I think in mathlib we are not afraid of doing large refactors, not to mention that the current combinatorial game library is only an isolated small corner of mathlib.

As a rule of thumb, I think in the case of non-defeq indexing types, the indexing type and the indexing function should be bundled and rewritten together, and equality between set.range is the condition that allows you to rewrite between two such bundled functions.

My approach doesn't forget about "concrete types", instead it designate a preferred indexing type via typeclass resolution. In the case of ordinal.pgame, Iio is arguably the indexing type we want, but it lives in a higher universe, so we must complete the construction using o.out.α first and change the indexing type later. Once we have our desired indexing type and function and know it's equivalent to the original via set.range, I do think we can forget the original indexing type and the transition functions between the indexing types. After all combinatorial game theory talks about sets of left and right options, so if there's anything that depends on the particular indexing type, that doesn't belong to CGT and it would be nice if our API hides it.

[Violeta Hernández]

Don't get me wrong, I'm open to new ideas, but hiding implementation details via an ad-hoc typeclass just doesn't seem like a good one. Once again, the current approach achieves the same thing, and I argue that it achieves it more clearly and easily.

[Violeta Hernández]

And even if we went with your approach, I'm not sure how that answers the question about simp lemmas. We might need them less often, sure, but there's still the possibility.

[Violeta Hernández]

In fact, even if we went with your approach, why would using set.range be preferable to the equivalence approach? And if it isn't, and we went with the equivalence approach, surely the only thing we'd accomplish is hiding the equivalence behind a typeclass, which doesn't seem like a good idea?

[Junyan Xu]

set.range is convenient as there is a large amount of APIs around it, for example docs#function.surjective.range_comp allows you to reindex by the domain of a surjective function to the original indexing type; an equivalence is in particular surjective.

Notice that since I aim to forget the original indexing type, there is no way I can keep the equivalence (which I referred to more generally as the "transition function"), so it has to be forgotten as well. Of course, if you reindex using g ∘ f instead of g, then the transition function f is effectively still there. In the ordinal.to_pgame case however, we have another preferred indexing function h = to_pgame with domain Iio o, and after proving that h = g ∘ f, we indeed forget about f and g, which is good IMO.

[Violeta Hernández]

There is a lot of API around equivalences too

[Violeta Hernández]

Another grounds on which I disagree with this refactor is that in Lean, types and functions are simply much more convenient than sets, no matter how you put it. Rephrasing traditionally set-theoretic concepts in terms of types is something mathlib doesn't shy away from, and I don't think we should either unless there's a clear benefit.

[Junyan Xu]

Let me repeat: I never propose to throw away the indexing type anywhere above. Even in the quotient indexed_set.setoid approach which gives you a type of small sets (as opposed to proper classes), you still construct a small set from an indexing type/function. What I said is results in CGT should be independent of the indexing type/function, so you are free to change to any equivalent indexing type/function, and this post contains the essential APIs to work with the equivalence. set.range is just the simplest way (among the four equivalent ways) of stating the most general condition (more general than equivalences) for two indexing types/functions to be considered equivalent. Typeclass mechanism can be used to automatically come up with the preferred indexing type/function.

[Violeta Hernández]

I see, so your approach is strictly more general

[Violeta Hernández]

I don't think there's any current circumstance where we need to deduplicate moves, and I can't think of a possible scenario for this

[Junyan Xu]

The intention of my current proposal is not to deduplicate move or to define the identity relation on pgames (that would require a condition more general than equality of ranges, as some options may be identical but not equal), but merely to freely switch the original move indexing type/function to our preferred one.

I think in your original examples zero, one, and pow_half, where the desired indexing type/function is defeq to the original, my proposal isn't of much use and dsimp would be good enough; the ordinal.to_pgame example that you raised later is a situation my proposal is aimed at: we want to change to a indexing type that is not only not defeq to the original, but actually live in a higher universe.

In the meantime, I've come up with another situation where my proposal would be useful, namely (-x).left_moves, which is equal to x.right_moves but not defeq, which necessitates docs#pgame.to_left_moves_neg and 8 lemmas following it. If we make x.right_moves the default indexing type for (-x).left_moves, we should be able to reduce the number of lemmas and simplify the development. I think the same holds true for addition (docs#pgame.to_left_moves_add) and multiplication as well, and other cases of non-defeq-ness due to the use of well_founded.fix (feel free to add examples!).

[Violeta Hernández]

Ah, I can see the appeal now

[Violeta Hernández]

I think there's an alternate solution that's a bit easier, though

[Violeta Hernández]

We can do induction lemmas

[Violeta Hernández]

"if a proposition holds true for any left move of x, it holds for any right move of -x"

[Violeta Hernández]

I think this would achieve the same goal more easily

[Violeta Hernández]

@Scott Morrison @Junyan Xu I think impartial shouldn't be a typeclass

[Violeta Hernández]

#3974, which is where it was made into a typeclass, gives two justifications:

• it means you don't have to use lemmas like impartial_add all the time
• grundy_value doesn't have this annoying extra argument

[Violeta Hernández]

The second reasoning is now obsolete, since I removed the impartial argument from grundy_value a while back
docs#pgame.grundy_value

[Violeta Hernández]

Although the theorems need it, the definition itself doesn't

[Violeta Hernández]

The first argument seems like not a very compelling reason on its own

[Violeta Hernández]

The major con of this decision is that it goes against the general design style that typeclasses are meant for types, with rare exceptions

[Violeta Hernández]

And of course, there's the issues of using unfreezingI

[Violeta Hernández]

I wonder what Scott's reasoning for being against this was

[Violeta Hernández]

(deleted)

[Junyan Xu]

One advantage of making it an typeclass is that we can introduce instance like

instance impartial_mk (α : Type u) (f : α → pgame.{u}) [∀ a, impartial (f a)] :
  impartial (pgame.mk α α f f) := sorry

and for new impartial pgames you define, you can use @[derive impartial] to automatically generate the instance. I don't know how good Lean is at inferring instances like ∀ a, impartial (f a), though.
This is more suitable for the "actual" impartial games, requiring the left options to be the same as the right options. It's not so suitable for the current mathlib definition, because the G ≈ -G condition can be nontrivial to verify and is not a typeclass.

Similarly, we might introduce

instance dicotic_mk_nonempty (xl xr) [nonempty xl] [nonempty xr]
  (xL : xl → pgame) (xR : xr → pgame) [∀ i, dicotic (xL i)] [∀ i, dicotic (xR i)] :
  dicotic (mk xl xr xL xR) := sorry

instance dicotic_mk_empty (xl xr) [is_empty xl] [is_empty xr] (xL : xl → pgame) (xR : xr → pgame) :
  dicotic (mk xl xr xL xR) := sorry
/- relabelling of the zero game, not of much use; `zero_dicotic` plus the above should suffice. -/
/- basically the same as `dicotic_of_is_empty_moves`. -/

If Lean has trouble inferring the forall instances, we might introduce

instance dicotic_mk_const (xl xr xL xR) [nonempty xl] [nonempty xr] [dicotic xL] [dicotic xR] :
  dicotic (mk xl xr (λ _, xL) (λ _, xR)) := sorry

which covers the case where xl and xr are punit.

[Violeta Hernández]

I'm still not sure if this justifies the typeclass approach. Sure, it's more convenient in some ways, but we aren't making every definition into a typeclass and I'm interested in knowing why

[Junyan Xu]

The major con of this decision is that it goes against the general design style that typeclasses are meant for types, with rare exceptions

Indeed not many examples of typeclasses come to mind that are not for types; typeclasses in file#order/rel_classes, file#algebra/covariant_and_contravariant, core/init/algebra/classes are mostly not classes on types but maybe they're meant for some canonical operations/relations on types.

In this particular case, since pgames are constructed in a hierarchical way, I think it makes sense to introduce classes on elements of pgame: deriving a property of a pgame from similar properties of its constituents is akin to deriving structure on / property of a more complicated type constructed from a simpler type, from the structure on / property of the simpler type, like docs#witt_vector.comm_ring or docs#mv_polynomial.unique_factorization_monoid. When we can automate derivation of a structure/property simply by pattern matching, and if it will be used a lot, then I think it's worth being made a typeclass and declare the patterns as instances.

[Violeta Hernández]

Well in that case, it's probably worth making numeric into a typeclass too

[Violeta Hernández]

I wonder what the maintainers think

[Junyan Xu]

For numeric, the left_lt_right condition isn't usually trivial to check, and lt isn't a typeclass. Of course, if one of the left/right move set is empty, then the condition is vacuously true, and this case could be made an instance.

[Violeta Hernández]

But why a typeclass? We already have a theorem that does the same thing

[Violeta Hernández]

docs#pgame.numeric_of_is_empty_left_moves

[Violeta Hernández]

Also, I've been told that an alternate and simpler approach is to do the thing you suggested a while back, a tactic to solve numeric goals

[Violeta Hernández]

This does have a precedent in mathlib, with tactics like monotonicity and continuity

[Violeta Hernández]

That said, I still haven't gotten any specific reason against the typeclass pattern, other than various people finding it annoying and little use throughout mathlib

[Violeta Hernández]

@Bhavik Mehta just told me that the main reason is to avoid overuse of typeclass inference

[Violeta Hernández]

So now the question is, how do we make these numericity and impartiality and whatnot tactics?

[Bhavik Mehta]

Violeta Hernández said:

Bhavik Mehta just told me that the main reason is to avoid overuse of typeclass inference

At least, that's what I think the reason is - there could well be a better reason!

[Junyan Xu]

Instead of replacing typeclass, the coherence tactic instead introduced two typeclasses, so I doesn't seem to be a universal pattern to replace typeclasses by tactics. And after all, apply_instance is also a tactic and it solves goals if you set up the instances right.

A key difference between numeric/impartial/dicotic and continuity/measurability/monotonicity is that the latter are used widely across mathlib, so overusing typeclasses may cause performance issues, especially when there are many instances of the typeclasses. For the relatively secluded theory of combinatorial games, it seems need not worry much about performance issues. Here (as in the case of coherence) I consider typeclass inference just as a domain-specific way to automate by pattern matching. (I think the typeclasses for the coherence are more secluded and only used in the tactic though.)

[Violeta Hernández]

I'm on board with you, but I still want to hear a maintainer's opinion

[Junyan Xu]

Maybe let us hear from @Scott Morrison since he authored both the first coherence tactic #13125 and part of the game library.

[Anne Baanen]

In my experience, typeclasses work well if nearly all instances can be inferred using only a set of theorems of the form P1 (f x) → P2 (g y) → ... → Q x y ... z, where f x and g y are stated literally and don't do any computation, and there's never theorems P → P, or both P → Q and Q → P at the same time. As soon as you have to deal with equalities (your instance is on fx' and fx' = f x but not literally the same expression), or there is the possibility of looping, you're going to get a bad time.

[Anne Baanen]

In this case, if there is a nontrivial equality on pgame (i.e. two pgames can be definitionally or propositionally equal without literally being written the same), I suspect typeclasses can't keep up.

[Anne Baanen]

I actually suspect the inference speed is not a huge issue in this case, in my experience the real slowdown comes from checking definitional equality of instances in types that have instances that have types etc.

[Anne Baanen]

One approach you could consider is to define a tactic meta def impartial_tac := apply_instance and use this as a docs#auto_param: instead of [impartial p] you write (h : impartial p . impartial_tac) and you basically get the same semantics at the moment, and when instances don't scale you replace the code of impartial_tac with something smarter.

[Anne Baanen]

Drawback is that instance implicits like [impartial p] are much more common than auto_params so there's the possiblity that some tactics (or some parts of the elaborator) can't handle auto_param well.

[Anne Baanen]

Which is why you should first try using apply_instance as definition for the auto_param, then you can be sure that nothing breaks before you upgrade the tactic.

[Kevin Buzzard]

@Anne Baanen I really love the insights you give to this community :heart: Thank you.

[Violeta Hernández]

Do we have any consensus on keeping/refactoring impartial?

[Violeta Hernández]

It seems like the general consensus isn't a good design pattern even though it's slightly useful sometimes

[Violeta Hernández]

So, not really a strong argument either way

[Violeta Hernández]

There might be a sort of "death by a thousand cuts" argument against having it as a class

[Violeta Hernández]

Actually, let me list out pros and cons

Pros:

• theorems like impartial_add, impartial_neg, impartial_sub, impartial_zero can be omitted
• we might be able to derive the class in some common circumstances

Cons:

• we have resetI issues when we want to manipulate an impartial pre-game, like e.g. doing induction on it or unfolding the definition
• pre-game equality is really finicky and rarely definitional (due to the inductive definitions), so instances aren't super effective
• typeclasses seem to be somewhat of an antipattern in this situation (there's limited precedent)
• grundy_value no longer depends on the typeclass parameter, this was one of the original reasons for the typeclass
• a tactic could do both of the pros

[Violeta Hernández]

I'd also argue that the pros are barely anything to write home about. It's super simple to just call these theorems explicitly.

[Violeta Hernández]

So, even if there's not a strong argument either way, there seem to be much more weak arguments in favor of ditching the class

[Violeta Hernández]

Oh, and one last con: if we keep impartial as a class, then it stands to reason we should do the same for other definitions that are closed under basic operations, like numeric games, or small games, or dicotic games, so the cons scale up

[Eric Wieser]

I think we're missing some basic machinery mathlib-wide for propositions closed under operations

[Eric Wieser]

docs#submonoid_class and docs#is_submonoid come close, but neither seems to be used much for this type of thing

[Violeta Hernández]

As you may have noticed, I've been a bit busy tying up what I consider to be loose ends with the game API

[Violeta Hernández]

Nothing incredibly important, but still, a lot of things that are breaking changes

[Violeta Hernández]

Once I'm done with all that, I'll be free to clean up the multiplication proof and hopefully PR it

[Violeta Hernández]

Unrelated but what's up with docs#pgame.restricted?

[Violeta Hernández]

Might have asked before but I'm thinking about this again and I'm confused

[Violeta Hernández]

The description would be accurate if L and R were injective, but they aren't

[Violeta Hernández]

And I can't think of any natural examples of a game being a restriction of another, except for the case of relabellings

[Violeta Hernández]

So this really just seems like an auxiliary definition of sorts

[Violeta Hernández]

Maybe the idea was to define it in terms of injective functions and prove x <= y from that, but then someone realized you didn't need the injective hypothesis

[Violeta Hernández]

I don't think the definition is worthless, it's certainly an... interesting way to show an inequality. But maybe it should be renamed, and at the very least the docstring should be changed

[Violeta Hernández]

Another question, what's up with docs#pgame.equiv.has_coe?

[Violeta Hernández]

I don't think it's currently used anywhere

[Violeta Hernández]

Is there any precedent for using casts for proofs?

[Violeta Hernández]

I just had this idea that, in retrospect, is something @Junyan Xu had suggested

[Violeta Hernández]

We should make a comparison function for games, that outputs one of four outcomes

[Violeta Hernández]

Less, equivalent, greater, fuzzy

[Violeta Hernández]

There's a lot we could do with such a function

[Violeta Hernández]

Of particular interest to me are the fact this function can be lifted to games and surreals, and that its value is the same when you add a game to both sides

[Violeta Hernández]

By proving this, we could get a lot of lemmas currently either taking a lot of API space or missing, almost for free

[Violeta Hernández]

For instance, to prove cmp w x = cmp y z it suffices to prove w \le x \iff y \le z and x \le w \iff z \le y, which in many cases can be reduced to just the \le case by symmetry

[Violeta Hernández]

But that gives you r w x \iff r y z for \le and < and \equiv and \fuzzy for free which is super cool

[Violeta Hernández]

I'll prove some basic theorems about this comparison function

[Violeta Hernández]

I can't do a lot since I currently have like three sweeping changes on the same files PR'd

[Violeta Hernández]

Speaking of which, if so done could review my "comparison API review" and my refactor on relabellings that would be awesome

[Violeta Hernández]

Oh wow

[Violeta Hernández]

This new API on comparison is so overpowered I was able to comfortably prove pretty much every single variant of the covariant and contravariant theorems on pre-games without ever even appealing to the game structure

[Violeta Hernández]

It's extremely boilerplatey, but that's what peak performance looks like ;)

[Yaël Dillies]

Violeta Hernández said:

For instance, to prove cmp w x = cmp y z it suffices to prove w ≤ x ↔ y ≤ z and x ≤ w ↔ z ≤ y, which in many cases can be reduced to just the `≤ case by symmetry

Do you know about docs#lt_iff_lt_of_le_iff_le'?

[Junyan Xu]

Should we introduce fuzzy and lf for any preorder? And equiv (≈), which is already there if we use docs#antisymm_rel.setoid.

[Junyan Xu]

I think this cmp function can be defined on all preorders without trouble.

[Yaël Dillies]

docs#cmp is already a thing, but it has linear orders in mind.

[Violeta Hernández]

Yaël Dillies said:

Violeta Hernández said:

For instance, to prove cmp w x = cmp y z it suffices to prove w ≤ x ↔ y ≤ z and x ≤ w ↔ z ≤ y, which in many cases can be reduced to just the `≤ case by symmetry

Do you know about docs#lt_iff_lt_of_le_iff_le'?

Yep, these aren't quite the same lemmas though

[Yaël Dillies]

Sure, you also need docs#iff.not. But my point is that those two are enough.

[Violeta Hernández]

Junyan Xu said:

Should we introduce fuzzy and lf for any preorder? And equiv (≈), which is already there if we use docs#antisymm_rel.setoid.

We discussed this back when I introduced lf. Our conclusion was basically that yes, we could define this on all partial orders, but it wouldn't be very useful, since we couldn't think of any other example where the relation ¬ x ≤ yhad any particular importance.

[Violeta Hernández]

Further, if we just defined it in the obvious way, ¬ x ≤ y, we'd mess up the def-eqs on pre-games. We'd need to take the approach of lt, where it's defined as a field of the preorder class, and that just seems awkward.

[Violeta Hernández]

Not to mention, the name lf wouldn't make sense at all outside of games

[Violeta Hernández]

Yaël Dillies said:

Sure, you also need docs#iff.not. But my point is that those two are enough.

I'm talking about a partial order here though, not a linear order

[Violeta Hernández]

Now as for a general cmp function on preorders, we could totally do that

[Violeta Hernández]

We should have the fields lt, gt, equiv, and incomp

[Violeta Hernández]

We can even provide some API for converting between these values and those given by cmp on linear orders

[Yaël Dillies]

Who talked about linear orders? docs#lt_iff_lt_of_le_iff_le is for linear_orders, but docs#lt_iff_lt_of_le_iff_le' is for any preorder.

[Violeta Hernández]

Oh I see! I read the wrong theorem

[Violeta Hernández]

Yeah, what I basically did was prove this but for all the other relations on games

[Violeta Hernández]

Yeah I think that's the play here

[Violeta Hernández]

I'll add the comparison function on preorders, then use it to prove results about pre-games

[Violeta Hernández]

I think I just deciphered what docs#pgame.restricted really "means"

[Violeta Hernández]

And it's... disappointing

[Violeta Hernández]

Replacr the functions L and R and the hypotheses by existence lemmas

[Violeta Hernández]

And you literally just get a weaker version of the converse of docs#pgame.le_def

[Violeta Hernández]

So really, any inequality x \le y you can prove by building a restriction, can be proven by just using le_def

[Violeta Hernández]

I think that settles it, this needs to go

[Violeta Hernández]

I'm back!

[Violeta Hernández]

Junyan Xu said:

I've finished the proof of P1 with my symmetry approach at https://github.com/leanprover-community/mathlib/compare/surreal_mul_symm'?expand=1#diff-cfb19983c79209e00ac093e670e2db956ca48e00238011a5854479250cbaec67R318
I'll leave P2 and P4 to tomorrow.

I'll try and merge this with what we have.

[Violeta Hernández]

I hadn't noticed your comments on docs#pgame.quot_mul_comm and docs#pgame.quot_neg_mul, that seems like a nice thing to do on the side

[Violeta Hernández]

I want to try PR-ing the mul_option stuff, but #15252 is currerntly blocking that

[Violeta Hernández]

I think that's the last thing we would need before PRing the surreal multiplication proof

[Junyan Xu]

#15252 has a merge conflict now

[Violeta Hernández]

Ah true, it will conflict with my recent swapping of arguments on relabellings

[Violeta Hernández]

On that note, I've been thinking about relabellings again

[Violeta Hernández]

I think I might have brought this up before, but now I'm more convinced: we eventually need to ditch relabellings in favor of extensional equivalence

[Violeta Hernández]

Relabellings are just a consequence of our implementation of games, which doesn't coincide with the ZFC one

[Violeta Hernández]

The definition of extensional equivalence, e.g. being "identical" games, would be pretty much the same one as for docs#pSet.equiv: x ≡ y when every left move of x is extensionally equivalent to some left move of y, and viceversa, and likewise for right moves

[Violeta Hernández]

We could then define the quotient of pre-games by extensional equivalence, which would correspond to the actual ZFC notion of pre-games

[Violeta Hernández]

It's definitely a confusing situation, since we would have pgame which is an implementation detail, then some other type (igame?) for ZFC pre-games (which they don't call pre-games, they just call them games), and then actually game corresponding to ZFC pre-games quotiented by antisymmetry

[Violeta Hernández]

And surreals of course

[Violeta Hernández]

The nice thing about igame is that you can define left and right moves of igame as igames themselves, which is something you can't do with neither games nor surreals

[Violeta Hernández]

Which means we can define the birthday of an igame too

[Violeta Hernández]

And we can also correctly define short igames as an igame with a finite left and right move set, and prove that an igame is short iff it has finite birthday, a result that isn't true on pgame

[Violeta Hernández]

The philosophy here would be the same one as with docs#pSet vs docs#Set: we treat the former as an implementation detail, only proving the necessary results, and move everything to the latter

[Junyan Xu]

Violeta Hernández said:

I think I might have brought this up before, but now I'm more convinced: we eventually need to ditch relabellings in favor of extensional equivalence

docs#pSet.equiv is purely in terms of quantifiers, while docs#pgame.relabelling has the equivalences/functions that go between the left/right moves of two equivalent games. I remember you previously said it's useful to have those functions; if that's true we may consider keeping relabelling instead of ditching it, but maybe the lesson from docs#pSet tells us we don't really need those functions.

[Violeta Hernández]

I previously said that we use those functions. The single place where they're used is in the definition of short, which as I've mentioned previously doesn't match mathematical usage.

[Violeta Hernández]

We could still define identical games in terms of functions, i.e. explicit maps from left moves of x to identical left moves of y, and all the others, instead of just having the quantifiers

[Violeta Hernández]

This might still enable the VM to play short games, though I don't know if that's a priority

[Violeta Hernández]

In any case, it's clear to me that relabellings are a quirk of Lean's type theory, rather that something mathematicians would care much about.

[Violeta Hernández]

@Scott Morrison was the one who made the code for short so I'd like to hear his opinion.

[Violeta Hernández]

I'm wondering

[Violeta Hernández]

If #15289 is merged, lf will no longer have a weird inductive definition

[Violeta Hernández]

It will literally be defined as (≥)ᶜ

[Violeta Hernández]

So, in order to be able to use this smoothly on both pgame and game, maybe we should make ⧏ notation for (≥)ᶜ?

[Violeta Hernández]

I also suggested here that we could define more general notation ⋚ for "equal up to antisymmetry" and ∥ for incomparability

[Violeta Hernández]

So we wouldn't need specialized pgame.equiv and pgame.fuzzy predicates, nor their game counterparts, nor their igame counterparts if we ever do that

[Violeta Hernández]

Or you know what?

[Violeta Hernández]

Maybe we don't need lf anymore

[Violeta Hernández]

Which is probably somewhat of a hot take given the effort we put into making lf into what it is

[Violeta Hernández]

There was previously the argument that lf was useful because it provided a nice def-eq for le, but that no longer applies after the aforementioned refactor

[Violeta Hernández]

In fact, changing the def-eq barely broke anything

[Junyan Xu]

What's that nice def-eq? I think one reason for keeping lf is it makes statements like src#pgame.lf_of_le_of_lf look natural.

[Junyan Xu]

and it's everywhere in the literature

[Violeta Hernández]

The nice def-eqs in question are the ones given by docs#pgame.le_iff_forall_lf and docs#pgame.lf_iff_exists_le

[Violeta Hernández]

I guess they're not exactly def-eqs but they're really close

[Violeta Hernández]

It's true that lf makes some statements look more natural. But I don't think the statements translated into preorders are particularly unclear either. We could just prove not_le_of_le_of_not_le and now we don't need to prove it separately for pgame and game

[Violeta Hernández]

Again, there's also the option of just making lf a notation on an arbitrary preorder, and make aliases for the theorems we want to port

[Violeta Hernández]

Ultimately what I want is to prove as few results on preorders as possible. All that should be done elsewhere, and we should strive not to duplicate that in the game theory files.

[Violeta Hernández]

I wonder if we could have a whole file set_theory/game/lf.lean where we introduce the notation and all relevant aliases

[Violeta Hernández]

That way, if we want to use lf notation on pre-games, games, surreals, or any future quotient or subtype we come up with, we can just open that namespace/locale and get it

[Violeta Hernández]

I'm still not sure if we need the aliases though, maybe we can keep the notation but still use not_le or not_ge in theorem names?

[FR]

Maybe a bit outdated, can we still get any convenient computable constructing functions if we use extensional equivalence? I recently found it hard to define something like smallset Set → Set (smallset is quotient of indexed set which is used for pSet and pgame) without giving up computability.

[Yuyang Zhao]

Violeta Hernández said:

It's definitely a confusing situation, since we would have pgame which is an implementation detail, then some other type (igame?) for ZFC pre-games (which they don't call pre-games, they just call them games), and then actually game corresponding to ZFC pre-games quotiented by antisymmetry

I feel like we probably shouldn't call a docs#game a game. We can't really play a docs#game.

[Kevin Buzzard]

I think it's important to stick to the terminology in the mathematical literature.

[Yuyang Zhao]

So igames should just be called games. Then what should we call current docs#game (games quotiented by antisymmetry)?

[Kevin Buzzard]

Are you suggesting that docs#game is not what Conway calls a game? I am a bit confused.

[Kevin Buzzard]

On ONAG p76 (sorry, reading from my physical copy) Conway stresses the definition of two games being equal, uses the symbol = for it, and says "when we speak of the game 0, we mean to refer also to the games 1-1, *+* and so on".

[Yuyang Zhao]

Conway talks about the identity of games in the book, which implies that "games" actually contain more structure - we can't talk about the identity of games after quotient. But I admit it's also reasonable to call docs#game games, and equality is likely more important than identity.

[Trebor Huang]

Conway is just doing the usual mathematician thing and calling all three types "games".

[Violeta Hernández]

Kevin Buzzard said:

On ONAG p76 (sorry, reading from my physical copy) Conway stresses the definition of two games being equal, uses the symbol = for it, and says "when we speak of the game 0, we mean to refer also to the games 1-1, *+* and so on".

Conway does a very weird thing where he distinguishes between equality of games, and identity, which he takes as stronger. Of course, mathlib would not do things this way.

[Yuyang Zhao]

Violeta Hernández said:

I think I might have brought this up before, but now I'm more convinced: we eventually need to ditch relabellings in favor of extensional equivalence
Relabellings are just a consequence of our implementation of games, which doesn't coincide with the ZFC one

I'm trying to define real identical and remove relabelling. See #18515.

[Yuyang Zhao]

I removed all the relabelling except those about short. I am not sure how to change the definition of short appropriately so that it respects identity.

[Yuyang Zhao]

Maybe I should define igame first, then define short for igame.

[Violeta Hernández]

Yuyang Zhao said:

I removed all the relabelling except those about short. I am not sure how to change the definition of short appropriately so that it respects identity.

Short games should be those with a finite birthday

[Yuyang Zhao]

Yes, this definition can be used for pgame, but most of the properties of short games seem to need to be proved for igame.

[Junyan Xu]

Combinatorial game enthusiasts: CGSuite 2.0 was released with support for standard rulesets, loopy games, misère impartial games, and surreal numbers. May serve as inspiration to some extent for our implementation.

[Yuyang Zhao]

Because mathlib has been ported, #5901 is the PR for mathlib4.

[Timo Carlin-Burns]

The current definition of Relabelling is too restrictive compared to Identical, but was kept in #7162 for potential computational use cases (it is in Type _ not Prop). It's possible to define a Type _ which is compatible with Identical like this

inductive Relabelling : PGame.{u} → PGame.{u} → Type (u + 1)
  |
  mk {x y : PGame}
    (toFunL : x.LeftMoves → y.LeftMoves)
    (invFunL : y.LeftMoves → x.LeftMoves)
    (toFunR : x.RightMoves → y.RightMoves)
    (invFunR : y.RightMoves → x.RightMoves) :
      (∀ i, Relabelling (x.moveLeft i) (y.moveLeft (toFunL i))) →
      (∀ j, Relabelling (x.moveLeft (invFunL j)) (y.moveLeft j)) →
      (∀ i, Relabelling (x.moveRight i) (y.moveRight (toFunR i))) →
      (∀ j, Relabelling (x.moveRight (invFunR j)) (y.moveRight j)) → Relabelling x y

I have proven in a branch that with this definition, Identical x y \iff Nonempty (Relabelling x y).

I don't know what the computational use cases in mind for Relabelling are, but would this be a better definition for them? And would there be any benefit to redefining Identical x y as Nonempty (Relabelling x y) with this definition?

[Timo Carlin-Burns]

Ah this has been thought of already:

Violeta Hernández said:

We could still define identical games in terms of functions, i.e. explicit maps from left moves of x to identical left moves of y, and all the others, instead of just having the quantifiers

[Yuyang Zhao]

It is now mainly needed for file Mathlib.SetTheory.Game.State.

[Yuyang Zhao]

Timo Carlin-Burns said:

I don't know what the computational use cases in mind for Relabelling are, but would this be a better definition for them? And would there be any benefit to redefining Identical x y as Nonempty (Relabelling x y) with this definition?

They handle multiplicity differently. If docs#PSet.Equiv did what Relabelling does, then docs#ZFSet would be an analog of docs#Multiset instead of docs#Finset.

[Yuyang Zhao]

Ah sorry, I realized you were talking about your new definition.

[Yuyang Zhao]

That might be an option, but it would no longer preserve the current PGame.Short.

[Yuyang Zhao]

Of course, PGame.Short itself is likely to be removed...

[Timo Carlin-Burns]

I don't see any references to relabelling in the definition of Short, so we're just talking about whether x.Short -> Relabelling x y -> y.Short, right? If you want such a version of Short which is computational, you could always define it as the dependent product def RShort x := (y : PGame) \times y.Short \times Relabelling x y

[Yuyang Zhao]

Yes I'm talking about docs#SetTheory.PGame.shortOfRelabelling. I'm not sure what we should do with PGame.Short, I might remove the current definition.