# 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 MSetProperties Zerob Sumbool Lia DecidableTypeEx.
Require FSetEqProperties.

Module WEqPropertiesOn (Import E:DecidableType)(M:WSetsOn E).
Module Import MP := WPropertiesOn E M.
Import FM Dec.F.
Import M.

Section BasicProperties.

Some old specifications written with boolean equalities.
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
Properties of remove
Properties of is_empty
Properties of singleton
Properties of union
Properties of inter
Properties of diff

Lemma diff_subset: subset (diff s s') s=true.

Lemma diff_subset_equal:
subset s s'=true -> equal (diff s s') empty=true.

Lemma remove_inter_singleton:
equal (remove x s) (diff s (singleton x))=true.

Lemma diff_inter_empty:
equal (inter (diff s s') (inter s s')) empty=true.

Lemma diff_inter_all:
equal (union (diff s s') (inter s s')) s=true.

End BasicProperties.

#[global]
#[global]
Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1
subset_refl subset_equal subset_antisym

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:Proper (E.eq==>eqA==>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
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,
Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.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
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: Proper (E.eq==>Logic.eq) f.

Let Comp' : Proper (E.eq==>Logic.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 := (Proper (E.eq==>Logic.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 : elt -> bool, Proper (E.eq==>Logic.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),
Proper (E.eq==>eqA==>eqA) f -> transpose eqA f ->
Proper (E.eq==>eqA==>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 WEqPropertiesOn.

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.