Surreal numbers

Stream: Is there code for X?

[Bassem Safieldeen]

For fun, I am trying to formalize a piece of mathematical scripture from Donald Knuth's book, "Surreal Numbers":

/-
In the beginning, everything was void, and J. H. W. H Conway
began to create numbers. Conway said, "Let there be two rules
which bring forth all numbers large and small."
-/

/-
"This shall be the first rule: Every number corresponds to two
sets of previously created numbers, such that no member of the
left set is greater than or equal to any member of the right
set."
-/
structure number : Type :=
(left_set : set number)
(right_set : set number)
(H : ∀ xᵣ ∈ right_set, ¬ ∃ xₗ ∈ left_set, xₗ ≥ xᵣ)

/-
"And the second rule shall be this: One number is less than or
equal to another number if and only if no member of the first
number's left set is greater than or equal to the second number,
and no member of the second number's right set is less than or
equal to the first number."
-/
def leq (x : number) (y : number) : Prop :=
∀ xₗ ∈ x.left_set, ¬ (xₗ ≥ y) ∧ ∀ yᵣ ∈ y.right_set, ¬ (leq yᵣ x)

/-
And Conway examined these two rules he had created, and behold!
They were very good.
-/

/-
And the first number was created from the void right set and the
void left set. Conway called this number, "zero," and said it
shall be a sign to separate positive numbers from negative numbers.
-/
def zero : number := ⟨{},{},sorry⟩

/-
Conway proved that zero was less than or equal to zero, and he
saw that it was good. And the evening and the morning were the
day of zero.
-/
theorem zero_leq_zero : leq zero zero :=
begin
    sorry,
end

/-
On the next day, two more numbers were created, one with zero
as its left set and one with zero as its right set. And Conway
called the former number "one," and the latter he called
"minus one."
-/
def one       : number := ⟨{zero},{}⟩

def minus_one : number := ⟨{},{zero}⟩

/-
And he proved that minus one was less than but not
equal to zero and zero is less than but not equal to one.
-/
theorem minus_one_lt_zero : minus_one < zero := sorry

theorem zero_lt_one : zero < one := sorry

/-
And the evening ...
-/

There are clearly a lot of problems that I need to fix before this compiles. The most prominent problem I guess is that I can't use structure to define a type that I use in the structure definition. I tried to think about how to do it as an inductive type but I didn't get very far. Also, when I searched for Zulip threads containing "surreal numbers" I found this thread, but what was said about surreal numbers was a little over my head.

Any ideas? :)

[Johan Commelin]

Typo: he latter her called "minus one." .. her should be he.

[Johan Commelin]

inductive number : Type
| mk : Π (left_set : set number) (right_set : set number)
       (H : ∀ xᵣ ∈ right_set, ¬ ∃ xₗ ∈ left_set, xₗ ≥ xᵣ), number

doesn't compile, because it mentions inequality, but it is a step closer to your goal.

[Johan Commelin]

If you really want this literate coding style... not sure if you can pull it off

[Johan Commelin]

Maybe you can do something with mutual inductives... I've never used them before

[Bassem Safieldeen]

Johan Commelin said:

If you really want this literate coding style... not sure if you can pull it off

Style is not a priority; Different styles are ok.

[Bassem Safieldeen]

Johan Commelin said:

inductive number : Type
| mk : Π (left_set : set number) (right_set : set number)
       (H : ∀ xᵣ ∈ right_set, ¬ ∃ xₗ ∈ left_set, xₗ ≥ xᵣ), number

doesn't compile, because it mentions inequality, but it is a step closer to your goal.

This is helpful, thanks!

[Mario Carneiro]

That inductive structure is inconsistent

[Mario Carneiro]

you can't have an inductive with a constructor set T -> T, it violates cantor's theorem

[Mario Carneiro]

The resolution is not entirely obvious, and is developed in set_theory.surreal: src#pgame

[Mario Carneiro]

(Not sure why the link is broken, try https://github.com/leanprover-community/mathlib/blob/master/src/set_theory/pgame.lean#L116)

[Kevin Buzzard]

Conway himself admits in ONAG that he can envisage problems in formalising the definition within e.g. set theory, and implies that basically this is a good reason for ignoring set theory here because what he's doing clearly works, so if the framework doesn't accept it then the framework is wrong. We (Scott and Mario) got it working in Lean but it took some thought :-)

[Alex J. Best]

The link is probably broken as the 7 character shortening of the git hash to 69db7a3 is ambiguous, we have a commit 69db7a3f and 69db7a33 (most recent) now.

[Johan Commelin]

Does this mean that the repo is now officially "big"?

[Alex J. Best]

Yeah I can't tell if we were just unlucky here or if we should change doc-gen to use 8 or digits :confused:

[Kevin Buzzard]

If it's not completely trivial to change, one could just wait until it happens again? We might just be (un)"lucky" rather than big.

[Mario Carneiro]

doc-gen#92 just popped up, which looks related

[Alex J. Best]

Well it would be trivial to change 7 to 8 I think, but maybe better to modify https://github.com/leanprover-community/doc-gen/blob/9f9e8e8ae363877f05d72bce950b95e0b3693344/print_docs.py#L77 to call git rev-parse --short=7 blah to find the minimal truncation that works.

[Bryan Gin-ge Chen]

Hmm, that doesn't seem to work in this case (at least locally) since the other commit 69db7a3f isn't on a branch.