Zulip Chat Archive

Stream: maths

Topic: Multiplication on int is well-defined


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 28 2020 at 14:57):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 28 2020 at 16:30):

Where is my automation? Is this hard?

view this post on Zulip Kevin Buzzard (Jun 28 2020 at 16:30):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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))

view this post on Zulip 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.)

view this post on Zulip Kevin Buzzard (Jun 28 2020 at 18:33):

What sorcery is this?

view this post on Zulip Kenny Lau (Jun 28 2020 at 18:35):

so why is Coq so much faster?

view this post on Zulip 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

view this post on Zulip Heather Macbeth (Jun 28 2020 at 18:36):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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