Library Coq.FSets.FSetWeakInterface
Set interfaces for types with only a decidable equality, but no ordering
Require Export Bool.
Require Export DecidableType.
Set Implicit Arguments.
Unset Strict Implicit.
Compatibility of a boolean function with respect to an equality.
Definition compat_bool (A:Set)(eqA: A->A->Prop)(f: A-> bool) :=
forall x y : A, eqA x y -> f x = f y.
Compatibility of a predicate with respect to an equality.
Definition compat_P (A:Set)(eqA: A->A->Prop)(P : A -> Prop) :=
forall x y : A, eqA x y -> P x -> P y.
Hint Unfold compat_bool compat_P.
Non-dependent signature
Signature
S presents sets as purely informative programs
together with axioms
Module Type S.
Declare Module E : DecidableType.
Definition elt := E.t.
Parameter t : Set.
the abstract type of sets
Logical predicates
Parameter In : elt -> t -> Prop.
Definition Equal s s' := forall a : elt, In a s <-> In a s'.
Definition Subset s s' := forall a : elt, In a s -> In a s'.
Definition Empty s := forall a : elt, ~ In a s.
Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
Notation "s [=] t" := (Equal s t) (at level 70, no associativity).
Notation "s [<=] t" := (Subset s t) (at level 70, no associativity).
Parameter empty : t.
The empty set.
Parameter is_empty : t -> bool.
Test whether a set is empty or not.
Parameter mem : elt -> t -> bool.
mem x s tests whether x belongs to the set s.
Parameter add : elt -> t -> t.
add x s returns a set containing all elements of s,
plus x. If x was already in s, s is returned unchanged.
Parameter singleton : elt -> t.
singleton x returns the one-element set containing only x.
Parameter remove : elt -> t -> t.
remove x s returns a set containing all elements of s,
except x. If x was not in s, s is returned unchanged.
Parameter union : t -> t -> t.
Set union.
Parameter inter : t -> t -> t.
Set intersection.
Parameter diff : t -> t -> t.
Set difference.
Parameter equal : t -> t -> bool.
equal s1 s2 tests whether the sets s1 and s2 are
equal, that is, contain equal elements.
Parameter subset : t -> t -> bool.
subset s1 s2 tests whether the set s1 is a subset of
the set s2.
Coq comment:
iter is useless in a purely functional world
iter: (elt -> unit) -> set -> unit. i
iter f s applies f in turn to all elements of s.
The order in which the elements of s are presented to f
is unspecified.
Parameter fold : forall A : Set, (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.
Parameter for_all : (elt -> bool) -> t -> bool.
for_all p s checks if all elements of the set
satisfy the predicate p.
Parameter exists_ : (elt -> bool) -> t -> bool.
exists p s checks if at least one element of
the set satisfies the predicate p.
Parameter filter : (elt -> bool) -> t -> t.
filter p s returns the set of all elements in s
that satisfy predicate p.
Parameter partition : (elt -> bool) -> t -> t * t.
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.
Parameter cardinal : t -> nat.
Return the number of elements of a set.
Coq comment: nat instead of int ...
Parameter elements : t -> list elt.
Return the list of all elements of the given set, in any order.
Parameter choose : t -> option elt.
Return one element of the given set, or raise
Not_found if
the set is empty. Which element is chosen is unspecified.
Equal sets could return different elements.
Coq comment:
Not_found is represented by the option type
Section Spec.
Variable s s' : t.
Variable x y : elt.
Specification of
In
Parameter In_1 : E.eq x y -> In x s -> In y s.
Specification of
mem
Parameter mem_1 : In x s -> mem x s = true.
Parameter mem_2 : mem x s = true -> In x s.
Specification of
equal
Parameter equal_1 : Equal s s' -> equal s s' = true.
Parameter equal_2 : equal s s' = true -> Equal s s'.
Specification of
subset
Parameter subset_1 : Subset s s' -> subset s s' = true.
Parameter subset_2 : subset s s' = true -> Subset s s'.
Specification of
empty
Parameter empty_1 : Empty empty.
Specification of
is_empty
Parameter is_empty_1 : Empty s -> is_empty s = true.
Parameter is_empty_2 : is_empty s = true -> Empty s.
Specification of
add
Parameter add_1 : E.eq x y -> In y (add x s).
Parameter add_2 : In y s -> In y (add x s).
Parameter add_3 : ~ E.eq x y -> In y (add x s) -> In y s.
Specification of
remove
Parameter remove_1 : E.eq x y -> ~ In y (remove x s).
Parameter remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).
Parameter remove_3 : In y (remove x s) -> In y s.
Specification of
singleton
Parameter singleton_1 : In y (singleton x) -> E.eq x y.
Parameter singleton_2 : E.eq x y -> In y (singleton x).
Specification of
union
Parameter union_1 : In x (union s s') -> In x s \/ In x s'.
Parameter union_2 : In x s -> In x (union s s').
Parameter union_3 : In x s' -> In x (union s s').
Specification of
inter
Parameter inter_1 : In x (inter s s') -> In x s.
Parameter inter_2 : In x (inter s s') -> In x s'.
Parameter inter_3 : In x s -> In x s' -> In x (inter s s').
Specification of
diff
Parameter diff_1 : In x (diff s s') -> In x s.
Parameter diff_2 : In x (diff s s') -> ~ In x s'.
Parameter diff_3 : In x s -> ~ In x s' -> In x (diff s s').
Specification of
fold
Parameter fold_1 : forall (A : Set) (i : A) (f : elt -> A -> A),
fold f s i = fold_left (fun a e => f e a) (elements s) i.
Specification of
cardinal
Parameter cardinal_1 : cardinal s = length (elements s).
Section Filter.
Variable f : elt -> bool.
Specification of
filter
Parameter filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s.
Parameter filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true.
Parameter filter_3 :
compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).
Specification of
for_all
Parameter for_all_1 :
compat_bool E.eq f ->
For_all (fun x => f x = true) s -> for_all f s = true.
Parameter for_all_2 :
compat_bool E.eq f ->
for_all f s = true -> For_all (fun x => f x = true) s.
Specification of
exists
Parameter exists_1 :
compat_bool E.eq f ->
Exists (fun x => f x = true) s -> exists_ f s = true.
Parameter exists_2 :
compat_bool E.eq f ->
exists_ f s = true -> Exists (fun x => f x = true) s.
Specification of
partition
Parameter partition_1 :
compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s).
Parameter partition_2 :
compat_bool E.eq f ->
Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
End Filter.
Specification of
elements
Parameter elements_1 : In x s -> InA E.eq x (elements s).
Parameter elements_2 : InA E.eq x (elements s) -> In x s.
Parameter elements_3 : NoDupA E.eq (elements s).
Specification of
choose
Parameter choose_1 : choose s = Some x -> In x s.
Parameter choose_2 : choose s = None -> Empty s.
End Spec.
Hint Immediate In_1.
Hint Resolve mem_1 mem_2 equal_1 equal_2 subset_1 subset_2 empty_1
is_empty_1 is_empty_2 choose_1 choose_2 add_1 add_2 add_3 remove_1
remove_2 remove_3 singleton_1 singleton_2 union_1 union_2 union_3 inter_1
inter_2 inter_3 diff_1 diff_2 diff_3 filter_1 filter_2 filter_3 for_all_1
for_all_2 exists_1 exists_2 partition_1 partition_2 elements_1 elements_2
elements_3.
End S.