Coq 证明策略

Question

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

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

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

Answer 1

正如 Vinz 的回答中指出的那样，您可以找到关于 plus 的双射性定理。直接在 Coq 标准库中。您也可以在 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利用其双射性。最后，可以应用归纳假设来完成证明。