## 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 [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 [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) :=
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 inint, 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 ints, 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