listset.v 3.97 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
2
(* This file is distributed under the terms of the BSD license. *)
3
(** This file implements finite set as unordered lists without duplicates
4
removed. This implementation forms a monad. *)
5
Require Export base decidable collections list.
Robbert Krebbers's avatar
Robbert Krebbers committed
6

7
Record listset A := Listset { listset_car: list A }.
8 9
Arguments listset_car {_} _.
Arguments Listset {_} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
10

11 12
Section listset.
Context {A : Type}.
Robbert Krebbers's avatar
Robbert Krebbers committed
13

14 15 16
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].
17
Instance listset_union: Union (listset A) := λ l k,
18
  let (l') := l in let (k') := k in Listset (l' ++ k').
Robbert Krebbers's avatar
Robbert Krebbers committed
19

20
Global Instance: SimpleCollection A (listset A).
21
Proof.
22 23 24
  split.
  * by apply not_elem_of_nil.
  * by apply elem_of_list_singleton.
Robbert Krebbers's avatar
Robbert Krebbers committed
25
  * intros [?] [?]. apply elem_of_app.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
27 28 29 30 31 32 33 34 35 36
Lemma listset_empty_alt X : X    listset_car X = [].
Proof.
  destruct X as [l]; split; [|by intros; simplify_equality'].
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
37

38
Context `{ x y : A, Decision (x = y)}.
Robbert Krebbers's avatar
Robbert Krebbers committed
39

40
Instance listset_intersection: Intersection (listset A) := λ l k,
41
  let (l') := l in let (k') := k in Listset (list_intersection l' k').
42
Instance listset_difference: Difference (listset A) := λ l k,
43
  let (l') := l in let (k') := k in Listset (list_difference l' k').
Robbert Krebbers's avatar
Robbert Krebbers committed
44
Instance listset_intersection_with: IntersectionWith A (listset A) := λ f l k,
45
  let (l') := l in let (k') := k in Listset (list_intersection_with f l' k').
Robbert Krebbers's avatar
Robbert Krebbers committed
46
Instance listset_filter: Filter A (listset A) := λ P _ l,
47
  let (l') := l in Listset (filter P l').
Robbert Krebbers's avatar
Robbert Krebbers committed
48

49
Instance: Collection A (listset A).
50
Proof.
51 52
  split.
  * apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
53 54
  * intros [?] [?]. apply elem_of_list_intersection.
  * intros [?] [?]. apply elem_of_list_difference.
55
Qed.
56
Instance listset_elems: Elements A (listset A) := remove_dups  listset_car.
57
Global Instance: FinCollection A (listset A).
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59
Proof.
  split.
60
  * apply _.
61 62
  * intros. apply elem_of_remove_dups.
  * intros. apply NoDup_remove_dups.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
Qed.
64 65 66 67 68 69 70
Global Instance: CollectionOps A (listset A).
Proof.
  split.
  * apply _.
  * intros ? [?] [?]. apply elem_of_list_intersection_with.
  * intros [?] ??. apply elem_of_list_filter.
Qed.
71
End listset.
Robbert Krebbers's avatar
Robbert Krebbers committed
72

73 74 75 76 77 78 79 80 81 82 83 84
(** 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86
Hint Extern 1 (IntersectionWith _ (listset _)) =>
  eapply @listset_intersection_with : typeclass_instances.
87 88 89 90
Hint Extern 1 (Difference (listset _)) =>
  eapply @listset_difference : typeclass_instances.
Hint Extern 1 (Elements _ (listset _)) =>
  eapply @listset_elems : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
91 92
Hint Extern 1 (Filter _ (listset _)) =>
  eapply @listset_filter : typeclass_instances.
93

94
Instance listset_ret: MRet listset := λ A x, {[ x ]}.
95
Instance listset_fmap: FMap listset := λ A B f l,
96
  let (l') := l in Listset (f <$> l').
97
Instance listset_bind: MBind listset := λ A B f l,
98
  let (l') := l in Listset (mbind (listset_car  f) l').
99 100 101
Instance listset_join: MJoin listset := λ A, mbind id.

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