Commit d7643649 by Robbert Krebbers

### 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.```
parent f511129c
 ... ... @@ -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 ... ...
 ... ... @@ -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}. ... ...
 ... ... @@ -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, ... ...
 ... ... @@ -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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!