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的工具从中提取一些统计信息。