The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Thu, 25 Apr 2013 15:21:44 +0200,
Vincent BENAYOUN 
<benayoun.vincent AT gmail.com>
 a écrit :

> 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 ?

The quick answer is that you cannot.

P is in Prop (and is not a singleton type), so you cannot perform
induction on it to produce something in Type.

So the only argument on which you could recurse would be 's', but it is
not an inductive type, so you are doomed.

In fact there could have been a tricked if belonging to s was decidable
(ie. you can provide a function dec from label to bool such that dec x
= true <=> x ∈ s) and have the possibility to recurse over labels.
And even in those conditions you need a function telling if a "Finite _
s" is or is not empty.

To understand why, it is so, consider the following set:

Inductive unit := tt.

And now the following Ensemble:

Definition X (n : nat) : Ensemble unit
:= fun _ => …
   (*stating that the nth Turing Machine halts on any input *).

Now, for any n, X n is trivially Finite in a classical context (either
it is empty or it is a singleton).

Now, if you could define "finite_set_to_list", then you could decide
the halting property.

I think you need a stronger notion for Ensemble (for instance a label
-> bool rather than label -> Prop) and/or Finite.

> 
> 
> 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