Skip to content

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 with map_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
}.