Consistently use `set_` prefix.

The MR closes #24 (closed).

• Consistently set_ prefixes (instead of collection_).
• Rename the Collection type class into Set_. Likewise, SimpleCollection is called SemiSet, and FinCollection is called FinSet, and CollectionMonad is called MonadSet.
• Rename collections.v and fin_collections.v into sets.v and fin_sets.v, respectively.
• Rename set A := A → Prop (theories/set.v) into propset, and likewise bset into boolset.
• Consistently prefer X_to_Y for conversion functions, e.g. list_to_map instead of the former map_of_list.

Sed script uses

This MR is the result of the following sed script. It only had one bug, it wrongly replaced Vector.of_list into Vector.set_of_list. Note that I'm not using \b all the time because I also wanted to fix up lemma names.

sed '
s/SimpleCollection/SemiSet/g;
s/FinCollection/FinSet/g;
s/CollectionMonad/MonadSet/g;
s/Collection/Set\_/g;
s/collection\_simple/set\_semi\_set/g;
s/fin\_collection/fin\_set/g;
s/collection\_monad\_simple/monad\_set\_semi\_set/g;
s/collection\_equiv/set\_equiv/g;
s/\bbset/boolset/g;
s/mkBSet/BoolSet/g;
s/mkSet/PropSet/g;
s/set\_equivalence/set\_equiv\_equivalence/g;
s/collection\_subseteq/set\_subseteq/g;
s/collection\_disjoint/set\_disjoint/g;
s/collection\_fold/set\_fold/g;
s/collection\_map/set\_map/g;
s/collection\_size/set\_size/g;
s/collection\_filter/set\_filter/g;
s/collection\_guard/set\_guard/g;
s/collection\_choose/set\_choose/g;
s/collection\_ind/set\_ind/g;
s/collection\_wf/set\_wf/g;
s/map\_to\_collection/map\_to\_set/g;
s/map\_of\_collection/set\_to\_map/g;
s/map\_of\_list/list\_to\_map/g;
s/map\_of\_to_list/list\_to\_map\_to\_list/g;
s/map\_to\_of\_list/map\_to\_list\_to\_map/g;
s/\bof\_list/list\_to\_set/g;
s/\bof\_option/option\_to\_set/g;
s/elem\_of\_of\_list/elem\_of\_list\_to\_set/g;
s/elem\_of\_of\_option/elem\_of\_option\_to\_set/g;
s/collection\_not\_subset\_inv/set\_not\_subset\_inv/g;
s/seq\_set/set\_seq/g;
s/collections/sets/g;
s/collection/set/g;
s/to\_gmap/gset\_to\_gmap/g;
s/of\_bools/bools\_to\_natset/g;
s/to_bools/natset\_to\_bools/g;
' -i $(find -name "*.v")

Impact on dependencies

I have patches for Iris, lambdarust, Iron, fri-coq and iris-examples. The amount of renaming that had to be done was fairly minimal, and was mostly done automatically using the above sed script.

• Iris: 42 lines changed
• Iris-examples: 8 lines changed
• Iron: no changes needed
• Lambdarust: 17 lines changed
• Fri-coq: 83 lines changed (mostly changing set into propset by hand)

theories/base.v

@@ -2,7 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects type class interfaces, notations, and general theorems
 that are used throughout the whole development. Most importantly it contains
-abstract interfaces for ordered structures, collections, and various other data
+abstract interfaces for ordered structures, sets, and various other data
 structures. *)
 
 From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
@@ -753,9 +753,9 @@ End sig_map.
 Arguments sig_map _ _ _ _ _ _ !_ / : assert.
 
 
-(** * Operations on collections *)
+(** * Operations on sets *)
 (** We define operational type classes for the traditional operations and
-relations on collections: the empty collection [∅], the union [(∪)],
+relations on sets: the empty set [∅], the union [(∪)],
 intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
 [(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *)
 Class Empty A := empty: A.
@@ -1053,7 +1053,7 @@ Instance: Params (@partial_alter) 4 := {}.
 Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [dom C m] should yield the domain of [m]. That is a finite
-collection of type [C] that contains the keys that are a member of [m]. *)
+set of type [C] that contains the keys that are a member of [m]. *)
 Class Dom (M C : Type) := dom: M → C.
 Hint Mode Dom ! ! : typeclass_instances.
 Instance: Params (@dom) 3 := {}.
@@ -1110,23 +1110,28 @@ Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
 Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
 
 
