Zulip Chat Archive

Stream: maths

Topic: the integer game


view this post on Zulip 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 N2\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?

view this post on Zulip Mario Carneiro (Oct 25 2019 at 18:16):

I think that's likely

view this post on Zulip Mario Carneiro (Oct 25 2019 at 18:17):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Oct 25 2019 at 19:13):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Oct 25 2019 at 19:15):

Well, you did prove two + two = four by refl

view this post on Zulip Reid Barton (Oct 25 2019 at 19:15):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Oct 25 2019 at 19:17):

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

view this post on Zulip Mario Carneiro (Oct 25 2019 at 19:17):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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 N2\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 N2\mathbb{N}^2; the integers mod nn as a quotient of Z\mathbb{Z})? @Kevin Buzzard have you started writing anything down for the "integer game"? — I would be happy to be your guinea pig.

view this post on Zulip 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.

view this post on Zulip 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