MSets: a new generation of FSets

Same global ideas (in particular the use of modules/functors), but:

- frequent use of Type Classes inside interfaces/implementation.
  For instance, no more eq_refl/eq_sym/eq_trans, but Equivalence.
  A class StrictOrder for lt in OrderedType. Extensive use of Proper
  and rewrite.

- now that rewrite is mature, we write specifications of set operators
  via iff instead of many separate requirements based on ->. For instance
   add_spec : In y (add x s) <-> E.eq y x \/ In x s.
  Old-style specs are available in the functor Facts.

- compare is now a pure function (t -> t -> comparison) instead of
  returning a dependent type Compare.

- The "Raw" functors (the ones dealing with e.g. list with no
  sortedness proofs yet, but morally sorted when operating on them)
  are given proper interfaces and a generic functor allows to obtain
  a regular set implementation out of a "raw" one.

The last two points allow to manipulate set objects that are completely free
of proof-parts if one wants to. Later proofs will rely on type-classes
instance search mechanism.

No need to emphasis the fact that this new version is severely incompatible
with the earlier one. I've no precise ideas yet on how allowing an easy
transition (functors ?). For the moment, these new Sets are placed alongside
the old ones, in directory MSets (M for Modular, to constrast with forthcoming
CSets, see below). A few files exist currently in version foo.v and foo2.v,
I'll try to merge them without breaking things. Old FSets will probably move
to a contrib later.

Still to be done:
 - adapt FMap in the same way
 - integrate misc stuff like multisets or the map function
 - CSets, i.e. Sets based on Type Classes : Integration of code contributed by
    S. Lescuyer is on the way.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12384 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 158 insertions, 0 deletions

