Library Coq.FSets.FSetFacts


Finite sets library

This functor derives additional facts from FSetInterface.S. These facts are mainly the specifications of FSetInterface.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 FSetInterface.
Set Implicit Arguments.

First, a functor for Weak Sets in functorial version.

Module WFacts_fun (Import E : DecidableType)(Import M : WSfun E).

Notation eq_dec := E.eq_dec.
Definition eqb x y := if eq_dec x y then true else false.

Specifications written using equivalences


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).

Lemma union_iff : In x (union s s') <-> In x s \/ In x s'.

Lemma inter_iff : In x (inter s s') <-> In x s /\ In x s'.

Lemma diff_iff : In x (diff s s') <-> In x s /\ ~ In x s'.

Variable f : elt->bool.

Lemma filter_iff : compat_bool E.eq f -> (In x (filter f s) <-> In x s /\ f x = true).

Lemma for_all_iff : compat_bool E.eq f ->
  (For_all (fun x => f x = true) s <-> for_all f s = true).

Lemma exists_iff : compat_bool E.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.

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 : compat_bool E.eq f -> mem x (filter f s) = mem x s && f x.

Lemma for_all_b : compat_bool E.eq f ->
  for_all f s = forallb f (elements s).

Lemma exists_b : compat_bool E.eq f ->
  exists_ f s = existsb f (elements s).

End BoolSpec.

E.eq and Equal are setoid equalities


Instance E_ST : Equivalence E.eq.

Instance Equal_ST : Equivalence Equal.

Instance In_m : Proper (E.eq ==> Equal ==> iff) In.

Instance is_empty_m : Proper (Equal==> Logic.eq) is_empty.

Instance Empty_m : Proper (Equal ==> iff) 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.


Lemma Subset_refl : forall s, s[<=]s.

Lemma Subset_trans : forall s s' s'', s[<=]s'->s'[<=]s''->s[<=]s''.

Add Relation t Subset
 reflexivity proved by Subset_refl
 transitivity proved by Subset_trans
 as SubsetSetoid.

Instance In_s_m : Morphisms.Proper (E.eq ==> Subset ++> Basics.impl) In | 1.

Add Morphism Empty with signature Subset --> Basics.impl as Empty_s_m.

Add Morphism add with signature E.eq ==> Subset ++> Subset as add_s_m.

Add Morphism remove with signature E.eq ==> Subset ++> Subset as remove_s_m.

Add Morphism union with signature Subset ++> Subset ++> Subset as union_s_m.

Add Morphism inter with signature Subset ++> Subset ++> Subset as inter_s_m.

Add Morphism diff with signature Subset ++> Subset --> Subset as diff_s_m.


Lemma filter_equal : forall f, compat_bool E.eq f ->
  forall s s', s[=]s' -> filter f s [=] filter f s'.

Lemma filter_ext : forall f f', compat_bool E.eq f -> (forall x, f x = f' x) ->
 forall s s', s[=]s' -> filter f s [=] filter f' s'.

Lemma filter_subset : forall f, compat_bool E.eq f ->
  forall s s', s[<=]s' -> filter f s [<=] filter f s'.



End WFacts_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 Facts functor which is meant to be used on modules (M:S) can simply be an alias of WFacts.

Module WFacts (M:WS) := WFacts_fun M.E M.
Module Facts := WFacts.