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

2 files changed, 124 insertions, 2 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index fe2f55311..a0ce827a9 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -279,7 +279,7 @@ Program Instance compose_proper A B C R₀ R₁ R₂ :
     unfold compose. apply H. apply H0. apply H1.
   Qed.
 
-(** Coq functions are morphisms for leibniz equality,
+(** Coq functions are morphisms for Leibniz equality,
    applied only if really needed. *)
 
 Instance reflexive_eq_dom_reflexive (A : Type) `(Reflexive B R') :
@@ -488,3 +488,98 @@ Ltac proper_reflexive :=
   end.
 
 Hint Extern 7 (@Proper _ _ _) => proper_reflexive : typeclass_instances.
+
+
+(** When the relation on the domain is symmetric, we can
+    inverse the relation on the codomain. Same for binary functions. *)
+
+Lemma proper_sym_flip
+ `(Symmetric A R1)`(Proper (A->B) (R1==>R2) f) :
+ Proper (R1==>inverse R2) f.
+Proof.
+intros A R1 Sym B R2 f Hf.
+intros x x' Hxx'. apply Hf, Sym, Hxx'.
+Qed.
+
+Lemma proper_sym_flip_2
+ `(Symmetric A R1)`(Symmetric B R2)`(Proper (A->B->C) (R1==>R2==>R3) f) :
+ Proper (R1==>R2==>inverse R3) f.
+Proof.
+intros A R1 Sym1 B R2 Sym2 C R3 f Hf.
+intros x x' Hxx' y y' Hyy'. apply Hf; auto.
+Qed.
+
+(** When the relation on the domain is symmetric, a predicate is
+  compatible with [iff] as soon as it is compatible with [impl].
+  Same with a binary relation. *)
+
+Lemma proper_sym_impl_iff `(Symmetric A R)`(Proper _ (R==>impl) f) :
+ Proper (R==>iff) f.
+Proof.
+intros A R Sym f Hf x x' Hxx'. repeat red in Hf. split; eauto.
+Qed.
+
+Lemma proper_sym_impl_iff_2
+ `(Symmetric A R)`(Symmetric B R')`(Proper _ (R==>R'==>impl) f) :
+ Proper (R==>R'==>iff) f.
+Proof.
+intros A R Sym B R' Sym' f Hf x x' Hxx' y y' Hyy'.
+repeat red in Hf. split; eauto.
+Qed.
+
+(** A [PartialOrder] is compatible with its underlying equivalence. *)
+
+Instance PartialOrder_proper `(PartialOrder A eqA R) :
+  Proper (eqA==>eqA==>iff) R.
+Proof.
+intros.
+apply proper_sym_impl_iff_2; auto with *.
+intros x x' Hx y y' Hy Hr.
+transitivity x.
+generalize (partial_order_equivalence x x'); compute; intuition.
+transitivity y; auto.
+generalize (partial_order_equivalence y y'); compute; intuition.
+Qed.
+
+(** From a [PartialOrder] to the corresponding [StrictOrder]:
+     [lt = le /\ ~eq].
+    If the order is total, we could also say [gt = ~le]. *)
+
+Instance PartialOrder_StrictOrder `(PartialOrder A eqA R) :
+  StrictOrder (relation_conjunction R (complement eqA)).
+Proof.
+split; compute.
+intros x (_,Hx). apply Hx, Equivalence_Reflexive.
+intros x y z (Hxy,Hxy') (Hyz,Hyz'). split.
+apply PreOrder_Transitive with y; assumption.
+intro Hxz.
+apply Hxy'.
+apply partial_order_antisym; auto.
+rewrite Hxz; auto.
+Qed.
+
+(** From a [StrictOrder] to the corresponding [PartialOrder]:
+     [le = lt \/ eq].
+    If the order is total, we could also say [ge = ~lt]. *)
+
+Instance StrictOrder_PreOrder
+ `(Equivalence A eqA, StrictOrder A R, Proper _ (eqA==>eqA==>iff) R) :
+ PreOrder (relation_disjunction R eqA).
+Proof.
+split.
+intros x. right. reflexivity.
+intros x y z [Hxy|Hxy] [Hyz|Hyz].
+left. transitivity y; auto.
+left. rewrite <- Hyz; auto.
+left. rewrite Hxy; auto.
+right. transitivity y; auto.
+Qed.
+
+Instance StrictOrder_PartialOrder
+  `(Equivalence A eqA, StrictOrder A R, Proper _ (eqA==>eqA==>iff) R) :
+  PartialOrder eqA (relation_disjunction R eqA).
+Proof.
+intros. intros x y. compute. intuition.
+elim (StrictOrder_Irreflexive x).
+transitivity y; auto.
+Qed.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index bc25fe488..83095720a 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -47,7 +47,7 @@ Class Reflexive {A} (R : relation A) :=
 Class Irreflexive {A} (R : relation A) :=
   irreflexivity : Reflexive (complement R).
 
-Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclasses_instances.
+Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances.
 
 Class Symmetric {A} (R : relation A) :=
   symmetry : forall x y, R x y -> R y x.
@@ -417,3 +417,30 @@ Instance: RewriteRelation (@relation_equivalence A).
    a rewrite relation. *)
 
 Instance equivalence_rewrite_relation `(Equivalence A eqA) : RewriteRelation eqA.
+
+(** Strict Order *)
+
+Class StrictOrder {A : Type} (R : relation A) := {
+  StrictOrder_Irreflexive :> Irreflexive R ;
+  StrictOrder_Transitive :> Transitive R
+}.
+
+Instance StrictOrder_Asymmetric `(StrictOrder A R) : Asymmetric R.
+Proof.
+  firstorder.
+Qed.
+
+(** Inversing a [StrictOrder] gives another [StrictOrder] *)
+
+Instance StrictOrder_inverse `(StrictOrder A R) : StrictOrder (inverse R).
+
+(** Same for [PartialOrder]. *)
+
+Instance PreOrder_inverse `(PreOrder A R) : PreOrder (inverse R).
+
+Instance PartialOrder_inverse `(PartialOrder A eqA R) :
+ PartialOrder eqA (inverse R).
+Proof.
+firstorder.
+Qed.
+