# Library Coq.MSets.MSetProperties

# Finite sets library

This functor derives additional properties from MSetInterface.S. Contrary to the functor in MSetEqProperties it uses predicates over sets instead of sets operations, i.e. In x s instead of mem x s=true, Equal s s' instead of equal s s'=true, etc.
Require Export MSetInterface.
Require Import DecidableTypeEx OrdersLists MSetFacts MSetDecide.
Hint Unfold transpose.
First, a functor for Weak Sets in functorial version.
Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
Module Import Dec := WDecideOn E M.
Module Import FM := Dec.F .
Import M.
Lemma In_dec : forall x s, { In x s } + { ~ In x s }.
Definition Add x s s' := forall y, In y s' <-> E.eq x y \/ In y s.
Lemma Add_Equal : forall x s s', Add x s s' <-> s' [=] add x s.
Ltac expAdd := repeat rewrite Add_Equal.
Section BasicProperties.
Variable s s' s'' s1 s2 s3 : t.
Variable x x' : elt.
Lemma equal_refl : s [=] s.
Lemma equal_sym : s [=] s' -> s' [=] s.
Lemma equal_trans : s1 [=] s2 -> s2 [=] s3 -> s1 [=] s3.
Lemma subset_refl : s [<=] s.
Lemma subset_trans : s1 [<=] s2 -> s2 [<=] s3 -> s1 [<=] s3.
Lemma subset_antisym : s [<=] s' -> s' [<=] s -> s [=] s'.
Lemma subset_equal : s [=] s' -> s [<=] s'.
Lemma subset_empty : empty [<=] s.
Lemma subset_remove_3 : s1 [<=] s2 -> remove x s1 [<=] s2.
Lemma subset_diff : s1 [<=] s3 -> diff s1 s2 [<=] s3.
Lemma subset_add_3 : In x s2 -> s1 [<=] s2 -> add x s1 [<=] s2.
Lemma subset_add_2 : s1 [<=] s2 -> s1 [<=] add x s2.
Lemma in_subset : In x s1 -> s1 [<=] s2 -> In x s2.
Lemma double_inclusion : s1 [=] s2 <-> s1 [<=] s2 /\ s2 [<=] s1.
Lemma empty_is_empty_1 : Empty s -> s [=] empty.
Lemma empty_is_empty_2 : s [=] empty -> Empty s.
Lemma add_equal : In x s -> add x s [=] s.
Lemma add_add : add x (add x' s) [=] add x' (add x s).
Lemma remove_equal : ~ In x s -> remove x s [=] s.
Lemma Equal_remove : s [=] s' -> remove x s [=] remove x s'.
Lemma add_remove : In x s -> add x (remove x s) [=] s.
Lemma remove_add : ~ In x s -> remove x (add x s) [=] s.
Lemma singleton_equal_add : singleton x [=] add x empty.
Lemma remove_singleton_empty :
In x s -> remove x s [=] empty -> singleton x [=] s.
Lemma union_sym : union s s' [=] union s' s.
Lemma union_subset_equal : s [<=] s' -> union s s' [=] s'.
Lemma union_equal_1 : s [=] s' -> union s s'' [=] union s' s''.
Lemma union_equal_2 : s' [=] s'' -> union s s' [=] union s s''.
Lemma union_assoc : union (union s s') s'' [=] union s (union s' s'').
Lemma add_union_singleton : add x s [=] union (singleton x) s.
Lemma union_add : union (add x s) s' [=] add x (union s s').
Lemma union_remove_add_1 :
union (remove x s) (add x s') [=] union (add x s) (remove x s').
Lemma union_remove_add_2 : In x s ->
union (remove x s) (add x s') [=] union s s'.
Lemma union_subset_1 : s [<=] union s s'.
Lemma union_subset_2 : s' [<=] union s s'.
Lemma union_subset_3 : s [<=] s'' -> s' [<=] s'' -> union s s' [<=] s''.
Lemma union_subset_4 : s [<=] s' -> union s s'' [<=] union s' s''.
Lemma union_subset_5 : s [<=] s' -> union s'' s [<=] union s'' s'.
Lemma empty_union_1 : Empty s -> union s s' [=] s'.
Lemma empty_union_2 : Empty s -> union s' s [=] s'.
Lemma not_in_union : ~ In x s -> ~ In x s' -> ~ In x (union s s').
Lemma inter_sym : inter s s' [=] inter s' s.
Lemma inter_subset_equal : s [<=] s' -> inter s s' [=] s.
Lemma inter_equal_1 : s [=] s' -> inter s s'' [=] inter s' s''.
Lemma inter_equal_2 : s' [=] s'' -> inter s s' [=] inter s s''.
Lemma inter_assoc : inter (inter s s') s'' [=] inter s (inter s' s'').
Lemma union_inter_1 : inter (union s s') s'' [=] union (inter s s'') (inter s' s'').
Lemma union_inter_2 : union (inter s s') s'' [=] inter (union s s'') (union s' s'').
Lemma inter_add_1 : In x s' -> inter (add x s) s' [=] add x (inter s s').
Lemma inter_add_2 : ~ In x s' -> inter (add x s) s' [=] inter s s'.
Lemma empty_inter_1 : Empty s -> Empty (inter s s').
Lemma empty_inter_2 : Empty s' -> Empty (inter s s').
Lemma inter_subset_1 : inter s s' [<=] s.
Lemma inter_subset_2 : inter s s' [<=] s'.
Lemma inter_subset_3 :
s'' [<=] s -> s'' [<=] s' -> s'' [<=] inter s s'.
Lemma empty_diff_1 : Empty s -> Empty (diff s s').
Lemma empty_diff_2 : Empty s -> diff s' s [=] s'.
Lemma diff_subset : diff s s' [<=] s.
Lemma diff_subset_equal : s [<=] s' -> diff s s' [=] empty.
Lemma remove_diff_singleton :
remove x s [=] diff s (singleton x).
Lemma diff_inter_empty : inter (diff s s') (inter s s') [=] empty.
Lemma diff_inter_all : union (diff s s') (inter s s') [=] s.
Lemma Add_add : Add x s (add x s).
Lemma Add_remove : In x s -> Add x (remove x s) s.
Lemma union_Add : Add x s s' -> Add x (union s s'') (union s' s'').
Lemma inter_Add :
In x s'' -> Add x s s' -> Add x (inter s s'') (inter s' s'').
Lemma union_Equal :
In x s'' -> Add x s s' -> union s s'' [=] union s' s''.
Lemma inter_Add_2 :
~ In x s'' -> Add x s s' -> inter s s'' [=] inter s' s''.
End BasicProperties.
Hint Immediate equal_sym add_remove remove_add union_sym inter_sym: set.
Hint Resolve equal_refl equal_trans subset_refl subset_equal subset_antisym
subset_trans subset_empty subset_remove_3 subset_diff subset_add_3
subset_add_2 in_subset empty_is_empty_1 empty_is_empty_2 add_equal
remove_equal singleton_equal_add union_subset_equal union_equal_1
union_equal_2 union_assoc add_union_singleton union_add union_subset_1
union_subset_2 union_subset_3 inter_subset_equal inter_equal_1 inter_equal_2
inter_assoc union_inter_1 union_inter_2 inter_add_1 inter_add_2
empty_inter_1 empty_inter_2 empty_union_1 empty_union_2 empty_diff_1
empty_diff_2 union_Add inter_Add union_Equal inter_Add_2 not_in_union
inter_subset_1 inter_subset_2 inter_subset_3 diff_subset diff_subset_equal
remove_diff_singleton diff_inter_empty diff_inter_all Add_add Add_remove
Equal_remove add_add : set.

