coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Letouzey <Pierre.Letouzey AT lri.fr>
- To: Jean-Yves Vion-Dury <jean-yves.vion-dury AT inrialpes.fr>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] "Concrete" <-> "Abstract" Sets ?
- Date: Tue, 30 Sep 2003 17:43:50 +0200 (MEST)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club] "Concrete" <-> "Abstract" Sets ?, Jean-Yves Vion-Dury
- Re: [Coq-Club] "Concrete" <-> "Abstract" Sets ?, Pierre Letouzey
Archive powered by MhonArc 2.6.16.