在 Coq 中归纳定义整数归纳定义受关系约束

问题描述

在 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，但我不知道如何做到这一点。

解决方法

您实际上要求的是商数归纳类型 (QIT)，目前在 Coq 中不受支持，尽管有一种方法可以使用私有归纳类型来破解此限制（例如，请参阅 these slides） .不言而喻，这远不是推荐的选项（至少在 Coq 中，情况在支持 HIT（QIT 的通用版本）的 cubeal-agda 中是不同的。

一般来说，Coq 不提供任意商。标准解决方案要么使用 setoids（即配备等价关系的类型，并表明您的所有构造都保留这些等价关系，这相当繁重）或使用您想要做的商的特定方面（见 {{ 3}})。整数的情况实际上是那篇论文的主要例子之一。