on cache autant que possible Raw dans FSet(Weak)List.Make

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

2 files changed, 354 insertions, 212 deletions

diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
index 5b2c083195..ac26d57864 100644
--- a/theories/FSets/FSetList.v
+++ b/theories/FSets/FSetList.v
@@ -1029,135 +1029,214 @@ End Raw.
 
 Module Make (X: OrderedType) <: S with Module E := X.
 
- Module E := X.
  Module Raw := Raw X. 
+ Import Raw.
+ Module E := X.
 
  Record slist : Set :=  {this :> Raw.t; sorted : sort X.lt this}.
  Definition t := slist. 
  Definition elt := X.t.
  
- Definition In (x : elt) (s : t) := InA X.eq x s.(this).
- 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.
-  
- Definition In_1 (s : t) := Raw.MX.In_eq (l:=s.(this)).
- 
- Definition mem (x : elt) (s : t) := Raw.mem x s.
- Definition mem_1 (s : t) := Raw.mem_1 (sorted s). 
- Definition mem_2 (s : t) := Raw.mem_2 (s:=s).
-
- Definition add x s := Build_slist (Raw.add_sort (sorted s) x).
- Definition add_1 (s : t) := Raw.add_1 (sorted s).
- Definition add_2 (s : t) := Raw.add_2 (sorted s).
- Definition add_3 (s : t) := Raw.add_3 (sorted s).
-
- Definition remove x s := Build_slist (Raw.remove_sort (sorted s) x).
- Definition remove_1 (s : t) := Raw.remove_1 (sorted s).
- Definition remove_2 (s : t) := Raw.remove_2 (sorted s).
- Definition remove_3 (s : t) := Raw.remove_3 (sorted s).
+ Definition In (x : elt) (s : t) : Prop := InA X.eq x s.(this).
+ Definition Equal (s s':t) : Prop := forall a : elt, In a s <-> In a s'.
+ Definition Subset (s s':t) : Prop := forall a : elt, In a s -> In a s'.
+ Definition Empty (s:t) : Prop := forall a : elt, ~ In a s.
+ Definition For_all (P : elt -> Prop)(s:t) : Prop := forall x, In x s -> P x.
+ Definition Exists (P : elt -> Prop)(s:t) : Prop := exists x, In x s /\ P x.
+
+ Definition mem (x : elt) (s : t) : bool := mem x s.
+ Definition add (x : elt)(s : t) : t := Build_slist (add_sort (sorted s) x).
+ Definition remove (x : elt)(s : t) : t := Build_slist (remove_sort (sorted s) x).
+ Definition singleton (x : elt) : t  := Build_slist (singleton_sort x).
+ Definition union (s s' : t) : t :=
+   Build_slist (union_sort (sorted s) (sorted s')). 
+ Definition inter (s s' : t) : t :=
+   Build_slist (inter_sort (sorted s) (sorted s')). 
+ Definition diff (s s' : t) : t :=
+   Build_slist (diff_sort (sorted s) (sorted s')). 
+ Definition equal (s s' : t) : bool := equal s s'. 
+ Definition subset (s s' : t) : bool := subset s s'.
+ Definition empty : t := Build_slist empty_sort.
+ Definition is_empty (s : t) : bool := is_empty s.
+ Definition elements (s : t) : list elt := elements s.
+ Definition min_elt (s : t) : option elt := min_elt s.
+ Definition max_elt (s : t) : option elt := max_elt s.
+ Definition choose (s : t) : option elt  := choose s.
+ Definition fold (B : Set) (f : elt -> B -> B) (s : t) : B -> B := fold (B:=B) f s. 
+ Definition cardinal (s : t) : nat := cardinal s.
+ Definition filter (f : elt -> bool) (s : t) : t :=
+   Build_slist (filter_sort (sorted s) f).
+ Definition for_all (f : elt -> bool) (s : t) : bool := for_all f s.
+ Definition exists_ (f : elt -> bool) (s : t) : bool := exists_ f s.
+ Definition partition (f : elt -> bool) (s : t) : t * t :=
+   let p := partition f s in
+   (Build_slist (this:=fst p) (partition_sort_1 (sorted s) f),
+   Build_slist (this:=snd p) (partition_sort_2 (sorted s) f)).
+ Definition eq (s s' : t) : Prop := eq s s'.
+ Definition lt (s s' : t) : Prop := lt s s'.
+
+ Section Spec. 
+  Variable s s' s'': t.
+  Variable x y : elt.
+
+  Lemma In_1 : X.eq x y -> In x s -> In y s. 
+  Proof. exact (fun H H' => MX.In_eq H H'). Qed.
  
- Definition singleton x := Build_slist (Raw.singleton_sort x).
- Definition singleton_1 := Raw.singleton_1.
- Definition singleton_2 := Raw.singleton_2.
-  
- Definition union (s s' : t) :=
-   Build_slist (Raw.union_sort (sorted s) (sorted s')). 
- Definition union_1 (s s' : t) := Raw.union_1 (sorted s) (sorted s').
- Definition union_2 (s s' : t) := Raw.union_2 (sorted s) (sorted s').
- Definition union_3 (s s' : t) := Raw.union_3 (sorted s) (sorted s').
-
- Definition inter (s s' : t) :=
-   Build_slist (Raw.inter_sort (sorted s) (sorted s')). 
- Definition inter_1 (s s' : t) := Raw.inter_1 (sorted s) (sorted s').
- Definition inter_2 (s s' : t) := Raw.inter_2 (sorted s) (sorted s').
- Definition inter_3 (s s' : t) := Raw.inter_3 (sorted s) (sorted s').
- 
- Definition diff (s s' : t) :=
-   Build_slist (Raw.diff_sort (sorted s) (sorted s')). 
- Definition diff_1 (s s' : t) := Raw.diff_1 (sorted s) (sorted s').
- Definition diff_2 (s s' : t) := Raw.diff_2 (sorted s) (sorted s').
- Definition diff_3 (s s' : t) := Raw.diff_3 (sorted s) (sorted s').
+  Lemma mem_1 : In x s -> mem x s = true.
+  Proof. exact (fun H => mem_1 s.(sorted) H). Qed.
+  Lemma mem_2 : mem x s = true -> In x s. 
+  Proof. exact (fun H => mem_2 H). Qed.
  
- Definition equal (s s' : t) := Raw.equal s s'. 
- Definition equal_1 (s s' : t) := Raw.equal_1 (sorted s) (sorted s').  
- Definition equal_2 (s s' : t) := Raw.equal_2 (s:=s) (s':=s').
- 
- Definition subset (s s' : t) := Raw.subset s s'.
- Definition subset_1 (s s' : t) := Raw.subset_1 (sorted s) (sorted s').  
- Definition subset_2 (s s' : t) := Raw.subset_2 (s:=s) (s':=s').
+  Lemma equal_1 : Equal s s' -> equal s s' = true.
+  Proof. exact (equal_1 s.(sorted) s'.(sorted)). Qed.
+  Lemma equal_2 : equal s s' = true -> Equal s s'.
+  Proof. exact (fun H => equal_2 H). Qed.
 
- Definition empty := Build_slist Raw.empty_sort.
- Definition empty_1 := Raw.empty_1.
- 
- Definition is_empty (s : t) := Raw.is_empty s.
- Definition is_empty_1 (s : t) := Raw.is_empty_1 (s:=s).
- Definition is_empty_2 (s : t) := Raw.is_empty_2 (s:=s).
-
- Definition elements (s : t) := Raw.elements s.
- Definition elements_1 (s : t) := Raw.elements_1 (s:=s).
- Definition elements_2 (s : t) := Raw.elements_2 (s:=s).
- Definition elements_3 (s : t) := Raw.elements_3 (sorted s).
- 
- Definition min_elt (s : t) := Raw.min_elt s.
- Definition min_elt_1 (s : t) := Raw.min_elt_1 (s:=s).
- Definition min_elt_2 (s : t) := Raw.min_elt_2 (sorted s).
- Definition min_elt_3 (s : t) := Raw.min_elt_3 (s:=s).
-
- Definition max_elt (s : t) := Raw.max_elt s.
- Definition max_elt_1 (s : t) := Raw.max_elt_1 (s:=s).
- Definition max_elt_2 (s : t) := Raw.max_elt_2 (sorted s).
- Definition max_elt_3 (s : t) := Raw.max_elt_3 (s:=s).
-  
- Definition choose := min_elt.
- Definition choose_1 := min_elt_1.
- Definition choose_2 := min_elt_3.
- 
- Definition fold (B : Set) (f : elt -> B -> B) (s : t) := Raw.fold (B:=B) f s. 
- Definition fold_1 (s : t) := Raw.fold_1 (sorted s). 
- 
- Definition cardinal (s : t) := Raw.cardinal s.
- Definition cardinal_1 (s : t) := Raw.cardinal_1 (sorted s). 
+  Lemma subset_1 : Subset s s' -> subset s s' = true.
+  Proof. exact (subset_1 s.(sorted) s'.(sorted)). Qed.
+  Lemma subset_2 : subset s s' = true -> Subset s s'.
+  Proof. exact (fun H => subset_2 H). Qed.
+
+  Lemma empty_1 : Empty empty.
+  Proof. exact empty_1. Qed.
+
+  Lemma is_empty_1 : Empty s -> is_empty s = true. 
+  Proof. exact (fun H => is_empty_1 H). Qed.
+  Lemma is_empty_2 : is_empty s = true -> Empty s.
+  Proof. exact (fun H => is_empty_2 H). Qed.
  
- Definition filter (f : elt -> bool) (s : t) :=
-   Build_slist (Raw.filter_sort (sorted s) f).
- Definition filter_1 (s : t) := Raw.filter_1 (s:=s).
- Definition filter_2 (s : t) := Raw.filter_2 (s:=s).
- Definition filter_3 (s : t) := Raw.filter_3 (s:=s).
+  Lemma add_1 : X.eq x y -> In y (add x s).
+  Proof. exact (fun H => add_1 s.(sorted) H). Qed.
+  Lemma add_2 : In y s -> In y (add x s).
+  Proof. exact (fun H => add_2 s.(sorted) x H). Qed.
+  Lemma add_3 : ~ X.eq x y -> In y (add x s) -> In y s. 
+  Proof. exact (fun H => add_3 s.(sorted) H). Qed.
+
+  Lemma remove_1 : X.eq x y -> ~ In y (remove x s).
+  Proof. exact (fun H => remove_1 s.(sorted) H). Qed.
+  Lemma remove_2 : ~ X.eq x y -> In y s -> In y (remove x s).
+  Proof. exact (fun H H' => remove_2 s.(sorted) H H'). Qed.
+  Lemma remove_3 : In y (remove x s) -> In y s.
+  Proof. exact (fun H => remove_3 s.(sorted) H). Qed.
+
+  Lemma singleton_1 : In y (singleton x) -> X.eq x y. 
+  Proof. exact (fun H => singleton_1 H). Qed.
+  Lemma singleton_2 : X.eq x y -> In y (singleton x). 
+  Proof. exact (fun H => singleton_2 H). Qed.
+
+  Lemma union_1 : In x (union s s') -> In x s \/ In x s'.
+  Proof. exact (fun H => union_1 s.(sorted) s'.(sorted) H). Qed.
+  Lemma union_2 : In x s -> In x (union s s'). 
+  Proof. exact (fun H => union_2 s.(sorted) s'.(sorted) H). Qed.
+  Lemma union_3 : In x s' -> In x (union s s').
+  Proof. exact (fun H => union_3 s.(sorted) s'.(sorted) H). Qed.
+
+  Lemma inter_1 : In x (inter s s') -> In x s.
+  Proof. exact (fun H => inter_1 s.(sorted) s'.(sorted) H). Qed.
+  Lemma inter_2 : In x (inter s s') -> In x s'.
+  Proof. exact (fun H => inter_2 s.(sorted) s'.(sorted) H). Qed.
+  Lemma inter_3 : In x s -> In x s' -> In x (inter s s').
+  Proof. exact (fun H => inter_3 s.(sorted) s'.(sorted) H). Qed.
+
+  Lemma diff_1 : In x (diff s s') -> In x s. 
+  Proof. exact (fun H => diff_1 s.(sorted) s'.(sorted) H). Qed.
+  Lemma diff_2 : In x (diff s s') -> ~ In x s'.
+  Proof. exact (fun H => diff_2 s.(sorted) s'.(sorted) H). Qed.
+  Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s').
+  Proof. exact (fun H => diff_3 s.(sorted) s'.(sorted) H). Qed.
  
- Definition for_all (f : elt -> bool) (s : t) := Raw.for_all f s.
- Definition for_all_1 (s : t) := Raw.for_all_1 (s:=s). 
- Definition for_all_2 (s : t) := Raw.for_all_2 (s:=s). 
-
- Definition exists_ (f : elt -> bool) (s : t) := Raw.exists_ f s.
- Definition exists_1 (s : t) := Raw.exists_1 (s:=s). 
- Definition exists_2 (s : t) := Raw.exists_2 (s:=s). 
-
- Definition partition (f : elt -> bool) (s : t) :=
-   let p := Raw.partition f s in
-   (Build_slist (this:=fst p) (Raw.partition_sort_1 (sorted s) f),
-   Build_slist (this:=snd p) (Raw.partition_sort_2 (sorted s) f)).
- Definition partition_1 (s : t) := Raw.partition_1 s.
- Definition partition_2 (s : t) := Raw.partition_2 s. 
-
- Definition eq (s s' : t) := Raw.eq s s'.
- Definition eq_refl (s : t) := Raw.eq_refl s.
- Definition eq_sym (s s' : t) := Raw.eq_sym (s:=s) (s':=s').
- Definition eq_trans (s s' s'' : t) :=
-   Raw.eq_trans (s:=s) (s':=s') (s'':=s'').
+  Lemma fold_1 : forall (A : Set) (i : A) (f : elt -> A -> A),
+      fold f s i = fold_left (fun a e => f e a) (elements s) i.
+  Proof. exact (fold_1 s.(sorted)). Qed.
+
+  Lemma cardinal_1 : cardinal s = length (elements s).
+  Proof. exact (cardinal_1 s.(sorted)). Qed.
+
+  Section Filter.
   
- Definition lt (s s' : t) := Raw.lt s s'.
- Definition lt_trans (s s' s'' : t) :=
-   Raw.lt_trans (s:=s) (s':=s') (s'':=s'').
- Definition lt_not_eq (s s' : t) := Raw.lt_not_eq (sorted s) (sorted s').
-
- Definition compare : forall s s' : t, Compare lt eq s s'.
- Proof.
- intros; elim (Raw.compare (sorted s) (sorted s'));
-  [ constructor 1 | constructor 2 | constructor 3 ]; 
-  auto. 
- Defined.
+  Variable f : elt -> bool.
+
+  Lemma filter_1 : compat_bool X.eq f -> In x (filter f s) -> In x s. 
+  Proof. exact (@filter_1 s x f). Qed.
+  Lemma filter_2 : compat_bool X.eq f -> In x (filter f s) -> f x = true. 
+  Proof. exact (@filter_2 s x f). Qed.
+  Lemma filter_3 :
+      compat_bool X.eq f -> In x s -> f x = true -> In x (filter f s).
+  Proof. exact (@filter_3 s x f). Qed.
+
+  Lemma for_all_1 :
+      compat_bool X.eq f ->
+      For_all (fun x => f x = true) s -> for_all f s = true.
+  Proof. exact (@for_all_1 s f). Qed.
+  Lemma for_all_2 :
+      compat_bool X.eq f ->
+      for_all f s = true -> For_all (fun x => f x = true) s.
+  Proof. exact (@for_all_2 s f). Qed.
+
+  Lemma exists_1 :
+      compat_bool X.eq f ->
+      Exists (fun x => f x = true) s -> exists_ f s = true.
+  Proof. exact (@exists_1 s f). Qed.
+  Lemma exists_2 :
+      compat_bool X.eq f ->
+      exists_ f s = true -> Exists (fun x => f x = true) s.
+  Proof. exact (@exists_2 s f). Qed.
+
+  Lemma partition_1 :
+      compat_bool X.eq f -> Equal (fst (partition f s)) (filter f s).
+  Proof. exact (@partition_1 s f). Qed.
+  Lemma partition_2 :
+      compat_bool X.eq f ->
+      Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
+  Proof. exact (@partition_2 s f). Qed.
+
+  End Filter.
+
+  Lemma elements_1 : In x s -> InA X.eq x (elements s).
+  Proof. exact (fun H => elements_1 H). Qed.
+  Lemma elements_2 : InA X.eq x (elements s) -> In x s.
+  Proof. exact (fun H => elements_2 H). Qed.
+  Lemma elements_3 : sort X.lt (elements s).
+  Proof. exact (elements_3 s.(sorted)). Qed.
+
+  Lemma min_elt_1 : min_elt s = Some x -> In x s. 
+  Proof. exact (fun H => min_elt_1 H). Qed.
+  Lemma min_elt_2 : min_elt s = Some x -> In y s -> ~ X.lt y x. 
+  Proof. exact (fun H => min_elt_2 s.(sorted) H). Qed.
+  Lemma min_elt_3 : min_elt s = None -> Empty s.
+  Proof. exact (fun H => min_elt_3 H). Qed.
+
+  Lemma max_elt_1 : max_elt s = Some x -> In x s. 
+  Proof. exact (fun H => max_elt_1 H). Qed.
+  Lemma max_elt_2 : max_elt s = Some x -> In y s -> ~ X.lt x y. 
+  Proof. exact (fun H => max_elt_2 s.(sorted) H). Qed.
+  Lemma max_elt_3 : max_elt s = None -> Empty s.
+  Proof. exact (fun H => max_elt_3 H). Qed.
+
+  Lemma choose_1 : choose s = Some x -> In x s.
+  Proof. exact (fun H => choose_1 H). Qed.
+  Lemma choose_2 : choose s = None -> Empty s.
+  Proof. exact (fun H => choose_2 H). Qed.
+
+  Lemma eq_refl : eq s s.
+  Proof. exact (eq_refl s). Qed.
+  Lemma eq_sym : eq s s' -> eq s' s.
+  Proof. exact (@eq_sym s s'). Qed.
+  Lemma eq_trans : eq s s' -> eq s' s'' -> eq s s''.
+  Proof. exact (@eq_trans s s' s''). Qed.
+
+  Lemma lt_trans : lt s s' -> lt s' s'' -> lt s s''.
+  Proof. exact (@lt_trans s s' s''). Qed.
+  Lemma lt_not_eq : lt s s' -> ~ eq s s'.
+  Proof. exact (lt_not_eq s.(sorted) s'.(sorted)). Qed.
+
+  Definition compare : Compare lt eq s s'.
+  Proof.
+  elim (compare s.(sorted) s'.(sorted));
+   [ constructor 1 | constructor 2 | constructor 3 ]; 
+   auto. 
+  Defined.
+
+ End Spec.
 
 End Make.
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index 0d2f96fdad..130d31d1d0 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -759,115 +759,178 @@ End Raw.
 
 Module Make (X: DecidableType) <: S with Module E := X.
 
- Module E := X.
  Module Raw := Raw X. 
+ Import Raw.
+ Module E := X.
 
  Record slist : Set :=  {this :> Raw.t; unique : NoDupA X.eq this}.
  Definition t := slist. 
  Definition elt := X.t.
  
  Definition In (x : elt) (s : t) := InA X.eq x s.(this).
- 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 Equal (s s':t) := forall a : elt, In a s <-> In a s'.
+ Definition Subset (s s':t) := forall a : elt, In a s -> In a s'.
+ Definition Empty (s:t) := forall a : elt, ~ In a s.
  Definition For_all (P : elt -> Prop) (s : t) :=
    forall x : elt, In x s -> P x.
  Definition Exists (P : elt -> Prop) (s : t) := exists x : elt, In x s /\ P x.
-  
- Definition In_1 (s : t) := Raw.In_eq (s:=s).
- 
- Definition mem (x : elt) (s : t) := Raw.mem x s.
- Definition mem_1 (s : t) := Raw.mem_1 (s:=s). 
- Definition mem_2 (s : t) := Raw.mem_2 (s:=s).
-
- Definition add x s := Build_slist (Raw.add_unique (unique s) x).
- Definition add_1 (s : t) := Raw.add_1 (unique s).
- Definition add_2 (s : t) := Raw.add_2 (unique s).
- Definition add_3 (s : t) := Raw.add_3 (unique s).
-
- Definition remove x s := Build_slist (Raw.remove_unique (unique s) x).
- Definition remove_1 (s : t) := Raw.remove_1 (unique s).
- Definition remove_2 (s : t) := Raw.remove_2 (unique s).
- Definition remove_3 (s : t) := Raw.remove_3 (unique s).
+
+ Definition mem (x : elt) (s : t) : bool := mem x s.
+ Definition add (x : elt)(s : t) : t  := Build_slist (add_unique (unique s) x).
+ Definition remove (x : elt)(s : t) : t := Build_slist (remove_unique (unique s) x).
+ Definition singleton (x : elt) : t := Build_slist (singleton_unique x).
+ Definition union (s s' : t) : t :=
+   Build_slist (union_unique (unique s) (unique s')). 
+ Definition inter (s s' : t) : t :=
+   Build_slist (inter_unique (unique s) (unique s')). 
+ Definition diff (s s' : t) : t :=
+   Build_slist (diff_unique (unique s) (unique s')). 
+ Definition equal (s s' : t) : bool := equal s s'. 
+ Definition subset (s s' : t) : bool := subset s s'.
+ Definition empty : t := Build_slist empty_unique.
+ Definition is_empty (s : t) : bool := is_empty s.
+ Definition elements (s : t) : list elt := elements s.
+ Definition choose (s:t) : option elt := choose s.
+ Definition fold (B : Set) (f : elt -> B -> B) (s : t) : B -> B := fold (B:=B) f s. 
+ Definition cardinal (s : t) : nat := cardinal s.
+ Definition filter (f : elt -> bool) (s : t) : t :=
+   Build_slist (filter_unique (unique s) f).
+ Definition for_all (f : elt -> bool) (s : t) : bool := for_all f s.
+ Definition exists_ (f : elt -> bool) (s : t) : bool := exists_ f s.
+ Definition partition (f : elt -> bool) (s : t) : t * t :=
+   let p := partition f s in
+   (Build_slist (this:=fst p) (partition_unique_1 (unique s) f),
+   Build_slist (this:=snd p) (partition_unique_2 (unique s) f)).
+
+ Section Spec. 
+  Variable s s' : t.
+  Variable x y : elt.
+
+  Lemma In_1 : X.eq x y -> In x s -> In y s. 
+  Proof. exact (fun H H' => In_eq H H'). Qed.
  
- Definition singleton x := Build_slist (Raw.singleton_unique x).
- Definition singleton_1 := Raw.singleton_1.
- Definition singleton_2 := Raw.singleton_2.
-  
- Definition union (s s' : t) :=
-   Build_slist (Raw.union_unique (unique s) (unique s')). 
- Definition union_1 (s s' : t) := Raw.union_1 (unique s) (unique s').
- Definition union_2 (s s' : t) := Raw.union_2 (unique s) (unique s').
- Definition union_3 (s s' : t) := Raw.union_3 (unique s) (unique s').
-
- Definition inter (s s' : t) :=
-   Build_slist (Raw.inter_unique (unique s) (unique s')). 
- Definition inter_1 (s s' : t) := Raw.inter_1 (unique s) (unique s').
- Definition inter_2 (s s' : t) := Raw.inter_2 (unique s) (unique s').
- Definition inter_3 (s s' : t) := Raw.inter_3 (unique s) (unique s').
+  Lemma mem_1 : In x s -> mem x s = true.
+  Proof. exact (fun H => mem_1 H). Qed.
+  Lemma mem_2 : mem x s = true -> In x s. 
+  Proof. exact (fun H => mem_2 H). Qed.
  
- Definition diff (s s' : t) :=
-   Build_slist (Raw.diff_unique (unique s) (unique s')). 
- Definition diff_1 (s s' : t) := Raw.diff_1 (unique s) (unique s').
- Definition diff_2 (s s' : t) := Raw.diff_2 (unique s) (unique s').
- Definition diff_3 (s s' : t) := Raw.diff_3 (unique s) (unique s').
+  Lemma equal_1 : Equal s s' -> equal s s' = true.
+  Proof. exact (equal_1 s.(unique) s'.(unique)). Qed.
+  Lemma equal_2 : equal s s' = true -> Equal s s'.
+  Proof. exact (equal_2 s.(unique) s'.(unique)). Qed.
+
+  Lemma subset_1 : Subset s s' -> subset s s' = true.
+  Proof. exact (subset_1 s.(unique) s'.(unique)). Qed.
+  Lemma subset_2 : subset s s' = true -> Subset s s'.
+  Proof. exact (subset_2 s.(unique) s'.(unique)). Qed.
+
+  Lemma empty_1 : Empty empty.
+  Proof. exact empty_1. Qed.
+
+  Lemma is_empty_1 : Empty s -> is_empty s = true. 
+  Proof. exact (fun H => is_empty_1 H). Qed.
+  Lemma is_empty_2 : is_empty s = true -> Empty s.
+  Proof. exact (fun H => is_empty_2 H). Qed.
  
- Definition equal (s s' : t) := Raw.equal s s'. 
- Definition equal_1 (s s' : t) := Raw.equal_1 (unique s) (unique s').  
- Definition equal_2 (s s' : t) := Raw.equal_2 (unique s) (unique s').
+  Lemma add_1 : X.eq x y -> In y (add x s).
+  Proof. exact (fun H => add_1 s.(unique) H). Qed.
+  Lemma add_2 : In y s -> In y (add x s).
+  Proof. exact (fun H => add_2 s.(unique) x H). Qed.
+  Lemma add_3 : ~ X.eq x y -> In y (add x s) -> In y s. 
+  Proof. exact (fun H => add_3 s.(unique) H). Qed.
+
+  Lemma remove_1 : X.eq x y -> ~ In y (remove x s).
+  Proof. exact (fun H => remove_1 s.(unique) H). Qed.
+  Lemma remove_2 : ~ X.eq x y -> In y s -> In y (remove x s).
+  Proof. exact (fun H H' => remove_2 s.(unique) H H'). Qed.
+  Lemma remove_3 : In y (remove x s) -> In y s.
+  Proof. exact (fun H => remove_3 s.(unique) H). Qed.
+
+  Lemma singleton_1 : In y (singleton x) -> X.eq x y. 
+  Proof. exact (fun H => singleton_1 H). Qed.
+  Lemma singleton_2 : X.eq x y -> In y (singleton x). 
+  Proof. exact (fun H => singleton_2 H). Qed.
+
+  Lemma union_1 : In x (union s s') -> In x s \/ In x s'.
+  Proof. exact (fun H => union_1 s.(unique) s'.(unique) H). Qed.
+  Lemma union_2 : In x s -> In x (union s s'). 
+  Proof. exact (fun H => union_2 s.(unique) s'.(unique) H). Qed.
+  Lemma union_3 : In x s' -> In x (union s s').
+  Proof. exact (fun H => union_3 s.(unique) s'.(unique) H). Qed.
+
+  Lemma inter_1 : In x (inter s s') -> In x s.
+  Proof. exact (fun H => inter_1 s.(unique) s'.(unique) H). Qed.
+  Lemma inter_2 : In x (inter s s') -> In x s'.
+  Proof. exact (fun H => inter_2 s.(unique) s'.(unique) H). Qed.
+  Lemma inter_3 : In x s -> In x s' -> In x (inter s s').
+  Proof. exact (fun H => inter_3 s.(unique) s'.(unique) H). Qed.
+
+  Lemma diff_1 : In x (diff s s') -> In x s. 
+  Proof. exact (fun H => diff_1 s.(unique) s'.(unique) H). Qed.
+  Lemma diff_2 : In x (diff s s') -> ~ In x s'.
+  Proof. exact (fun H => diff_2 s.(unique) s'.(unique) H). Qed.
+  Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s').
+  Proof. exact (fun H => diff_3 s.(unique) s'.(unique) H). Qed.
  
- Definition subset (s s' : t) := Raw.subset s s'.
- Definition subset_1 (s s' : t) := Raw.subset_1 (unique s) (unique s').  
- Definition subset_2 (s s' : t) := Raw.subset_2 (unique s) (unique s').
+  Lemma fold_1 : forall (A : Set) (i : A) (f : elt -> A -> A),
+      fold f s i = fold_left (fun a e => f e a) (elements s) i.
+  Proof. exact (fold_1 s.(unique)). Qed.
 
- Definition empty := Build_slist Raw.empty_unique.
- Definition empty_1 := Raw.empty_1.
- 
- Definition is_empty (s : t) := Raw.is_empty s.
- Definition is_empty_1 (s : t) := Raw.is_empty_1 (s:=s).
- Definition is_empty_2 (s : t) := Raw.is_empty_2 (s:=s).
-
- Definition elements (s : t) := Raw.elements s.
- Definition elements_1 (s : t) := Raw.elements_1 (s:=s).
- Definition elements_2 (s : t) := Raw.elements_2 (s:=s).
- Definition elements_3 (s : t) := Raw.elements_3 (unique s).
-  
- Definition choose (s:t) := Raw.choose s.
- Definition choose_1 (s : t) := Raw.choose_1 (s:=s).
- Definition choose_2 (s : t) := Raw.choose_2 (s:=s).
+  Lemma cardinal_1 : cardinal s = length (elements s).
+  Proof. exact (cardinal_1 s.(unique)). Qed.
+
+  Section Filter.
   
- Definition fold (B : Set) (f : elt -> B -> B) (s : t) := Raw.fold (B:=B) f s. 
- Definition fold_1 (s : t) := Raw.fold_1 (unique s). 
- 
- Definition cardinal (s : t) := Raw.cardinal s.
- Definition cardinal_1 (s : t) := Raw.cardinal_1 (unique s). 
- 
- Definition filter (f : elt -> bool) (s : t) :=
-   Build_slist (Raw.filter_unique (unique s) f).
- Definition filter_1 (s : t)(x:elt)(f: elt -> bool)(H:compat_bool X.eq f) := 
-    @Raw.filter_1 s x f.
- Definition filter_2 (s : t) := Raw.filter_2 (s:=s).
- Definition filter_3 (s : t) := Raw.filter_3 (s:=s).
- 
- Definition for_all (f : elt -> bool) (s : t) := Raw.for_all f s.
- Definition for_all_1 (s : t) := Raw.for_all_1 (s:=s). 
- Definition for_all_2 (s : t) := Raw.for_all_2 (s:=s). 
-
- Definition exists_ (f : elt -> bool) (s : t) := Raw.exists_ f s.
- Definition exists_1 (s : t) := Raw.exists_1 (s:=s). 
- Definition exists_2 (s : t) := Raw.exists_2 (s:=s). 
-
- Definition partition (f : elt -> bool) (s : t) :=
-   let p := Raw.partition f s in
-   (Build_slist (this:=fst p) (Raw.partition_unique_1 (unique s) f),
-   Build_slist (this:=snd p) (Raw.partition_unique_2 (unique s) f)).
- Definition partition_1 (s : t) := Raw.partition_1 s.
- Definition partition_2 (s : t) := Raw.partition_2 s. 
-
- Definition eq (s s' : t) := Raw.eq s s'.
- Definition eq_refl (s : t) := Raw.eq_refl s.
- Definition eq_sym (s s' : t) := Raw.eq_sym (s:=s) (s':=s').
- Definition eq_trans (s s' s'' : t) :=
-   Raw.eq_trans (s:=s) (s':=s') (s'':=s'').
+  Variable f : elt -> bool.
+
+  Lemma filter_1 : compat_bool X.eq f -> In x (filter f s) -> In x s. 
+  Proof. exact (fun H => @filter_1 s x f). Qed.
+  Lemma filter_2 : compat_bool X.eq f -> In x (filter f s) -> f x = true. 
+  Proof. exact (@filter_2 s x f). Qed.
+  Lemma filter_3 :
+      compat_bool X.eq f -> In x s -> f x = true -> In x (filter f s).
+  Proof. exact (@filter_3 s x f). Qed.
+
+  Lemma for_all_1 :
+      compat_bool X.eq f ->
+      For_all (fun x => f x = true) s -> for_all f s = true.
+  Proof. exact (@for_all_1 s f). Qed.
+  Lemma for_all_2 :
+      compat_bool X.eq f ->
+      for_all f s = true -> For_all (fun x => f x = true) s.
+  Proof. exact (@for_all_2 s f). Qed.
+
+  Lemma exists_1 :
+      compat_bool X.eq f ->
+      Exists (fun x => f x = true) s -> exists_ f s = true.
+  Proof. exact (@exists_1 s f). Qed.
+  Lemma exists_2 :
+      compat_bool X.eq f ->
+      exists_ f s = true -> Exists (fun x => f x = true) s.
+  Proof. exact (@exists_2 s f). Qed.
+
+  Lemma partition_1 :
+      compat_bool X.eq f -> Equal (fst (partition f s)) (filter f s).
+  Proof. exact (@partition_1 s f). Qed.
+  Lemma partition_2 :
+      compat_bool X.eq f ->
+      Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
+  Proof. exact (@partition_2 s f). Qed.
+
+  End Filter.
+
+  Lemma elements_1 : In x s -> InA X.eq x (elements s).
+  Proof. exact (fun H => elements_1 H). Qed.
+  Lemma elements_2 : InA X.eq x (elements s) -> In x s.
+  Proof. exact (fun H => elements_2 H). Qed.
+  Lemma elements_3 : NoDupA X.eq (elements s).
+  Proof. exact (elements_3 s.(unique)). Qed.
+
+  Lemma choose_1 : choose s = Some x -> In x s.
+  Proof. exact (fun H => choose_1 H). Qed.
+  Lemma choose_2 : choose s = None -> Empty s.
+  Proof. exact (fun H => choose_2 H). Qed.
+
+ End Spec.
 
 End Make.