integer multiplication well-defined

Stream: maths

[Kevin Buzzard]

On the plane to Pittsburgh I was idly thinking about "the integer game". If one defines the integers as being $\mathbb{N}^2/\sim$ with $\sim$ the usual equivalence relation, then everything goes pretty smoothly until you want to prove multiplication is well-defined, and then you end up with

i j k l m n p q : ℕ,
h1 : (i, j) ≈ (m, n),
h2 : (k, l) ≈ (p, q)
⊢ (i * k + j * l, i * l + k * j) ≈ (m * p + n * q, m * q + p * n)

which turns into this:

1 goal
i j k l m n p q : ℕ,
h2 : k + q = p + l,
h1 : i + n = m + j
⊢ i * k + j * l + (m * q + p * n) = m * p + n * q + (i * l + k * j)

which took me about 9 lines of calc :-/ (start by applying add_left_inj and then alternate lines of ring and rw hi). Am I right in thinking that there's no automation which will do this? There is probably a one-line "miracle proof" if you figure out some auxiliary ring theory equality. Modulo this, the proof that the integers are a ring comes out quite nicely.

[Kenny Lau]

maybe don't use equivalence relation

[Kenny Lau]

use quot and r (i,j) (i+1,j+1)

[Kevin Buzzard]

Here's what I did: https://gist.github.com/kbuzzard/e86eb3788caab340d5c40732de23d131

[Kevin Buzzard]

I want to make it look familiar to mathematicians. There will be a one-line proof of the stupid nat thing, just figure out why $ik+jl+mq+np-(mp+nq+il+kj)$ is in the ideal of $\mathbb{Z}[i,j,k,l,m,n,p,q]$ generated by the relations (i.e. write it explicitly as a linear combination), then tidy up to get rid of all negs, prove it by ring and then you're just a rewrite away.