integer multiplication and nlinarith

Stream: maths

[Kevin Buzzard]

At Imperial the students have just been learning about the definition of integers as $\mathbb{N}^2$ modulo the equivalence relation $(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]

I'm guessing what's happening is effectively turning everything into statements about $\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]

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]

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

[Rob Lewis]

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

[Rob Lewis]

Same for omega I believe.

[Kevin Lacker]

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]

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]

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

[Mario Carneiro]

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

[Floris van Doorn]

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]

@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]

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]

:-) 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]

okay, i literally laughed out loud

[Kevin Buzzard]

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]

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]

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 $\geq0$ and one constructor for $\leq -1$ somehow implicitly announces that the centre of symmetry of the integers is at the point $-0.5$. With the definition of $\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 $n\mapsto g^n$ being a group homomorphism $(\mathbb{Z},+)\to G$ makes me die a little inside; my conclusion really is that I just shouldn't be looking. With the $\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]

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

[Mario Carneiro]

By the way, there is actually a really nice way to see $n\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 $\mathbb{Z}$ as a subset of $\mathbb{Z}_2$, the 2-adic numbers, and mapping $x\mapsto 1-x$ on every digit yields the function $-n-1$.

[Johan Commelin]

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

• First define $\mathbb{N}$ (Peano style)
• Then teach them modular arithmatic: $\mathbb{N}/n\mathbb{N}$
• Time for projective limits! We can now build $\lim_n (\mathbb{N}/2^n\mathbb{N})$, and call this (??) $\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 $\mathbb{Z}$.

Let's go for it!

[Mario Carneiro]

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!”