时间戳

首页 > 解决方案 > Coq：存在于 Set 中的非列表数据结构？

functional-programming - Coq：存在于 Set 中的非列表数据结构？

问题描述

如果我有以下行：

Definition Foo : Set := list nat.

然后我编译没有问题。

但是，假设我想对Coq.Lists.ListSet一个将有限集表示为列表的库做同样的事情：

(*Section first_definitions.
 Variable A : Type.
Definition listset := list A.*)
Definition Bar : Set := listset nat.

我收到以下错误：

The term "listset nat" has type "Type" while it is expected to have type 
"Set" (universe inconsistency).
  1. 有没有办法“铸造” listset，让它生活在Set而不是Type？即，如果我知道我将使用listsettype 的参数Set，有没有办法让它Set以某种方式存在于层次结构中？
  2. 为什么错误发生在listset，而不是list，什么时候listset被定义为list？

注意：实际类型被调用set，但我已将其重命名listset以避免与排序混淆Set。

编辑：=替换为:=

标签： functional-programmingcoqdependent-typetheorem-proving

解决方案

  1. 当 listset 被定义为 list 时，为什么 listset 会发生错误，而不是 list 会发生错误？

因为list是一个模板 Universe 多态归纳定义（参见About list.），在这种情况下，这意味着如果list应用于 in 的类型Set，结果仍然是 in Set。

  1. 有没有办法“铸造” listset，让它生活在Set而不是Type？

AFAIK，没有办法让定义模板宇宙多态，但你可以让它们像这样宇宙多态：

Polymorphic Definition listset (A : Type) : Type := list A.
Check listset nat : Set.

另一种选择是使用Set Universe Polymorphism命令，这样您就不需要在定义前加上Polymorphic关键字。此功能在撰写本文时处于实验状态。而且它不追溯适用，所以我想你需要自己分叉ListSet.

推荐阅读