# Library Coq.MSets.MSetFacts

# Finite sets library

This functor derives additional facts from MSetInterface.S. These facts are mainly the specifications of MSetInterface.S written using different styles: equivalence and boolean equalities. Moreover, we prove that E.Eq and Equal are setoid equalities.
Require Import DecidableTypeEx.
Require Export MSetInterface.
First, a functor for Weak Sets in functorial version.
Module WFactsOn (Import E : DecidableType)(Import M : WSetsOn E).
Notation eq_dec := E.eq_dec.
Definition eqb x y := if eq_dec x y then true else false.

# Specifications written using implications :

this used to be the default interface.
Section ImplSpec.
Variable s s' : t.
Variable x y : elt.
Lemma In_1 : E.eq x y -> In x s -> In y s.
Lemma mem_1 : In x s -> mem x s = true.
Lemma mem_2 : mem x s = true -> In x s.
Lemma equal_1 : Equal s s' -> equal s s' = true.
Lemma equal_2 : equal s s' = true -> Equal s s'.
Lemma subset_1 : Subset s s' -> subset s s' = true.
Lemma subset_2 : subset s s' = true -> Subset s s'.
Lemma is_empty_1 : Empty s -> is_empty s = true.
Lemma is_empty_2 : is_empty s = true -> Empty s.
Lemma add_1 : E.eq x y -> In y (add x s).
Lemma add_2 : In y s -> In y (add x s).
Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s.
Lemma remove_1 : E.eq x y -> ~ In y (remove x s).
Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).
Lemma remove_3 : In y (remove x s) -> In y s.
Lemma singleton_1 : In y (singleton x) -> E.eq x y.
Lemma singleton_2 : E.eq x y -> In y (singleton x).
Lemma union_1 : In x (union s s') -> In x s \/ In x s'.
Lemma union_2 : In x s -> In x (union s s').
Lemma union_3 : In x s' -> In x (union s s').
Lemma inter_1 : In x (inter s s') -> In x s.
Lemma inter_2 : In x (inter s s') -> In x s'.
Lemma inter_3 : In x s -> In x s' -> In x (inter s s').
Lemma diff_1 : In x (diff s s') -> In x s.
Lemma diff_2 : In x (diff s s') -> ~ In x s'.
Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s').
Variable f : elt -> bool.
Notation compatb := (Proper (E.eq==>Logic.eq)) (only parsing).
Lemma filter_1 : compatb f -> In x (filter f s) -> In x s.
Lemma filter_2 : compatb f -> In x (filter f s) -> f x = true.
Lemma filter_3 : compatb f -> In x s -> f x = true -> In x (filter f s).
Lemma for_all_1 : compatb f ->
For_all (fun x => f x = true) s -> for_all f s = true.
Lemma for_all_2 : compatb f ->
for_all f s = true -> For_all (fun x => f x = true) s.
Lemma exists_1 : compatb f ->
Exists (fun x => f x = true) s -> exists_ f s = true.
Lemma exists_2 : compatb f ->
exists_ f s = true -> Exists (fun x => f x = true) s.
Lemma elements_1 : In x s -> InA E.eq x (elements s).
Lemma elements_2 : InA E.eq x (elements s) -> In x s.
End ImplSpec.
Notation empty_1 := empty_spec (only parsing).
Notation fold_1 := fold_spec (only parsing).
Notation cardinal_1 := cardinal_spec (only parsing).
Notation partition_1 := partition_spec1 (only parsing).
Notation partition_2 := partition_spec2 (only parsing).
Notation choose_1 := choose_spec1 (only parsing).
Notation choose_2 := choose_spec2 (only parsing).
Notation elements_3w := elements_spec2w (only parsing).
Hint Resolve mem_1 equal_1 subset_1 empty_1
is_empty_1 choose_1 choose_2 add_1 add_2 remove_1
remove_2 singleton_2 union_1 union_2 union_3
inter_3 diff_3 fold_1 filter_3 for_all_1 exists_1
partition_1 partition_2 elements_1 elements_3w
: set.
Hint Immediate In_1 mem_2 equal_2 subset_2 is_empty_2 add_3
remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2
filter_1 filter_2 for_all_2 exists_2 elements_2
: set.

# Specifications written using equivalences :

this is now provided by the default interface.
Section IffSpec.
Variable s s' s'' : t.
Variable x y z : elt.
Lemma In_eq_iff : E.eq x y -> (In x s <-> In y s).
Lemma mem_iff : In x s <-> mem x s = true.
Lemma not_mem_iff : ~In x s <-> mem x s = false.
Lemma equal_iff : s[=]s' <-> equal s s' = true.
Lemma subset_iff : s[<=]s' <-> subset s s' = true.
Lemma empty_iff : In x empty <-> False.
Lemma is_empty_iff : Empty s <-> is_empty s = true.
Lemma singleton_iff : In y (singleton x) <-> E.eq x y.
Lemma add_iff : In y (add x s) <-> E.eq x y \/ In y s.
Lemma add_neq_iff : ~ E.eq x y -> (In y (add x s) <-> In y s).
Lemma remove_iff : In y (remove x s) <-> In y s /\ ~E.eq x y.
Lemma remove_neq_iff : ~ E.eq x y -> (In y (remove x s) <-> In y s).
Variable f : elt -> bool.
Lemma for_all_iff : Proper (E.eq==>Logic.eq) f ->
(For_all (fun x => f x = true) s <-> for_all f s = true).
Lemma exists_iff : Proper (E.eq==>Logic.eq) f ->
(Exists (fun x => f x = true) s <-> exists_ f s = true).
Lemma elements_iff : In x s <-> InA E.eq x (elements s).
End IffSpec.
Notation union_iff := union_spec (only parsing).
Notation inter_iff := inter_spec (only parsing).
Notation diff_iff := diff_spec (only parsing).
Notation filter_iff := filter_spec (only parsing).
Useful tactic for simplifying expressions like In y (add x (union s s'))
Ltac set_iff :=
repeat (progress (
rewrite add_iff || rewrite remove_iff || rewrite singleton_iff
|| rewrite union_iff || rewrite inter_iff || rewrite diff_iff
|| rewrite empty_iff)).

# Specifications written using boolean predicates

Section BoolSpec.
Variable s s' s'' : t.
Variable x y z : elt.
Lemma mem_b : E.eq x y -> mem x s = mem y s.
Lemma empty_b : mem y empty = false.
Lemma add_b : mem y (add x s) = eqb x y || mem y s.
Lemma add_neq_b : ~ E.eq x y -> mem y (add x s) = mem y s.
Lemma remove_b : mem y (remove x s) = mem y s && negb (eqb x y).
Lemma remove_neq_b : ~ E.eq x y -> mem y (remove x s) = mem y s.
Lemma singleton_b : mem y (singleton x) = eqb x y.
Lemma union_b : mem x (union s s') = mem x s || mem x s'.
Lemma inter_b : mem x (inter s s') = mem x s && mem x s'.
Lemma diff_b : mem x (diff s s') = mem x s && negb (mem x s').
Lemma elements_b : mem x s = existsb (eqb x) (elements s).
Variable f : elt->bool.
Lemma filter_b : Proper (E.eq==>Logic.eq) f -> mem x (filter f s) = mem x s && f x.
Lemma for_all_b : Proper (E.eq==>Logic.eq) f ->
for_all f s = forallb f (elements s).
Lemma exists_b : Proper (E.eq==>Logic.eq) f ->
exists_ f s = existsb f (elements s).
End BoolSpec.

# Declarations of morphisms with respects to E.eq and Equal

Instance In_m : Proper (E.eq==>Equal==>iff) In.
Instance Empty_m : Proper (Equal==>iff) Empty.
Instance is_empty_m : Proper (Equal==>Logic.eq) is_empty.
Instance mem_m : Proper (E.eq==>Equal==>Logic.eq) mem.
Instance singleton_m : Proper (E.eq==>Equal) singleton.
Instance add_m : Proper (E.eq==>Equal==>Equal) add.
Instance remove_m : Proper (E.eq==>Equal==>Equal) remove.
Instance union_m : Proper (Equal==>Equal==>Equal) union.
Instance inter_m : Proper (Equal==>Equal==>Equal) inter.
Instance diff_m : Proper (Equal==>Equal==>Equal) diff.
Instance Subset_m : Proper (Equal==>Equal==>iff) Subset.
Instance subset_m : Proper (Equal==>Equal==>Logic.eq) subset.
Instance equal_m : Proper (Equal==>Equal==>Logic.eq) equal.
Instance SubsetSetoid : PreOrder Subset.
Definition Subset_refl := @PreOrder_Reflexive _ _ SubsetSetoid.
Definition Subset_trans := @PreOrder_Transitive _ _ SubsetSetoid.
Instance In_s_m : Morphisms.Proper (E.eq ==> Subset ++> impl) In | 1.
Instance Empty_s_m : Proper (Subset-->impl) Empty.
Instance add_s_m : Proper (E.eq==>Subset++>Subset) add.
Instance remove_s_m : Proper (E.eq==>Subset++>Subset) remove.
Instance union_s_m : Proper (Subset++>Subset++>Subset) union.
Instance inter_s_m : Proper (Subset++>Subset++>Subset) inter.
Instance diff_s_m : Proper (Subset++>Subset-->Subset) diff.
Instance filter_equal : forall `(Proper _ (E.eq==>Logic.eq) f),
Proper (Equal==>Equal) (filter f).
Instance filter_subset : forall `(Proper _ (E.eq==>Logic.eq) f),
Proper (Subset==>Subset) (filter f).
Lemma filter_ext : forall f f', Proper (E.eq==>Logic.eq) f -> (forall x, f x = f' x) ->
forall s s', s[=]s' -> filter f s [=] filter f' s'.
End WFactsOn.
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 Facts functor which is meant to be used on modules (M:S) can simply be an alias of WFacts.
Module WFacts (M:WSets) := WFactsOn M.E M.
Module Facts := WFacts.