如何定義Coq中N個元素的有限集合？

Question

如何定義一般參數N：nat，N個元素的有限集合$ A_ {0}，... A_ {N-1} $？ 有沒有一種優雅的方式來做到遞歸定義？有人能夠將我推薦爲關於這種結構的推理嗎？

Answer 1

一個非常方便的解決方案是定義n次序，'I_n作爲記錄：

Definition 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。

此外，上面鏈接的庫提供了使用有限類型的一般定義，包括將它們映射到它們的基數序號。