Library Coq.FSets.FSetEqProperties
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.
Some old specifications written with boolean equalities.
properties of mem
Properties of equal
Properties of choose
Properties of add
Properties of remove
Properties of is_empty
Properties of singleton
Properties of union
Properties of inter
Properties of diff
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
Properties of cardinal
Properties of filter
Variable f:elt->bool.
Variable Comp:
compat_bool E.eq f.
Let Comp' :
compat_bool E.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
Properties of exists
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,
compat_nat E.eq f ->
compat_nat E.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,
compat_nat E.eq f ->
compat_nat E.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.