coq - 在 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 进行替换不起作用(!))可以通过其他策略实现自动化吗？然后我必须将定理“移植”回 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 ，顺便说一句，这是可判定的。摘自 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”