Library Coq.MSets.MSetInterface
Set interfaces, inspired by the one of Ocaml. When compared with
Ocaml, the main differences are:
- the lack of iter function, useless since Coq is purely functional
- the use of option types instead of Not_found exceptions
- the use of nat instead of int for the cardinal function
Several variants of the set interfaces are available:
- WSetsOn : functorial signature for weak sets
- WSets : self-contained version of WSets
- SetsOn : functorial signature for ordered sets
- Sets : self-contained version of Sets
- WRawSets : a signature for weak sets that may be ill-formed
- RawSets : same for ordered sets
If unsure,
S = Sets is probably what you're looking for: most other
signatures are subsets of it, while
Sets can be obtained from
RawSets via the use of a subset type (see (W)Raw2Sets below).
The empty set.
Test whether a set is empty or not.
mem x s tests whether x belongs to the set s.
add x s returns a set containing all elements of s,
plus x. If x was already in s, s is returned unchanged.
singleton x returns the one-element set containing only x.
remove x s returns a set containing all elements of s,
except x. If x was not in s, s is returned unchanged.
Set union.
Set intersection.
Set difference.
equal s1 s2 tests whether the sets s1 and s2 are
equal, that is, contain equal elements.
subset s1 s2 tests whether the set s1 is a subset of
the set s2.
Parameter fold :
forall A :
Type, (
elt ->
A ->
A) ->
t ->
A ->
A.
fold f s a computes (f xN ... (f x2 (f x1 a))...),
where x1 ... xN are the elements of s.
The order in which elements of s are presented to f is
unspecified.
for_all p s checks if all elements of the set
satisfy the predicate p.
exists p s checks if at least one element of
the set satisfies the predicate p.
filter p s returns the set of all elements in s
that satisfy predicate p.
partition p s returns a pair of sets (s1, s2), where
s1 is the set of all the elements of s that satisfy the
predicate p, and s2 is the set of all the elements of
s that do not satisfy p.
Return the number of elements of a set.
Return the list of all elements of the given set, in any order.
Return one element of the given set, or None if
the set is empty. Which element is chosen is unspecified.
Equal sets could return different elements.
the abstract type of sets
Functorial signature for weak sets
Weak sets are sets without ordering on base elements, only
a decidable equality.
First, we ask for all the functions
Logical predicates
eq is obviously an equivalence, for subtyping only
Specifications of set operators
When compared with ordered sets, here comes the only
property that is really weaker:
Static signature for weak sets
Similar to the functorial signature
WSetsOn, except that the
module
E of base elements is incorporated in the signature.
Functorial signature for sets on ordered elements
Based on
WSetsOn, plus ordering on sets and
min_elt and
max_elt
and some stronger specifications for other functions.
Total ordering between sets. Can be used as the ordering function
for doing sets of sets.
Return the smallest element of the given set
(with respect to the E.compare ordering),
or None if the set is empty.
Same as min_elt, but returns the largest element of the
given set.
Additional specification of elements
Remark: since fold is specified via elements, this stronger
specification of elements has an indirect impact on fold,
which can now be proved to receive elements in increasing order.
Additional specification of choose
Static signature for sets on ordered elements
Similar to the functorial signature
SetsOn, except that the
module
E of base elements is incorporated in the signature.
Some subtyping tests
WSetsOn ---> WSets
| |
| |
V V
SetsOn ---> Sets
Module S_WS (M : Sets) <: WSets := M.
Module Sfun_WSfun (E:OrderedType)(M : SetsOn E) <: WSetsOn E := M.
Module S_Sfun (M : Sets) <: SetsOn M.E := M.
Module WS_WSfun (M : WSets) <: WSetsOn M.E := M.
Signatures for set representations with ill-formed values.
Motivation:
For many implementation of finite sets (AVL trees, sorted
lists, lists without duplicates), we use the same two-layer
approach:
- A first module deals with the datatype (eg. list or tree) without
any restriction on the values we consider. In this module (named
"Raw" in the past), some results are stated under the assumption
that some invariant (e.g. sortedness) holds for the input sets. We
also prove that this invariant is preserved by set operators.
- A second module implements the exact Sets interface by
using a subtype, for instance
{ l : list A | sorted l }.
This module is a mere wrapper around the first Raw module.
With the interfaces below, we give some respectability to
the "Raw" modules. This allows the interested users to directly
access them via the interfaces. Even better, we can build once
and for all a functor doing the transition between Raw and usual Sets.
Description:
The type
t of sets may contain ill-formed values on which our
set operators may give wrong answers. In particular,
mem
may not see a element in a ill-formed set (think for instance of a
unsorted list being given to an optimized
mem that stops
its search as soon as a strictly larger element is encountered).
Unlike optimized operators, the
In predicate is supposed to
always be correct, even on ill-formed sets. Same for
Equal and
other logical predicates.
A predicate parameter
Ok is used to discriminate between
well-formed and ill-formed values. Some lemmas hold only on sets
validating
Ok. This predicate
Ok is required to be
preserved by set operators. Moreover, a boolean function
isok
should exist for identifying (at least some of) the well-formed sets.
First, we ask for all the functions
Is a set well-formed or ill-formed ?
In order to be able to validate (at least some) particular sets as
well-formed, we ask for a boolean function for (semi-)deciding
predicate Ok. If Ok isn't decidable, isok may be the
always-false function.
Logical predicates
First, all operations are compatible with the well-formed predicate.
Now, the specifications, with constraints on the input sets.
Section Spec.
Variable s s':
t.
Variable x y :
elt.
Variable f :
elt ->
bool.
Notation compatb := (
Proper (
E.eq==>Logic.eq)) (
only parsing).
Parameter mem_spec :
forall `{
Ok s},
mem x s = true <-> In x s.
Parameter equal_spec :
forall `{
Ok s,
Ok s'},
equal s s' = true <-> s[=]s'.
Parameter subset_spec :
forall `{
Ok s,
Ok s'},
subset s s' = true <-> s[<=]s'.
Parameter empty_spec :
Empty empty.
Parameter is_empty_spec :
is_empty s = true <-> Empty s.
Parameter add_spec :
forall `{
Ok s},
In y (
add x s)
<-> E.eq y x \/ In y s.
Parameter remove_spec :
forall `{
Ok s},
In y (
remove x s)
<-> In y s /\ ~E.eq y x.
Parameter singleton_spec :
In y (
singleton x)
<-> E.eq y x.
Parameter union_spec :
forall `{
Ok s,
Ok s'},
In x (
union s s')
<-> In x s \/ In x s'.
Parameter inter_spec :
forall `{
Ok s,
Ok s'},
In x (
inter s s')
<-> In x s /\ In x s'.
Parameter diff_spec :
forall `{
Ok s,
Ok s'},
In x (
diff s s')
<-> In x s /\ ~In x s'.
Parameter fold_spec :
forall (
A :
Type) (
i :
A) (
f :
elt ->
A ->
A),
fold f s i = fold_left (
flip f) (
elements s)
i.
Parameter cardinal_spec :
forall `{
Ok s},
cardinal s = length (
elements s).
Parameter filter_spec :
compatb f ->
(
In x (
filter f s)
<-> In x s /\ f x = true).
Parameter for_all_spec :
compatb f ->
(
for_all f s = true <-> For_all (
fun x =>
f x = true)
s).
Parameter exists_spec :
compatb f ->
(
exists_ f s = true <-> Exists (
fun x =>
f x = true)
s).
Parameter partition_spec1 :
compatb f ->
fst (
partition f s)
[=] filter f s.
Parameter partition_spec2 :
compatb f ->
snd (
partition f s)
[=] filter (
fun x =>
negb (
f x))
s.
Parameter elements_spec1 :
InA E.eq x (
elements s)
<-> In x s.
Parameter elements_spec2w :
forall `{
Ok s},
NoDupA E.eq (
elements s).
Parameter choose_spec1 :
choose s = Some x ->
In x s.
Parameter choose_spec2 :
choose s = None ->
Empty s.
End Spec.
End WRawSets.
From weak raw sets to weak usual sets
We avoid creating induction principles for the Record
Same approach for ordered sets
Specification of compare
Additional specification of elements
Specification of min_elt
Specification of max_elt
Additional specification of choose
From Raw to usual sets
Specification of lt
Additional specification of elements
Specification of min_elt
Specification of max_elt
Additional specification of choose
We provide an ordering for sets-as-sorted-lists