The Coq mailing list

[rk1 <rkam2001 AT hotmail.com>]

This question is more directed toward anyone who is familiar with or has used
Loic Pottier's "Basic notions of algebra" user supplied library of March
'99.  The zip is called "Sophia-Antipolis/Algebra".

Basically I'm wondering about a pretty simple definition, which seems to be
surprisingly impossible with the Sophia-Antipolis library as is.  Cardinals
are defined inductively, but finite sets are not.  I was trying to define a
specialized Sum operator (which does not exist yet in the Sophia-Antipolis
library) that simply, given a set containing a finite number of finite sets,
adds up the cardinalities of each of the contained sets and returns the
result.  It seems to me after banging my head against it for a long time,
that this is impossible if finite sets were not originally defined
inductively (as is done for example in the standard library FSetList).  It
seems to me that FSetList, for example, by using Inductive and Fixpoint
definitions for building up finite sets from scratch (kind of like cons for
lists), it *builds in* the axiom of choice into the notion of finite sets
themselves.  Thus, defining a Sum operator like I hoped would be
straightforward.

Am I forced to include ClassicalChoice or other standard library, in my work
with the Sophia-Antipolis library, to define my Sum?
-- 
View this message in context: 
http://www.nabble.com/Axiom-of-choice-equivalent-to-Defining-finite-sets-as-lists-tf3719805.html#a10407516
Sent from the Coq mailing list archive at Nabble.com.