如何在 Coq 中定义 N 个元素的有限集？

Question

对于一般参数 N:nat ，如何定义 N 个元素的有限集 $ A_{0},...A_{N-1} $ ？ 有没有一种优雅的方法可以通过递归定义来做到这一点？有人可以指出我对这种结构进行推理的好例子吗？

Answer 1

一个非常方便的解决方案是将nth 序数，'I_n 定义为记录：

Record ordinal n := {
    val :> nat;
    _   : val < n;
}.

也就是说，一对自然数，加上一个证明该自然数小于n，其中< : nat -> nat -> bool。在这里使用可计算的比较运算符非常方便，特别是意味着证明本身不是很“重要”，这是您通常想要的。

这是math-comp 中使用的解决方案，它具有很好的属性，主要是val、val_inj : injective val 的注入性，这意味着您可以使用您的新数据类型重用nat 上的大部分标准操作。请注意，您可能希望将添加定义为 add i j := max n.-1 (i+j) 或 (i+j) %% n。

此外，上面链接的库提供了处理有限类型的一般定义，包括将它们双射到它们的基数。