Coq 中的引理和定理有什么区别

Question

我不知道在哪些情况下应该使用

Theorem

而不是

Lemma

或相反。这之间有什么区别（语法除外）

Theorem l : 2 = 2.
  trivial.
Qed.

还有这个

Lemma l : 2 = 2.
  trivial.
Qed.

？

Answer 1

就语言而言，

Theorem

和

Lemma

之间没有区别。选择其中一种的原因纯粹是心理上的。 您还可以根据您赋予结果的重要性使用

Remark

、

Fact

、

Corollary

、

Proposition

。这是 Coq 参考手册中的相关链接。

一些项目的代码风格指南只允许使用一个关键字以保持统一。这可能有助于阅读源代码并允许使用简单的类似 grep 的工具从中提取一些统计信息。