# Zulip Chat Archive

## Stream: maths

### Topic: the integer game

#### Kevin Buzzard (Oct 25 2019 at 17:51):

One of the things that really surprised me about core Lean two years ago was that the integers were defined in this really mathematically ugly way, as the disjoint union of two copies of the naturals. As any mathematician knows, the integers are actually defined to be the equivalence classes of an equivalence relation on $\mathbb{N}^2$. I probably asked this two years ago but was in no position to understand the response, so I'm asking again now: why are the integers defined in this way? If I never want to compute with an actual integer, but just want to prove theorems about them (e.g. that they're a ring), then am I actually better off defining them as equivalence classes?

#### Mario Carneiro (Oct 25 2019 at 18:16):

I think that's likely

#### Mario Carneiro (Oct 25 2019 at 18:17):

As you've identified, the reason this is done is for computation

#### Chris Hughes (Oct 25 2019 at 19:11):

But natural numbers are disastrous computationally in the kernel, and integers are just GMP integers in the VM, ignoring the inductive def, so I still don't really get this.

#### Reid Barton (Oct 25 2019 at 19:13):

It still has the advantage that, for example, 2 - 1 is defeq to 1

#### Kevin Buzzard (Oct 25 2019 at 19:13):

I'm thinking about the sequel to the natural number game and I'm wondering if I'd be better off just going straight for the equivalence relation approach. I'm looking for potential disadvantages. It would be the same sort of thing -- just take a bunch of typeclasses which int has and try and prove them for myint from first principles.

#### Kevin Buzzard (Oct 25 2019 at 19:14):

I don't care about defeq. Mathematicians don't understand this and I actively encourage them to `rw add_zero`

in the natural number game

#### Reid Barton (Oct 25 2019 at 19:15):

Well, you did prove `two + two = four`

by `refl`

#### Reid Barton (Oct 25 2019 at 19:15):

but I agree it's not that compelling a reason for the purpose of integer game

#### Mario Carneiro (Oct 25 2019 at 19:17):

I think the integer game with a quotient construction should be about as hard as the complex number game

#### Reid Barton (Oct 25 2019 at 19:17):

It also has the advantage that it introduces the quotient game mechanic

#### Mario Carneiro (Oct 25 2019 at 19:17):

you get less defeq, but that's more representative of higher math anyway

#### Kevin Buzzard (Oct 25 2019 at 20:05):

I prove 2+2=4 by refl in the article, but this is not done in the natural number game itself; no number higher than 1 appears in the natural number game and I tell them that to prove their first theorems about `1`

they must `rw one_eq_succ_zero`

. I did not want to get bogged down with the difference between definitional equality and equality-because-of-a-theorem.

#### Kevin Buzzard (Oct 25 2019 at 20:07):

It also has the advantage that it introduces the quotient game mechanic

Right. The natural number game introduces induction, and the integer game could introduce the universal property of quotients early on. I don't actually know how much one would have to use it to prove theorems, I'm a bit unclear about how the proofs look if you do it with quotients; I've only looked at core Lean and there everything is just a + / - case split because of the definition.

#### Mario Carneiro (Oct 25 2019 at 21:03):

Actually, most of the proofs about integer properties go via the quotient indirectly (or at least it did, while `transfer`

was still in core; we may have reverted to the old proof)

#### Luis O'Shea (Nov 10 2019 at 17:15):

One of the things that really surprised me about core Lean two years ago was that the integers were defined in this really mathematically ugly way, as the disjoint union of two copies of the naturals. As any mathematician knows, the integers are actually defined to be the equivalence classes of an equivalence relation on $\mathbb{N}^2$.

In learning Lean I wanted to experiment with quotients. I looked up the definition of the integers, and, like @Kevin Buzzard, was a little surprised by the official definition. I also read his post Maths in Lean : quotients and equivalence classes.

Are there any resources where simple examples of quotients are explored? The two examples that KB mentions in his post seem ideal to me (the integers as a quotient of $\mathbb{N}^2$; the integers mod $n$ as a quotient of $\mathbb{Z}$)? @Kevin Buzzard have you started writing anything down for the "integer game"? — I would be happy to be your guinea pig.

#### Kevin Buzzard (Nov 10 2019 at 17:17):

I've spent many hours this weekend working on the natural number game, I don't really have time to think about the integer game at the minute. But I did once write this: https://github.com/leanprover-community/mathlib/blob/master/docs/tutorial/Zmod37.lean which might help beginners to see how Lean uses quotients in practice.

#### Luis O'Shea (Nov 10 2019 at 17:19):

Thanks! That seems to the kind of resource I was looking for.

Last updated: May 14 2021 at 19:21 UTC