1
(***********************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
4
(* \VV/ *************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(***********************************************************************)
9
(* $Id: FSetEqProperties.v 11720 2008-12-28 07:12:15Z letouzey $ *)
11
(** * Finite sets library *)
13
(** This module proves many properties of finite sets that
14
are consequences of the axiomatization in [FsetInterface]
15
Contrary to the functor in [FsetProperties] it uses
16
sets operations instead of predicates over sets, i.e.
17
[mem x s=true] instead of [In x s],
18
[equal s s'=true] instead of [Equal s s'], etc. *)
20
Require Import FSetProperties Zerob Sumbool Omega DecidableTypeEx.
22
Module WEqProperties_fun (Import E:DecidableType)(M:WSfun E).
23
Module Import MP := WProperties_fun E M.
27
Definition Add := MP.Add.
29
Section BasicProperties.
31
(** Some old specifications written with boolean equalities. *)
37
E.eq x y -> mem x s=mem y s.
39
intro H; rewrite H; auto.
43
(forall a, mem a s=mem a s') -> equal s s'=true.
45
intros; apply equal_1; unfold Equal; intros.
46
do 2 rewrite mem_iff; rewrite H; tauto.
50
equal s s'=true -> forall a, mem a s=mem a s'.
52
intros; rewrite (equal_2 H); auto.
56
(forall a, mem a s=true->mem a s'=true) -> subset s s'=true.
58
intros; apply subset_1; unfold Subset; intros a.
59
do 2 rewrite mem_iff; auto.
63
subset s s'=true -> forall a, mem a s=true -> mem a s'=true.
65
intros H a; do 2 rewrite <- mem_iff; apply subset_2; auto.
68
Lemma empty_mem: mem x empty=false.
70
rewrite <- not_mem_iff; auto with set.
73
Lemma is_empty_equal_empty: is_empty s = equal s empty.
75
apply bool_1; split; intros.
77
rewrite <- is_empty_iff; auto with set.
80
Lemma choose_mem_1: choose s=Some x -> mem x s=true.
85
Lemma choose_mem_2: choose s=None -> is_empty s=true.
90
Lemma add_mem_1: mem x (add x s)=true.
95
Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s.
100
Lemma remove_mem_1: mem x (remove x s)=false.
102
rewrite <- not_mem_iff; auto with set.
105
Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s.
110
Lemma singleton_equal_add:
111
equal (singleton x) (add x empty)=true.
113
rewrite (singleton_equal_add x); auto with set.
117
mem x (union s s')=mem x s || mem x s'.
123
mem x (inter s s')=mem x s && mem x s'.
129
mem x (diff s s')=mem x s && negb (mem x s').
134
(** properties of [mem] *)
136
Lemma mem_3 : ~In x s -> mem x s=false.
138
intros; rewrite <- not_mem_iff; auto.
141
Lemma mem_4 : mem x s=false -> ~In x s.
143
intros; rewrite not_mem_iff; auto.
146
(** Properties of [equal] *)
148
Lemma equal_refl: equal s s=true.
153
Lemma equal_sym: equal s s'=equal s' s.
155
intros; apply bool_1; do 2 rewrite <- equal_iff; intuition.
159
equal s s'=true -> equal s' s''=true -> equal s s''=true.
161
intros; rewrite (equal_2 H); auto.
165
equal s s'=true -> equal s s''=equal s' s''.
167
intros; rewrite (equal_2 H); auto.
170
Lemma equal_cardinal:
171
equal s s'=true -> cardinal s=cardinal s'.
176
(* Properties of [subset] *)
178
Lemma subset_refl: subset s s=true.
183
Lemma subset_antisym:
184
subset s s'=true -> subset s' s=true -> equal s s'=true.
190
subset s s'=true -> subset s' s''=true -> subset s s''=true.
192
do 3 rewrite <- subset_iff; intros.
193
apply subset_trans with s'; auto.
197
equal s s'=true -> subset s s'=true.
202
(** Properties of [choose] *)
205
is_empty s=false -> {x:elt|choose s=Some x /\ mem x s=true}.
208
generalize (@choose_1 s) (@choose_2 s).
209
destruct (choose s);intros.
210
exists e;auto with set.
211
generalize (H1 (refl_equal None)); clear H1.
212
intros; rewrite (is_empty_1 H1) in H; discriminate.
215
Lemma choose_mem_4: choose empty=None.
217
generalize (@choose_1 empty).
218
case (@choose empty);intros;auto.
219
elim (@empty_1 e); auto.
222
(** Properties of [add] *)
225
mem y s=true -> mem y (add x s)=true.
231
mem x s=true -> equal (add x s) s=true.
236
(** Properties of [remove] *)
239
mem y (remove x s)=true -> mem y s=true.
241
rewrite remove_b; intros H;destruct (andb_prop _ _ H); auto.
245
mem x s=false -> equal (remove x s) s=true.
247
intros; apply equal_1; apply remove_equal.
248
rewrite not_mem_iff; auto.
252
mem x s=true -> equal (add x (remove x s)) s=true.
254
intros; apply equal_1; apply add_remove; auto with set.
258
mem x s=false -> equal (remove x (add x s)) s=true.
260
intros; apply equal_1; apply remove_add; auto.
261
rewrite not_mem_iff; auto.
264
(** Properties of [is_empty] *)
266
Lemma is_empty_cardinal: is_empty s = zerob (cardinal s).
268
intros; apply bool_1; split; intros.
269
rewrite MP.cardinal_1; simpl; auto with set.
270
assert (cardinal s = 0) by (apply zerob_true_elim; auto).
274
(** Properties of [singleton] *)
276
Lemma singleton_mem_1: mem x (singleton x)=true.
281
Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false.
283
intros; rewrite singleton_b.
284
unfold eqb; destruct (E.eq_dec x y); intuition.
287
Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y.
289
intros; apply singleton_1; auto with set.
292
(** Properties of [union] *)
295
equal (union s s') (union s' s)=true.
300
Lemma union_subset_equal:
301
subset s s'=true -> equal (union s s') s'=true.
307
equal s s'=true-> equal (union s s'') (union s' s'')=true.
313
equal s' s''=true-> equal (union s s') (union s s'')=true.
319
equal (union (union s s') s'') (union s (union s' s''))=true.
324
Lemma add_union_singleton:
325
equal (add x s) (union (singleton x) s)=true.
331
equal (union (add x s) s') (add x (union s s'))=true.
336
(* caracterisation of [union] via [subset] *)
338
Lemma union_subset_1: subset s (union s s')=true.
343
Lemma union_subset_2: subset s' (union s s')=true.
348
Lemma union_subset_3:
349
subset s s''=true -> subset s' s''=true ->
350
subset (union s s') s''=true.
352
intros; apply subset_1; apply union_subset_3; auto with set.
355
(** Properties of [inter] *)
357
Lemma inter_sym: equal (inter s s') (inter s' s)=true.
362
Lemma inter_subset_equal:
363
subset s s'=true -> equal (inter s s') s=true.
369
equal s s'=true -> equal (inter s s'') (inter s' s'')=true.
375
equal s' s''=true -> equal (inter s s') (inter s s'')=true.
381
equal (inter (inter s s') s'') (inter s (inter s' s''))=true.
387
equal (inter (union s s') s'') (union (inter s s'') (inter s' s''))=true.
393
equal (union (inter s s') s'') (inter (union s s'') (union s' s''))=true.
398
Lemma inter_add_1: mem x s'=true ->
399
equal (inter (add x s) s') (add x (inter s s'))=true.
404
Lemma inter_add_2: mem x s'=false ->
405
equal (inter (add x s) s') (inter s s')=true.
407
intros; apply equal_1; apply inter_add_2.
408
rewrite not_mem_iff; auto.
411
(* caracterisation of [union] via [subset] *)
413
Lemma inter_subset_1: subset (inter s s') s=true.
418
Lemma inter_subset_2: subset (inter s s') s'=true.
423
Lemma inter_subset_3:
424
subset s'' s=true -> subset s'' s'=true ->
425
subset s'' (inter s s')=true.
427
intros; apply subset_1; apply inter_subset_3; auto with set.
430
(** Properties of [diff] *)
432
Lemma diff_subset: subset (diff s s') s=true.
437
Lemma diff_subset_equal:
438
subset s s'=true -> equal (diff s s') empty=true.
443
Lemma remove_inter_singleton:
444
equal (remove x s) (diff s (singleton x))=true.
449
Lemma diff_inter_empty:
450
equal (inter (diff s s') (inter s s')) empty=true.
455
Lemma diff_inter_all:
456
equal (union (diff s s') (inter s s')) s=true.
463
Hint Immediate empty_mem is_empty_equal_empty add_mem_1
464
remove_mem_1 singleton_equal_add union_mem inter_mem
465
diff_mem equal_sym add_remove remove_add : set.
466
Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1
467
choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal
468
subset_refl subset_equal subset_antisym
469
add_mem_3 add_equal remove_mem_3 remove_equal : set.
472
(** General recursion principle *)
474
Lemma set_rec: forall (P:t->Type),
475
(forall s s', equal s s'=true -> P s -> P s') ->
476
(forall s x, mem x s=false -> P s -> P (add x s)) ->
477
P empty -> forall s, P s.
480
apply set_induction; auto; intros.
481
apply X with empty; auto with set.
482
apply X with (add x s0); auto with set.
483
apply equal_1; intro a; rewrite add_iff; rewrite (H0 a); tauto.
484
apply X0; auto with set; apply mem_3; auto.
487
(** Properties of [fold] *)
489
Lemma exclusive_set : forall s s' x,
490
~(In x s/\In x s') <-> mem x s && mem x s'=false.
492
intros; do 2 rewrite mem_iff.
493
destruct (mem x s); destruct (mem x s'); intuition.
497
Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA).
498
Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
500
Variables (s s':t)(x:elt).
502
Lemma fold_empty: (fold f empty i) = i.
504
apply fold_empty; auto.
508
equal s s'=true -> eqA (fold f s i) (fold f s' i).
510
intros; apply fold_equal with (eqA:=eqA); auto with set.
514
mem x s=false -> eqA (fold f (add x s) i) (f x (fold f s i)).
516
intros; apply fold_add with (eqA:=eqA); auto.
517
rewrite not_mem_iff; auto.
521
mem x s=true -> eqA (fold f (add x s) i) (fold f s i).
523
intros; apply add_fold with (eqA:=eqA); auto with set.
527
mem x s=true -> eqA (f x (fold f (remove x s) i)) (fold f s i).
529
intros; apply remove_fold_1 with (eqA:=eqA); auto with set.
533
mem x s=false -> eqA (fold f (remove x s) i) (fold f s i).
535
intros; apply remove_fold_2 with (eqA:=eqA); auto.
536
rewrite not_mem_iff; auto.
540
(forall x, mem x s && mem x s'=false) ->
541
eqA (fold f (union s s') i) (fold f s (fold f s' i)).
543
intros; apply fold_union with (eqA:=eqA); auto.
544
intros; rewrite exclusive_set; auto.
549
(** Properties of [cardinal] *)
551
Lemma add_cardinal_1:
552
forall s x, mem x s=true -> cardinal (add x s)=cardinal s.
557
Lemma add_cardinal_2:
558
forall s x, mem x s=false -> cardinal (add x s)=S (cardinal s).
560
intros; apply add_cardinal_2; auto.
561
rewrite not_mem_iff; auto.
564
Lemma remove_cardinal_1:
565
forall s x, mem x s=true -> S (cardinal (remove x s))=cardinal s.
567
intros; apply remove_cardinal_1; auto with set.
570
Lemma remove_cardinal_2:
571
forall s x, mem x s=false -> cardinal (remove x s)=cardinal s.
573
intros; apply Equal_cardinal; apply equal_2; auto with set.
576
Lemma union_cardinal:
577
forall s s', (forall x, mem x s && mem x s'=false) ->
578
cardinal (union s s')=cardinal s+cardinal s'.
580
intros; apply union_cardinal; auto; intros.
581
rewrite exclusive_set; auto.
584
Lemma subset_cardinal:
585
forall s s', subset s s'=true -> cardinal s<=cardinal s'.
587
intros; apply subset_cardinal; auto with set.
592
(** Properties of [filter] *)
594
Variable f:elt->bool.
595
Variable Comp: compat_bool E.eq f.
597
Let Comp' : compat_bool E.eq (fun x =>negb (f x)).
599
unfold compat_bool in *; intros; f_equal; auto.
602
Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x.
604
intros; apply filter_b; auto.
607
Lemma for_all_filter:
608
forall s, for_all f s=is_empty (filter (fun x => negb (f x)) s).
610
intros; apply bool_1; split; intros.
612
unfold Empty; intros.
613
rewrite filter_iff; auto.
615
rewrite <- (@for_all_iff s f) in H; auto.
616
rewrite (H a H0) in H1; discriminate.
617
apply for_all_1; auto; red; intros.
618
revert H; rewrite <- is_empty_iff.
619
unfold Empty; intro H; generalize (H x); clear H.
620
rewrite filter_iff; auto.
621
destruct (f x); auto.
624
Lemma exists_filter :
625
forall s, exists_ f s=negb (is_empty (filter f s)).
627
intros; apply bool_1; split; intros.
628
destruct (exists_2 Comp H) as (a,(Ha1,Ha2)).
630
red; intros; apply (@is_empty_2 _ H0 a); auto with set.
631
generalize (@choose_1 (filter f s)) (@choose_2 (filter f s)).
632
destruct (choose (filter f s)).
633
intros H0 _; apply exists_1; auto.
634
exists e; generalize (H0 e); rewrite filter_iff; auto.
636
rewrite (is_empty_1 (H0 (refl_equal None))) in H; auto; discriminate.
639
Lemma partition_filter_1:
640
forall s, equal (fst (partition f s)) (filter f s)=true.
645
Lemma partition_filter_2:
646
forall s, equal (snd (partition f s)) (filter (fun x => negb (f x)) s)=true.
651
Lemma filter_add_1 : forall s x, f x = true ->
652
filter f (add x s) [=] add x (filter f s).
654
red; intros; set_iff; do 2 (rewrite filter_iff; auto); set_iff.
656
rewrite <- H; apply Comp; auto.
659
Lemma filter_add_2 : forall s x, f x = false ->
660
filter f (add x s) [=] filter f s.
662
red; intros; do 2 (rewrite filter_iff; auto); set_iff.
664
assert (f x = f a) by (apply Comp; auto).
665
rewrite H in H1; rewrite H2 in H1; discriminate.
668
Lemma add_filter_1 : forall s s' x,
669
f x=true -> (Add x s s') -> (Add x (filter f s) (filter f s')).
671
unfold Add, MP.Add; intros.
672
repeat rewrite filter_iff; auto.
673
rewrite H0; clear H0.
674
assert (E.eq x y -> f y = true) by
675
(intro H0; rewrite <- (Comp _ _ H0); auto).
679
Lemma add_filter_2 : forall s s' x,
680
f x=false -> (Add x s s') -> filter f s [=] filter f s'.
682
unfold Add, MP.Add, Equal; intros.
683
repeat rewrite filter_iff; auto.
684
rewrite H0; clear H0.
685
assert (f a = true -> ~E.eq x a).
687
rewrite (Comp _ _ H1) in H.
688
rewrite H in H0; discriminate.
692
Lemma union_filter: forall f g, (compat_bool E.eq f) -> (compat_bool E.eq g) ->
693
forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s.
697
assert (compat_bool E.eq (fun x => orb (f x) (g x))).
698
unfold compat_bool; intros.
699
rewrite (H x y H1); rewrite (H0 x y H1); auto.
700
unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto.
701
assert (f a || g a = true <-> f a = true \/ g a = true).
702
split; auto with bool.
703
intro H3; destruct (orb_prop _ _ H3); auto.
707
Lemma filter_union: forall s s', filter f (union s s') [=] union (filter f s) (filter f s').
709
unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto; set_iff; tauto.
712
(** Properties of [for_all] *)
714
Lemma for_all_mem_1: forall s,
715
(forall x, (mem x s)=true->(f x)=true) -> (for_all f s)=true.
718
rewrite for_all_filter; auto.
719
rewrite is_empty_equal_empty.
720
apply equal_mem_1;intros.
721
rewrite filter_b; auto.
723
generalize (H a); case (mem a s);intros;auto.
727
Lemma for_all_mem_2: forall s,
728
(for_all f s)=true -> forall x,(mem x s)=true -> (f x)=true.
731
rewrite for_all_filter in H; auto.
732
rewrite is_empty_equal_empty in H.
733
generalize (equal_mem_2 _ _ H x).
734
rewrite filter_b; auto.
736
rewrite H0; simpl;intros.
737
replace true with (negb false);auto;apply negb_sym;auto.
741
forall s x,(mem x s)=true -> (f x)=false -> (for_all f s)=false.
744
apply (bool_eq_ind (for_all f s));intros;auto.
745
rewrite for_all_filter in H1; auto.
746
rewrite is_empty_equal_empty in H1.
747
generalize (equal_mem_2 _ _ H1 x).
748
rewrite filter_b; auto.
756
forall s, for_all f s=false -> {x:elt | mem x s=true /\ f x=false}.
759
rewrite for_all_filter in H; auto.
760
destruct (choose_mem_3 _ H) as (x,(H0,H1));intros.
762
rewrite filter_b in H1; auto.
763
elim (andb_prop _ _ H1).
765
replace false with (negb true);auto;apply negb_sym;auto.
768
(** Properties of [exists] *)
770
Lemma for_all_exists:
771
forall s, exists_ f s = negb (for_all (fun x =>negb (f x)) s).
774
rewrite for_all_b; auto.
775
rewrite exists_b; auto.
776
induction (elements s); simpl; auto.
777
destruct (f a); simpl; auto.
783
Variable f:elt->bool.
784
Variable Comp: compat_bool E.eq f.
786
Let Comp' : compat_bool E.eq (fun x =>negb (f x)).
788
unfold compat_bool in *; intros; f_equal; auto.
792
forall s, (forall x, mem x s=true->f x=false) -> exists_ f s=false.
795
rewrite for_all_exists; auto.
796
rewrite for_all_mem_1;auto with bool.
797
intros;generalize (H x H0);intros.
798
symmetry;apply negb_sym;simpl;auto.
802
forall s, exists_ f s=false -> forall x, mem x s=true -> f x=false.
805
rewrite for_all_exists in H; auto.
806
replace false with (negb true);auto;apply negb_sym;symmetry.
807
rewrite (for_all_mem_2 (fun x => negb (f x)) Comp' s);simpl;auto.
808
replace true with (negb false);auto;apply negb_sym;auto.
812
forall s x, mem x s=true -> f x=true -> exists_ f s=true.
815
rewrite for_all_exists; auto.
816
symmetry;apply negb_sym;simpl.
817
apply for_all_mem_3 with x;auto.
822
forall s, exists_ f s=true -> {x:elt | (mem x s)=true /\ (f x)=true}.
825
rewrite for_all_exists in H; auto.
826
elim (for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros.
829
replace true with (negb false);auto;apply negb_sym;auto.
830
replace false with (negb true);auto;apply negb_sym;auto.
837
(** Adding a valuation function on all elements of a set. *)
839
Definition sum (f:elt -> nat)(s:t) := fold (fun x => plus (f x)) s 0.
840
Notation compat_opL := (compat_op E.eq (@Logic.eq _)).
841
Notation transposeL := (transpose (@Logic.eq _)).
844
forall f g, compat_nat E.eq f -> compat_nat E.eq g ->
845
forall s, sum (fun x =>f x+g x) s = sum f s + sum g s.
849
assert (fc : compat_opL (fun x:elt =>plus (f x))). auto.
850
assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros; omega.
851
assert (gc : compat_opL (fun x:elt => plus (g x))). auto.
852
assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros; omega.
853
assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). auto.
854
assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega.
855
assert (st : Equivalence (@Logic.eq nat)) by (split; congruence).
856
intros s;pattern s; apply set_rec.
858
rewrite <- (fold_equal _ _ st _ fc ft 0 _ _ H).
859
rewrite <- (fold_equal _ _ st _ gc gt 0 _ _ H).
860
rewrite <- (fold_equal _ _ st _ fgc fgt 0 _ _ H); auto.
861
intros; do 3 (rewrite (fold_add _ _ st);auto).
862
rewrite H0;simpl;omega.
863
do 3 rewrite fold_empty;auto.
866
Lemma sum_filter : forall f, (compat_bool E.eq f) ->
867
forall s, (sum (fun x => if f x then 1 else 0) s) = (cardinal (filter f s)).
869
unfold sum; intros f Hf.
870
assert (st : Equivalence (@Logic.eq nat)) by (split; congruence).
871
assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))).
873
rewrite (Hf x x' H); auto.
874
assert (ct : transposeL (fun x => plus (if f x then 1 else 0))).
876
intros s;pattern s; apply set_rec.
879
rewrite <- (fold_equal _ _ st _ cc ct 0 _ _ H).
880
rewrite <- (MP.Equal_cardinal (filter_equal Hf (equal_2 H))); auto.
881
intros; rewrite (fold_add _ _ st _ cc ct); auto.
882
generalize (@add_filter_1 f Hf s0 (add x s0) x) (@add_filter_2 f Hf s0 (add x s0) x) .
883
assert (~ In x (filter f s0)).
884
intro H1; rewrite (mem_1 (filter_1 Hf H1)) in H; discriminate H.
885
case (f x); simpl; intros.
886
rewrite (MP.cardinal_2 H1 (H2 (refl_equal true) (MP.Add_add s0 x))); auto.
887
rewrite <- (MP.Equal_cardinal (H3 (refl_equal false) (MP.Add_add s0 x))); auto.
888
intros; rewrite fold_empty;auto.
889
rewrite MP.cardinal_1; auto.
890
unfold Empty; intros.
891
rewrite filter_iff; auto; set_iff; tauto.
895
forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)
897
(compat_op E.eq eqA f) -> (transpose eqA f) ->
898
(compat_op E.eq eqA g) -> (transpose eqA g) ->
899
forall (i:A)(s:t),(forall x:elt, (In x s) -> forall y, (eqA (f x y) (g x y))) ->
900
(eqA (fold f s i) (fold g s i)).
902
intros A eqA st f g fc ft gc gt i.
903
intro s; pattern s; apply set_rec; intros.
904
transitivity (fold f s0 i).
905
apply fold_equal with (eqA:=eqA); auto.
906
rewrite equal_sym; auto.
907
transitivity (fold g s0 i).
908
apply H0; intros; apply H1; auto with set.
909
elim (equal_2 H x); auto with set; intros.
910
apply fold_equal with (eqA:=eqA); auto with set.
911
transitivity (f x (fold f s0 i)).
912
apply fold_add with (eqA:=eqA); auto with set.
913
transitivity (g x (fold f s0 i)); auto with set.
914
transitivity (g x (fold g s0 i)); auto with set.
915
symmetry; apply fold_add with (eqA:=eqA); auto.
916
do 2 rewrite fold_empty; reflexivity.
920
forall f g, compat_nat E.eq f -> compat_nat E.eq g ->
921
forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s.
923
unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto.
930
End WEqProperties_fun.
932
(** Now comes variants for self-contained weak sets and for full sets.
933
For these variants, only one argument is necessary. Thanks to
934
the subtyping [WS<=S], the [EqProperties] functor which is meant to be
935
used on modules [(M:S)] can simply be an alias of [WEqProperties]. *)
937
Module WEqProperties (M:WS) := WEqProperties_fun M.E M.
938
Module EqProperties := WEqProperties.
added
removed
theories/FSets/FSetEqProperties.v
