How to define finite set of N elements in Coq?

问题:

How to define, for general parameter N:nat , finite set of N elements, $ A_{0},...A_{N-1} $ ? Is there an elegant way to do it by recursive definition? Could someone point me into good example of reasoning about such structures?

回答1:

A very convenient solution is to define the nth ordinal, 'I_n as a record:

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

that is to say, a pair of a natural number, plus a proof that such natural number is less than n, where < : nat -> nat -> bool. It is very convenient to use a computable comparison operator here, in particular means that the proof itself is not very "important", which is what you normally want.

This is the solution used in math-comp, and it has nice properties, mainly injectivity of val, val_inj : injective val, which means that you can reuse most of the standard operations over nat with your new datatype. Note that you may want to define addition as either add i j := max n.-1 (i+j) or as (i+j) %% n.

Additionally, the library linked above provides general definitions for working with finite types, including a bijection of them to their cardinal ordinal.