CODEWITHSUNDEEP
coq
larsr
larsr

Reputation: 5811

Solving polynomial equation systems in Coq

I ended up with the following goal, which disappointingly wasn't solved by neither the tactics in Psatz nor Omega.

Require Import Psatz Omega.
Goal forall n n0 n1 n2 n3 n4 n5 n6,
       n5 + n4 = n6 + n3 ->
       n1 + n0 = n2 + n ->
       n5 * n1 + n6 * n2 + n3 * n0 + n * n4 =
       n5 * n2 + n1 * n6 + n3 * n + n0 * n4.
intros.
Fail lia.
Fail omega.

Lazy as I am, I tested all combination of values up to 30, and it matched in all instances, so I think the goal is valid.

Is there some other way to solve this goal (preferably as automatically as possible)?

Also, when will omega and lia fail (for valid equation systems)? I noticed to my surprise that omega didn't even solve a*b = b*a.

EDIT:

It is possible to solve it with the lia tactic for Z integers after doing some manual substitutions. (Doing the substitutions for nat does not work (!)) Can that be automated by some other tactic? And then I have to "port" the theorem back to nat... How would I do that?

Require Import ZArith.
Open Scope Z.
Lemma help:
  forall n n0 n1 n2 n3 n4 n5 n6,
    n >= 0 -> n0 >= 0 -> n1 >= 0 ->
    n2 >= 0 -> n3 >= 0 -> n4 >= 0 ->
    n5 >= 0 -> n6 >= 0 ->

    n5 + n4 = n6 + n3 ->
    n1 + n0 = n2 + n ->
    n5 * n1 + n6 * n2 + n3 * n0 + n * n4 =
    n5 * n2 + n1 * n6 + n3 * n + n0 * n4.

  intros.
  Fail lia.
  assert (n5 = n6 + n3 - n4) by lia; subst n5.
  assert (n1 = n2 + n  - n0) by lia; subst n1.
  Fail omega.
  lia.
Qed.
Close Scope Z.

Upvotes: 4

Views: 452

Answers (2)

ejgallego
ejgallego

Reputation: 6852

For this kind of "prototyping", using external SMT solvers in addition to Coq's procedures may also be a good idea.

A mature choice is the why3 tactic (note: you'll need why3 head to work with Coq 8.5), but other options are possible such as this

Upvotes: 1

Anton Trunov
Anton Trunov

Reputation: 15424

In your case nia will solve the goal. A quote from the Coq reference manual:

nia is an incomplete proof procedure for integer non-linear arithmetic (see Section 22.6)

And since the equations are not linear, this will work (even in nat_scope):

Goal forall n n0 n1 n2 n3 n4 n5 n6,
       n5 + n4 = n6 + n3 ->
       n1 + n0 = n2 + n ->
       n5 * n1 + n6 * n2 + n3 * n0 + n * n4 =
       n5 * n2 + n1 * n6 + n3 * n + n0 * n4.
intros.
nia.
Qed.

As for the omega part of the question:

... omega didn't even solve a*b = b*a

omega is based on Presburger arithmetic, which is, by the way, decidable. An excerpt from the Coq manual:

Multiplication is handled by omega but only goals where at least one of the two multiplicands of products is a constant are solvable. This is the restriction meant by “Presburger arithmetic”

Upvotes: 3

Related Questions