diff --git a/theories/MSets/MSetToFiniteSet.v b/theories/MSets/MSetToFiniteSet.v
new file mode 100644
index 000000000..e8f8ab5e9
--- /dev/null
+++ b/theories/MSets/MSetToFiniteSet.v
@@ -0,0 +1,158 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(** * Finite sets library : conversion to old [Finite_sets] *)
+
+Require Import Ensembles Finite_sets.
+Require Import MSetInterface MSetProperties OrderedType2Ex DecidableType2Ex.
+
+(** * Going from [MSets] with usual Leibniz equality
+    to the good old [Ensembles] and [Finite_sets] theory. *)
+
+Module WS_to_Finite_set (U:UsualDecidableType)(M: WSfun U).
+ Module MP:= WProperties_fun U M.
+ Import M MP FM Ensembles Finite_sets.
+
+ Definition mkEns : M.t -> Ensemble M.elt :=
+   fun s x => M.In x s.
+
+ Notation " !! " := mkEns.
+
+ Lemma In_In : forall s x, M.In x s <-> In _ (!!s) x.
+ Proof.
+ unfold In; compute; auto with extcore.
+ Qed.
+
+ Lemma Subset_Included : forall s s',  s[<=]s'  <-> Included _ (!!s) (!!s').
+ Proof.
+ unfold Subset, Included, In, mkEns; intuition.
+ Qed.
+
+ Notation " a === b " := (Same_set M.elt a b) (at level 70, no associativity).
+
+ Lemma Equal_Same_set : forall s s', s[=]s' <-> !!s === !!s'.
+ Proof.
+ intros.
+ rewrite double_inclusion.
+ unfold Subset, Included, Same_set, In, mkEns; intuition.
+ Qed.
+
+ Lemma empty_Empty_Set : !!M.empty === Empty_set _.
+ Proof.
+ unfold Same_set, Included, mkEns, In.
+ split; intro; set_iff; inversion 1.
+ Qed.
+
+ Lemma Empty_Empty_set : forall s, Empty s -> !!s === Empty_set _.
+ Proof.
+ unfold Same_set, Included, mkEns, In.
+ split; intros.
+ destruct(H x H0).
+ inversion H0.
+ Qed.
+
+ Lemma singleton_Singleton : forall x, !!(M.singleton x) === Singleton _ x .
+ Proof.
+ unfold Same_set, Included, mkEns, In.
+ split; intro; set_iff; inversion 1; try constructor; auto.
+ Qed.
+
+ Lemma union_Union : forall s s', !!(union s s') === Union _ (!!s) (!!s').
+ Proof.
+ unfold Same_set, Included, mkEns, In.
+ split; intro; set_iff; inversion 1; [ constructor 1 | constructor 2 | | ]; auto.
+ Qed.
+
+ Lemma inter_Intersection : forall s s', !!(inter s s') === Intersection _ (!!s) (!!s').
+ Proof.
+ unfold Same_set, Included, mkEns, In.
+ split; intro; set_iff; inversion 1; try constructor; auto.
+ Qed.
+
+ Lemma add_Add : forall x s, !!(add x s) === Add _ (!!s) x.
+ Proof.
+ unfold Same_set, Included, mkEns, In.
+ split; intro; set_iff; inversion 1; auto with sets.
+ inversion H0.
+ constructor 2; constructor.
+ constructor 1; auto.
+ Qed.
+
+ Lemma Add_Add : forall x s s', MP.Add x s s' -> !!s' === Add _ (!!s) x.
+ Proof.
+ unfold Same_set, Included, mkEns, In.
+ split; intros.
+ red in H; rewrite H in H0.
+ destruct H0.
+ inversion H0.
+ constructor 2; constructor.
+ constructor 1; auto.
+ red in H; rewrite H.
+ inversion H0; auto.
+ inversion H1; auto.
+ Qed.
+
+ Lemma remove_Subtract : forall x s, !!(remove x s) === Subtract _ (!!s) x.
+ Proof.
+ unfold Same_set, Included, mkEns, In.
+ split; intro; set_iff; inversion 1; auto with sets.
+ split; auto.
+ contradict H1.
+ inversion H1; auto.
+ Qed.
+
+ Lemma mkEns_Finite : forall s, Finite _ (!!s).
+ Proof.
+ intro s; pattern s; apply set_induction; clear s; intros.
+ intros; replace (!!s) with (Empty_set elt); auto with sets.
+ symmetry; apply Extensionality_Ensembles.
+ apply Empty_Empty_set; auto.
+ replace (!!s') with (Add _ (!!s) x).
+ constructor 2; auto.
+ symmetry; apply Extensionality_Ensembles.
+ apply Add_Add; auto.
+ Qed.
+
+ Lemma mkEns_cardinal : forall s, cardinal _ (!!s) (M.cardinal s).
+ Proof.
+ intro s; pattern s; apply set_induction; clear s; intros.
+ intros; replace (!!s) with (Empty_set elt); auto with sets.
+ rewrite cardinal_1; auto with sets.
+ symmetry; apply Extensionality_Ensembles.
+ apply Empty_Empty_set; auto.
+ replace (!!s') with (Add _ (!!s) x).
+ rewrite (cardinal_2 H0 H1); auto with sets.
+ symmetry; apply Extensionality_Ensembles.
+ apply Add_Add; auto.
+ Qed.
+
+ (** we can even build a function from Finite Ensemble to MSet
+     ... at least in Prop. *)
+
+ Lemma Ens_to_MSet : forall e : Ensemble M.elt, Finite _ e ->
+   exists s:M.t, !!s === e.
+ Proof.
+ induction 1.
+ exists M.empty.
+ apply empty_Empty_Set.
+ destruct IHFinite as (s,Hs).
+ exists (M.add x s).
+ apply Extensionality_Ensembles in Hs.
+ rewrite <- Hs.
+ apply add_Add.
+ Qed.
+
+End WS_to_Finite_set.
+
+
+Module S_to_Finite_set (U:UsualOrderedType)(M: Sfun U) :=
+  WS_to_Finite_set U M.
+
+