Le Thu, 10 Nov 2011 08:43:40 +0000,

*Post by Ramana Kumar*Dear Coq Club

Could someone point me to an example of how to actually use MSets?

Apart from Require Import Coq.MSets.MSets. everything else I try to do

seems to fail.

I'm sure a working example would help in figuring them out.

Specifically, I would like to define a type that, basically. includes

a finite list of another one of my inductive types as a component. I

would imagine that I'd need to make sure that my type has a decidable

equality on it before using MSets. So I would also appreciate an

example of the easiest way to ensure that Coq knows that my type has

decidable equality (especially when it is obvious).

Thanks

Ramana

What do you mean by "decidable equality"?

Something like "forall (s1 s2: set A), {s1=s2}+{s1<>s2}" or some weaker

stuff like : "forall (s1 s2: set A),

(forall x, In x s1 <-> In x s2)

+{x:A | (In x s1 /\ ~(In x s2)) \/ (In x s2 /\ ~(In x s1))}"

For the first case (intentionnal equality), I doubt you have it in the

current implementation of MSets.

This is due to the fact that if I well remember, MSet is just a module

Type, so it can have many implementations, and for some implementations

(for instance with AVL), you have no guarantee that you have a unique

representant.

If you want intentionnal equality, you need to find an implementation

which ensures that you have unicity of representants (and of course

have a proof of it).

I also hope that your two types are not mutually recursives.

After looking at http://coq.inria.fr/stdlib/Coq.MSets.MSetList.html#,

it seems that you can do it with sorted lists (less efficient than AVL

though).

-------------------------------------------------------

Require Import MSets.

Require Import MSetList.

Print OrderedTypeWithLeibniz.

Module OWL.

Definition t := nat.

Definition eq := @eq t.

Instance eq_equiv : Equivalence eq.

Definition lt := lt.

Instance lt_strorder : StrictOrder lt.

Instance lt_compat : Proper (eq ==> eq ==> iff) lt.

Proof.

now unfold eq; split; subst.

Qed.

SearchPattern (nat -> nat -> comparison).

Definition compare := Compare_dec.nat_compare.

SearchAbout CompSpec.

(*So, nothing here on nat*)

Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).

Proof.

SearchPattern (forall x y, Compare_dec.nat_compare x y = _ -> _).

intros; case_eq (compare x y); constructor.

now apply Compare_dec.nat_compare_eq.

now apply Compare_dec.nat_compare_Lt_lt.

now apply Compare_dec.nat_compare_Gt_gt.

Qed.

SearchPattern (forall (a b:nat), {a=b}+{a<>b}).

Definition eq_dec := Peano_dec.eq_nat_dec.

Definition eq_leibniz a b (H:eq a b) := H.

End OWL.

Module NatSet := MakeWithLeibniz OWL.

Inductive exemple :=

| A : exemple

| B : NatSet.t -> exemple

| C : NatSet.t -> bool -> exemple.

Definition eq_dec : forall (a b:exemple), {a=b}+{a<>b}.

intros; decide equality.

destruct (NatSet.eq_dec t t0).

now left; apply NatSet.eq_leibniz.

right; intro; apply n; clear n; subst.

reflexivity.

apply bool_dec.

destruct (NatSet.eq_dec t t0).

now left; apply NatSet.eq_leibniz.

right; intro; apply n; clear n; subst.

reflexivity.

Defined.