# Properties of elements

Lemma elements_Empty : forall s, Empty s <-> elements s = nil.
Lemma elements_empty : elements empty = nil.

# Conversions between lists and sets

Definition of_list (l : list elt) := List.fold_right add empty l.
Definition to_list := elements.
Lemma of_list_1 : forall l x, In x (of_list l) <-> InA E.eq x l.
Lemma of_list_2 : forall l, equivlistA E.eq (to_list (of_list l)) l.
Lemma of_list_3 : forall s, of_list (to_list s) [=] s.

# Fold

Section Fold.
Notation NoDup := (NoDupA E.eq).
Notation InA := (InA E.eq).

## Induction principles for fold (contributed by S. Lescuyer)

In the following lemma, the step hypothesis is deliberately restricted to the precise set s we are considering.
Theorem fold_rec :
forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A)(s:t),
(forall s', Empty s' -> P s' i) ->
(forall x a s' s'', In x s -> ~ In x s' -> Add x s' s'' ->
P s' a -> P s'' (f x a)) ->
P s (fold f s i).
Same, with empty and add instead of Empty and Add. In this case, P must be compatible with equality of sets
Theorem fold_rec_bis :
forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A)(s:t),
(forall s s' a, s [=] s' -> P s a -> P s' a) ->
(P empty i) ->
(forall x a s', In x s -> ~ In x s' -> P s' a -> P (add x s') (f x a)) ->
P s (fold f s i).
Lemma fold_rec_nodep :
forall (A:Type)(P : A -> Type)(f : elt -> A -> A)(i:A)(s:t),
P i -> (forall x a, In x s -> P a -> P (f x a)) ->
P (fold f s i).
fold_rec_weak is a weaker principle than fold_rec_bis : the step hypothesis must here be applicable to any x. At the same time, it looks more like an induction principle, and hence can be easier to use.
Lemma fold_rec_weak :
forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A),
(forall s s' a, s [=] s' -> P s a -> P s' a) ->
P empty i ->
(forall x a s, ~ In x s -> P s a -> P (add x s) (f x a)) ->
forall s, P s (fold f s i).
Lemma fold_rel :
forall (A B:Type)(R : A -> B -> Type)
(f : elt -> A -> A)(g : elt -> B -> B)(i : A)(j : B)(s : t),
R i j ->
(forall x a b, In x s -> R a b -> R (f x a) (g x b)) ->
R (fold f s i) (fold g s j).
From the induction principle on fold, we can deduce some general induction principles on sets.
Lemma set_induction :
forall P : t -> Type,
(forall s, Empty s -> P s) ->
(forall s s', P s -> forall x, ~ In x s -> Add x s s' -> P s') ->
forall s, P s.
Lemma set_induction_bis :
forall P : t -> Type,
(forall s s', s [=] s' -> P s -> P s') ->
P empty ->
(forall x s, ~ In x s -> P s -> P (add x s)) ->
forall s, P s.
fold can be used to reconstruct the same initial set.
Lemma fold_identity : forall s, fold add s empty [=] s.

## Alternative (weaker) specifications for fold

When MSets was first designed, the order in which Ocaml's Set.fold takes the set elements was unspecified. This specification reflects this fact:
Lemma fold_0 :
forall s (A : Type) (i : A) (f : elt -> A -> A),
exists l : list elt ,
NoDup l /\
( forall x : elt, In x s <-> InA x l ) /\
fold f s i = fold_right f i l.
An alternate (and previous) specification for fold was based on the recursive structure of a set. It is now lemmas fold_1 and fold_2.
Lemma fold_1 :
forall s (A : Type) (eqA : A -> A -> Prop)
(st : Equivalence eqA) (i : A) (f : elt -> A -> A),
Empty s -> eqA (fold f s i) i.
Lemma fold_2 :
forall s s' x (A : Type) (eqA : A -> A -> Prop)
(st : Equivalence eqA) (i : A) (f : elt -> A -> A),
Proper (E.eq ==> eqA ==> eqA) f ->
transpose eqA f ->
~ In x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
In fact, fold on empty sets is more than equivalent to the initial element, it is Leibniz-equal to it.
Lemma fold_1b :
forall s (A : Type)(i : A) (f : elt -> A -> A),
Empty s -> ( fold f s i ) = i.
Section Fold_More.
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).
Lemma fold_commutes : forall i s x,
eqA (fold f s (f x i)) (f x (fold f s i)).

## Fold is a morphism

Lemma fold_init : forall i i' s, eqA i i' ->
eqA (fold f s i) (fold f s i').
Lemma fold_equal :
forall i s s', s [=] s' -> eqA (fold f s i) (fold f s' i).

## Fold and other set operators

Lemma fold_empty : forall i, fold f empty i = i.
Lemma fold_add : forall i s x, ~ In x s ->
eqA (fold f (add x s) i) (f x (fold f s i)).
Lemma add_fold : forall i s x, In x s ->
eqA (fold f (add x s) i) (fold f s i).
Lemma remove_fold_1: forall i s x, In x s ->
eqA (f x (fold f (remove x s) i)) (fold f s i).
Lemma remove_fold_2: forall i s x, ~ In x s ->
eqA (fold f (remove x s) i) (fold f s i).
Lemma fold_union_inter : forall i s s',
eqA (fold f (union s s') (fold f (inter s s') i))
(fold f s (fold f s' i)).
Lemma fold_diff_inter : forall i s s',
eqA (fold f (diff s s') (fold f (inter s s') i)) (fold f s i).
Lemma fold_union: forall i s s',
(forall x, ~( In x s /\ In x s' )) ->
eqA (fold f (union s s') i) (fold f s (fold f s' i)).
End Fold_More.
Lemma fold_plus :
forall s p, fold (fun _ => S) s p = fold (fun _ => S) s 0 + p.
End Fold.

# Cardinal

## Characterization of cardinal in terms of fold

Lemma cardinal_fold : forall s, cardinal s = fold (fun _ => S) s 0.

## Old specifications for cardinal.

Lemma cardinal_0 :
forall s, exists l : list elt ,
NoDupA E.eq l /\
( forall x : elt, In x s <-> InA E.eq x l ) /\
cardinal s = length l.
Lemma cardinal_1 : forall s, Empty s -> cardinal s = 0.
Lemma cardinal_2 :
forall s s' x, ~ In x s -> Add x s s' -> cardinal s' = S (cardinal s).

## Cardinal and (non-)emptiness

Lemma cardinal_Empty : forall s, Empty s <-> cardinal s = 0.
Lemma cardinal_inv_1 : forall s, cardinal s = 0 -> Empty s.
Hint Resolve cardinal_inv_1.
Lemma cardinal_inv_2 :
forall s n, cardinal s = S n -> { x : elt | In x s }.
Lemma cardinal_inv_2b :
forall s, cardinal s <> 0 -> { x : elt | In x s }.

## Cardinal is a morphism

Lemma Equal_cardinal : forall s s', s [=] s' -> cardinal s = cardinal s'.
Instance cardinal_m : Proper (Equal ==> Logic.eq) cardinal.
Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal.

## Cardinal and set operators

Lemma empty_cardinal : cardinal empty = 0.
Hint Immediate empty_cardinal cardinal_1 : set.
Lemma singleton_cardinal : forall x, cardinal (singleton x) = 1.
Hint Resolve singleton_cardinal: set.
Lemma diff_inter_cardinal :
forall s s', cardinal (diff s s') + cardinal (inter s s') = cardinal s .
Lemma union_cardinal:
forall s s', (forall x, ~( In x s /\ In x s' )) ->
cardinal (union s s')= cardinal s + cardinal s'.
Lemma subset_cardinal :
forall s s', s [<=] s' -> cardinal s <= cardinal s' .
Lemma subset_cardinal_lt :
forall s s' x, s [<=] s' -> In x s' -> ~ In x s -> cardinal s < cardinal s'.
Theorem union_inter_cardinal :
forall s s', cardinal (union s s') + cardinal (inter s s') = cardinal s + cardinal s' .
Lemma union_cardinal_inter :
forall s s', cardinal (union s s') = cardinal s + cardinal s' - cardinal (inter s s').
Lemma union_cardinal_le :
forall s s', cardinal (union s s') <= cardinal s + cardinal s'.
Lemma add_cardinal_1 :
forall s x, In x s -> cardinal (add x s) = cardinal s.
Lemma add_cardinal_2 :
forall s x, ~ In x s -> cardinal (add x s) = S (cardinal s).
Lemma remove_cardinal_1 :
forall s x, In x s -> S (cardinal (remove x s)) = cardinal s.
Lemma remove_cardinal_2 :
forall s x, ~ In x s -> cardinal (remove x s) = cardinal s.
Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2.
End WPropertiesOn.
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 Properties functor which is meant to be used on modules (M:S) can simply be an alias of WProperties.
Module WProperties (M:WSets) := WPropertiesOn M.E M.
Module Properties := WProperties.
Now comes some properties specific to the element ordering, invalid for Weak Sets.
Module OrdProperties (M:Sets).
Module Import ME:=OrderedTypeFacts(M.E).
Module Import ML:=OrderedTypeLists(M.E).
Module Import P := Properties M.
Import FM.
Import M.E.
Import M.
Hint Resolve elements_spec2.
Hint Immediate
min_elt_spec1 min_elt_spec2 min_elt_spec3
max_elt_spec1 max_elt_spec2 max_elt_spec3 : set.
First, a specialized version of SortA_equivlistA_eqlistA:
Lemma sort_equivlistA_eqlistA : forall l l' : list elt,
sort E.lt l -> sort E.lt l' -> equivlistA E.eq l l' -> eqlistA E.eq l l'.
Definition gtb x y := match E.compare x y with Gt => true | _ => false end.
Definition leb x := fun y => negb (gtb x y).
Definition elements_lt x s := List.filter (gtb x) (elements s).
Definition elements_ge x s := List.filter (leb x) (elements s).
Lemma gtb_1 : forall x y, gtb x y = true <-> E.lt y x.
Lemma leb_1 : forall x y, leb x y = true <-> ~ E.lt y x.
Instance gtb_compat x : Proper (E.eq ==> Logic.eq) (gtb x).
Instance leb_compat x : Proper (E.eq ==> Logic.eq) (leb x).
Hint Resolve gtb_compat leb_compat.
Lemma elements_split : forall x s,
elements s = elements_lt x s ++ elements_ge x s.
Lemma elements_Add : forall s s' x, ~ In x s -> Add x s s' ->
eqlistA E.eq (elements s') (elements_lt x s ++ x :: elements_ge x s).
Definition Above x s := forall y, In y s -> E.lt y x.
Definition Below x s := forall y, In y s -> E.lt x y.
Lemma elements_Add_Above : forall s s' x,
Above x s -> Add x s s' ->
eqlistA E.eq (elements s') (elements s ++ x :: nil).
Lemma elements_Add_Below : forall s s' x,
Below x s -> Add x s s' ->
eqlistA E.eq (elements s') (x :: elements s).
Two other induction principles on sets: we can be more restrictive on the element we add at each step.
Lemma set_induction_max :
forall P : t -> Type,
(forall s : t, Empty s -> P s) ->
(forall s s', P s -> forall x, Above x s -> Add x s s' -> P s') ->
forall s : t, P s.
Lemma set_induction_min :
forall P : t -> Type,
(forall s : t, Empty s -> P s) ->
(forall s s', P s -> forall x, Below x s -> Add x s s' -> P s') ->
forall s : t, P s.
More properties of fold : behavior with respect to Above/Below
Lemma fold_3 :
forall s s' x (A : Type) (eqA : A -> A -> Prop)
(st : Equivalence eqA) (i : A) (f : elt -> A -> A),
Proper (E.eq ==> eqA ==> eqA) f ->
Above x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
Lemma fold_4 :
forall s s' x (A : Type) (eqA : A -> A -> Prop)
(st : Equivalence eqA) (i : A) (f : elt -> A -> A),
Proper (E.eq ==> eqA ==> eqA) f ->
Below x s -> Add x s s' -> eqA (fold f s' i) (fold f s (f x i)).
The following results have already been proved earlier, but we can now prove them with one hypothesis less: no need for (transpose eqA f).
Section FoldOpt.
Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA).
Variables (f:elt->A->A)(Comp:Proper (E.eq ==> eqA ==> eqA) f).
Lemma fold_equal :
forall i s s', s [=] s' -> eqA (fold f s i) (fold f s' i).
Lemma add_fold : forall i s x, In x s ->
eqA (fold f (add x s) i) (fold f s i).
Lemma remove_fold_2: forall i s x, ~ In x s ->
eqA (fold f (remove x s) i) (fold f s i).
End FoldOpt.
An alternative version of choose_3
Lemma choose_equal : forall s s', Equal s s' ->
match choose s, choose s' with
| Some x, Some x' => E.eq x x'
| None, None => True
| _, _ => False
end.
End OrdProperties.