The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

On Tue, 30 Sep 2003, Jean-Yves Vion-Dury wrote:

> Dear Coq'ers,
>
> I have trouble trying to connect to views of sets. The first one is
> "concretely" defined e.g.
>
> Variable A:Set.
>
> Inductive set:Set := empty: set | item: A -> set -> set.
>
> Then, it is possible to define set related algorithms, e.g
> set_mem:A->set->bool,  set_add, ...
> as done in the ListSets standard lib.
>
> Then, let us suppose we would like to characterize these algorithms
> thanks to a correspondence
> to the logical theorie of sets, as found in the "Ensembles" standard
> library.
>
> In ListSets, a propositional inclusion "set_In" is defined through a
> Fixpoint, and then a soundness is established
> with
>
> Lemma set_mem_correct1 :
>     (a:A)(x:set)(set_mem a x)=true -> (set_In a x).
>
> But is it possible to relate more directly to the set theory defined in
> the "Ensembles" standard library, ?
>
> Any idea/help much appreciated
>
> Jean-Yves
>

I'm not sure to fully understand your question. Anyway, you can at least
transform a ListSet into an Ensemble:

Definition ListSet_to_Ensemble := [A:Set][s:(set A)][a:A](set_In a s).

Then the "In" predicate over this Ensemble is exactly the "set_In"
predicate.

The reverse transformation (from an Ensemble to a ListSet) cannot be done
in Coq since Ensemble is something logical (in Prop sort) that can't be
used to build an informative data-type like ListSet. And anyway an
Ensemble can represent an infinite set whereas ListSet cannot.


Besides, I would like to advertise a new contribution concerning
Finite Sets in Coq, using modules and functor to be generic.
You can have a look at http://www.lri.fr/~filliatr/fsets/ ;(needs Coq
current CVS to compile). In this development you can found stricly more
than in ListSet, in particular efficients implementation of sets via AVL
or Red-Black trees.

Pierre Letouzey