Library Coq.FSets.FSetEqProperties
Finite sets library
Require Import FSetProperties Zerob Sumbool DecidableTypeEx.
Module WEqProperties_fun (Import E:DecidableType)(M:WSfun E).
Module Import MP := WProperties_fun E M.
Import FM Dec.F.
Import M.
Definition Add := MP.Add.
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_1: mem x (add x 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.
Lemma singleton_equal_add:
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
Lemma equal_refl: equal s s=true.
Lemma equal_sym: equal s s'=equal s' s.
Lemma equal_trans:
equal s s'=true -> equal s' s''=true -> equal s s''=true.
Lemma equal_equal:
equal s s'=true -> equal s s''=equal s' s''.
Lemma equal_cardinal:
equal s s'=true -> cardinal s=cardinal s'.
Lemma subset_refl: subset s s=true.
Lemma subset_antisym:
subset s s'=true -> subset s' s=true -> equal s s'=true.
Lemma subset_trans:
subset s s'=true -> subset s' s''=true -> subset s s''=true.
Lemma subset_equal:
equal s s'=true -> subset s s'=true.
Properties of choose
Lemma choose_mem_3:
is_empty s=false -> {x:elt|choose s=Some x /\ mem x s=true}.
Lemma choose_mem_4: choose empty=None.
Properties of add
Lemma add_mem_3:
mem y s=true -> mem y (add x s)=true.
Lemma add_equal:
mem x s=true -> equal (add x s) s=true.
Properties of remove
Lemma remove_mem_3:
mem y (remove x s)=true -> mem y s=true.
Lemma remove_equal:
mem x s=false -> equal (remove x s) s=true.
Lemma add_remove:
mem x s=true -> equal (add x (remove x s)) s=true.
Lemma remove_add:
mem x s=false -> equal (remove x (add x s)) s=true.
Properties of is_empty
Lemma is_empty_cardinal: is_empty s = zerob (cardinal s).
Properties of singleton
Lemma singleton_mem_1: mem x (singleton x)=true.
Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false.
Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y.
Properties of union
Lemma union_sym:
equal (union s s') (union s' s)=true.
Lemma union_subset_equal:
subset s s'=true -> equal (union s s') s'=true.
Lemma union_equal_1:
equal s s'=true-> equal (union s s'') (union s' s'')=true.
Lemma union_equal_2:
equal s' s''=true-> equal (union s s') (union s s'')=true.
Lemma union_assoc:
equal (union (union s s') s'') (union s (union s' s''))=true.
Lemma add_union_singleton:
equal (add x s) (union (singleton x) s)=true.
Lemma union_add:
equal (union (add x s) s') (add x (union s s'))=true.
Lemma union_subset_1: subset s (union s s')=true.
Lemma union_subset_2: subset s' (union s s')=true.
Lemma union_subset_3:
subset s s''=true -> subset s' s''=true ->
subset (union s s') s''=true.
Properties of inter
Lemma inter_sym: equal (inter s s') (inter s' s)=true.
Lemma inter_subset_equal:
subset s s'=true -> equal (inter s s') s=true.
Lemma inter_equal_1:
equal s s'=true -> equal (inter s s'') (inter s' s'')=true.
Lemma inter_equal_2:
equal s' s''=true -> equal (inter s s') (inter s s'')=true.
Lemma inter_assoc:
equal (inter (inter s s') s'') (inter s (inter s' s''))=true.
Lemma union_inter_1:
equal (inter (union s s') s'') (union (inter s s'') (inter s' s''))=true.
Lemma union_inter_2:
equal (union (inter s s') s'') (inter (union s s'') (union s' s''))=true.
Lemma inter_add_1: mem x s'=true ->
equal (inter (add x s) s') (add x (inter s s'))=true.
Lemma inter_add_2: mem x s'=false ->
equal (inter (add x s) s') (inter s s')=true.
Lemma inter_subset_1: subset (inter s s') s=true.
Lemma inter_subset_2: subset (inter s s') s'=true.
Lemma inter_subset_3:
subset s'' s=true -> subset s'' s'=true ->
subset s'' (inter s s')=true.
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.
Hint Immediate empty_mem is_empty_equal_empty add_mem_1
remove_mem_1 singleton_equal_add union_mem inter_mem
diff_mem equal_sym add_remove remove_add : set.
Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1
choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal
subset_refl subset_equal subset_antisym
add_mem_3 add_equal remove_mem_3 remove_equal : set.
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).
Lemma fold_add:
mem x s=false -> eqA (fold f (add x s) i) (f x (fold f s i)).
Lemma add_fold:
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
Lemma add_cardinal_1:
forall s x, mem x s=true -> cardinal (add x s)=cardinal s.
Lemma add_cardinal_2:
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 ->
filter f (add x s) [=] add x (filter f s).
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.
Module WEqProperties (M:WS) := WEqProperties_fun M.E M.
Module EqProperties := WEqProperties.