1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
(** * Finite sets library *)
(** 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 (ASet)(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 (ASet)(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 *)
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' s'' t.
Variable x y z elt.
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.
(** 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).
(** 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.
(** Specification of [choose] *)
Parameter choose_1 choose s = Some x -> In x s.
Parameter choose_2 choose s = None -> Empty s.
End Filter.
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.
End S.
|
