listset.v 4.01 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite set as unordered lists without duplicates
removed. This implementation forms a monad. *)
5
From prelude Require Export collections list.
Robbert Krebbers's avatar
Robbert Krebbers committed
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23

Record listset A := Listset { listset_car: list A }.
Arguments listset_car {_} _.
Arguments Listset {_} _.

Section listset.
Context {A : Type}.

Instance listset_elem_of: ElemOf A (listset A) := λ x l, x  listset_car l.
Instance listset_empty: Empty (listset A) := Listset [].
Instance listset_singleton: Singleton A (listset A) := λ x, Listset [x].
Instance listset_union: Union (listset A) := λ l k,
  let (l') := l in let (k') := k in Listset (l' ++ k').
Global Opaque listset_singleton listset_empty.

Global Instance: SimpleCollection A (listset A).
Proof.
  split.
24 25 26
  - by apply not_elem_of_nil.
  - by apply elem_of_list_singleton.
  - intros [?] [?]. apply elem_of_app.
Robbert Krebbers's avatar
Robbert Krebbers committed
27 28 29
Qed.
Lemma listset_empty_alt X : X    listset_car X = [].
Proof.
30
  destruct X as [l]; split; [|by intros; simplify_eq/=].
Robbert Krebbers's avatar
Robbert Krebbers committed
31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52
  intros [Hl _]; destruct l as [|x l]; [done|]. feed inversion (Hl x); left.
Qed. 
Global Instance listset_empty_dec (X : listset A) : Decision (X  ).
Proof.
 refine (cast_if (decide (listset_car X = [])));
  abstract (by rewrite listset_empty_alt).
Defined.

Context `{ x y : A, Decision (x = y)}.

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.
  split.
53 54 55
  - apply _.
  - intros [?] [?]. apply elem_of_list_intersection.
  - intros [?] [?]. apply elem_of_list_difference.
Robbert Krebbers's avatar
Robbert Krebbers committed
56 57 58 59 60
Qed.
Instance listset_elems: Elements A (listset A) := remove_dups  listset_car.
Global Instance: FinCollection A (listset A).
Proof.
  split.
61 62 63
  - apply _.
  - intros. apply elem_of_remove_dups.
  - intros. apply NoDup_remove_dups.
Robbert Krebbers's avatar
Robbert Krebbers committed
64 65 66 67
Qed.
Global Instance: CollectionOps A (listset A).
Proof.
  split.
68 69 70
  - apply _.
  - intros ? [?] [?]. apply elem_of_list_intersection_with.
  - intros [?] ??. apply elem_of_list_filter.
Robbert Krebbers's avatar
Robbert Krebbers committed
71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
Qed.
End listset.

(** These instances are declared using [Hint Extern] to avoid too
eager type class search. *)
Hint Extern 1 (ElemOf _ (listset _)) =>
  eapply @listset_elem_of : typeclass_instances.
Hint Extern 1 (Empty (listset _)) =>
  eapply @listset_empty : typeclass_instances.
Hint Extern 1 (Singleton _ (listset _)) =>
  eapply @listset_singleton : typeclass_instances.
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,
  let (l') := l in Listset (f <$> l').
Instance listset_bind: MBind listset := λ A B f l,
  let (l') := l in Listset (mbind (listset_car  f) l').
Instance listset_join: MJoin listset := λ A, mbind id.

Instance: CollectionMonad listset.
Proof.
  split.
105 106 107 108 109
  - intros. apply _.
  - intros ??? [?] ?. apply elem_of_list_bind.
  - intros. apply elem_of_list_ret.
  - intros ??? [?]. apply elem_of_list_fmap.
  - intros ? [?] ?. unfold mjoin, listset_join, elem_of, listset_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
110 111
    simpl. by rewrite elem_of_list_bind.
Qed.