Multiplication on int is well-defined

Stream: maths

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

Where is my automation? Is this hard?

[Kevin Buzzard]

Aah -- it suffices to prove it for all the variables inint, and ring can do that

[Mario Carneiro]

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]

The general automation for things like this is the ring_rw / groebner tactics we've been talking about

[Bryan Gin-ge Chen]

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]

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]

Oh, nlinarith solves it too! (but it's kind of slow: elaboration: tactic execution took 1.78s.)

[Kevin Buzzard]

What sorcery is this?

[Kenny Lau]

so why is Coq so much faster?

[Bhavik Mehta]

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]

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

[Karl Palmskog]

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]

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]

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]

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]

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]

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]

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