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 plus
或SearchPattern (_ + _ = _ + _ -> _)
,您可以检查关于+
的可用引理。但是如果你没有导入正确的模块,那可能就没用了。我通常做的是去看在线文档。 Here is the documentation for plus,您可以特别关注plus_reg_l
和plus_reg_r
。
【讨论】:
以上是关于Coq 证明策略的主要内容,如果未能解决你的问题,请参考以下文章
我想对Peano nats进行归纳,但我想证明属性P超过nats 1 ... n。 Coq是否提供了这样做的策略/工具?