The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Thu, Sep 27, 2012 at 6:12 AM, Andrej Bauer 
<andrej.bauer AT andrej.com>
 wrote:
>> Class Enumeration (A:Type) : Type :=
>> | elements : list A.
>>
>> Implicit Arguments elements [[Enumeration]].
>>
>> Definition finite_card (A:Type) `{Enumeration A} : nat :=
>>   length (elements A).
>>
>> (* I'm not sure whether it's better to require the enumeration be
>>    exhaustive and have no duplications, before allowing the application
>>    of this notation. *)
>> Notation "# A" := (finite_card A) (at level 0).
>
> If your intention is to represent finite sets as Enumerations, then
> finite_card is not well-defined precisely for the reason you notice:
> an enumeration may list some elements several times. Thus the
> enumerations [1,2,1] and [1,2] both name the same set, but they have
> different lengths.

Of course finite_card, as I've written it, isn't well-defined.  What I
was trying to get at with the comment is: is it best to force it to be
well-defined using something like this?

Definition finite_card (A:Type) `{ExhaustiveEnumeration A}
  `{!NonRedundantEnumeration A} : nat :=
length (elements A).

Or is it better to have more of a separation between syntax and
semantics?  So the exhaustivity and non-redundancy conditions would
only come into play when you're proving something like: finite_card A
(Enumeration := enum1) = finite_card A (Enumeration := enum2).

(In fact, some time ago somebody else referred me to a paper on
different notions of "finiteness" like "enumerability", "bounded
size", "noetherian", "streamless" and discussing that they're all
non-equivalent in an intuitionistic world.)

In a serious usage, you'd probably also want to replace nat with N or
something of the kind for more efficiency with the large numbers that
tend to pop up in combinatorics.  Ultimately, for use in the class,
I'd hope all this would be hidden away in the bowels of course
materials and students would never have to deal with it.  They'd just
use higher-level statements like "bijective f -> #A = #B", "# {x:A | P
x \/ Q x} = #(sig P) + #(sig Q) - # {x:A | P x /\ Q x}", etc., or it
could underlie a "last resort" computation method which probably
wouldn't be very efficient for large types.
-- 
Daniel Schepler