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: FSetProperties.v 11720 2008-12-28 07:12:15Z letouzey $ *)
11
(** * Finite sets library *)
13
(** This functor derives additional properties from [FSetInterface.S].
14
Contrary to the functor in [FSetEqProperties] it uses
15
predicates over sets instead of sets operations, i.e.
16
[In x s] instead of [mem x s=true],
17
[Equal s s'] instead of [equal s s'=true], etc. *)
19
Require Export FSetInterface.
20
Require Import DecidableTypeEx FSetFacts FSetDecide.
21
Set Implicit Arguments.
22
Unset Strict Implicit.
24
Hint Unfold transpose compat_op.
25
Hint Extern 1 (Equivalence _) => constructor; congruence.
27
(** First, a functor for Weak Sets in functorial version. *)
29
Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
30
Module Import Dec := WDecide_fun E M.
31
Module Import FM := Dec.F (* FSetFacts.WFacts_fun E M *).
34
Lemma In_dec : forall x s, {In x s} + {~ In x s}.
36
intros; generalize (mem_iff s x); case (mem x s); intuition.
39
Definition Add x s s' := forall y, In y s' <-> E.eq x y \/ In y s.
41
Lemma Add_Equal : forall x s s', Add x s s' <-> s' [=] add x s.
51
Ltac expAdd := repeat rewrite Add_Equal.
53
Section BasicProperties.
55
Variable s s' s'' s1 s2 s3 : t.
58
Lemma equal_refl : s[=]s.
61
Lemma equal_sym : s[=]s' -> s'[=]s.
64
Lemma equal_trans : s1[=]s2 -> s2[=]s3 -> s1[=]s3.
67
Lemma subset_refl : s[<=]s.
70
Lemma subset_trans : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3.
73
Lemma subset_antisym : s[<=]s' -> s'[<=]s -> s[=]s'.
76
Lemma subset_equal : s[=]s' -> s[<=]s'.
79
Lemma subset_empty : empty[<=]s.
82
Lemma subset_remove_3 : s1[<=]s2 -> remove x s1 [<=] s2.
85
Lemma subset_diff : s1[<=]s3 -> diff s1 s2 [<=] s3.
88
Lemma subset_add_3 : In x s2 -> s1[<=]s2 -> add x s1 [<=] s2.
91
Lemma subset_add_2 : s1[<=]s2 -> s1[<=] add x s2.
94
Lemma in_subset : In x s1 -> s1[<=]s2 -> In x s2.
97
Lemma double_inclusion : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1.
98
Proof. intuition fsetdec. Qed.
100
Lemma empty_is_empty_1 : Empty s -> s[=]empty.
103
Lemma empty_is_empty_2 : s[=]empty -> Empty s.
106
Lemma add_equal : In x s -> add x s [=] s.
109
Lemma add_add : add x (add x' s) [=] add x' (add x s).
112
Lemma remove_equal : ~ In x s -> remove x s [=] s.
115
Lemma Equal_remove : s[=]s' -> remove x s [=] remove x s'.
118
Lemma add_remove : In x s -> add x (remove x s) [=] s.
121
Lemma remove_add : ~In x s -> remove x (add x s) [=] s.
124
Lemma singleton_equal_add : singleton x [=] add x empty.
127
Lemma remove_singleton_empty :
128
In x s -> remove x s [=] empty -> singleton x [=] s.
131
Lemma union_sym : union s s' [=] union s' s.
134
Lemma union_subset_equal : s[<=]s' -> union s s' [=] s'.
137
Lemma union_equal_1 : s[=]s' -> union s s'' [=] union s' s''.
140
Lemma union_equal_2 : s'[=]s'' -> union s s' [=] union s s''.
143
Lemma union_assoc : union (union s s') s'' [=] union s (union s' s'').
146
Lemma add_union_singleton : add x s [=] union (singleton x) s.
149
Lemma union_add : union (add x s) s' [=] add x (union s s').
152
Lemma union_remove_add_1 :
153
union (remove x s) (add x s') [=] union (add x s) (remove x s').
156
Lemma union_remove_add_2 : In x s ->
157
union (remove x s) (add x s') [=] union s s'.
160
Lemma union_subset_1 : s [<=] union s s'.
163
Lemma union_subset_2 : s' [<=] union s s'.
166
Lemma union_subset_3 : s[<=]s'' -> s'[<=]s'' -> union s s' [<=] s''.
169
Lemma union_subset_4 : s[<=]s' -> union s s'' [<=] union s' s''.
172
Lemma union_subset_5 : s[<=]s' -> union s'' s [<=] union s'' s'.
175
Lemma empty_union_1 : Empty s -> union s s' [=] s'.
178
Lemma empty_union_2 : Empty s -> union s' s [=] s'.
181
Lemma not_in_union : ~In x s -> ~In x s' -> ~In x (union s s').
184
Lemma inter_sym : inter s s' [=] inter s' s.
187
Lemma inter_subset_equal : s[<=]s' -> inter s s' [=] s.
190
Lemma inter_equal_1 : s[=]s' -> inter s s'' [=] inter s' s''.
193
Lemma inter_equal_2 : s'[=]s'' -> inter s s' [=] inter s s''.
196
Lemma inter_assoc : inter (inter s s') s'' [=] inter s (inter s' s'').
199
Lemma union_inter_1 : inter (union s s') s'' [=] union (inter s s'') (inter s' s'').
202
Lemma union_inter_2 : union (inter s s') s'' [=] inter (union s s'') (union s' s'').
205
Lemma inter_add_1 : In x s' -> inter (add x s) s' [=] add x (inter s s').
208
Lemma inter_add_2 : ~ In x s' -> inter (add x s) s' [=] inter s s'.
211
Lemma empty_inter_1 : Empty s -> Empty (inter s s').
214
Lemma empty_inter_2 : Empty s' -> Empty (inter s s').
217
Lemma inter_subset_1 : inter s s' [<=] s.
220
Lemma inter_subset_2 : inter s s' [<=] s'.
223
Lemma inter_subset_3 :
224
s''[<=]s -> s''[<=]s' -> s''[<=] inter s s'.
227
Lemma empty_diff_1 : Empty s -> Empty (diff s s').
230
Lemma empty_diff_2 : Empty s -> diff s' s [=] s'.
233
Lemma diff_subset : diff s s' [<=] s.
236
Lemma diff_subset_equal : s[<=]s' -> diff s s' [=] empty.
239
Lemma remove_diff_singleton :
240
remove x s [=] diff s (singleton x).
243
Lemma diff_inter_empty : inter (diff s s') (inter s s') [=] empty.
246
Lemma diff_inter_all : union (diff s s') (inter s s') [=] s.
249
Lemma Add_add : Add x s (add x s).
250
Proof. expAdd; fsetdec. Qed.
252
Lemma Add_remove : In x s -> Add x (remove x s) s.
253
Proof. expAdd; fsetdec. Qed.
255
Lemma union_Add : Add x s s' -> Add x (union s s'') (union s' s'').
256
Proof. expAdd; fsetdec. Qed.
259
In x s'' -> Add x s s' -> Add x (inter s s'') (inter s' s'').
260
Proof. expAdd; fsetdec. Qed.
263
In x s'' -> Add x s s' -> union s s'' [=] union s' s''.
264
Proof. expAdd; fsetdec. Qed.
267
~In x s'' -> Add x s s' -> inter s s'' [=] inter s' s''.
268
Proof. expAdd; fsetdec. Qed.
272
Hint Immediate equal_sym add_remove remove_add union_sym inter_sym: set.
273
Hint Resolve equal_refl equal_trans subset_refl subset_equal subset_antisym
274
subset_trans subset_empty subset_remove_3 subset_diff subset_add_3
275
subset_add_2 in_subset empty_is_empty_1 empty_is_empty_2 add_equal
276
remove_equal singleton_equal_add union_subset_equal union_equal_1
277
union_equal_2 union_assoc add_union_singleton union_add union_subset_1
278
union_subset_2 union_subset_3 inter_subset_equal inter_equal_1 inter_equal_2
279
inter_assoc union_inter_1 union_inter_2 inter_add_1 inter_add_2
280
empty_inter_1 empty_inter_2 empty_union_1 empty_union_2 empty_diff_1
281
empty_diff_2 union_Add inter_Add union_Equal inter_Add_2 not_in_union
282
inter_subset_1 inter_subset_2 inter_subset_3 diff_subset diff_subset_equal
283
remove_diff_singleton diff_inter_empty diff_inter_all Add_add Add_remove
284
Equal_remove add_add : set.
286
(** * Properties of elements *)
288
Lemma elements_Empty : forall s, Empty s <-> elements s = nil.
293
assert (forall a, ~ List.In a (elements s)).
296
rewrite elements_iff.
297
rewrite InA_alt; exists a; auto.
298
destruct (elements s); auto.
299
elim (H0 e); simpl; auto.
301
rewrite elements_iff in H0.
302
rewrite InA_alt in H0; destruct H0.
303
rewrite H in H0; destruct H0 as (_,H0); inversion H0.
306
Lemma elements_empty : elements empty = nil.
308
rewrite <-elements_Empty; auto with set.
311
(** * Conversions between lists and sets *)
313
Definition of_list (l : list elt) := List.fold_right add empty l.
315
Definition to_list := elements.
317
Lemma of_list_1 : forall l x, In x (of_list l) <-> InA E.eq x l.
319
induction l; simpl; intro x.
320
rewrite empty_iff, InA_nil. intuition.
321
rewrite add_iff, InA_cons, IHl. intuition.
324
Lemma of_list_2 : forall l, equivlistA E.eq (to_list (of_list l)) l.
326
unfold to_list; red; intros.
327
rewrite <- elements_iff; apply of_list_1.
330
Lemma of_list_3 : forall s, of_list (to_list s) [=] s.
332
unfold to_list; red; intros.
333
rewrite of_list_1; symmetry; apply elements_iff.
340
Notation NoDup := (NoDupA E.eq).
341
Notation InA := (InA E.eq).
343
(** ** Induction principles for fold (contributed by S. Lescuyer) *)
345
(** In the following lemma, the step hypothesis is deliberately restricted
346
to the precise set s we are considering. *)
349
forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A)(s:t),
350
(forall s', Empty s' -> P s' i) ->
351
(forall x a s' s'', In x s -> ~In x s' -> Add x s' s'' ->
352
P s' a -> P s'' (f x a)) ->
355
intros A P f i s Pempty Pstep.
356
rewrite fold_1, <- fold_left_rev_right.
357
set (l:=rev (elements s)).
358
assert (Pstep' : forall x a s' s'', InA x l -> ~In x s' -> Add x s' s'' ->
359
P s' a -> P s'' (f x a)).
360
intros; eapply Pstep; eauto.
361
rewrite elements_iff, <- InA_rev; auto.
362
assert (Hdup : NoDup l) by
363
(unfold l; eauto using elements_3w, NoDupA_rev).
364
assert (Hsame : forall x, In x s <-> InA x l) by
365
(unfold l; intros; rewrite elements_iff, InA_rev; intuition).
366
clear Pstep; clearbody l; revert s Hsame; induction l.
368
intros s Hsame; simpl.
369
apply Pempty. intro x. rewrite Hsame, InA_nil; intuition.
371
intros s Hsame; simpl.
372
apply Pstep' with (of_list l); auto.
373
inversion_clear Hdup; rewrite of_list_1; auto.
374
red. intros. rewrite Hsame, of_list_1, InA_cons; intuition.
376
intros; eapply Pstep'; eauto.
377
inversion_clear Hdup; auto.
381
(** Same, with [empty] and [add] instead of [Empty] and [Add]. In this
382
case, [P] must be compatible with equality of sets *)
384
Theorem fold_rec_bis :
385
forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A)(s:t),
386
(forall s s' a, s[=]s' -> P s a -> P s' a) ->
388
(forall x a s', In x s -> ~In x s' -> P s' a -> P (add x s') (f x a)) ->
391
intros A P f i s Pmorphism Pempty Pstep.
392
apply fold_rec; intros.
393
apply Pmorphism with empty; auto with set.
394
rewrite Add_Equal in H1; auto with set.
395
apply Pmorphism with (add x s'); auto with set.
398
Lemma fold_rec_nodep :
399
forall (A:Type)(P : A -> Type)(f : elt -> A -> A)(i:A)(s:t),
400
P i -> (forall x a, In x s -> P a -> P (f x a)) ->
403
intros; apply fold_rec_bis with (P:=fun _ => P); auto.
406
(** [fold_rec_weak] is a weaker principle than [fold_rec_bis] :
407
the step hypothesis must here be applicable to any [x].
408
At the same time, it looks more like an induction principle,
409
and hence can be easier to use. *)
411
Lemma fold_rec_weak :
412
forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A),
413
(forall s s' a, s[=]s' -> P s a -> P s' a) ->
415
(forall x a s, ~In x s -> P s a -> P (add x s) (f x a)) ->
416
forall s, P s (fold f s i).
418
intros; apply fold_rec_bis; auto.
422
forall (A B:Type)(R : A -> B -> Type)
423
(f : elt -> A -> A)(g : elt -> B -> B)(i : A)(j : B)(s : t),
425
(forall x a b, In x s -> R a b -> R (f x a) (g x b)) ->
426
R (fold f s i) (fold g s j).
428
intros A B R f g i j s Rempty Rstep.
429
do 2 rewrite fold_1, <- fold_left_rev_right.
430
set (l:=rev (elements s)).
431
assert (Rstep' : forall x a b, InA x l -> R a b -> R (f x a) (g x b)) by
432
(intros; apply Rstep; auto; rewrite elements_iff, <- InA_rev; auto).
433
clearbody l; clear Rstep s.
434
induction l; simpl; auto.
437
(** From the induction principle on [fold], we can deduce some general
438
induction principles on sets. *)
440
Lemma set_induction :
441
forall P : t -> Type,
442
(forall s, Empty s -> P s) ->
443
(forall s s', P s -> forall x, ~In x s -> Add x s s' -> P s') ->
446
intros. apply (@fold_rec _ (fun s _ => P s) (fun _ _ => tt) tt s); eauto.
449
Lemma set_induction_bis :
450
forall P : t -> Type,
451
(forall s s', s [=] s' -> P s -> P s') ->
453
(forall x s, ~In x s -> P s -> P (add x s)) ->
457
apply (@fold_rec_bis _ (fun s _ => P s) (fun _ _ => tt) tt s); eauto.
460
(** [fold] can be used to reconstruct the same initial set. *)
462
Lemma fold_identity : forall s, fold add s empty [=] s.
465
apply fold_rec with (P:=fun s acc => acc[=]s); auto with set.
466
intros. rewrite H2; rewrite Add_Equal in H1; auto with set.
469
(** ** Alternative (weaker) specifications for [fold] *)
471
(** When [FSets] was first designed, the order in which Ocaml's [Set.fold]
472
takes the set elements was unspecified. This specification reflects
477
forall s (A : Type) (i : A) (f : elt -> A -> A),
480
(forall x : elt, In x s <-> InA x l) /\
481
fold f s i = fold_right f i l.
483
intros; exists (rev (elements s)); split.
484
apply NoDupA_rev; auto with set.
487
rewrite elements_iff; do 2 rewrite InA_alt.
488
split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition.
489
rewrite fold_left_rev_right.
493
(** An alternate (and previous) specification for [fold] was based on
494
the recursive structure of a set. It is now lemmas [fold_1] and
498
forall s (A : Type) (eqA : A -> A -> Prop)
499
(st : Equivalence eqA) (i : A) (f : elt -> A -> A),
500
Empty s -> eqA (fold f s i) i.
502
unfold Empty; intros; destruct (fold_0 s i f) as (l,(H1, (H2, H3))).
503
rewrite H3; clear H3.
504
generalize H H2; clear H H2; case l; simpl; intros.
507
elim (H2 e); intuition.
511
forall s s' x (A : Type) (eqA : A -> A -> Prop)
512
(st : Equivalence eqA) (i : A) (f : elt -> A -> A),
513
compat_op E.eq eqA f ->
515
~ In x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
517
intros; destruct (fold_0 s i f) as (l,(Hl, (Hl1, Hl2)));
518
destruct (fold_0 s' i f) as (l',(Hl', (Hl'1, Hl'2))).
519
rewrite Hl2; rewrite Hl'2; clear Hl2 Hl'2.
520
apply fold_right_add with (eqA:=E.eq)(eqB:=eqA); auto.
522
rewrite <- Hl1; auto.
523
intros a; rewrite InA_cons; rewrite <- Hl1; rewrite <- Hl'1;
524
rewrite (H2 a); intuition.
527
(** In fact, [fold] on empty sets is more than equivalent to
528
the initial element, it is Leibniz-equal to it. *)
531
forall s (A : Type)(i : A) (f : elt -> A -> A),
532
Empty s -> (fold f s i) = i.
536
rewrite elements_Empty in H; rewrite H; simpl; auto.
541
Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA).
542
Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
544
Lemma fold_commutes : forall i s x,
545
eqA (fold f s (f x i)) (f x (fold f s i)).
548
apply fold_rel with (R:=fun u v => eqA u (f x v)); intros.
550
transitivity (f x0 (f x b)); auto.
553
(** ** Fold is a morphism *)
555
Lemma fold_init : forall i i' s, eqA i i' ->
556
eqA (fold f s i) (fold f s i').
558
intros. apply fold_rel with (R:=eqA); auto.
562
forall i s s', s[=]s' -> eqA (fold f s i) (fold f s' i).
564
intros i s; pattern s; apply set_induction; clear s; intros.
567
symmetry; apply fold_1; auto.
569
transitivity (f x (fold f s i)).
570
apply fold_2 with (eqA := eqA); auto.
571
symmetry; apply fold_2 with (eqA := eqA); auto.
572
unfold Add in *; intros.
576
(** ** Fold and other set operators *)
578
Lemma fold_empty : forall i, fold f empty i = i.
580
intros i; apply fold_1b; auto with set.
583
Lemma fold_add : forall i s x, ~In x s ->
584
eqA (fold f (add x s) i) (f x (fold f s i)).
586
intros; apply fold_2 with (eqA := eqA); auto with set.
589
Lemma add_fold : forall i s x, In x s ->
590
eqA (fold f (add x s) i) (fold f s i).
592
intros; apply fold_equal; auto with set.
595
Lemma remove_fold_1: forall i s x, In x s ->
596
eqA (f x (fold f (remove x s) i)) (fold f s i).
600
apply fold_2 with (eqA:=eqA); auto with set.
603
Lemma remove_fold_2: forall i s x, ~In x s ->
604
eqA (fold f (remove x s) i) (fold f s i).
607
apply fold_equal; auto with set.
610
Lemma fold_union_inter : forall i s s',
611
eqA (fold f (union s s') (fold f (inter s s') i))
612
(fold f s (fold f s' i)).
614
intros; pattern s; apply set_induction; clear s; intros.
615
transitivity (fold f s' (fold f (inter s s') i)).
616
apply fold_equal; auto with set.
617
transitivity (fold f s' i).
618
apply fold_init; auto.
619
apply fold_1; auto with set.
620
symmetry; apply fold_1; auto.
622
destruct (In_dec x s').
624
transitivity (fold f (union s'' s') (f x (fold f (inter s s') i))); auto with set.
625
apply fold_init; auto.
626
apply fold_2 with (eqA:=eqA); auto with set.
627
rewrite inter_iff; intuition.
628
transitivity (f x (fold f s (fold f s' i))).
629
transitivity (fold f (union s s') (f x (fold f (inter s s') i))).
630
apply fold_equal; auto.
631
apply equal_sym; apply union_Equal with x; auto with set.
632
transitivity (f x (fold f (union s s') (fold f (inter s s') i))).
633
apply fold_commutes; auto.
635
symmetry; apply fold_2 with (eqA:=eqA); auto.
637
transitivity (f x (fold f (union s s') (fold f (inter s'' s') i))).
638
apply fold_2 with (eqA:=eqA); auto with set.
639
transitivity (f x (fold f (union s s') (fold f (inter s s') i))).
641
apply fold_init;auto.
642
apply fold_equal;auto.
643
apply equal_sym; apply inter_Add_2 with x; auto with set.
644
transitivity (f x (fold f s (fold f s' i))).
646
symmetry; apply fold_2 with (eqA:=eqA); auto.
649
Lemma fold_diff_inter : forall i s s',
650
eqA (fold f (diff s s') (fold f (inter s s') i)) (fold f s i).
653
transitivity (fold f (union (diff s s') (inter s s'))
654
(fold f (inter (diff s s') (inter s s')) i)).
655
symmetry; apply fold_union_inter; auto.
656
transitivity (fold f s (fold f (inter (diff s s') (inter s s')) i)).
657
apply fold_equal; auto with set.
658
apply fold_init; auto.
659
apply fold_1; auto with set.
662
Lemma fold_union: forall i s s',
663
(forall x, ~(In x s/\In x s')) ->
664
eqA (fold f (union s s') i) (fold f s (fold f s' i)).
667
transitivity (fold f (union s s') (fold f (inter s s') i)).
668
apply fold_init; auto.
669
symmetry; apply fold_1; auto with set.
670
unfold Empty; intro a; generalize (H a); set_iff; tauto.
671
apply fold_union_inter; auto.
677
forall s p, fold (fun _ => S) s p = fold (fun _ => S) s 0 + p.
679
intros. apply fold_rel with (R:=fun u v => u = v + p); simpl; auto.
686
(** ** Characterization of cardinal in terms of fold *)
688
Lemma cardinal_fold : forall s, cardinal s = fold (fun _ => S) s 0.
690
intros; rewrite cardinal_1; rewrite M.fold_1.
691
symmetry; apply fold_left_length; auto.
694
(** ** Old specifications for [cardinal]. *)
697
forall s, exists l : list elt,
699
(forall x : elt, In x s <-> InA E.eq x l) /\
700
cardinal s = length l.
702
intros; exists (elements s); intuition; apply cardinal_1.
705
Lemma cardinal_1 : forall s, Empty s -> cardinal s = 0.
707
intros; rewrite cardinal_fold; apply fold_1; auto.
711
forall s s' x, ~ In x s -> Add x s s' -> cardinal s' = S (cardinal s).
713
intros; do 2 rewrite cardinal_fold.
714
change S with ((fun _ => S) x).
718
(** ** Cardinal and (non-)emptiness *)
720
Lemma cardinal_Empty : forall s, Empty s <-> cardinal s = 0.
723
rewrite elements_Empty, M.cardinal_1.
724
destruct (elements s); intuition; discriminate.
727
Lemma cardinal_inv_1 : forall s, cardinal s = 0 -> Empty s.
729
intros; rewrite cardinal_Empty; auto.
731
Hint Resolve cardinal_inv_1.
733
Lemma cardinal_inv_2 :
734
forall s n, cardinal s = S n -> { x : elt | In x s }.
736
intros; rewrite M.cardinal_1 in H.
737
generalize (elements_2 (s:=s)).
738
destruct (elements s); try discriminate.
742
Lemma cardinal_inv_2b :
743
forall s, cardinal s <> 0 -> { x : elt | In x s }.
745
intro; generalize (@cardinal_inv_2 s); destruct cardinal;
749
(** ** Cardinal is a morphism *)
751
Lemma Equal_cardinal : forall s s', s[=]s' -> cardinal s = cardinal s'.
754
remember (cardinal s) as n; symmetry in Heqn; revert s s' Heqn H.
756
apply cardinal_1; rewrite <- H; auto.
757
destruct (cardinal_inv_2 Heqn) as (x,H2).
759
rewrite (cardinal_2 (s:=remove x s) (s':=s) (x:=x)); auto with set.
760
rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); eauto with set.
763
Add Morphism cardinal : cardinal_m.
765
exact Equal_cardinal.
768
Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal.
770
(** ** Cardinal and set operators *)
772
Lemma empty_cardinal : cardinal empty = 0.
774
rewrite cardinal_fold; apply fold_1; auto with set.
777
Hint Immediate empty_cardinal cardinal_1 : set.
779
Lemma singleton_cardinal : forall x, cardinal (singleton x) = 1.
782
rewrite (singleton_equal_add x).
783
replace 0 with (cardinal empty); auto with set.
784
apply cardinal_2 with x; auto with set.
787
Hint Resolve singleton_cardinal: set.
789
Lemma diff_inter_cardinal :
790
forall s s', cardinal (diff s s') + cardinal (inter s s') = cardinal s .
792
intros; do 3 rewrite cardinal_fold.
793
rewrite <- fold_plus.
794
apply fold_diff_inter with (eqA:=@Logic.eq nat); auto.
797
Lemma union_cardinal:
798
forall s s', (forall x, ~(In x s/\In x s')) ->
799
cardinal (union s s')=cardinal s+cardinal s'.
801
intros; do 3 rewrite cardinal_fold.
802
rewrite <- fold_plus.
803
apply fold_union; auto.
806
Lemma subset_cardinal :
807
forall s s', s[<=]s' -> cardinal s <= cardinal s' .
810
rewrite <- (diff_inter_cardinal s' s).
811
rewrite (inter_sym s' s).
812
rewrite (inter_subset_equal H); auto with arith.
815
Lemma subset_cardinal_lt :
816
forall s s' x, s[<=]s' -> In x s' -> ~In x s -> cardinal s < cardinal s'.
819
rewrite <- (diff_inter_cardinal s' s).
820
rewrite (inter_sym s' s).
821
rewrite (inter_subset_equal H).
822
generalize (@cardinal_inv_1 (diff s' s)).
823
destruct (cardinal (diff s' s)).
824
intro H2; destruct (H2 (refl_equal _) x).
827
change (0 + cardinal s < S n + cardinal s).
828
apply Plus.plus_lt_le_compat; auto with arith.
831
Theorem union_inter_cardinal :
832
forall s s', cardinal (union s s') + cardinal (inter s s') = cardinal s + cardinal s' .
835
do 4 rewrite cardinal_fold.
836
do 2 rewrite <- fold_plus.
837
apply fold_union_inter with (eqA:=@Logic.eq nat); auto.
840
Lemma union_cardinal_inter :
841
forall s s', cardinal (union s s') = cardinal s + cardinal s' - cardinal (inter s s').
844
rewrite <- union_inter_cardinal.
845
rewrite Plus.plus_comm.
849
Lemma union_cardinal_le :
850
forall s s', cardinal (union s s') <= cardinal s + cardinal s'.
852
intros; generalize (union_inter_cardinal s s').
853
intros; rewrite <- H; auto with arith.
856
Lemma add_cardinal_1 :
857
forall s x, In x s -> cardinal (add x s) = cardinal s.
862
Lemma add_cardinal_2 :
863
forall s x, ~In x s -> cardinal (add x s) = S (cardinal s).
866
do 2 rewrite cardinal_fold.
867
change S with ((fun _ => S) x);
868
apply fold_add with (eqA:=@Logic.eq nat); auto.
871
Lemma remove_cardinal_1 :
872
forall s x, In x s -> S (cardinal (remove x s)) = cardinal s.
875
do 2 rewrite cardinal_fold.
876
change S with ((fun _ =>S) x).
877
apply remove_fold_1 with (eqA:=@Logic.eq nat); auto.
880
Lemma remove_cardinal_2 :
881
forall s x, ~In x s -> cardinal (remove x s) = cardinal s.
886
Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2.
890
(** Now comes variants for self-contained weak sets and for full sets.
891
For these variants, only one argument is necessary. Thanks to
892
the subtyping [WS<=S], the [Properties] functor which is meant to be
893
used on modules [(M:S)] can simply be an alias of [WProperties]. *)
895
Module WProperties (M:WS) := WProperties_fun M.E M.
896
Module Properties := WProperties.
899
(** Now comes some properties specific to the element ordering,
900
invalid for Weak Sets. *)
902
Module OrdProperties (M:S).
903
Module ME:=OrderedTypeFacts(M.E).
904
Module Import P := Properties M.
909
(** First, a specialized version of SortA_equivlistA_eqlistA: *)
910
Lemma sort_equivlistA_eqlistA : forall l l' : list elt,
911
sort E.lt l -> sort E.lt l' -> equivlistA E.eq l l' -> eqlistA E.eq l l'.
913
apply SortA_equivlistA_eqlistA; eauto.
916
Definition gtb x y := match E.compare x y with GT _ => true | _ => false end.
917
Definition leb x := fun y => negb (gtb x y).
919
Definition elements_lt x s := List.filter (gtb x) (elements s).
920
Definition elements_ge x s := List.filter (leb x) (elements s).
922
Lemma gtb_1 : forall x y, gtb x y = true <-> E.lt y x.
924
intros; unfold gtb; destruct (E.compare x y); intuition; try discriminate; ME.order.
927
Lemma leb_1 : forall x y, leb x y = true <-> ~E.lt y x.
929
intros; unfold leb, gtb; destruct (E.compare x y); intuition; try discriminate; ME.order.
932
Lemma gtb_compat : forall x, compat_bool E.eq (gtb x).
935
generalize (gtb_1 x a)(gtb_1 x b); destruct (gtb x a); destruct (gtb x b); auto.
937
symmetry; rewrite H1.
938
apply ME.eq_lt with a; auto.
942
apply ME.eq_lt with b; auto.
946
Lemma leb_compat : forall x, compat_bool E.eq (leb x).
948
red; intros x a b H; unfold leb.
949
f_equal; apply gtb_compat; auto.
951
Hint Resolve gtb_compat leb_compat.
953
Lemma elements_split : forall x s,
954
elements s = elements_lt x s ++ elements_ge x s.
956
unfold elements_lt, elements_ge, leb; intros.
957
eapply (@filter_split _ E.eq); eauto with set. ME.order. ME.order. ME.order.
961
unfold gtb in *; destruct (E.compare x y); intuition; try discriminate; ME.order.
965
Lemma elements_Add : forall s s' x, ~In x s -> Add x s s' ->
966
eqlistA E.eq (elements s') (elements_lt x s ++ x :: elements_ge x s).
968
intros; unfold elements_ge, elements_lt.
969
apply sort_equivlistA_eqlistA; auto with set.
970
apply (@SortA_app _ E.eq); auto.
971
apply (@filter_sort _ E.eq); auto with set; eauto with set.
973
apply (@filter_sort _ E.eq); auto with set; eauto with set.
974
rewrite ME.Inf_alt by (apply (@filter_sort _ E.eq); eauto with set).
976
rewrite filter_InA in H1; auto; destruct H1.
978
rewrite <- elements_iff in H1.
980
contradict H; rewrite H; auto.
983
rewrite filter_InA in H1; auto; destruct H1.
987
rewrite filter_InA in H4; auto; destruct H4.
991
rewrite InA_app_iff; rewrite InA_cons.
992
do 2 (rewrite filter_InA; auto).
993
do 2 rewrite <- elements_iff.
994
rewrite leb_1; rewrite gtb_1.
995
rewrite (H0 a); intuition.
996
destruct (E.compare a x); intuition.
997
right; right; split; auto.
1001
Definition Above x s := forall y, In y s -> E.lt y x.
1002
Definition Below x s := forall y, In y s -> E.lt x y.
1004
Lemma elements_Add_Above : forall s s' x,
1005
Above x s -> Add x s s' ->
1006
eqlistA E.eq (elements s') (elements s ++ x::nil).
1009
apply sort_equivlistA_eqlistA; auto with set.
1010
apply (@SortA_app _ E.eq); auto with set.
1013
rewrite <- elements_iff in H1.
1014
apply ME.lt_eq with x; auto.
1017
rewrite InA_app_iff; rewrite InA_cons; rewrite InA_nil.
1018
do 2 rewrite <- elements_iff; rewrite (H0 a); intuition.
1021
Lemma elements_Add_Below : forall s s' x,
1022
Below x s -> Add x s s' ->
1023
eqlistA E.eq (elements s') (x::elements s).
1026
apply sort_equivlistA_eqlistA; auto with set.
1027
change (sort E.lt ((x::nil) ++ elements s)).
1028
apply (@SortA_app _ E.eq); auto with set.
1031
rewrite <- elements_iff in H2.
1032
apply ME.eq_lt with x; auto.
1036
do 2 rewrite <- elements_iff; rewrite (H0 a); intuition.
1039
(** Two other induction principles on sets: we can be more restrictive
1040
on the element we add at each step. *)
1042
Lemma set_induction_max :
1043
forall P : t -> Type,
1044
(forall s : t, Empty s -> P s) ->
1045
(forall s s', P s -> forall x, Above x s -> Add x s s' -> P s') ->
1048
intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto.
1049
case_eq (max_elt s); intros.
1050
apply X0 with (remove e s) e; auto with set.
1052
assert (S n = S (cardinal (remove e s))).
1053
rewrite Heqn; apply cardinal_2 with e; auto with set.
1056
rewrite remove_iff in H0; destruct H0.
1057
generalize (@max_elt_2 s e y H H0); ME.order.
1059
assert (H0:=max_elt_3 H).
1060
rewrite cardinal_Empty in H0; rewrite H0 in Heqn; inversion Heqn.
1063
Lemma set_induction_min :
1064
forall P : t -> Type,
1065
(forall s : t, Empty s -> P s) ->
1066
(forall s s', P s -> forall x, Below x s -> Add x s s' -> P s') ->
1069
intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto.
1070
case_eq (min_elt s); intros.
1071
apply X0 with (remove e s) e; auto with set.
1073
assert (S n = S (cardinal (remove e s))).
1074
rewrite Heqn; apply cardinal_2 with e; auto with set.
1077
rewrite remove_iff in H0; destruct H0.
1078
generalize (@min_elt_2 s e y H H0); ME.order.
1080
assert (H0:=min_elt_3 H).
1081
rewrite cardinal_Empty in H0; auto; rewrite H0 in Heqn; inversion Heqn.
1084
(** More properties of [fold] : behavior with respect to Above/Below *)
1087
forall s s' x (A : Type) (eqA : A -> A -> Prop)
1088
(st : Equivalence eqA) (i : A) (f : elt -> A -> A),
1089
compat_op E.eq eqA f ->
1090
Above x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
1093
do 2 rewrite M.fold_1.
1094
do 2 rewrite <- fold_left_rev_right.
1095
change (f x (fold_right f i (rev (elements s)))) with
1096
(fold_right f i (rev (x::nil)++rev (elements s))).
1097
apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.
1098
rewrite <- distr_rev.
1100
apply elements_Add_Above; auto.
1104
forall s s' x (A : Type) (eqA : A -> A -> Prop)
1105
(st : Equivalence eqA) (i : A) (f : elt -> A -> A),
1106
compat_op E.eq eqA f ->
1107
Below x s -> Add x s s' -> eqA (fold f s' i) (fold f s (f x i)).
1110
do 2 rewrite M.fold_1.
1111
set (g:=fun (a : A) (e : elt) => f e a).
1112
change (eqA (fold_left g (elements s') i) (fold_left g (x::elements s) i)).
1114
do 2 rewrite <- fold_left_rev_right.
1115
apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.
1117
apply elements_Add_Below; auto.
1120
(** The following results have already been proved earlier,
1121
but we can now prove them with one hypothesis less:
1122
no need for [(transpose eqA f)]. *)
1125
Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA).
1126
Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f).
1129
forall i s s', s[=]s' -> eqA (fold f s i) (fold f s' i).
1131
intros; do 2 rewrite M.fold_1.
1132
do 2 rewrite <- fold_left_rev_right.
1133
apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.
1135
apply sort_equivlistA_eqlistA; auto with set.
1136
red; intro a; do 2 rewrite <- elements_iff; auto.
1139
Lemma add_fold : forall i s x, In x s ->
1140
eqA (fold f (add x s) i) (fold f s i).
1142
intros; apply fold_equal; auto with set.
1145
Lemma remove_fold_2: forall i s x, ~In x s ->
1146
eqA (fold f (remove x s) i) (fold f s i).
1149
apply fold_equal; auto with set.
1154
(** An alternative version of [choose_3] *)
1156
Lemma choose_equal : forall s s', Equal s s' ->
1157
match choose s, choose s' with
1158
| Some x, Some x' => E.eq x x'
1159
| None, None => True
1164
generalize (@choose_1 s)(@choose_2 s)
1165
(@choose_1 s')(@choose_2 s')(@choose_3 s s');
1166
destruct (choose s); destruct (choose s'); simpl; intuition.
1167
apply H5 with e; rewrite <-H; auto.
1168
apply H5 with e; rewrite H; auto.
added
removed
theories/FSets/FSetProperties.v
