Inconsistent naming: `set_` and `_collection`
Naming of connectives related to sets is inconsistent, e.g.:
-
set_Forall
,set_Exists
,set_solver
,set_finite
seq_set
-
collection_map
,collection_filter
,collection_fold
,collection_size
,collection_equiv
,collection_subseteq
,collection_disjoint
-
of_option
,of_list
For finite maps, things are much more consistent: there we only use the prefix map_
.
I would like to do the same for sets, so use set_
everywhere---that's shortest and most consistent. It would mean that we have to rename at least the following:
set_set → set_seq
-
collection_map → set_map
,collection_filter → set_filter
,collection_fold → set_fold
,collection_size → set_size
,collection_equiv → set_equiv
,collection_subseteq → set_subseteq
,collection_disjoint → set_disjoint
. -
of_option
→set_of_option
,of_list
→set_of_list
(which is consistent withmap_of_list
).
Impact on other developments
I don't think the impact of this will be particularly big.
- For most of the notions, we are using operational type classes or notations anyway, i.e. we do not use the explicit names. Examples:
≡
(collection_equiv
),⊆
(collection_subseteq
),filter
(collection_filter
),##
(collection_disjoint
). - For most of the reasoning about sets, we use
set_solver
. - All remaining renaming can easily be done by a
sed
script.
Naming of the classes
Maybe we should get rid of the whole "Collection" name altogether. This will be more invasive, since names of files will also change.
Also, we cannot just rename the type class Collection
into Set
since Set
is a reserved keyword.
Class Collection A C `{ElemOf A C, Empty C, Singleton A C,
Union C, Intersection C, Difference C} : Prop := {
collection_simple :>> SimpleCollection A C;
elem_of_intersection X Y (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y;
elem_of_difference X Y (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y
}.