Как доказать, что "Type <> Set" (т.е. тип не равен Set) в Coq? - PullRequest
Новая
       122

Как доказать, что "Type <> Set" (т.е. тип не равен Set) в Coq?

3 голосов
/ 31 мая 2019

Существует ли отношение равенства или неравенства между Type и Set в Coq?

Я изучаю систему типов Coq и понимаю, что тип Set равен Type@{Set+1}, а тип Type@{k} равен Type@{k+1}. Я пытался доказать это Type = Set, а затем пытался доказать Type <> Set, но в обоих случаях мне это не удалось.

Я начал с 

Lemma set_is_type :  Type = Set.
Proof.
reflexivity.

, который выдает сообщение об ошибке, говорящее о том, что Невозможно объединить "Set" с "Type@ndomTop.74}" .

Тогда я попробовал 

Lemma set_is_not_type : Type <> Set.
Proof.
intros contra.

На данный момент я не знаю, как поступить. Тактика discriminate не сработала, ни inversion contra.

Какую из двух приведенных выше лемм можно доказать?

1 Ответ

5 голосов
/ 01 июня 2019

Это на самом деле не совсем тривиальная теорема.Чтобы показать, что Type = Set приводит к парадоксу (и, следовательно, наличие отдельных уровней Type необходимо), вам нужно использовать стандартный результат, похожий на парадокс Рассела из теории множеств.В частности, вам понадобится парадокс Хюркена , который, по сути, говорит, что меньшие Type s не могут быть в равной степени с большими Type s (помните, что Type полиморфна в Coq, и вв частности, Set является самым низким уровнем (или вторым самым низким, если вы включите Prop)).

Конкретную теорему, которую мы хотим, можно найти в стандартной библиотеке. 

Require Logic.Hurkens.
Import Logic.Hurkens.TypeNeqSmallType.

Check paradox.

paradox имеет тип подписи forall A : Type, Type = A -> False.Это в значительной степени то, что мы хотим доказать, поскольку Set: Type (по крайней мере, если Type достаточно велико). 

Lemma set_is_not_type: Type <> Set.
Proof.
  intro F.
  exact (paradox _ F).
Defined.

Coq автоматически устанавливает ограничения на Type в этой лемме, чтобы гарантировать, чтоSet: Type.

С другой стороны, Set равен некоторому уровню Type, поэтому мы должны быть в состоянии доказать, что Type = Set с некоторымиразличные ограничения на это Type.Самым простым способом, который я нашел, было доказать это Type = Type, но затем создать экземпляр этой теоремы с помощью Set.По какой-то причине, как вы обнаружили, рефлексивность не может сама по себе навязывать ограничения вселенной.Чтобы сделать это, нам нужно сделать обе леммы полиморфными вселенной, чтобы их можно было создавать с определенным уровнем вселенной. 

Polymorphic Lemma type_is_type: Type = Type.
Proof.
  reflexivity.
Defined.

Polymorphic Lemma type_is_set: Type = Set.
Proof.
  apply type_is_type.
Defined.

Самый простой способ сделать все универсальным полиморфным - поставить Set Universe Polymorphism. перед всеми.

...