the integer game

Stream: maths

[Kevin Buzzard]

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]

I think that's likely

[Mario Carneiro]

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

[Chris Hughes]

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]

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

[Kevin Buzzard]

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]

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]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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