时间戳

首页 > 解决方案 > 使一个术语属于 Coq 中两种不同类型的不同层次结构？

types - 使一个术语属于 Coq 中两种不同类型的不同层次结构？

问题描述

我们从类型的层次结构中了解SetisType(0)和 is 的Type(i)类型Type(i+1)。因此对于 的任何项t，Type(i)它也是 的Type(i+1)。是否可以在 Coq 中使用此构造？例如，假设我们有

                              apple: Fruit, apple : Food

并且由于水果是食物，我想构建类型Fruit和Food这样Fruit的类型Type(i)，Food即Type(j)i < j 和因此 Fruits : Food。Coq 中是否存在这种可能性，如果没有，是否有任何其他方法可以形成具有这种结构的东西？

标签： typescoq

解决方案

原则上，可以定义apple为一种类型来实现你想要的：

Definition Food := Type.
Definition Fruit : Food := Type.
Inductive apple : Fruit :=.

Check apple : Fruit.
Check apple : Food.

这定义了一个名为and的新（空）类型apple常量，如您所愿。FruitFood

但是，我怀疑这种编码在实践中不会很有用。例如，如果Fruit不假设 Coq 核心之外的非建设性公理，就不可能在类型上定义相等运算符。此外，Fruit并且Food将是非常奇怪的类型，因为它们将包含许多违反直觉的居民；例如，termapple -> apple也有 type Fruit。我们需要更多上下文来确定这种编码是否会给您的开发带来任何麻烦。

（在 Coq 中，使用强制转换或子集类型{x : T | P x}来实现类似效果是司空见惯的，而不是诉诸子类型化。例如，检查这个答案或这个问题。）

推荐阅读