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

Question

我不知道在什么情况下我应该使用 Theorem 而不是 Lemma 或者相反。这之间有什么区别(尽管在句法上)

Theorem l : 2 = 2.
  trivial.
Qed.

还有这个

Lemma l : 2 = 2.
  trivial.
Qed.

?

Answer 1

就语言而言，Theorem 和Lemma 没有区别。选择一个而不是另一个的原因纯粹是心理上的。您还可以根据您赋予结果的重要性使用Remark、Fact、Corollary、Proposition。这是 relevant link在 Coq 引用手册中。

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