# Zulip Chat Archive

## Stream: maths

### Topic: Multiplication on int is well-defined

#### Kevin Buzzard (Jun 28 2020 at 14:57):

In other words,

```
example (p q r s t u v w : ℕ) (h1 : p + u = q + t) (h2 : r + w = s + v) :
p * r + q * s + (t * w + u * v) = p * s + q * r + (t * v + u * w) :=
begin
have h3 : (p + u) * r = (q + t) * r,
rw h1,
rw [add_mul, add_mul] at h3,
apply @nat.add_left_cancel (u * r),
rw [show u * r + (p * r + q * s + (t * w + u * v)) = p * r + u * r + q * s + t * w + u * v, by ring],
rw h3,
rw [show q * r + t * r + q * s + t * w + u * v = t * (r + w) + q * s + u * v + q * r, by ring],
rw [show u * r + (p * s + q * r + (t * v + u * w)) = u * (r + w) + p * s + t * v + q * r, by ring],
rw [h2, mul_add, mul_add],
rw [show t * s + t * v + q * s + u * v + q * r = t * s + q * s + t * v + u * v + q * r, by ring],
--uv cancels tv cancels qr cancels
suffices : t * s + q * s = (p + u) * s,
rw this, ring,
rw h1,
ring,
end
```

Are there better techniques for this? Note that this is all nat hell.

#### Kevin Buzzard (Jun 28 2020 at 14:57):

This is what you get when you try to define multiplication on the quotient.

#### Mario Carneiro (Jun 28 2020 at 15:24):

Here's the most organized proof I can make based on your script:

```
example (p q r s t u v w : ℕ) (h1 : p + u = q + t) (h2 : r + w = s + v) :
p * r + q * s + (t * w + u * v) = p * s + q * r + (t * v + u * w) :=
nat.add_left_cancel $ calc
u * r + (p * r + q * s + (t * w + u * v))
= t * w + (p + u) * r + q * s + u * v : by ring
... = t * (s + v) + q * r + q * s + u * v : by rw [h1, ← h2]; ring
... = u * v + (q + t) * s + q * r + t * v : by ring
... = u * (r + w) + p * s + q * r + t * v : by rw [← h1, h2]; ring
... = u * r + (p * s + q * r + (t * v + u * w)) : by ring
```

#### Kevin Buzzard (Jun 28 2020 at 16:30):

Where is my automation? Is this hard?

#### Kevin Buzzard (Jun 28 2020 at 16:30):

Aah -- it suffices to prove it for all the variables in`int`

, and `ring`

can do that

#### Mario Carneiro (Jun 28 2020 at 16:52):

Of course you can also coerce everything to `int`

and then this is easy by `ring`

but I'm assuming you don't have that

#### Mario Carneiro (Jun 28 2020 at 16:53):

The general automation for things like this is the `ring_rw`

/ `groebner`

tactics we've been talking about

#### Bryan Gin-ge Chen (Jun 28 2020 at 16:58):

Mario Carneiro said:

Of course you can also coerce everything to

`int`

and then this is easy by`ring`

but I'm assuming you don't have that

`zify at *`

coerces everything to `int`

s, but it doesn't seem to help much in this case.

#### Karl Palmskog (Jun 28 2020 at 17:00):

just wanted to check if the Lean community is aware of Coq's ongoing modernization of Micromega (`lia`

, `nia`

, etc., tactics)? For example, `lia`

in Coq 8.11 directly solves the above goal. (`Finished transaction in 0.042 secs (0.034u,0.s) (successful)`

)

#### Bryan Gin-ge Chen (Jun 28 2020 at 17:03):

Oh, `nlinarith`

solves it too! (but it's kind of slow: `elaboration: tactic execution took 1.78s`

.)

#### Kevin Buzzard (Jun 28 2020 at 18:33):

What sorcery is this?

#### Kenny Lau (Jun 28 2020 at 18:35):

so why is Coq so much faster?

#### Bhavik Mehta (Jun 28 2020 at 18:36):

Does the `lia`

proof in Coq solve it over `int`

or `nat`

? Looking at that link, it seems that `lia`

uses arithmetic over `int`

, so it's not exactly the same problem as this one

#### Heather Macbeth (Jun 28 2020 at 18:36):

@Kenny Lau , @Rob Lewis has been working on this for weeks.

#### Karl Palmskog (Jun 28 2020 at 18:43):

`lia`

transforms goals with `nat`

, `Z`

, etc., to an abstract internal representation. The Coq `zify`

tactic is modular and allows one to inject types that map into `Z`

/`nat`

using type classes, which allows `lia`

to solve goals on them. For example, this has been done for MathComp's `nat`

/`int`

, which are subtly different from those in the Coq stdlib: https://github.com/pi8027/mczify

#### Karl Palmskog (Jun 28 2020 at 18:45):

for completeness, there is also some other more general automation in Coq for similar more abstract problems: https://github.com/coq-community/aac-tactics https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrAC.v https://github.com/coq-community/atbr (we also have two flavors of Gröbner bases https://github.com/coq-community/buchberger https://github.com/thery/grobner)

#### Rob Lewis (Jun 29 2020 at 11:21):

I'm surprised that `lia`

solves this, since it doesn't look linear! `omega`

is the closest Lean equivalent to `lia`

, but it has a bunch of bugs and its implementer doesn't seem interested in fixing them. One of the bugs is relevant here, it doesn't atomize multiplication of variables properly. I don't know if this is in scope for `omega`

even if this bug were fixed, since I don't immediately see the linear problem it should pick up.

#### Rob Lewis (Jun 29 2020 at 11:22):

I'm also surprised by why `nlinarith`

is so slow on this. It's spending over half its time... checking whether variables are defeq, even though it's only unfolding `reducible`

definitions.

#### Karl Palmskog (Jun 29 2020 at 12:35):

for completeness, this was on Coq 8.11.2:

```
Require Import Lia.
Lemma example (p q r s t u v w : nat) (h1 : p + u = q + t) (h2 : r + w = s + v) :
p * r + q * s + (t * w + u * v) = p * s + q * r + (t * v + u * w).
Proof.
Time lia.
Qed.
```

Also perhaps of interest that Coq's `omega`

is going to be deprecated in 8.12.0 in favor of `lia`

.

#### Rob Lewis (Jun 29 2020 at 12:40):

Oh, yeah, I'm not saying I don't believe that `lia`

solved it :) I tried it myself. But it means my idea of what `lia`

does must be wrong.

#### Karl Palmskog (Jun 29 2020 at 13:50):

@Rob Lewis if you have any questions about the functionality/limitations of `lia`

, you should reach out to Frédéric Besson via email (his preferred contact method from when I asked). He is the main implementer and from what I can tell drives the effort of improving `lia`

/`zify`

/etc.

Last updated: May 14 2021 at 20:13 UTC