Coq 无法统一——如何改变假设？

Question

这里是 Coq 初学者。

我有以下愚蠢的定理：

  Theorem plus_same : forall a b c : nat,
      a+b=a+c -> b=c.
  Proof. Admitted.

  Theorem advanced_commutivity:
    forall x y z w : nat, x + y + (z+w) = x + z + (y + w).
  Proof.
    intros x y z w.
    apply (plus_same x (y + (z+w)) (z + (y + w))).

但是，当我尝试运行 apply 行时，出现错误：

Unable to unify "y + (z + w) = z + (y + w)" with
 "x + y + (z + w) = x + z + (y + w)".

我需要在这里改变我的假设吗？如何将此处的 plus_same 应用于 advanced_commutivity 证明中的论点？

Answer 1

您误读了您的目标：x + y + (z + w)代表(x + y) + (z + w)，因为+注册为left-associative，与x + (y + (z + w))不同。

所以为了应用你的引理，你应该首先通过用另一个 Lemma plus_assoc : forall x y z, x + y + z = x + (y + z).

重写来重新关联你的 +

Coq 无法统一——如何改变假设？

Coq unable to unify -- how to change hypothesis?

coq

coq-tactic