summaryrefslogtreecommitdiff
path: root/theories/MSets/MSetInterface.v
blob: 194cb904c57dc3ae3dc2226345d91bd71947982e (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
(***********************************************************************)
(*  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 set library *)

(** Set interfaces, inspired by the one of Ocaml. When compared with
    Ocaml, the main differences are:
    - the lack of [iter] function, useless since Coq is purely functional
    - the use of [option] types instead of [Not_found] exceptions
    - the use of [nat] instead of [int] for the [cardinal] function

    Several variants of the set interfaces are available:
    - [WSetsOn] : functorial signature for weak sets
    - [WSets]   : self-contained version of [WSets]
    - [SetsOn]  : functorial signature for ordered sets
    - [Sets]    : self-contained version of [Sets]
    - [WRawSets] : a signature for weak sets that may be ill-formed
    - [RawSets]  : same for ordered sets

    If unsure, [S = Sets] is probably what you're looking for: most other
    signatures are subsets of it, while [Sets] can be obtained from
    [RawSets] via the use of a subset type (see (W)Raw2Sets below).
*)

Require Export Bool SetoidList RelationClasses Morphisms
 RelationPairs Equalities Orders OrdersFacts.
Set Implicit Arguments.
Unset Strict Implicit.

Module Type TypElt.
 Parameters t elt : Type.
End TypElt.

Module Type HasWOps (Import T:TypElt).

  Parameter empty : t.
  (** The empty set. *)

  Parameter is_empty : t -> bool.
  (** Test whether a set is empty or not. *)

  Parameter mem : elt -> t -> bool.
  (** [mem x s] tests whether [x] belongs to the set [s]. *)

  Parameter add : elt -> t -> t.
  (** [add x s] returns a set containing all elements of [s],
  plus [x]. If [x] was already in [s], [s] is returned unchanged. *)

  Parameter singleton : elt -> t.
  (** [singleton x] returns the one-element set containing only [x]. *)

  Parameter remove : elt -> t -> t.
  (** [remove x s] returns a set containing all elements of [s],
  except [x]. If [x] was not in [s], [s] is returned unchanged. *)

  Parameter union : t -> t -> t.
  (** Set union. *)

  Parameter inter : t -> t -> t.
  (** Set intersection. *)

  Parameter diff : t -> t -> t.
  (** Set difference. *)

  Parameter equal : t -> t -> bool.
  (** [equal s1 s2] tests whether the sets [s1] and [s2] are
  equal, that is, contain equal elements. *)

  Parameter subset : t -> t -> bool.
  (** [subset s1 s2] tests whether the set [s1] is a subset of
  the set [s2]. *)

  Parameter fold : forall A : Type, (elt -> A -> A) -> t -> A -> A.
  (** [fold f s a] computes [(f xN ... (f x2 (f x1 a))...)],
  where [x1 ... xN] are the elements of [s].
  The order in which elements of [s] are presented to [f] is
  unspecified. *)

  Parameter for_all : (elt -> bool) -> t -> bool.
  (** [for_all p s] checks if all elements of the set
  satisfy the predicate [p]. *)

  Parameter exists_ : (elt -> bool) -> t -> bool.
  (** [exists p s] checks if at least one element of
  the set satisfies the predicate [p]. *)

  Parameter filter : (elt -> bool) -> t -> t.
  (** [filter p s] returns the set of all elements in [s]
  that satisfy predicate [p]. *)

  Parameter partition : (elt -> bool) -> t -> t * t.
  (** [partition p s] returns a pair of sets [(s1, s2)], where
  [s1] is the set of all the elements of [s] that satisfy the
  predicate [p], and [s2] is the set of all the elements of
  [s] that do not satisfy [p]. *)

  Parameter cardinal : t -> nat.
  (** Return the number of elements of a set. *)

  Parameter elements : t -> list elt.
  (** Return the list of all elements of the given set, in any order. *)

  Parameter choose : t -> option elt.
  (** Return one element of the given set, or [None] if
  the set is empty. Which element is chosen is unspecified.
  Equal sets could return different elements. *)

End HasWOps.

Module Type WOps (E : DecidableType).
  Definition elt := E.t.
  Parameter t : Type. (** the abstract type of sets *)
  Include HasWOps.
End WOps.


(** ** Functorial signature for weak sets

    Weak sets are sets without ordering on base elements, only
    a decidable equality. *)

Module Type WSetsOn (E : DecidableType).
  (** First, we ask for all the functions *)
  Include WOps E.

  (** Logical predicates *)
  Parameter In : elt -> t -> Prop.
  Declare Instance In_compat : Proper (E.eq==>eq==>iff) In.

  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.

  Notation "s  [=]  t" := (Equal s t) (at level 70, no associativity).
  Notation "s  [<=]  t" := (Subset s t) (at level 70, no associativity).

  Definition eq : t -> t -> Prop := Equal.
  Include IsEq. (** [eq] is obviously an equivalence, for subtyping only *)
  Include HasEqDec.

  (** Specifications of set operators *)

  Section Spec.
  Variable s s': t.
  Variable x y : elt.
  Variable f : elt -> bool.
  Notation compatb := (Proper (E.eq==>Logic.eq)) (only parsing).

  Parameter mem_spec : mem x s = true <-> In x s.
  Parameter equal_spec : equal s s' = true <-> s[=]s'.
  Parameter subset_spec : subset s s' = true <-> s[<=]s'.
  Parameter empty_spec : Empty empty.
  Parameter is_empty_spec : is_empty s = true <-> Empty s.
  Parameter add_spec : In y (add x s) <-> E.eq y x \/ In y s.
  Parameter remove_spec : In y (remove x s) <-> In y s /\ ~E.eq y x.
  Parameter singleton_spec : In y (singleton x) <-> E.eq y x.
  Parameter union_spec : In x (union s s') <-> In x s \/ In x s'.
  Parameter inter_spec : In x (inter s s') <-> In x s /\ In x s'.
  Parameter diff_spec : In x (diff s s') <-> In x s /\ ~In x s'.
  Parameter fold_spec : forall (A : Type) (i : A) (f : elt -> A -> A),
    fold f s i = fold_left (flip f) (elements s) i.
  Parameter cardinal_spec : cardinal s = length (elements s).
  Parameter filter_spec : compatb f ->
    (In x (filter f s) <-> In x s /\ f x = true).
  Parameter for_all_spec : compatb f ->
    (for_all f s = true <-> For_all (fun x => f x = true) s).
  Parameter exists_spec : compatb f ->
    (exists_ f s = true <-> Exists (fun x => f x = true) s).
  Parameter partition_spec1 : compatb f ->
    fst (partition f s) [=] filter f s.
  Parameter partition_spec2 : compatb f ->
    snd (partition f s) [=] filter (fun x => negb (f x)) s.
  Parameter elements_spec1 : InA E.eq x (elements s) <-> In x s.
  (** When compared with ordered sets, here comes the only
      property that is really weaker: *)
  Parameter elements_spec2w : NoDupA E.eq (elements s).
  Parameter choose_spec1 : choose s = Some x -> In x s.
  Parameter choose_spec2 : choose s = None -> Empty s.

  End Spec.

End WSetsOn.

(** ** Static signature for weak sets

    Similar to the functorial signature [WSetsOn], except that the
    module [E] of base elements is incorporated in the signature. *)

Module Type WSets.
  Declare Module E : DecidableType.
  Include WSetsOn E.
End WSets.

(** ** Functorial signature for sets on ordered elements

    Based on [WSetsOn], plus ordering on sets and [min_elt] and [max_elt]
    and some stronger specifications for other functions. *)

Module Type HasOrdOps (Import T:TypElt).

  Parameter compare : t -> t -> comparison.
  (** Total ordering between sets. Can be used as the ordering function
  for doing sets of sets. *)

  Parameter min_elt : t -> option elt.
  (** Return the smallest element of the given set
  (with respect to the [E.compare] ordering),
  or [None] if the set is empty. *)

  Parameter max_elt : t -> option elt.
  (** Same as [min_elt], but returns the largest element of the
  given set. *)

End HasOrdOps.

Module Type Ops (E : OrderedType) := WOps E <+ HasOrdOps.


Module Type SetsOn (E : OrderedType).
  Include WSetsOn E <+ HasOrdOps <+ HasLt <+ IsStrOrder.

  Section Spec.
  Variable s s': t.
  Variable x y : elt.

  Parameter compare_spec : CompSpec eq lt s s' (compare s s').

  (** Additional specification of [elements] *)
  Parameter elements_spec2 : sort E.lt (elements s).

  (** Remark: since [fold] is specified via [elements], this stronger
   specification of [elements] has an indirect impact on [fold],
   which can now be proved to receive elements in increasing order.
  *)

  Parameter min_elt_spec1 : min_elt s = Some x -> In x s.
  Parameter min_elt_spec2 : min_elt s = Some x -> In y s -> ~ E.lt y x.
  Parameter min_elt_spec3 : min_elt s = None -> Empty s.

  Parameter max_elt_spec1 : max_elt s = Some x -> In x s.
  Parameter max_elt_spec2 : max_elt s = Some x -> In y s -> ~ E.lt x y.
  Parameter max_elt_spec3 : max_elt s = None -> Empty s.

  (** Additional specification of [choose] *)
  Parameter choose_spec3 : choose s = Some x -> choose s' = Some y ->
    Equal s s' -> E.eq x y.

  End Spec.

End SetsOn.


(** ** Static signature for sets on ordered elements

    Similar to the functorial signature [SetsOn], except that the
    module [E] of base elements is incorporated in the signature. *)

Module Type Sets.
  Declare Module E : OrderedType.
  Include SetsOn E.
End Sets.

Module Type S := Sets.


(** ** Some subtyping tests
<<
WSetsOn ---> WSets
 |           |
 |           |
 V           V
SetsOn  ---> Sets

Module S_WS (M : Sets) <: WSets := M.
Module Sfun_WSfun (E:OrderedType)(M : SetsOn E) <: WSetsOn E := M.
Module S_Sfun (M : Sets) <: SetsOn M.E := M.
Module WS_WSfun (M : WSets) <: WSetsOn M.E := M.
>>
*)



(** ** Signatures for set representations with ill-formed values.

   Motivation:

   For many implementation of finite sets (AVL trees, sorted
   lists, lists without duplicates), we use the same two-layer
   approach:

   - A first module deals with the datatype (eg. list or tree) without
   any restriction on the values we consider. In this module (named
   "Raw" in the past), some results are stated under the assumption
   that some invariant (e.g. sortedness) holds for the input sets. We
   also prove that this invariant is preserved by set operators.

   - A second module implements the exact Sets interface by
   using a subtype, for instance [{ l : list A | sorted l }].
   This module is a mere wrapper around the first Raw module.

   With the interfaces below, we give some respectability to
   the "Raw" modules. This allows the interested users to directly
   access them via the interfaces. Even better, we can build once
   and for all a functor doing the transition between Raw and usual Sets.

   Description:

   The type [t] of sets may contain ill-formed values on which our
   set operators may give wrong answers. In particular, [mem]
   may not see a element in a ill-formed set (think for instance of a
   unsorted list being given to an optimized [mem] that stops
   its search as soon as a strictly larger element is encountered).

   Unlike optimized operators, the [In] predicate is supposed to
   always be correct, even on ill-formed sets. Same for [Equal] and
   other logical predicates.

   A predicate parameter [Ok] is used to discriminate between
   well-formed and ill-formed values. Some lemmas hold only on sets
   validating [Ok]. This predicate [Ok] is required to be
   preserved by set operators. Moreover, a boolean function [isok]
   should exist for identifying (at least some of) the well-formed sets.

*)


Module Type WRawSets (E : DecidableType).
  (** First, we ask for all the functions *)
  Include WOps E.

  (** Is a set well-formed or ill-formed ? *)

  Parameter IsOk : t -> Prop.
  Class Ok (s:t) : Prop := ok : IsOk s.

  (** In order to be able to validate (at least some) particular sets as
      well-formed, we ask for a boolean function for (semi-)deciding
      predicate [Ok]. If [Ok] isn't decidable, [isok] may be the
      always-false function. *)
  Parameter isok : t -> bool.
  Declare Instance isok_Ok s `(isok s = true) : Ok s | 10.

  (** Logical predicates *)
  Parameter In : elt -> t -> Prop.
  Declare Instance In_compat : Proper (E.eq==>eq==>iff) In.

  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.

  Notation "s  [=]  t" := (Equal s t) (at level 70, no associativity).
  Notation "s  [<=]  t" := (Subset s t) (at level 70, no associativity).

  Definition eq : t -> t -> Prop := Equal.
  Declare Instance eq_equiv : Equivalence eq.

  (** First, all operations are compatible with the well-formed predicate. *)

  Declare Instance empty_ok : Ok empty.
  Declare Instance add_ok s x `(Ok s) : Ok (add x s).
  Declare Instance remove_ok s x `(Ok s) : Ok (remove x s).
  Declare Instance singleton_ok x : Ok (singleton x).
  Declare Instance union_ok s s' `(Ok s, Ok s') : Ok (union s s').
  Declare Instance inter_ok s s' `(Ok s, Ok s') : Ok (inter s s').
  Declare Instance diff_ok s s' `(Ok s, Ok s') : Ok (diff s s').
  Declare Instance filter_ok s f `(Ok s) : Ok (filter f s).
  Declare Instance partition_ok1 s f `(Ok s) : Ok (fst (partition f s)).
  Declare Instance partition_ok2 s f `(Ok s) : Ok (snd (partition f s)).

  (** Now, the specifications, with constraints on the input sets. *)

  Section Spec.
  Variable s s': t.
  Variable x y : elt.
  Variable f : elt -> bool.
  Notation compatb := (Proper (E.eq==>Logic.eq)) (only parsing).

  Parameter mem_spec : forall `{Ok s}, mem x s = true <-> In x s.
  Parameter equal_spec : forall `{Ok s, Ok s'},
    equal s s' = true <-> s[=]s'.
  Parameter subset_spec : forall `{Ok s, Ok s'},
    subset s s' = true <-> s[<=]s'.
  Parameter empty_spec : Empty empty.
  Parameter is_empty_spec : is_empty s = true <-> Empty s.
  Parameter add_spec : forall `{Ok s},
    In y (add x s) <-> E.eq y x \/ In y s.
  Parameter remove_spec : forall `{Ok s},
    In y (remove x s) <-> In y s /\ ~E.eq y x.
  Parameter singleton_spec : In y (singleton x) <-> E.eq y x.
  Parameter union_spec : forall `{Ok s, Ok s'},
    In x (union s s') <-> In x s \/ In x s'.
  Parameter inter_spec : forall `{Ok s, Ok s'},
    In x (inter s s') <-> In x s /\ In x s'.
  Parameter diff_spec : forall `{Ok s, Ok s'},
    In x (diff s s') <-> In x s /\ ~In x s'.
  Parameter fold_spec : forall (A : Type) (i : A) (f : elt -> A -> A),
    fold f s i = fold_left (flip f) (elements s) i.
  Parameter cardinal_spec : forall `{Ok s},
    cardinal s = length (elements s).
  Parameter filter_spec : compatb f ->
    (In x (filter f s) <-> In x s /\ f x = true).
  Parameter for_all_spec : compatb f ->
    (for_all f s = true <-> For_all (fun x => f x = true) s).
  Parameter exists_spec : compatb f ->
    (exists_ f s = true <-> Exists (fun x => f x = true) s).
  Parameter partition_spec1 : compatb f ->
    fst (partition f s) [=] filter f s.
  Parameter partition_spec2 : compatb f ->
    snd (partition f s) [=] filter (fun x => negb (f x)) s.
  Parameter elements_spec1 : InA E.eq x (elements s) <-> In x s.
  Parameter elements_spec2w : forall `{Ok s}, NoDupA E.eq (elements s).
  Parameter choose_spec1 : choose s = Some x -> In x s.
  Parameter choose_spec2 : choose s = None -> Empty s.

  End Spec.

End WRawSets.

(** From weak raw sets to weak usual sets *)

Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E.

 (** We avoid creating induction principles for the Record *)
 Local Unset Elimination Schemes.
 Local Unset Case Analysis Schemes.

 Definition elt := E.t.

 Record t_ := Mkt {this :> M.t; is_ok : M.Ok this}.
 Definition t := t_.
 Implicit Arguments Mkt [ [is_ok] ].
 Hint Resolve is_ok : typeclass_instances.

 Definition In (x : elt)(s : t) := M.In x s.(this).
 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, In x s -> P x.
 Definition Exists (P : elt -> Prop)(s : t) := exists x, In x s /\ P x.

 Definition mem (x : elt)(s : t) := M.mem x s.
 Definition add (x : elt)(s : t) : t := Mkt (M.add x s).
 Definition remove (x : elt)(s : t) : t := Mkt (M.remove x s).
 Definition singleton (x : elt) : t := Mkt (M.singleton x).
 Definition union (s s' : t) : t := Mkt (M.union s s').
 Definition inter (s s' : t) : t := Mkt (M.inter s s').
 Definition diff (s s' : t) : t := Mkt (M.diff s s').
 Definition equal (s s' : t) := M.equal s s'.
 Definition subset (s s' : t) := M.subset s s'.
 Definition empty : t := Mkt M.empty.
 Definition is_empty (s : t) := M.is_empty s.
 Definition elements (s : t) : list elt := M.elements s.
 Definition choose (s : t) : option elt := M.choose s.
 Definition fold (A : Type)(f : elt -> A -> A)(s : t) : A -> A := M.fold f s.
 Definition cardinal (s : t) := M.cardinal s.
 Definition filter (f : elt -> bool)(s : t) : t := Mkt (M.filter f s).
 Definition for_all (f : elt -> bool)(s : t) := M.for_all f s.
 Definition exists_ (f : elt -> bool)(s : t) := M.exists_ f s.
 Definition partition (f : elt -> bool)(s : t) : t * t :=
   let p := M.partition f s in (Mkt (fst p), Mkt (snd p)).

 Instance In_compat : Proper (E.eq==>eq==>iff) In.
 Proof. repeat red. intros; apply M.In_compat; congruence. Qed.

 Definition eq : t -> t -> Prop := Equal.

 Instance eq_equiv : Equivalence eq.
 Proof. firstorder. Qed.

 Definition eq_dec : forall (s s':t), { eq s s' }+{ ~eq s s' }.
 Proof.
  intros (s,Hs) (s',Hs').
  change ({M.Equal s s'}+{~M.Equal s s'}).
  destruct (M.equal s s') as [ ]_eqn:H; [left|right];
   rewrite <- M.equal_spec; congruence.
 Defined.


 Section Spec.
  Variable s s' : t.
  Variable x y : elt.
  Variable f : elt -> bool.
  Notation compatb := (Proper (E.eq==>Logic.eq)) (only parsing).

  Lemma mem_spec : mem x s = true <-> In x s.
  Proof. exact (@M.mem_spec _ _ _). Qed.
  Lemma equal_spec : equal s s' = true <-> Equal s s'.
  Proof. exact (@M.equal_spec _ _ _ _). Qed.
  Lemma subset_spec : subset s s' = true <-> Subset s s'.
  Proof. exact (@M.subset_spec _ _ _ _). Qed.
  Lemma empty_spec : Empty empty.
  Proof. exact M.empty_spec. Qed.
  Lemma is_empty_spec : is_empty s = true <-> Empty s.
  Proof. exact (@M.is_empty_spec _). Qed.
  Lemma add_spec : In y (add x s) <-> E.eq y x \/ In y s.
  Proof. exact (@M.add_spec _ _ _ _). Qed.
  Lemma remove_spec : In y (remove x s) <-> In y s /\ ~E.eq y x.
  Proof. exact (@M.remove_spec _ _ _ _). Qed.
  Lemma singleton_spec : In y (singleton x) <-> E.eq y x.
  Proof. exact (@M.singleton_spec _ _). Qed.
  Lemma union_spec : In x (union s s') <-> In x s \/ In x s'.
  Proof. exact (@M.union_spec _ _ _ _ _). Qed.
  Lemma inter_spec : In x (inter s s') <-> In x s /\ In x s'.
  Proof. exact (@M.inter_spec _ _ _ _ _). Qed.
  Lemma diff_spec : In x (diff s s') <-> In x s /\ ~In x s'.
  Proof. exact (@M.diff_spec _ _ _ _ _). Qed.
  Lemma fold_spec : forall (A : Type) (i : A) (f : elt -> A -> A),
      fold f s i = fold_left (fun a e => f e a) (elements s) i.
  Proof. exact (@M.fold_spec _). Qed.
  Lemma cardinal_spec : cardinal s = length (elements s).
  Proof. exact (@M.cardinal_spec s _). Qed.
  Lemma filter_spec : compatb f ->
    (In x (filter f s) <-> In x s /\ f x = true).
  Proof. exact (@M.filter_spec _ _ _). Qed.
  Lemma for_all_spec : compatb f ->
    (for_all f s = true <-> For_all (fun x => f x = true) s).
  Proof. exact (@M.for_all_spec _ _). Qed.
  Lemma exists_spec : compatb f ->
    (exists_ f s = true <-> Exists (fun x => f x = true) s).
  Proof. exact (@M.exists_spec _ _). Qed.
  Lemma partition_spec1 : compatb f -> Equal (fst (partition f s)) (filter f s).
  Proof. exact (@M.partition_spec1 _ _). Qed.
  Lemma partition_spec2 : compatb f ->
      Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
  Proof. exact (@M.partition_spec2 _ _). Qed.
  Lemma elements_spec1 : InA E.eq x (elements s) <-> In x s.
  Proof. exact (@M.elements_spec1 _ _). Qed.
  Lemma elements_spec2w : NoDupA E.eq (elements s).
  Proof. exact (@M.elements_spec2w _ _). Qed.
  Lemma choose_spec1 : choose s = Some x -> In x s.
  Proof. exact (@M.choose_spec1 _ _). Qed.
  Lemma choose_spec2 : choose s = None -> Empty s.
  Proof. exact (@M.choose_spec2 _). Qed.

 End Spec.

End WRaw2SetsOn.

Module WRaw2Sets (D:DecidableType)(M:WRawSets D) <: WSets with Module E := D.
  Module E := D.
  Include WRaw2SetsOn D M.
End WRaw2Sets.

(** Same approach for ordered sets *)

Module Type RawSets (E : OrderedType).
  Include WRawSets E <+ HasOrdOps <+ HasLt <+ IsStrOrder.

  Section Spec.
  Variable s s': t.
  Variable x y : elt.

  (** Specification of [compare] *)
  Parameter compare_spec : forall `{Ok s, Ok s'}, CompSpec eq lt s s' (compare s s').

  (** Additional specification of [elements] *)
  Parameter elements_spec2 : forall `{Ok s}, sort E.lt (elements s).

  (** Specification of [min_elt] *)
  Parameter min_elt_spec1 : min_elt s = Some x -> In x s.
  Parameter min_elt_spec2 : forall `{Ok s}, min_elt s = Some x -> In y s -> ~ E.lt y x.
  Parameter min_elt_spec3 : min_elt s = None -> Empty s.

  (** Specification of [max_elt] *)
  Parameter max_elt_spec1 : max_elt s = Some x -> In x s.
  Parameter max_elt_spec2 : forall `{Ok s}, max_elt s = Some x -> In y s -> ~ E.lt x y.
  Parameter max_elt_spec3 : max_elt s = None -> Empty s.

  (** Additional specification of [choose] *)
  Parameter choose_spec3 : forall `{Ok s, Ok s'},
    choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y.

  End Spec.

End RawSets.

(** From Raw to usual sets *)

Module Raw2SetsOn (O:OrderedType)(M:RawSets O) <: SetsOn O.
  Include WRaw2SetsOn O M.

  Definition compare (s s':t) := M.compare s s'.
  Definition min_elt (s:t) : option elt := M.min_elt s.
  Definition max_elt (s:t) : option elt := M.max_elt s.
  Definition lt (s s':t) := M.lt s s'.

  (** Specification of [lt] *)
  Instance lt_strorder : StrictOrder lt.
  Proof. constructor ; unfold lt; red.
    unfold complement. red. intros. apply (irreflexivity H).
    intros. transitivity y; auto.
  Qed.

  Instance lt_compat : Proper (eq==>eq==>iff) lt.
  Proof.
  repeat red. unfold eq, lt.
  intros (s1,p1) (s2,p2) E (s1',p1') (s2',p2') E'; simpl.
  change (M.eq s1 s2) in E.
  change (M.eq s1' s2') in E'.
  rewrite E,E'; intuition.
  Qed.

  Section Spec.
  Variable s s' s'' : t.
  Variable x y : elt.

  Lemma compare_spec : CompSpec eq lt s s' (compare s s').
  Proof. unfold compare; destruct (@M.compare_spec s s' _ _); auto. Qed.

  (** Additional specification of [elements] *)
  Lemma elements_spec2 : sort O.lt (elements s).
  Proof. exact (@M.elements_spec2 _ _). Qed.

  (** Specification of [min_elt] *)
  Lemma min_elt_spec1 : min_elt s = Some x -> In x s.
  Proof. exact (@M.min_elt_spec1 _ _). Qed.
  Lemma min_elt_spec2 : min_elt s = Some x -> In y s -> ~ O.lt y x.
  Proof. exact (@M.min_elt_spec2 _ _ _ _). Qed.
  Lemma min_elt_spec3 : min_elt s = None -> Empty s.
  Proof. exact (@M.min_elt_spec3 _). Qed.

  (** Specification of [max_elt] *)
  Lemma max_elt_spec1 : max_elt s = Some x -> In x s.
  Proof. exact (@M.max_elt_spec1 _ _). Qed.
  Lemma max_elt_spec2 : max_elt s = Some x -> In y s -> ~ O.lt x y.
  Proof. exact (@M.max_elt_spec2 _ _ _ _). Qed.
  Lemma max_elt_spec3 : max_elt s = None -> Empty s.
  Proof. exact (@M.max_elt_spec3 _). Qed.

  (** Additional specification of [choose] *)
  Lemma choose_spec3 :
    choose s = Some x -> choose s' = Some y -> Equal s s' -> O.eq x y.
  Proof. exact (@M.choose_spec3 _ _ _ _ _ _). Qed.

  End Spec.

End Raw2SetsOn.

Module Raw2Sets (O:OrderedType)(M:RawSets O) <: Sets with Module E := O.
  Module E := O.
  Include Raw2SetsOn O M.
End Raw2Sets.


(** We provide an ordering for sets-as-sorted-lists *)

Module MakeListOrdering (O:OrderedType).
 Module MO:=OrderedTypeFacts O.

 Local Notation t := (list O.t).
 Local Notation In := (InA O.eq).

 Definition eq s s' := forall x, In x s <-> In x s'.

 Instance eq_equiv : Equivalence eq.

 Inductive lt_list : t -> t -> Prop :=
    | lt_nil : forall x s, lt_list nil (x :: s)
    | lt_cons_lt : forall x y s s',
        O.lt x y -> lt_list (x :: s) (y :: s')
    | lt_cons_eq : forall x y s s',
        O.eq x y -> lt_list s s' -> lt_list (x :: s) (y :: s').
 Hint Constructors lt_list.

 Definition lt := lt_list.
 Hint Unfold lt.

 Instance lt_strorder : StrictOrder lt.
 Proof.
 split.
 (* irreflexive *)
 assert (forall s s', s=s' -> ~lt s s').
  red; induction 2.
  discriminate.
  inversion H; subst.
  apply (StrictOrder_Irreflexive y); auto.
  inversion H; subst; auto.
 intros s Hs; exact (H s s (eq_refl s) Hs).
 (* transitive *)
 intros s s' s'' H; generalize s''; clear s''; elim H.
 intros x l s'' H'; inversion_clear H'; auto.
 intros x x' l l' E s'' H'; inversion_clear H'; auto.
 constructor 2. transitivity x'; auto.
 constructor 2. rewrite <- H0; auto.
 intros.
 inversion_clear H3.
 constructor 2. rewrite H0; auto.
 constructor 3; auto. transitivity y; auto. unfold lt in *; auto.
 Qed.

 Instance lt_compat' :
  Proper (eqlistA O.eq==>eqlistA O.eq==>iff) lt.
 Proof.
 apply proper_sym_impl_iff_2; auto with *.
 intros s1 s1' E1 s2 s2' E2 H.
 revert s1' E1 s2' E2.
 induction H; intros; inversion_clear E1; inversion_clear E2.
 constructor 1.
 constructor 2. MO.order.
 constructor 3. MO.order. unfold lt in *; auto.
 Qed.

 Lemma eq_cons :
  forall l1 l2 x y,
  O.eq x y -> eq l1 l2 -> eq (x :: l1) (y :: l2).
 Proof.
  unfold eq; intros l1 l2 x y Exy E12 z.
  split; inversion_clear 1.
  left; MO.order. right; rewrite <- E12; auto.
  left; MO.order. right; rewrite E12; auto.
 Qed.
 Hint Resolve eq_cons.

 Lemma cons_CompSpec : forall c x1 x2 l1 l2, O.eq x1 x2 ->
  CompSpec eq lt l1 l2 c -> CompSpec eq lt (x1::l1) (x2::l2) c.
 Proof.
  destruct c; simpl; inversion_clear 2; auto with relations.
 Qed.
 Hint Resolve cons_CompSpec.

End MakeListOrdering.