The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Thu, 10 Nov 2011 08:43:40 +0000,
Ramana Kumar 
<rk436 AT cam.ac.uk>
 a écrit :

> 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.