Coq 证明策略答案

【问题标题】：Coq proof tacticsCoq 证明策略
【发布时间】：2015-11-16 14:50:01
【问题描述】：

我是 Coq 证明系统的初学者（大约 4 天）。我已经很努力了，但我无法证明以下内容。

forall a b c : nat, S (S (a + b)) = S (S (a + c)) -> b = c.

据我所知，我们需要证明 + 的双射性，这样我们才能以某种方式使用f(b) = f(c) -> b = c。我该怎么做？

【问题讨论】：

标签： coq coq-tactic

【解决方案1】：

正如 Vinz 的回答中所指出的，您可以直接在 Coq 标准库中找到关于 plus 的双射性定理。你也可以在a 上直接使用原始策略和数学归纳法来证明它，如下所示。

Theorem plus_l_bij: forall a b c : nat, a + b = a + c -> b = c.
Proof.
induction a as [|a'].
  intros b c H. apply H.
  intros b c H. simpl plus in H. inversion H. apply IHa' in H1. apply H1.
Qed.

在induction a 之后，基本情况a = 0 是微不足道的。

第二种情况的证明a = S a'，重新排列

S a' + b = S a' + c

到

S (a' + b) = S (a' + c)

然后使用其双射性删除构造函数S。最后，可以应用归纳假设来完成证明。

【讨论】：

【解决方案2】：

使用SearchAbout plus 或SearchPattern (_ + _ = _ + _ -> _)，您可以检查关于+ 的可用引理。但是如果你没有导入正确的模块，那可能就没用了。我通常做的是去看在线文档。 Here is the documentation for plus，您可以特别关注plus_reg_l 和plus_reg_r。

【讨论】：