Coq 证明策略

Posted

技术标签:

【中文标题】Coq 证明策略【英文标题】:Coq proof tactics 【发布时间】: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。我该怎么做?

【问题讨论】:

【参考方案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 plusSearchPattern (_ + _ = _ + _ -> _),您可以检查关于+ 的可用引理。但是如果你没有导入正确的模块,那可能就没用了。我通常做的是去看在线文档。 Here is the documentation for plus,您可以特别关注plus_reg_lplus_reg_r

【讨论】:

以上是关于Coq 证明策略的主要内容,如果未能解决你的问题,请参考以下文章

我想对Peano nats进行归纳,但我想证明属性P超过nats 1 ... n。 Coq是否提供了这样做的策略/工具?

如何在 Coq 中使用归纳类型处理案例

Z3和coq的区别

使用 Coq 证明存在量词

在 Coq 中证明一个定理几乎只用重写——没有“聪明”

Coq:如何添加有意义的提示?