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

Question

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

Answer 1

一个非常方便的解决方案是将nth ordinal 定义'I_n为记录:

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

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

这是用来解决数学补偿,并具有良好的性能,主要的注入val,val_inj : injective val这意味着你可以重复使用最标准的操作在nat您的新的数据类型.请注意,您可能希望定义为另外两种add i j := max n.-1 (i+j)或作为(i+j) %% n.

此外,上面链接的库提供了使用有限类型的一般定义,包括将它们双射到它们的基数序数.