The Coq mailing list

[Jasper J Stein <jasper AT cs.kun.nl>]

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?