Zulip Chat Archive

Stream: maths

Topic: integer multiplication and nlinarith


Kevin Buzzard (Oct 30 2020 at 14:58):

At Imperial the students have just been learning about the definition of integers as N2\mathbb{N}^2 modulo the equivalence relation (i,j)(k,l)    i+l=k+j(i,j)\sim(k,l)\iff i+l=k+j. This is after the naturals have all been set up from first principles from Peano's axioms. It was claimed (not by me!) that the standard axioms of a commutative ring could be proved "easily" for the integers and everything was left as an exercise :D

So I did this exercise in Lean, and by far the hardest thing, at least for me, was to prove that multiplication was well-defined, i.e. descends to the quotient. When the dust clears, the problem is the following (thank you extract_goal :-) )

example (i j k l m n p q : )
  (h₁ : i + n = m + j)
  (h₂ : k + q = p + l) :
  i * k + j * l + (m * q + n * p) = m * p + n * q + (i * l + j * k) :=
begin
  admit,
end

omega doesn't work because the goal involves multiplication, and because we don't have Groebner bases I just rolled my eyes, added some carefully-chosen thing to both sides and did a big calc proof. I labelled this as "boss level" :-) and students (from Imperial and elsewhere) have been working on it (and rather easier stuff!) this afternoon on the discord.

@Shing Tak Lam tried hint, and hint pointed out that nlinarith solves the goal!

I was surprised. What the heck is nlinarith doing here? This goal seems to me to be a tricky goal about naturals, out of scope for omega. Kudos to @Rob Lewis for this!

Reid Barton (Oct 30 2020 at 15:05):

I'm guessing what's happening is effectively turning everything into statements about Z\mathbb{Z}, solving h_1 and h_2 for i and k and plugging them in, and finishing with ring. Note that the first statement uses the fact that we already know the original statement you were trying to prove.

Rob Lewis (Oct 30 2020 at 15:38):

nlinarith is roughly linarith plus "squares and products of nonnegative things are nonnegative." You can set_option trace.linarith true to see the linear problem it ends up solving. I don't know exactly what proof it finds, but it isn't solving h1 and h2 as a preprocessing step.

Rob Lewis (Oct 30 2020 at 15:39):

But as Reid points out this is definitely circular in one way or another.

Rob Lewis (Oct 30 2020 at 15:39):

You can't use linarith to define the integers because it immediately casts nats to ints.

Rob Lewis (Oct 30 2020 at 15:40):

Same for omega I believe.

Kevin Lacker (Oct 30 2020 at 15:45):

what a weird way to define the integers. I guess this is natural if you consider set products and equivalence relations to be a more basic thing than integers?

Bryan Gin-ge Chen (Oct 30 2020 at 15:50):

This is the definition I was taught when I was first learning that things like the integers needed to be formally defined. The idea of the construction here also generalizes well to turning other commutative monoids into abelian groups.

Kevin Lacker (Oct 30 2020 at 16:09):

interesting. i would have guessed people would do it like, for every positive number x you have both +x and -x

Mario Carneiro (Oct 30 2020 at 18:10):

this is uglier to get right; I mean, what about 0?

Floris van Doorn (Oct 30 2020 at 18:37):

I remember doing this back in Lean 0.1: https://github.com/leanprover/lean2/blob/148d475421d4512df3015758275def59238458ad/library/standard/data/int/basic.lean#L631-L633
Lean was... less convenient to use back then.

Kevin Buzzard (Oct 30 2020 at 21:01):

@Kevin Lacker today I finished teaching a 4 week intensive introduction to university mathematics to the 1st years at my university. Part 1 of the course (my part) involves defining sets, functions and equivalence relations, and we don't mention the integers at all! I prove things like composite of injective functions is injective and equivalence relations = partitions etc. Part 2 starts with the natural numbers defined by Peano's axioms and then uses the tools I've developed to define the integers and rationals as equivalence classes.

Kevin Lacker (Oct 30 2020 at 22:02):

recently I taught my 7-year-old about negative numbers. I did not use the strategy of, first define injective functions and equivalence relations

Kevin Buzzard (Oct 30 2020 at 22:05):

:-) I taught my 4 year old nephew about negative numbers; we started with the "what's the number before this one?" game, and then when we got stuck at 0 we moved onto localisation of monoids.

Kevin Lacker (Oct 30 2020 at 22:10):

okay, i literally laughed out loud

Kevin Buzzard (Oct 30 2020 at 22:11):

OK so I am bending the truth a little. But it was a productive session! At the end I told him to go and ask his mother what the number before negative 9 was. She got it wrong :D

Bryan Gin-ge Chen (Oct 30 2020 at 22:26):

I really enjoyed the blog post that Kevin wrote about it: https://xenaproject.wordpress.com/2020/06/27/teaching-dependent-type-theory-to-4-year-olds-via-mathematics/

Kevin Buzzard (Oct 30 2020 at 22:51):

There really is something which annoys me about Lean's definition of int, as a mathematician. I am in no position to say anything about implementation issues, and perhaps the definition is a stroke of genius, but having one constructor for 0\geq0 and one constructor for 1\leq -1 somehow implicitly announces that the centre of symmetry of the integers is at the point 0.5-0.5. With the definition of N2/\mathbb{N}^2/\sim one can see the symmetry at 0. What I have learnt from many conversations here is that I really should not worry about the actual definition, because if I want a certain structure on the integers I can simply make it myself. Looking at the mathlib proofs of things like ngnn\mapsto g^n being a group homomorphism (Z,+)G(\mathbb{Z},+)\to G makes me die a little inside; my conclusion really is that I just shouldn't be looking. With the N2\mathbb{N}^2 definition this comes out really naturally. From a type-theoretic perspective perhaps the opposite is true -- why use some zany quotient type when it's just a simple inductive type with two constructors?

Kevin Buzzard (Oct 30 2020 at 22:51):

Perhaps as a mathematician I am just constantly on the look out for symmetry? shrug

Mario Carneiro (Oct 31 2020 at 05:04):

By the way, there is actually a really nice way to see nn1n\mapsto-n-1 as a symmetry: it's the same as bitwise NOT in two's complement arithmetic (but on an infinite bit width). Put another way, I think you can take Z\mathbb{Z} as a subset of Z2\mathbb{Z}_2, the 2-adic numbers, and mapping x1xx\mapsto 1-x on every digit yields the function n1-n-1.

Johan Commelin (Oct 31 2020 at 05:12):

Right, so we should set up our maths curriculum in a different way:

  • First define N\mathbb{N} (Peano style)
  • Then teach them modular arithmatic: N/nN\mathbb{N}/n\mathbb{N}
  • Time for projective limits! We can now build limn(N/2nN)\lim_n (\mathbb{N}/2^n\mathbb{N}), and call this (??) N2\mathbb{N}_2
  • After some careful study, we see that there is a really interesting subring, obtained by the invariants under some natural involution.
  • Call this subring Z\mathbb{Z}.

Let's go for it!

Mario Carneiro (Oct 31 2020 at 05:19):

This approach also matches the modular reasoning of this kid:

John Cremona said:

I tried out the “what comes before” game with my 5-year old granddaughter, starting with 6 (“how old will you be on your next birthday?”). No hesitation at all right down to “what comes before 1?” “Zero!” and then to “what comes before zero?” she said “One hundred!” instantaneously. I asked her why and she said something like “the numbers are in a circle so it has to be the biggest number in the whole world!”


Last updated: Dec 20 2023 at 11:08 UTC