В чем разница между леммой и теоремой в 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, чтобы извлечь из него некоторую статистику.