The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-saarland.de>]

Hi

In order to define such a function, you need to assume an Axiom. 

If you Import Coq.Logic.ClassicalEpsilon you get an epsilon operator 
satisfying: 

Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) :
  (exists x, P x) -> P (epsilon i P)

Then you can first prove (by induction on Finite) that such a list exists for 
every set and afterwards use the epsilon operator to obtain such a list.

Regards
Christian

On 25.04.2013, at 15:21, Vincent BENAYOUN 
<benayoun.vincent AT gmail.com>
 wrote:

> Hi everybody,
> 
> I am using the Coq standard library for set.
> I consider :
> - Coq.Sets.Ensembles
> - Coq.Sets.Finite_sets
> 
> How can I write a function which take a finite set and return a list of its 
> elements ?
> I have written the following code which obviously doesn't work.
> How can I fix it ?
> 
> 
> Require Import Ensembles.
> Require Import Finite_sets.
> 
> Fixpoint finite_set_to_list (s:Ensemble label) (P:Finite _ s) : list label 
> :=
>   match P with
>     | Empty_is_finite => nil
>     | Union_is_finite s' P' x H => cons x (finite_set_to_list s' P')
>   end.
> 
> 
> Thanks in advance,
> Vincent