В чем разница между Аксиомой и Переменной в Coq - PullRequest
Новая
       85

В чем разница между Аксиомой и Переменной в Coq

3 голосов
/ 21 апреля 2020

В Coq я могу написать 

Variable A : False.
Axiom B : False.

, что предполагает False под именами A и B. Оба утверждения работают в качестве доказательства, поэтому я могу 

Theorem nothing_makes_sense : forall (a : Type), a.
  destruct true; exfalso.
  * apply A.
  * apply B.
Qed.

Какая разница? Когда я должен использовать один вместо другого?

1 Ответ

6 голосов
/ 21 апреля 2020

Рекомендуется использовать команды «Аксиома», «Гипотеза» и «Гипотеза» (и их формы во множественном числе) для логических постулатов (т. Е. Когда тип утверждения имеет тип Prop), а также использовать команды Parameter и Variable (и их формы во множественном числе) в других случаях (соответствующих объявлению абстрактного математического объекта).

И, как вы можете видеть из спецификации coq https://coq.inria.fr/refman/coq-cmdindex.html, они определены одинаково.

...