Stream: Is there code for X?

Topic: Surreal numbers

Bassem Safieldeen (Oct 27 2020 at 13:36):

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 (Oct 27 2020 at 13:46):

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

Johan Commelin (Oct 27 2020 at 13:49):

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 (Oct 27 2020 at 13:50):

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

Johan Commelin (Oct 27 2020 at 13:51):

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

Bassem Safieldeen (Oct 27 2020 at 13:52):

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 (Oct 27 2020 at 13:53):

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.

Mario Carneiro (Oct 27 2020 at 14:15):

That inductive structure is inconsistent

Mario Carneiro (Oct 27 2020 at 14:15):

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

Mario Carneiro (Oct 27 2020 at 14:17):

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

Mario Carneiro (Oct 27 2020 at 14:18):

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

Kevin Buzzard (Oct 27 2020 at 14:29):

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 (Oct 27 2020 at 14:36):

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 (Oct 27 2020 at 14:37):

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

Alex J. Best (Oct 27 2020 at 14:43):

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 (Oct 27 2020 at 14:49):

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 (Oct 27 2020 at 14:51):

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

Alex J. Best (Oct 27 2020 at 15:00):

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 (Oct 27 2020 at 15:28):

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

Last updated: May 07 2021 at 19:12 UTC