-(** * Axiomatization of collections *)
-(** The class [SimpleCollection A C] axiomatizes a collection of type [C] with
-elements of type [A]. *)
-Class SimpleCollection A C `{ElemOf A C,
+(** * Axiomatization of sets *)
+(** The classes [SemiSet A C] and [Set_ A C] axiomatize sset of type [C] with
+elements of type [A]. The first class, [SemiSet] does not include intersection
+and difference. It is useful for the case of lists, where decidable equality
+is needed to implement intersection and difference, but not union.
+
+Note that we cannot use the name [Set] since that is a reserved keyword. Hence
+we use [Set_]. *)
+Class SemiSet A C `{ElemOf A C,
     Empty C, Singleton A C, Union C} : Prop := {
   not_elem_of_empty (x : A) : x ∉ ∅;
   elem_of_singleton (x y : A) : x ∈ {[ y ]} ↔ x = y;
   elem_of_union X Y (x : A) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y
 }.
-Class Collection A C `{ElemOf A C, Empty C, Singleton A C,
+Class Set_ A C `{ElemOf A C, Empty C, Singleton A C,
     Union C, Intersection C, Difference C} : Prop := {
-  collection_simple :>> SimpleCollection A C;
+  set_semi_set :>> SemiSet 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
 }.
 
-(** We axiomative a finite collection as a collection whose elements can be
+(** We axiomative a finite set as a set whose elements can be
 enumerated as a list. These elements, given by the [elements] function, may be
 in any order and should not contain duplicates. *)
 Class Elements A C := elements: C → list A.
@@ -1159,9 +1164,9 @@ Qed.
 
 (** Decidability of equality of the carrier set is admissible, but we add it
 anyway so as to avoid cycles in type class search. *)
-Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C, Union C,
+Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
     Intersection C, Difference C, Elements A C, EqDecision A} : Prop := {
-  fin_collection :>> Collection A C;
+  fin_set_set :>> Set_ A C;
   elem_of_elements X x : x ∈ elements X ↔ x ∈ X;
   NoDup_elements X : NoDup (elements X)
 }.
@@ -1170,18 +1175,18 @@ Hint Mode Size ! : typeclass_instances.
 Arguments size {_ _} !_ / : simpl nomatch, assert.
 Instance: Params (@size) 2 := {}.
 
-(** The class [CollectionMonad M] axiomatizes a type constructor [M] that can be
-used to construct a collection [M A] with elements of type [A]. The advantage
-of this class, compared to [Collection], is that it also axiomatizes the
+(** The class [MonadSet M] axiomatizes a type constructor [M] that can be
+used to construct a set [M A] with elements of type [A]. The advantage
+of this class, compared to [Set_], is that it also axiomatizes the
 the monadic operations. The disadvantage, is that not many inhabits are
 possible (we will only provide an inhabitant using unordered lists without
-duplicates removed). More interesting implementations typically need
-decidability of equality, or a total order on the elements, which do not fit
+duplicates). More interesting implementations typically need
+decidable equality, or a total order on the elements, which do not fit
 in a type constructor of type [Type → Type]. *)
-Class CollectionMonad M `{∀ A, ElemOf A (M A),
+Class MonadSet M `{∀ A, ElemOf A (M A),
     ∀ A, Empty (M A), ∀ A, Singleton A (M A), ∀ A, Union (M A),
     !MBind M, !MRet M, !FMap M, !MJoin M} : Prop := {
-  collection_monad_simple A :> SimpleCollection A (M A);
+  monad_set_semi_set A :> SemiSet A (M A);
   elem_of_bind {A B} (f : A → M B) (X : M A) (x : B) :
     x ∈ X ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ X;
   elem_of_ret {A} (x y : A) : x ∈ mret y ↔ x = y;
@@ -1192,13 +1197,13 @@ Class CollectionMonad M `{∀ A, ElemOf A (M A),
 
 (** The function [fresh X] yields an element that is not contained in [X]. We
 will later prove that [fresh] is [Proper] with respect to the induced setoid
-equality on collections. *)
+equality on sets. *)
 Class Fresh A C := fresh: C → A.
 Hint Mode Fresh - ! : typeclass_instances.
 Instance: Params (@fresh) 3 := {}.
 Class FreshSpec A C `{ElemOf A C,
     Empty C, Singleton A C, Union C, Fresh A C} : Prop := {
-  fresh_collection_simple :>> SimpleCollection A C;
+  fresh_set_semi_set :>> SemiSet A C;
   fresh_proper_alt X Y : (∀ x, x ∈ X ↔ x ∈ Y) → fresh X = fresh Y;
   is_fresh (X : C) : fresh X ∉ X
 }.