Library Coq.FSets.FSetInterface
Set interfaces
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 : OrderedType.
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.
Definition eq : t -> t -> Prop := Equal.
Parameter lt : t -> t -> Prop.
Parameter compare : forall s s' : t, Compare lt eq s s'.
Total ordering between sets. Can be used as the ordering function
for doing sets of sets.
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, in increasing order.
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.
The returned list is sorted in increasing order with respect
to the ordering
Ord.compare, where Ord is the argument
given to {!Set.Make}.
Parameter min_elt : t -> option elt.
Return the smallest element of the given set
(with respect to the
Ord.compare ordering), or raise
Not_found if the set is empty.
Coq comment:
Not_found is represented by the option type
Parameter max_elt : t -> option elt.
Same as {!Set.S.min_elt}, but returns the largest element of the
given set.
Coq comment:
Not_found is represented by the option type
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,
but equal elements will be chosen for equal sets.
Coq comment:
Not_found is represented by the option type
Section Spec.
Variable s 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
eq
Parameter eq_refl : eq s s.
Parameter eq_sym : eq s s' -> eq s' s.
Parameter eq_trans : eq s s' -> eq s' s'' -> eq s s''.
Specification of
lt
Parameter lt_trans : lt s s' -> lt s' s'' -> lt s s''.
Parameter lt_not_eq : lt s s' -> ~ eq s 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 : s[=]s' -> equal s s' = true.
Parameter equal_2 : equal s s' = true ->s[=]s'.
Specification of
subset
Parameter subset_1 : s[<=]s' -> subset s s' = true.
Parameter subset_2 : subset s s' = true -> 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 ->
fst (partition f s) [=] filter f s.
Parameter partition_2 : compat_bool E.eq f ->
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 : sort E.lt (elements s).
Specification of
min_elt
Parameter min_elt_1 : min_elt s = Some x -> In x s.
Parameter min_elt_2 : min_elt s = Some x -> In y s -> ~ E.lt y x.
Parameter min_elt_3 : min_elt s = None -> Empty s.
Specification of
max_elt
Parameter max_elt_1 : max_elt s = Some x -> In x s.
Parameter max_elt_2 : max_elt s = Some x -> In y s -> ~ E.lt x y.
Parameter max_elt_3 : max_elt s = None -> Empty s.
Specification of
choose
Parameter choose_1 : choose s = Some x -> In x s.
Parameter choose_2 : choose s = None -> Empty s.
End Spec.
End S.
Module Type Sdep.
Declare Module E : OrderedType.
Definition elt := E.t.
Parameter t : Set.
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 Add x s s' := forall y, In y s' <-> E.eq x y \/ In y 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).
Definition eq : t -> t -> Prop := Equal.
Parameter lt : t -> t -> Prop.
Parameter compare : forall s s' : t, Compare lt eq s s'.
Parameter eq_refl : forall s : t, eq s s.
Parameter eq_sym : forall s s' : t, eq s s' -> eq s' s.
Parameter eq_trans : forall s s' s'' : t, eq s s' -> eq s' s'' -> eq s s''.
Parameter lt_trans : forall s s' s'' : t, lt s s' -> lt s' s'' -> lt s s''.
Parameter lt_not_eq : forall s s' : t, lt s s' -> ~ eq s s'.
Parameter eq_In : forall (s : t) (x y : elt), E.eq x y -> In x s -> In y s.
Parameter empty : {s : t | Empty s}.
Parameter is_empty : forall s : t, {Empty s} + {~ Empty s}.
Parameter mem : forall (x : elt) (s : t), {In x s} + {~ In x s}.
Parameter add : forall (x : elt) (s : t), {s' : t | Add x s s'}.
Parameter
singleton : forall x : elt, {s : t | forall y : elt, In y s <-> E.eq x y}.
Parameter
remove :
forall (x : elt) (s : t),
{s' : t | forall y : elt, In y s' <-> ~ E.eq x y /\ In y s}.
Parameter
union :
forall s s' : t,
{s'' : t | forall x : elt, In x s'' <-> In x s \/ In x s'}.
Parameter
inter :
forall s s' : t,
{s'' : t | forall x : elt, In x s'' <-> In x s /\ In x s'}.
Parameter
diff :
forall s s' : t,
{s'' : t | forall x : elt, In x s'' <-> In x s /\ ~ In x s'}.
Parameter equal : forall s s' : t, {s[=]s'} + {~ s[=]s'}.
Parameter subset : forall s s' : t, {Subset s s'} + {~ Subset s s'}.
Parameter
filter :
forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x})
(s : t),
{s' : t | compat_P E.eq P -> forall x : elt, In x s' <-> In x s /\ P x}.
Parameter
for_all :
forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x})
(s : t),
{compat_P E.eq P -> For_all P s} + {compat_P E.eq P -> ~ For_all P s}.
Parameter
exists_ :
forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x})
(s : t),
{compat_P E.eq P -> Exists P s} + {compat_P E.eq P -> ~ Exists P s}.
Parameter
partition :
forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x})
(s : t),
{partition : t * t |
let (s1, s2) := partition in
compat_P E.eq P ->
For_all P s1 /\
For_all (fun x => ~ P x) s2 /\
(forall x : elt, In x s <-> In x s1 \/ In x s2)}.
Parameter
elements :
forall s : t,
{l : list elt |
sort E.lt l /\ (forall x : elt, In x s <-> InA E.eq x l)}.
Parameter
fold :
forall (A : Set) (f : elt -> A -> A) (s : t) (i : A),
{r : A | let (l,_) := elements s in
r = fold_left (fun a e => f e a) l i}.
Parameter
cardinal :
forall s : t,
{r : nat | let (l,_) := elements s in r = length l }.
Parameter
min_elt :
forall s : t,
{x : elt | In x s /\ For_all (fun y => ~ E.lt y x) s} + {Empty s}.
Parameter
max_elt :
forall s : t,
{x : elt | In x s /\ For_all (fun y => ~ E.lt x y) s} + {Empty s}.
Parameter choose : forall s : t, {x : elt | In x s} + {Empty s}.
End Sdep.