在 Coq 中以归纳方式定义整数（根据关系进行归纳定义）

Question

在 Coq 中，可以如下归纳定义自然数：

Inductive nat :=
| zero : nat
| succ : nat -> nat.

我想知道是否可以以类似的方式归纳定义 整数？我可以做类似的事情

Inductive int :=
| zero : int
| succ : int -> int
| pred : int -> int.

但是我想在int 的定义中断言succ(pred x) = x 和pred(succ x) = x，我不知道该怎么做。

Answer 1

您真正要求的称为商归纳类型 (QIT)，目前 Coq 不支持，尽管有一种方法可以使用私有归纳类型解决此限制（例如，参见 these slides）。不言而喻，它远不是推荐的选项（至少在 Coq 中，支持 HIT（QIT 的通用版本）的cubical-agda 中的情况有所不同。

一般来说，Coq 不提供任意商。标准解决方案是去 setoids（即配备等价关系并显示所有结构都保留这些等价关系的类型，这是相当繁重的）或使用您想要做的商的特定方面（请参阅@987654322 @)。整数的情况实际上是该论文的主要示例之一。