How to use MSets

[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

[AUGER Cedric]

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.

[Adam Chlipala]

Incidentally, the commonness of this sort of question indicates a
fundamental problem with coqdoc or even with Coq source file
organization: there is no clear separation of implementation and
interface. Someone curious about how to use finite maps or sets should
be able to look at a file, like .mli files in OCaml, that clearly
specifies interfaces only. As it stands now, to see, e.g., the best way
to use the [FMapAVL] module, a newcomer has to know to scroll all the
way to its bottom, past all manner of implementation details, to find
the functor [Make]; and this description holds of the coqdoc output, too.

[Ramana Kumar]

Of course, I agree.
For the meanwhile I have this list.
I'm also unsure about the intended use of MSets... do I have to pick
an implementation, or can I write to an abstract interface for finite
sets and fill in the implementation later (for code extraction
purposes, say) or never?
If I did want to do that, and if MSets is not suitable, then what
could I use instead?

I'm also still keen to hear of existing examples to look at. Cedric
Auger, thanks for yours. It seems like the only place you actually use
MSets there is with the call to MakeWithLeibniz, right?

Post by Adam Chlipala
Incidentally, the commonness of this sort of question indicates a
there is no clear separation of implementation and interface.  Someone
curious about how to use finite maps or sets should be able to look at a
file, like .mli files in OCaml, that clearly specifies interfaces only.  As
it stands now, to see, e.g., the best way to use the [FMapAVL] module, a
newcomer has to know to scroll all the way to its bottom, past all manner of
implementation details, to find the functor [Make]; and this description
holds of the coqdoc output, too.

[AUGER Cedric]

Le Thu, 10 Nov 2011 13:42:12 +0000,

Post by Ramana Kumar
Of course, I agree.
For the meanwhile I have this list.
I'm also unsure about the intended use of MSets... do I have to pick
an implementation, or can I write to an abstract interface for finite
sets and fill in the implementation later (for code extraction
purposes, say) or never?
If I did want to do that, and if MSets is not suitable, then what
could I use instead?
I'm also still keen to hear of existing examples to look at. Cedric
Auger, thanks for yours. It seems like the only place you actually use
MSets there is with the call to MakeWithLeibniz, right?

MakeWithLeibniz is a functor.
In fact I do not use MSet with MakeWithLeibniz;
I build an MSet with MakeWithLeibniz.

I do not know if you have understood how does MSet work, so I try to
explain it more.

To have a set, a priori you only need a type;
but:

* you won't have efficient representation,
since given an element, you will have to check it against all
the elements of the set (since a raw type has no information on its
structure).

* you won't have unicity of representations,
since a permutation of all the elements of the set will produce
another representation of the same set.

To solve these problems, you have to provide more information on your
type.

That is the aim of an OrderedTypeWithLeibniz module (OWL in my
example),
you provide a comparison function so that you can have dichotomy to
search elements (although I doubt it is used in MSetList), and order
your elements so you have unicity of representations.

Then MakeWithLeibniz is a functor, which take the previous module
and builds a MSet module (in fact a slightly bigger module, since it
has more properties) which I called NatSet.

Then once you have applied your module to the functor, you don't need
the old module anymore nor the functor
(you can forget of OWL and MakeWithLeibniz,
only NatSet will be important).

Then if you want an empty set, use NatSet.empty;
if you want to add an element, use NatSet.add, and so on.

"Print MSet" will show you all the operations and lemmas you have
available.


So to sum up, the place where I use MSet is in the definition of
the inductive "exemple" and "eq_dec".

If you want to have more exemples, you can try something like
(not tested, and probably errors with order of the arguments):

Definition RefSet:NatSet.t :=
NatSet.add (NatSet.add (NatSet.add NatSet.empty 5) 8) 13.

Definition RefList: nat list := 8::13::8::5::nil.

Fixpoint build_set l :=
match l with
| nil => NatSet.empty
| n::l => NatSet.add (build_set l) n
end.

Eval compute in NatSet.equal (build_set RefList) RefSet.

---------------------------------------------------------------------
By the way, is there a way to really print the signature?
Because:

MSet : sig
Parameter t
Parameter empty
Parameter add
...
end

doesn't really give information, and you have to browse the standard
library to get them.

Post by Ramana Kumar

Post by Adam Chlipala
Incidentally, the commonness of this sort of question indicates a
fundamental problem with coqdoc or even with Coq source file
organization: there is no clear separation of implementation and
interface.  Someone curious about how to use finite maps or sets
should be able to look at a file, like .mli files in OCaml, that
clearly specifies interfaces only.  As it stands now, to see, e.g.,
the best way to use the [FMapAVL] module, a newcomer has to know to
scroll all the way to its bottom, past all manner of implementation
details, to find the functor [Make]; and this description holds of
the coqdoc output, too.

[Marco Servetto]

Incidentally, the commonness of this sort of question indicates a> fundamental problem with coqdoc or even with Coq source file organization:More, I believe that working with finite/multi sets and maps is order of magnitudo more complex that how it have to be.

I think there is the need that when in Gallina someone define any
inductive datatype,
a function for Leibniz equality and an absolute order is generated.
With those easy-to-generate (but crazy to write and MAINTAIN by hand)
We need also to have simple parametric types like *list*
for finite/multi sets and maps.
so that when one write stuff like

Inductive Foo : Set :=
| E : nat->Foo
| EE : nat ->Foo->Foo.

The system generate simple to use
Foo.beq and Foo.ble as functions Foo->Foo->bool
(a type like forall (s1 s2: set A), {s1=s2}+{s1<>s2} is simply TOO
complex, in 99% of the cases bool is enough precise, and this is one
of such cases)
Note that to generate Foo.beq and Foo.ble the system will reuse
nat.beq and nat.ble.

Now one can write

Require Import FSets.(* import the library *)

Define myFoos=(FSet Foo)[E 1, EE 1 (E 2)].(*example set*)

Theorem ex1: myFoos = ((FSet Foo).add (E 1) myFoos).
(*adding something that is already in there does not change the set*)
Proof.
compute.
(* i hope it to be enought, if right hints are automatically added
for proofs about FSetFoo.beq*)
reflexivity.
Qed.

With that, (FSet Foo) would be a (not easy to write, but easy to use)
type representing a finite set
over Foo and (FSet Foo).beq and (FSet Foo).ble would be equalities and
comparisions.
Using Foo.beq and Foo.ble is possible to guarantee uniquenes of
representation and so on and so forth. It can be also possible to
encode nice printing directive to visualize such sets inside proofs.
All based on simple syntax, no need for understanding "theories" for
the programmer.
Why it is not done in this way?
I'm surely missing something.... but.. what?
I understand that sometimes there are different needs... but i believe
this is really the most common scenario, why is not supported in this
way?