The Coq mailing list

[Venanzio Capretta <venanzio AT cs.kun.nl>]

Dear Jasper,
  I had the same problem and my solution was first to define the family of
finite sets "Finite : nat -> Set" inductively. (Finite n) is a set with n
elements. Then a finite subset of a set A with at most n elements can be
represented as an element of (Finite n) -> A.
If you look at the files for Universal Algebra on my web page
(www.cs.ku.nl/~venanzio) you will find the definitions and several tools
to work with them (like conversion with lists and isomorphism of (Finite
n) with {x:nat | x<n}) with the corresponding proofs.
You see that if f:(Finite n)->A, an element a:A can be represented by
different indexes, (f n)=(f m)=a. I didn't deal with the question because
it didn't matter to my development, and I have the feeling that you don't
need it either.
But it should be easy to define an "extensional" equality on (Finite n)->A
and make the setoid of finite subsets of A.
Best wishes,
  Venanzio

On Fri, 6 Apr 2001, Jasper J Stein wrote:

>
> Good afternoon all,
>
> Has anyone implemented a workable encoding of finite (sub)sets in Coq? I
> need them to state definitions like "a vector v is a linear combination
> of elements of a set S if there exist a finite number of elements
> y_1...y_n and scalars a_1...a_n such that x=a_1 y_1+...+a_n y_n.", or
> "the sumvector of a finite set of vectors is v_1+v_2+...", or " a
> vectorspace is finite if the set of basis elements is finite".
>
> I tried making subsets of the natural numbers (building upon an
> implementation of an algebraic hierarchy containing subsets by Loic
> Pottier) but it turned out not to work easily that way: the access to
> these subsets gets too involved, to the extent that I lost overview.
> This is not, in my opinion, a good way to go. I adhere the philosophy
> that a proof assistant should be exactly that: an +assistant+; and
> therefore it should make mathematical life easier instead of complicated.
>
> Since I want to have my enCoqed maths resemble textbook maths as closely
> as possible, I want to be able (in a relatively easy way) to e.g. access
> every single element, or given a binary operation +, apply it to the
> whole bunch of them one after each other (ie. (((a_1+a_2)+a_3)+...+a_n).)
>
> So, if any of you has, or knows about, a suitable implementation: please
> SHOOT...!
>
> Many thanks in advance,
>
> Jasper
> --
> In a world without walls and fences, who needs Windows and Gates?
>
>

----------------------
Venanzio Capretta
University of Nijmegen
Faculty of Mathematics
       and Informatics
the Nederlands
tel.: +31+24+3652647
----------------------