【发布时间】：2019-06-09 19:30:32
【问题描述】：
我不知道在哪些情况下我应该使用Theorem 而不是Lemma 或相反。这之间有什么区别（尽管在语法上）
Theorem l : 2 = 2.
trivial.
Qed.
还有这个
Lemma l : 2 = 2.
trivial.
Qed.
?
【问题讨论】：
标签： coq theorem-proving
【发布时间】：2019-06-09 19:30:32
【问题描述】：
就语言而言，Theorem 和 Lemma 之间没有区别。选择一个而不是另一个的原因纯粹是心理上的。
您还可以根据您对结果的重要性使用Remark、Fact、Corollary、Proposition。这是 Coq 参考手册中的relevant link。
一些项目的代码风格指南只允许使用一个关键字来统一。这可能有助于阅读源代码并允许使用类似 grep 的简单工具从中提取一些统计信息。
【讨论】：
-
其实，
Property也可以用于相同的目的，但似乎没有在任何地方记录。