7

我有以下引理，但证明不完整：

Lemma (s_is_plus_one : forall n:nat, S n = n + 1).
Proof.
  intros.
  reflexivity.
Qed.

这个证明失败了

Unable to unify "n + 1" with "S n".

这似乎eq_S是证明这一点的方法，但我不能应用它（它不能识别n + 1为S n: Error: Unable to find an instance for the variable y.）。我也试过ring了，但找不到关系。当我使用rewrite时，它只是减少到相同的最终目标。

我怎样才能完成这个证明？

4

1 回答 1

13

这与(+)定义的方式有关。您可以(+)通过关闭符号来访问 的基础定义（在 CoqIDE 中View > Display notations），看到符号(+)对应于函数Nat.add，然后调用Print Nat.add它为您提供：

Nat.add = 
fix add (n m : nat) {struct n} : nat :=
  match n with
  | O => m
  | S p => S (add p m)
  end

您可以看到它(+)是通过匹配它的第一个参数来定义的，其中 inn + 1是变量n。因为n不以Oor开头S（它不是“以构造函数为首的”），所以match不能减少。这意味着您将无法仅通过说这两个事物计算为相同的范式（这就是所reflexivity声称的）来证明相等性。

相反，您需要向 coq 解释为什么对于任何n等式都成立。在递归函数的情况下，一个经典的举动Nat.add是继续进行证明induction。它确实在这里完成了工作：

Lemma s_is_plus_one : forall n:nat, S n = n + 1.
Proof.
intros. induction n.
 - reflexivity.
 - simpl. rewrite <- IHn. reflexivity.
Qed.

你可以做的另一件事是注意1另一方面是构造函数为首的，这意味着如果只有你有1 + n而不是n + 1. 好吧，我们很幸运，因为在标准库中已经有人证明了它Nat.add是可交换的，所以我们可以使用它：

Lemma s_is_plus_one : forall n:nat, S n = n + 1.
Proof.
intros.
rewrite (Nat.add_comm n 1).
reflexivity.
Qed.

最后一种选择：使用，我们可以找到所有关于某个变量SearchAbout (?n + 1)模式的定理（问号在这里很重要）。第一个结果是真正相关的引理：?n + 1?n

Nat.add_1_r: forall n : nat, n + 1 = S n
于 2016-10-28T23:02:18.650 回答