Remove CollectionOps class.

This class whose name is horrible and purpose is arbitrary seems to be a
leftover of some experiment with ch2o, a long time a ago.

theories/base.v

@@ -908,13 +908,6 @@ Class Collection A C `{ElemOf A C, Empty C, Singleton 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
 }.
-Class CollectionOps A C `{ElemOf A C, Empty C, Singleton A C, Union C,
-    Intersection C, Difference C, IntersectionWith A C, Filter A C} : Prop := {
-  collection_ops :>> Collection A C;
-  elem_of_intersection_with (f : A → A → option A) X Y (x : A) :
-    x ∈ intersection_with f X Y ↔ ∃ x1 x2, x1 ∈ X ∧ x2 ∈ Y ∧ f x1 x2 = Some x;
-  elem_of_filter X P `{∀ x, Decision (P x)} x : x ∈ filter P X ↔ P x ∧ x ∈ X
-}.
 
 (** We axiomative a finite collection as a collection whose elements can be
 enumerated as a list. These elements, given by the [elements] function, may be

theories/collections.v

@@ -467,35 +467,6 @@ Section collection.
   End dec.
 End collection.
 
-Section collection_ops.
-  Context `{CollectionOps A C}.
-
-  Lemma elem_of_intersection_with_list (f : A → A → option A) Xs Y x :
-    x ∈ intersection_with_list f Y Xs ↔ ∃ xs y,
-      Forall2 (∈) xs Xs ∧ y ∈ Y ∧ foldr (λ x, (≫= f x)) (Some y) xs = Some x.
-  Proof.
-    split.
-    - revert x. induction Xs; simpl; intros x HXs; [eexists [], x; intuition|].
-      rewrite elem_of_intersection_with in HXs; destruct HXs as (x1&x2&?&?&?).
-      destruct (IHXs x2) as (xs & y & hy & ? & ?); trivial.
-      eexists (x1 :: xs), y. intuition (simplify_option_eq; auto).
-    - intros (xs & y & Hxs & ? & Hx). revert x Hx.
-      induction Hxs; intros; simplify_option_eq; [done |].
-      rewrite elem_of_intersection_with. naive_solver.
-  Qed.
-
-  Lemma intersection_with_list_ind (P Q : A → Prop) f Xs Y :
-    (∀ y, y ∈ Y → P y) →
-    Forall (λ X, ∀ x, x ∈ X → Q x) Xs →
-    (∀ x y z, Q x → P y → f x y = Some z → P z) →
-    ∀ x, x ∈ intersection_with_list f Y Xs → P x.
-  Proof.
-    intros HY HXs Hf. induction Xs; simplify_option_eq; [done |].
-    intros x Hx. rewrite elem_of_intersection_with in Hx.
-    decompose_Forall. destruct Hx as (? & ? & ? & ? & ?). eauto.
-  Qed.
-End collection_ops.
-
 (** * Sets without duplicates up to an equivalence *)
 Section NoDup.
   Context `{SimpleCollection A B} (R : relation A) `{!Equivalence R}.

theories/listset.v

@@ -42,10 +42,6 @@ Instance listset_intersection: Intersection (listset A) := λ l k,
   let (l') := l in let (k') := k in Listset (list_intersection l' k').
 Instance listset_difference: Difference (listset A) := λ l k,
   let (l') := l in let (k') := k in Listset (list_difference l' k').
-Instance listset_intersection_with: IntersectionWith A (listset A) := λ f l k,
-  let (l') := l in let (k') := k in Listset (list_intersection_with f l' k').
-Instance listset_filter: Filter A (listset A) := λ P _ l,
-  let (l') := l in Listset (filter P l').
 
 Instance: Collection A (listset A).
 Proof.
@@ -62,13 +58,6 @@ Proof.
   - intros. apply elem_of_remove_dups.
   - intros. apply NoDup_remove_dups.
 Qed.
-Global Instance: CollectionOps A (listset A).
-Proof.
-  split.
-  - apply _.
-  - intros ? [?] [?]. apply elem_of_list_intersection_with.
-  - intros [?] ??. apply elem_of_list_filter.
-Qed.
 End listset.
 
 (** These instances are declared using [Hint Extern] to avoid too
@@ -83,14 +72,10 @@ Hint Extern 1 (Union (listset _)) =>
   eapply @listset_union : typeclass_instances.
 Hint Extern 1 (Intersection (listset _)) =>
   eapply @listset_intersection : typeclass_instances.
-Hint Extern 1 (IntersectionWith _ (listset _)) =>
-  eapply @listset_intersection_with : typeclass_instances.
 Hint Extern 1 (Difference (listset _)) =>
   eapply @listset_difference : typeclass_instances.
 Hint Extern 1 (Elements _ (listset _)) =>
   eapply @listset_elems : typeclass_instances.
-Hint Extern 1 (Filter _ (listset _)) =>
-  eapply @listset_filter : typeclass_instances.
 
 Instance listset_ret: MRet listset := λ A x, {[ x ]}.
 Instance listset_fmap: FMap listset := λ A B f l,

theories/listset_nodup.v

@@ -29,12 +29,6 @@ Instance listset_nodup_intersection: Intersection C := λ l k,
 Instance listset_nodup_difference: Difference C := λ l k,
   let (l',Hl) := l in let (k',Hk) := k
   in ListsetNoDup _ (NoDup_list_difference _ k' Hl).
-Instance listset_nodup_intersection_with: IntersectionWith A C := λ f l k,
-  let (l',Hl) := l in let (k',Hk) := k
-  in ListsetNoDup
-    (remove_dups (list_intersection_with f l' k')) (NoDup_remove_dups _).
-Instance listset_nodup_filter: Filter A C := λ P _ l,
-  let (l',Hl) := l in ListsetNoDup _ (NoDup_filter P _ Hl).
 
 Instance: Collection A C.
 Proof.
@@ -49,15 +43,6 @@ Qed.
 Global Instance listset_nodup_elems: Elements A C := listset_nodup_car.
 Global Instance: FinCollection A C.
 Proof. split. apply _. done. by intros [??]. Qed.
-Global Instance: CollectionOps A C.
-Proof.
-  split.
-  - apply _.
-  - intros ? [??] [??] ?. unfold intersection_with, elem_of,
-      listset_nodup_intersection_with, listset_nodup_elem_of; simpl.
-    rewrite elem_of_remove_dups. by apply elem_of_list_intersection_with.
-  - intros [??] ???. apply elem_of_list_filter.
-Qed.
 End list_collection.
 
 Hint Extern 1 (ElemOf _ (listset_nodup _)) =>
@@ -74,5 +59,3 @@ Hint Extern 1 (Difference (listset_nodup _)) =>
   eapply @listset_nodup_difference : typeclass_instances.
 Hint Extern 1 (Elements _ (listset_nodup _)) =>
   eapply @listset_nodup_elems : typeclass_instances.
-Hint Extern 1 (Filter _ (listset_nodup _)) =>
-  eapply @listset_nodup_filter : typeclass_instances.