В чем разница между определениями и теоремами?

Question

В текущей версии Фондов программного обеспечения соответствующее объяснение сформулировано с намеренной задержкой.

Сначала мы использовали ключевое слово Theorem вместо Example. Эта разница в основном вопрос стиля; ключевые слова Example и Theorem (и некоторые другие, включая Lemma, Fact и Remark) означают в значительной степени то же самое для Coq.

(я поставил формулировку, использованную для введения неопределенности жирным шрифтом.)

В более ранней версии, очевидно, того же текста , она была поставлена ​​решительно :

Форма этой теоремы и доказательства практически идентичны приведенным выше примерам: единственное отличие состоит в том, что мы добавили квантификатор ∀ n:nat и что мы использовали ключевое слово Theorem вместо Example. В самом деле, последнее различие является чисто вопросом стиля; ключевые слова Example и Theorem (и несколько других, включая Lemma, Fact и Remark) означают точно то же самое для Coq.

(слова, вводящие силу, выделены жирным шрифтом.)

Глядя на официальную документацию , все эти слова и многое другое , принадлежат к той же грамматической категории «ключевое слово утверждения» :

assertion_keyword  ::=  Theorem | Lemma
                        Remark | Fact
                        Corollary | Property | Proposition
                        Definition | Example

В следующих двух разделах объясняется, как работают эти ключевые слова: «Определения» и «Утверждения и доказательства» . Вкратце:

Определения расширяют среду ассоциациями имен с терминами.

- И:

Утверждение утверждает предложение ( или тип), из которых доказательство (или обитатель этого типа) строится в интерактивном режиме с использованием тактики.

Но, насколько я понимаю, теорема также расширяет среду, и пример может быть построенным с тактикой. Итак, я не вижу, где эти вещи разные. Но Software Foundation - умная книга. Если они решили быть неуверенными, должна быть причина?

Answer 1

На сегодняшний день различия минимальны и могут быть обобщены следующим образом:

• Theorem/Example/Definition/... действительно дают разные записи в документации; это самое важное различие.
• Некоторые формы, такие как Theorem, не поддерживают синтаксическую форму Theorem foo := nat. для неинтерактивного режима, которая поддерживается, например, Definition.

Еще одно нетривиальное отличие заключается в том, используете ли вы интерактивный режим или нет. То есть:

Definition foo : Type := nat.

и

Definition foo : Type. Proof. apply nat. Qed.

будут использовать несколько разные пути кода из-за второго, создающего интерактивное доказательство; путь кода, когда определение отправляется ядру, немного отличается, но Coq 8.12 должен унифицировать их для всех практических целей, просто пометив второе доказательство как непрозрачное.

Answer 2

Я видел одно различие в том, что Definition s может дать немедленное определение, тогда как Lemma и Theorem не могут.

Definition one := 1.

Lemma two := 2. (* syntax error *)
Theorem three := 3. (* syntax error *)

Из остальных, только Example работает.

Remark four := 4. (* syntax error *)
Fact five := 5. (* syntax error *)
Corollary six := 6. (* syntax error *)
Property seven := 7. (* syntax error *)
Proposition eight := 8. (* syntax error *)
Example nine := 9. (* works! *)