The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Mon, Aug 14, 2006 at 10:01:03AM +0200, Lionel Elie Mamane wrote:
> On Fri, Aug 11, 2006 at 04:20:38PM -0400, 
> roconnor AT theorem.ca
>  wrote:
> 
> >> I am a newcomer to Coq and would like to know how to define
> >> sets of the form
> >> X={1,2,3}.
> 
> > There are multiple represations of sets in Coq.  It is most common
> > to represents sets as predicates.
> 
> Alternatively, for finite sets, a list/heap/... can be adequate is
> some cases. (If you use lists, you'll want to use another equality
> than the Coq equality as your main interesting equality.)


If indeed you can limit yourself to finite sets, then you might be
interested by the library FSet/FMap I've recently added to Coq. It
still have some sharp edges and no documentation yet apart from the
source files, but it's already quite usable. Below is a session done 
with Coq 8.1beta...

Best regards, 
Pierre Letouzey


(* Let's use fast integers. *)
Require Import ZArith. 
Open Scope Z_scope.

(* Some examples of ordered types, including Z *)
Require OrderedTypeEx.
(* One implementation of finite sets over an ordered type, based on lists *)
Require FSetList.  
(* Other possibility: FSetAVL, heavier for Coq but more efficient *)

(* We combine the two in a specialized module for sets of integers *)
Module IntSet := FSetList.Make(OrderedTypeEx.Z_as_OT).
Import IntSet.
(* To have a rough idea of what's available in this IntSet: *)
Print IntSet.

(* Your set: *)
Definition X := add 1 (add 2 (add 3 empty)).

(* Idem, with a nice notation: *)
Infix "++" := add (at level 30, right associativity).
Definition X' := 0++2++4++empty.

(* Some examples of computation: *)
Eval compute in (cardinal X).
Eval compute in (elements (inter X X')).