Церковные цифры и несоответствие вселенной - PullRequest
Новая
       72

Церковные цифры и несоответствие вселенной

1 голос
/ 10 марта 2019

В следующем коде утверждение add'_commut принимается Coq, но add_commut отклоняется из-за несоответствия юниверса. 

Set Universe Polymorphism.

Definition nat : Type := forall (X : Type), X -> (X -> X) -> X.

Definition succ (n : nat) : nat := fun X z s => s (n X z s).

Definition add' (m n : nat) : nat := fun X z s => m X (n X z s) s.

Definition nat_rec (z : nat) (s : nat -> nat) (n : nat) : nat := n nat z s.
Definition add (m n : nat) : nat := nat_rec n succ m.

Definition equal (A : Type) (a : A) : A -> Type := fun a' => forall (P : A -> Type), P a -> P a'.

Lemma add'_commut (m n : nat) : equal nat (add' m n) (add' n m).
Admitted.

Lemma add_commut (m n : nat) : equal nat (add m n) (add n m).
(*
In environment
m : nat
n : nat
The term "add n (fun X : Type => m X)" has type
 "nat@{Top.1078 Top.1079}"
while it is expected to have type
 "nat@{Top.1080 Top.1078}" (universe inconsistency).
*)

Как заставить это пройти?

1 Ответ

3 голосов
/ 11 марта 2019

Церковные цифры работают только в том случае, если вы включили непредсказуемый Set, вставив -arg -impredicative-set в файл _CoqProject или используя параметр командной строки -impredicative-set.Затем определите nat как: 

Definition nat : Set := forall (X : Set), X -> (X -> X) -> X.

Impredicative Set позволяет nat иметь точно такой же тип Set, который он определяет количественно.Без непредсказуемости nat должен иметь более высокий уровень вселенной, чем тот, на котором он количественно определен, хотя уровни скрыты от вас, пока вы не получите ошибку, как в вопросе.

Обратите внимание, что непредсказуемое Set равно несовместим с классической логикой.

...