CoqでN個の要素の有限集合を定義するには？

Question

一般的なパラメータNのための定義方法：nat、N個の要素の有限集合、$ A_ {0}、... A_ {N-1} $？ 再帰的な定義でそれを行うためのエレガントな方法はありますか？誰かが私にそのような構造についての推論の良い例を指摘できますか？

Answer 1

A非常に便利なソリューションをレコードとしてn番目序、'I_nを定義することです：

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

、自然数のペアを言うことです、プラス、このような自然数未満であることを証明n、< : nat -> nat -> boolです。計算可能な比較演算子を使用することは非常に便利です。特に、証明自体はあまり「重要」ではないことを意味します。これは通常あなたが望むものです。

これはmath-compで使用されるソリューションであり、そしてそれはあなたがあなたの新しいデータ型でnat上で標準的な操作のほとんどを再利用できることを意味し、素敵な性質、valの主単射、val_inj : injective valを持っています。加算をadd i j := max n.-1 (i+j)または(i+j) %% nとして定義することができます。

さらに、上記にリンクされたライブラリは、有限型を扱う一般的な定義を提供します。