# Finite sets library

This module proves many properties of finite sets that are consequences of the axiomatization in FsetInterface Contrary to the functor in FsetProperties it uses sets operations instead of predicates over sets, i.e. mem x s=true instead of In x s, equal s s'=true instead of Equal s s', etc.

Require Import FSetProperties Zerob Sumbool Omega DecidableTypeEx.

Module WEqProperties_fun (Import E:DecidableType)(M:WSfun E).
Module Import MP := WProperties_fun E M.
Import FM Dec.F.
Import M.

Section BasicProperties.

Some old specifications written with boolean equalities.

Variable s s' s'': t.
Variable x y z : elt.

Lemma mem_eq:
E.eq x y -> mem x s=mem y s.

Lemma equal_mem_1:
(forall a, mem a s=mem a s') -> equal s s'=true.

Lemma equal_mem_2:
equal s s'=true -> forall a, mem a s=mem a s'.

Lemma subset_mem_1:
(forall a, mem a s=true->mem a s'=true) -> subset s s'=true.

Lemma subset_mem_2:
subset s s'=true -> forall a, mem a s=true -> mem a s'=true.

Lemma empty_mem: mem x empty=false.

Lemma is_empty_equal_empty: is_empty s = equal s empty.

Lemma choose_mem_1: choose s=Some x -> mem x s=true.

Lemma choose_mem_2: choose s=None -> is_empty s=true.

Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s.

Lemma remove_mem_1: mem x (remove x s)=false.

Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s.

equal (singleton x) (add x empty)=true.

Lemma union_mem:
mem x (union s s')=mem x s || mem x s'.

Lemma inter_mem:
mem x (inter s s')=mem x s && mem x s'.

Lemma diff_mem:
mem x (diff s s')=mem x s && negb (mem x s').

properties of mem

Lemma mem_3 : ~In x s -> mem x s=false.

Lemma mem_4 : mem x s=false -> ~In x s.

Properties of equal
Properties of choose

mem y s=true -> mem y (add x s)=true.

mem x s=true -> equal (add x s) s=true.

Properties of remove
Properties of is_empty
Properties of singleton
Properties of union
Properties of inter
Properties of diff
General recursion principle

Lemma set_rec: forall (P:t->Type),
(forall s s', equal s s'=true -> P s -> P s') ->
(forall s x, mem x s=false -> P s -> P (add x s)) ->
P empty -> forall s, P s.

Properties of fold

Lemma exclusive_set : forall s s' x,
~(In x s/\In x s') <-> mem x s && mem x s'=false.

Section Fold.
Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA).
Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
Variables (i:A).
Variables (s s':t)(x:elt).

Lemma fold_empty: (fold f empty i) = i.

Lemma fold_equal:
equal s s'=true -> eqA (fold f s i) (fold f s' i).

mem x s=false -> eqA (fold f (add x s) i) (f x (fold f s i)).

mem x s=true -> eqA (fold f (add x s) i) (fold f s i).

Lemma remove_fold_1:
mem x s=true -> eqA (f x (fold f (remove x s) i)) (fold f s i).

Lemma remove_fold_2:
mem x s=false -> eqA (fold f (remove x s) i) (fold f s i).

Lemma fold_union:
(forall x, mem x s && mem x s'=false) ->
eqA (fold f (union s s') i) (fold f s (fold f s' i)).

End Fold.

Properties of cardinal

forall s x, mem x s=true -> cardinal (add x s)=cardinal s.

forall s x, mem x s=false -> cardinal (add x s)=S (cardinal s).

Lemma remove_cardinal_1:
forall s x, mem x s=true -> S (cardinal (remove x s))=cardinal s.

Lemma remove_cardinal_2:
forall s x, mem x s=false -> cardinal (remove x s)=cardinal s.

Lemma union_cardinal:
forall s s', (forall x, mem x s && mem x s'=false) ->
cardinal (union s s')=cardinal s+cardinal s'.

Lemma subset_cardinal:
forall s s', subset s s'=true -> cardinal s<=cardinal s'.

Section Bool.

Properties of filter

Variable f:elt->bool.
Variable Comp: Proper (E.eq==>Logic.eq) f.

Let Comp' : Proper (E.eq==>Logic.eq) (fun x =>negb (f x)).

Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x.

Lemma for_all_filter:
forall s, for_all f s=is_empty (filter (fun x => negb (f x)) s).

Lemma exists_filter :
forall s, exists_ f s=negb (is_empty (filter f s)).

Lemma partition_filter_1:
forall s, equal (fst (partition f s)) (filter f s)=true.

Lemma partition_filter_2:
forall s, equal (snd (partition f s)) (filter (fun x => negb (f x)) s)=true.

Lemma filter_add_1 : forall s x, f x = true ->

Lemma filter_add_2 : forall s x, f x = false ->
filter f (add x s) [=] filter f s.

Lemma add_filter_1 : forall s s' x,
f x=true -> (Add x s s') -> (Add x (filter f s) (filter f s')).

Lemma add_filter_2 : forall s s' x,
f x=false -> (Add x s s') -> filter f s [=] filter f s'.

Lemma union_filter: forall f g, (compat_bool E.eq f) -> (compat_bool E.eq g) ->
forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s.

Lemma filter_union: forall s s', filter f (union s s') [=] union (filter f s) (filter f s').

Properties of for_all

Lemma for_all_mem_1: forall s,
(forall x, (mem x s)=true->(f x)=true) -> (for_all f s)=true.

Lemma for_all_mem_2: forall s,
(for_all f s)=true -> forall x,(mem x s)=true -> (f x)=true.

Lemma for_all_mem_3:
forall s x,(mem x s)=true -> (f x)=false -> (for_all f s)=false.

Lemma for_all_mem_4:
forall s, for_all f s=false -> {x:elt | mem x s=true /\ f x=false}.

Properties of exists

Lemma for_all_exists:
forall s, exists_ f s = negb (for_all (fun x =>negb (f x)) s).

End Bool.
Section Bool'.

Variable f:elt->bool.
Variable Comp: compat_bool E.eq f.

Let Comp' : compat_bool E.eq (fun x =>negb (f x)).

Lemma exists_mem_1:
forall s, (forall x, mem x s=true->f x=false) -> exists_ f s=false.

Lemma exists_mem_2:
forall s, exists_ f s=false -> forall x, mem x s=true -> f x=false.

Lemma exists_mem_3:
forall s x, mem x s=true -> f x=true -> exists_ f s=true.

Lemma exists_mem_4:
forall s, exists_ f s=true -> {x:elt | (mem x s)=true /\ (f x)=true}.

End Bool'.

Section Sum.

Adding a valuation function on all elements of a set.

Definition sum (f:elt -> nat)(s:t) := fold (fun x => plus (f x)) s 0.
Notation compat_opL := (compat_op E.eq Logic.eq).
Notation transposeL := (transpose Logic.eq).

Lemma sum_plus :
forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g ->
forall s, sum (fun x =>f x+g x) s = sum f s + sum g s.

Lemma sum_filter : forall f, (compat_bool E.eq f) ->
forall s, (sum (fun x => if f x then 1 else 0) s) = (cardinal (filter f s)).

Lemma fold_compat :
forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)
(f g:elt->A->A),
(compat_op E.eq eqA f) -> (transpose eqA f) ->
(compat_op E.eq eqA g) -> (transpose eqA g) ->
forall (i:A)(s:t),(forall x:elt, (In x s) -> forall y, (eqA (f x y) (g x y))) ->
(eqA (fold f s i) (fold g s i)).

Lemma sum_compat :
forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g ->
forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s.

End Sum.

End WEqProperties_fun.

Now comes variants for self-contained weak sets and for full sets. For these variants, only one argument is necessary. Thanks to the subtyping WS<=S, the EqProperties functor which is meant to be used on modules (M:S) can simply be an alias of WEqProperties.