时间戳

首页 > 解决方案 > 教会数字和宇宙不一致

types - 教会数字和宇宙不一致

问题描述

在以下代码中，该语句add'_commut被 Coq 接受，但add_commut由于 Universe 不一致而被拒绝。

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).
*)

如何让它通过？

标签： typescoqtype-inferencelambda-calculuschurch-encoding

解决方案

只有在您打开 impredicativeSet时，教堂数字才有效，方法是放入-arg -impredicative-set您的_CoqProject文件或使用-impredicative-set命令行选项。然后定义nat为：

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

ImpredicativeSet允许具有与其量化nat的完全相同的类型。Set如果没有不可预测性，nat则必须具有比它量化的更高的宇宙级别，尽管这些级别对您是隐藏的，直到您遇到问题中的错误。

请注意，禁言式Set与经典逻辑不相容。

推荐阅读