在 Coq 中求解多项式方程组

Question

我最终实现了以下目标，令人失望的是，Psatz 和 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.

虽然我很懒，但我测试了最多 30 个值的所有组合，并且它在所有情况下都匹配，所以我认为目标是有效的。

是否有其他方法可以解决这个目标（最好尽可能自动）？

此外，omega 和 lia 何时会失败（对于有效的方程系统）？我惊讶地发现 omega 甚至没有解决 a*b = b*a.

编辑：

在进行一些手动替换后，可以使用 Z 整数的 lia 策略来解决它。（对 nat 进行替换是行不通的（！））这可以通过其他策略自动化吗？然后我必须 "port" 将定理返回到 nat...我该怎么做？

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.

Answer 1

在你的情况下 nia 将解决目标。引自 Coq 参考 manual:

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

并且由于方程不是线性的，这将起作用（即使在 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.

至于问题的omega部分：

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

omega 基于 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”

Answer 2

对于这种 "prototyping"，除了 Coq 的程序外，使用外部 SMT 求解器可能也是一个好主意。

成熟的选择是why3 tactic (note: you'll need why3 head to work with Coq 8.5), but other options are possible such as this

在 Coq 中求解多项式方程组

Solving polynomial equation systems in Coq

coq