coqtheorem-proving

What is the difference between Lemma and Theorem in Coq

I can't tell in which situations I should use Theorem over Lemma or the opposite. Is there any difference (except syntactical) between this

Theorem l : 2 = 2.
  trivial.
Qed.

and this

Lemma l : 2 = 2.
  trivial.
Qed.

?

Solution

  • There is no difference between Theorem and Lemma as far as the language is concerned. The reasons to choose one over another are purely psychological. You can also use Remark, Fact, Corollary, Proposition according to the importance you attribute to the result. Here is the relevant link in the Coq reference manual.

    Some projects' code style guides only allow one keyword to be used for uniformity. This might help reading source code and allow using simple grep-like tools to extract some statistics from it.