The Coq mailing list

[Jean-Yves Vion-Dury <jean-yves.vion-dury AT inrialpes.fr>]

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

--

Jean-Yves Vion-Dury   Research Scientist	Xerox Research Centre Europe
INRIA (sabbatical) 655 avenue de l'Europe, 38334 Montbonnot (FRANCE) Jean-Yves.Vion-Dury AT inrialpes.fr	from France:   0 4 76 61 53 83 from abroad: +33 4 76 61 53 83
you may have a look at the Circus Transformation Language?	www.alphaAve.com