The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Thu, Apr 25, 2013 at 6:21 AM, 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.

Assuming this was for mathematical formalization as opposed to program verification, I'd prove something like:

Definition finite_set_list_equiv (s:Ensemble label) (l:list label) : Prop :=
  (forall x:label, Ensembles.In s x <-> List.In x l) /\ NoDup l.

Lemma finite_set_has_list_equiv : forall s:Ensemble label,
  Finite _ s -> exists l, finite_set_list_equiv s l.
Proof.
induction 1.
...
Qed.

From this, using the axiom of choice, you would be able to conclude that there exists a function { s:Ensemble label | Finite _ s } -> list label such that each finite set gets sent to an "equivalent" list.  Or, using the "indefinite description" axiom would allow you to "define" such a function, though it definitely wouldn't be computable and even to classical mathematicians the "definition" would be suspect.  If you had some total ordering on your label type, you could replace the NoDup condition with the condition that l is strictly increasing, and then use "definite description" instead.
--
Daniel Schepler