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, 528 insertions, 0 deletions

diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
new file mode 100644
index 000000000..d5a85e6c2
--- /dev/null
+++ b/theories/MSets/MSetWeakList.v
@@ -0,0 +1,528 @@
+(***********************************************************************)
+(*  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 *)
+
+(** This file proposes an implementation of the non-dependant
+    interface [MSetWeakInterface.S] using lists without redundancy. *)
+
+Require Import MSetInterface.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Functions over lists
+
+   First, we provide sets as lists which are (morally) without redundancy.
+   The specs are proved under the additional condition of no redundancy.
+   And the functions returning sets are proved to preserve this invariant. *)
+
+
+(** ** The set operations. *)
+
+Module Ops (X: DecidableType) <: WOps X.
+
+  Definition elt := X.t.
+  Definition t := list elt.
+
+  Definition empty : t := nil.
+
+  Definition is_empty (l : t) : bool := if l then true else false.
+
+  Fixpoint mem (x : elt) (s : t) : bool :=
+    match s with
+    | nil => false
+    | y :: l =>
+           if X.eq_dec x y then true else mem x l
+    end.
+
+  Fixpoint add (x : elt) (s : t) : t :=
+    match s with
+    | nil => x :: nil
+    | y :: l =>
+        if X.eq_dec x y then s else y :: add x l
+    end.
+
+  Definition singleton (x : elt) : t := x :: nil.
+
+  Fixpoint remove (x : elt) (s : t) : t :=
+    match s with
+    | nil => nil
+    | y :: l =>
+        if X.eq_dec x y then l else y :: remove x l
+    end.
+
+  Definition fold (B : Type) (f : elt -> B -> B) (s : t) (i : B) : B :=
+    fold_left (flip f) s i.
+
+  Definition union (s : t) : t -> t := fold add s.
+
+  Definition diff (s s' : t) : t := fold remove s' s.
+
+  Definition inter (s s': t) : t :=
+    fold (fun x s => if mem x s' then add x s else s) s nil.
+
+  Definition subset (s s' : t) : bool := is_empty (diff s s').
+
+  Definition equal (s s' : t) : bool := andb (subset s s') (subset s' s).
+
+  Fixpoint filter (f : elt -> bool) (s : t) : t :=
+    match s with
+    | nil => nil
+    | x :: l => if f x then x :: filter f l else filter f l
+    end.
+
+  Fixpoint for_all (f : elt -> bool) (s : t) : bool :=
+    match s with
+    | nil => true
+    | x :: l => if f x then for_all f l else false
+    end.
+
+  Fixpoint exists_ (f : elt -> bool) (s : t) : bool :=
+    match s with
+    | nil => false
+    | x :: l => if f x then true else exists_ f l
+    end.
+
+  Fixpoint partition (f : elt -> bool) (s : t) : t * t :=
+    match s with
+    | nil => (nil, nil)
+    | x :: l =>
+        let (s1, s2) := partition f l in
+        if f x then (x :: s1, s2) else (s1, x :: s2)
+    end.
+
+  Definition cardinal (s : t) : nat := length s.
+
+  Definition elements (s : t) : list elt := s.
+
+  Definition choose (s : t) : option elt :=
+     match s with
+      | nil => None
+      | x::_ => Some x
+     end.
+
+End Ops.
+
+(** ** Proofs of set operation specifications. *)
+
+Module MakeRaw (X:DecidableType) <: WRawSets X.
+  Include Ops X.
+
+  Section ForNotations.
+  Notation NoDup := (NoDupA X.eq).
+  Notation In := (InA X.eq).
+
+  Definition IsOk := NoDup.
+
+  Class Ok (s:t) : Prop := { ok : NoDup s }.
+
+  Hint Constructors Ok.
+  Hint Resolve @ok.
+
+  Instance NoDup_Ok `(nd : NoDup s) : Ok s := nd.
+
+  Ltac inv_ok := match goal with
+   | H:Ok (_ :: _) |- _ => apply @ok in H; inversion_clear H; inv_ok
+   | H:Ok nil |- _ => clear H; inv_ok
+   | H:NoDup ?l |- _ => generalize (Build_Ok H); clear H; intro H; inv_ok
+   | _ => idtac
+  end.
+
+  Ltac inv := invlist InA; inv_ok.
+  Ltac constructors := repeat constructor.
+
+  Fixpoint isok l := match l with
+   | nil => true
+   | a::l => negb (mem a l) && isok l
+  end.
+
+  Definition Equal s s' := forall a : elt, In a s <-> In a s'.
+  Definition Subset s s' := forall a : elt, In a s -> In a s'.
+  Definition Empty s := forall a : elt, ~ In a s.
+  Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
+  Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
+
+  Lemma In_compat : Proper (X.eq==>eq==>iff) In.
+  Proof.
+  repeat red; intros. subst. rewrite H; auto.
+  Qed.
+
+  Lemma mem_spec : forall s x `{Ok s},
+   mem x s = true <-> In x s.
+  Proof.
+  induction s; intros.
+  split; intros; inv. discriminate.
+  simpl; destruct (X.eq_dec x a); split; intros; inv; auto.
+  right; rewrite <- IHs; auto.
+  rewrite IHs; auto.
+  Qed.
+
+  Lemma isok_iff : forall l, Ok l <-> isok l = true.
+  Proof.
+  induction l.
+  intuition.
+  simpl.
+  rewrite andb_true_iff.
+  rewrite negb_true_iff.
+  rewrite <- IHl.
+  split; intros H. inv.
+  split; auto.
+  apply not_true_is_false. rewrite mem_spec; auto.
+  destruct H; constructors; auto.
+  rewrite <- mem_spec; auto; congruence.
+  Qed.
+
+  Global Instance isok_Ok `(isok l = true) : Ok l | 10.
+  Proof.
+  intros. apply <- isok_iff; auto.
+  Qed.
+
+  Lemma add_spec :
+   forall (s : t) (x y : elt) {Hs : Ok s},
+     In y (add x s) <-> X.eq y x \/ In y s.
+  Proof.
+  induction s; simpl; intros.
+  intuition; inv; auto.
+  destruct X.eq_dec; inv; rewrite InA_cons, ?IHs; intuition.
+  left; eauto.
+  inv; auto.
+  Qed.
+
+  Global Instance add_ok s x `(Ok s) : Ok (add x s).
+  Proof.
+  induction s.
+  simpl; intuition.
+  intros; inv. simpl.
+  destruct X.eq_dec; auto.
+  constructors; auto.
+  intro; inv; auto.
+  rewrite add_spec in *; intuition.
+  Qed.
+
+  Lemma remove_spec :
+   forall (s : t) (x y : elt) {Hs : Ok s},
+     In y (remove x s) <-> In y s /\ ~X.eq y x.
+  Proof.
+  induction s; simpl; intros.
+  intuition; inv; auto.
+  destruct X.eq_dec; inv; rewrite !InA_cons, ?IHs; intuition.
+  elim H. setoid_replace a with y; eauto.
+  elim H3. setoid_replace x with y; eauto.
+  elim n. eauto.
+  Qed.
+
+  Global Instance remove_ok s x `(Ok s) : Ok (remove x s).
+  Proof.
+  induction s; simpl; intros.
+  auto.
+  destruct X.eq_dec; inv; auto.
+  constructors; auto.
+  rewrite remove_spec; intuition.
+  Qed.
+
+  Lemma singleton_ok : forall x : elt, Ok (singleton x).
+  Proof.
+  unfold singleton; simpl; constructors; auto. intro; inv.
+  Qed.
+
+  Lemma singleton_spec : forall x y : elt, In y (singleton x) <-> X.eq y x.
+  Proof.
+  unfold singleton; simpl; split; intros. inv; auto. left; auto.
+  Qed.
+
+  Lemma empty_ok : Ok empty.
+  Proof.
+  unfold empty; constructors.
+  Qed.
+
+  Lemma empty_spec : Empty empty.
+  Proof.
+  unfold Empty, empty; red; intros; inv.
+  Qed.
+
+  Lemma is_empty_spec : forall s : t, is_empty s = true <-> Empty s.
+  Proof.
+  unfold Empty; destruct s; simpl; split; intros; auto.
+  intro; inv.
+  discriminate.
+  elim (H e); auto.
+  Qed.
+
+  Lemma elements_spec1 : forall (s : t) (x : elt), In x (elements s) <-> In x s.
+  Proof.
+  unfold elements; intuition.
+  Qed.
+
+  Lemma elements_spec2w : forall (s : t) {Hs : Ok s}, NoDup (elements s).
+  Proof.
+  unfold elements; auto.
+  Qed.
+
+  Lemma fold_spec :
+   forall (s : t) (A : Type) (i : A) (f : elt -> A -> A),
+   fold f s i = fold_left (flip f) (elements s) i.
+  Proof.
+  reflexivity.
+  Qed.
+
+  Global Instance union_ok s s' `(Ok s, Ok s') : Ok (union s s').
+  Proof.
+  induction s; simpl; auto; intros; inv; unfold flip; auto with *.
+  Qed.
+
+  Lemma union_spec :
+   forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'},
+   In x (union s s') <-> In x s \/ In x s'.
+  Proof.
+  induction s; simpl in *; unfold flip; intros; auto; inv.
+  intuition; inv.
+  rewrite IHs, add_spec, InA_cons; intuition.
+  Qed.
+
+  Global Instance inter_ok s s' `(Ok s, Ok s') : Ok (inter s s').
+  Proof.
+  unfold inter, fold, flip; intros s.
+  set (acc := nil (A:=elt)).
+  assert (Hacc : Ok acc) by constructors.
+  clearbody acc; revert acc Hacc.
+  induction s; simpl; auto; intros. inv.
+  apply IHs; auto.
+  destruct (mem a s'); auto with *.
+  Qed.
+
+  Lemma inter_spec  :
+   forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'},
+   In x (inter s s') <-> In x s /\ In x s'.
+  Proof.
+  unfold inter, fold, flip; intros.
+  set (acc := nil (A:=elt)) in *.
+  assert (Hacc : Ok acc) by constructors.
+  assert (IFF : (In x s /\ In x s') <-> (In x s /\ In x s') \/ In x acc).
+   intuition; unfold acc in *; inv.
+  rewrite IFF; clear IFF. clearbody acc.
+  revert acc Hacc x s' Hs Hs'.
+  induction s; simpl; intros.
+  intuition; inv.
+  inv.
+  case_eq (mem a s'); intros Hm.
+  rewrite IHs, add_spec, InA_cons; intuition.
+  rewrite mem_spec in Hm; auto.
+  left; split; auto. rewrite H1; auto.
+  rewrite IHs, InA_cons; intuition.
+  rewrite H2, <- mem_spec in H3; auto. congruence.
+  Qed.
+
+  Global Instance diff_ok s s' `(Ok s, Ok s') : Ok (diff s s').
+  Proof.
+  unfold diff; intros s s'; revert s.
+  induction s'; simpl; unfold flip; auto; intros. inv; auto with *.
+  Qed.
+
+  Lemma diff_spec  :
+   forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'},
+   In x (diff s s') <-> In x s /\ ~In x s'.
+  Proof.
+  unfold diff; intros s s'; revert s.
+  induction s'; simpl; unfold flip.
+  intuition; inv.
+  intros. inv.
+  rewrite IHs', remove_spec, InA_cons; intuition.
+  Qed.
+
+  Lemma subset_spec :
+   forall (s s' : t) {Hs : Ok s} {Hs' : Ok s'},
+   subset s s' = true <-> Subset s s'.
+  Proof.
+  unfold subset, Subset; intros.
+  rewrite is_empty_spec.
+  unfold Empty; intros.
+  intuition.
+  specialize (H a). rewrite diff_spec in H; intuition.
+  rewrite <- (mem_spec a) in H |- *. destruct (mem a s'); intuition.
+  rewrite diff_spec in H0; intuition.
+  Qed.
+
+  Lemma equal_spec :
+   forall (s s' : t) {Hs : Ok s} {Hs' : Ok s'},
+   equal s s' = true <-> Equal s s'.
+  Proof.
+  unfold Equal, equal; intros.
+  rewrite andb_true_iff, !subset_spec.
+  unfold Subset; intuition. rewrite <- H; auto. rewrite H; auto.
+  Qed.
+
+  Definition choose_spec1 :
+    forall (s : t) (x : elt), choose s = Some x -> In x s.
+  Proof.
+  destruct s; simpl; intros; inversion H; auto.
+  Qed.
+
+  Definition choose_spec2 : forall s : t, choose s = None -> Empty s.
+  Proof.
+  destruct s; simpl; intros.
+  intros x H0; inversion H0.
+  inversion H.
+  Qed.
+
+  Lemma cardinal_spec :
+   forall (s : t) {Hs : Ok s}, cardinal s = length (elements s).
+  Proof.
+  auto.
+  Qed.
+
+  Lemma filter_spec' : forall s x f,
+   In x (filter f s) -> In x s.
+  Proof.
+  induction s; simpl.
+  intuition; inv.
+  intros; destruct (f a); inv; intuition; right; eauto.
+  Qed.
+
+  Lemma filter_spec :
+   forall (s : t) (x : elt) (f : elt -> bool),
+   Proper (X.eq==>eq) f ->
+   (In x (filter f s) <-> In x s /\ f x = true).
+  Proof.
+  induction s; simpl.
+  intuition; inv.
+  intros.
+  destruct (f a) as [ ]_eqn:E; rewrite ?InA_cons, IHs; intuition.
+  setoid_replace x with a; auto.
+  setoid_replace a with x in E; auto. congruence.
+  Qed.
+
+  Global Instance filter_ok s f `(Ok s) : Ok (filter f s).
+  Proof.
+  induction s; simpl.
+  auto.
+  intros; inv.
+  case (f a); auto.
+  constructors; auto.
+  contradict H0.
+  eapply filter_spec'; eauto.
+  Qed.
+
+  Lemma for_all_spec :
+   forall (s : t) (f : elt -> bool),
+   Proper (X.eq==>eq) f ->
+   (for_all f s = true <-> For_all (fun x => f x = true) s).
+  Proof.
+  unfold For_all; induction s; simpl.
+  intuition. inv.
+  intros; inv.
+  destruct (f a) as [ ]_eqn:F.
+  rewrite IHs; intuition. inv; auto.
+  setoid_replace x with a; auto.
+  split; intros H'; try discriminate.
+  intros.
+  rewrite <- F, <- (H' a); auto.
+  Qed.
+
+  Lemma exists_spec :
+   forall (s : t) (f : elt -> bool),
+   Proper (X.eq==>eq) f ->
+   (exists_ f s = true <-> Exists (fun x => f x = true) s).
+  Proof.
+  unfold Exists; induction s; simpl.
+  split; [discriminate| intros (x & Hx & _); inv].
+  intros.
+  destruct (f a) as [ ]_eqn:F.
+  split; auto.
+  exists a; auto.
+  rewrite IHs; firstorder.
+  inv.
+  setoid_replace a with x in F; auto; congruence.
+  exists x; auto.
+  Qed.
+
+  Lemma partition_spec1 :
+   forall (s : t) (f : elt -> bool),
+   Proper (X.eq==>eq) f ->
+   Equal (fst (partition f s)) (filter f s).
+  Proof.
+  simple induction s; simpl; auto; unfold Equal.
+  firstorder.
+  intros x l Hrec f Hf.
+  generalize (Hrec f Hf); clear Hrec.
+  case (partition f l); intros s1 s2; simpl; intros.
+  case (f x); simpl; firstorder; inversion H0; intros; firstorder.
+  Qed.
+
+  Lemma partition_spec2 :
+   forall (s : t) (f : elt -> bool),
+   Proper (X.eq==>eq) f ->
+   Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
+  Proof.
+  simple induction s; simpl; auto; unfold Equal.
+  firstorder.
+  intros x l Hrec f Hf.
+  generalize (Hrec f Hf); clear Hrec.
+  case (partition f l); intros s1 s2; simpl; intros.
+  case (f x); simpl; firstorder; inversion H0; intros; firstorder.
+  Qed.
+
+  Lemma partition_ok1' :
+   forall (s : t) {Hs : Ok s} (f : elt -> bool)(x:elt),
+    In x (fst (partition f s)) -> In x s.
+  Proof.
+  induction s; simpl; auto; intros. inv.
+  generalize (IHs H1 f x).
+  destruct (f a); destruct (partition f s); simpl in *; auto.
+  inversion_clear H; auto.
+  Qed.
+
+  Lemma partition_ok2' :
+   forall (s : t) {Hs : Ok s} (f : elt -> bool)(x:elt),
+    In x (snd (partition f s)) -> In x s.
+  Proof.
+  induction s; simpl; auto; intros. inv.
+  generalize (IHs H1 f x).
+  destruct (f a); destruct (partition f s); simpl in *; auto.
+  inversion_clear H; auto.
+  Qed.
+
+  Global Instance partition_ok1 s f `(Ok s) : Ok (fst (partition f s)).
+  Proof.
+  simple induction s; simpl.
+  auto.
+  intros x l Hrec f Hs; inv.
+  generalize (@partition_ok1' _ _ f x).
+  generalize (Hrec f H0).
+  case (f x); case (partition f l); simpl; constructors; auto.
+  Qed.
+
+  Global Instance partition_ok2 s f `(Ok s) : Ok (snd (partition f s)).
+  Proof.
+  simple induction s; simpl.
+  auto.
+  intros x l Hrec f Hs; inv.
+  generalize (@partition_ok2' _ _ f x).
+  generalize (Hrec f H0).
+  case (f x); case (partition f l); simpl; constructors; auto.
+  Qed.
+
+  End ForNotations.
+
+  Definition In := InA X.eq.
+  Definition eq := Equal.
+  Instance eq_equiv : Equivalence eq.
+
+End MakeRaw.
+
+(** * Encapsulation
+
+   Now, in order to really provide a functor implementing [S], we
+   need to encapsulate everything into a type of lists without redundancy. *)
+
+Module Make (X: DecidableType) <: WSets with Module E := X.
+ Module Raw := MakeRaw X.
+ Include WRaw2Sets X Raw.
+End Make.
+