如何解决在 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}})。整数的情况实际上是那篇论文的主要例子之一。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。