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

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

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

16 17 18 19 20 21 22
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,
Robbert Krebbers's avatar
Robbert Krebbers committed
23 24 25
  match l, k with
  | Listset l', Listset k' => Listset (l' ++ k')
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
26

27
Global Instance: SimpleCollection A (listset A).
28
Proof.
29 30 31
  split.
  * by apply not_elem_of_nil.
  * by apply elem_of_list_singleton.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
  * intros [?] [?]. apply elem_of_app.
Robbert Krebbers's avatar
Robbert Krebbers committed
33 34
Qed.

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

37
Instance listset_intersection: Intersection (listset A) := λ l k,
Robbert Krebbers's avatar
Robbert Krebbers committed
38 39 40
  match l, k with
  | Listset l', Listset k' => Listset (list_intersection l' k')
  end.
41
Instance listset_difference: Difference (listset A) := λ l k,
Robbert Krebbers's avatar
Robbert Krebbers committed
42 43 44 45 46 47 48 49 50 51 52
  match l, k with
  | Listset l', Listset k' => Listset (list_difference l' k')
  end.
Instance listset_intersection_with: IntersectionWith A (listset A) := λ f l k,
  match l, k with
  | Listset l', Listset k' => Listset (list_intersection_with f l' k')
  end.
Instance listset_filter: Filter A (listset A) := λ P _ l,
  match l with
  | Listset l' => Listset (filter P l')
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
53

54
Instance: Collection A (listset A).
55
Proof.
56 57
  split.
  * apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59
  * intros [?] [?]. apply elem_of_list_intersection.
  * intros [?] [?]. apply elem_of_list_difference.
60
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
61

62 63 64 65
Instance listset_elems: Elements A (listset A) :=
  remove_dups  listset_car.

Global Instance: FinCollection A (listset A).
Robbert Krebbers's avatar
Robbert Krebbers committed
66 67
Proof.
  split.
68 69 70
  * apply _.
  * symmetry. apply elem_of_remove_dups.
  * intros. apply remove_dups_nodup.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
Qed.
72 73 74 75 76 77 78 79

Global Instance: CollectionOps A (listset A).
Proof.
  split.
  * apply _.
  * intros ? [?] [?]. apply elem_of_list_intersection_with.
  * intros [?] ??. apply elem_of_list_filter.
Qed.
80
End listset.
Robbert Krebbers's avatar
Robbert Krebbers committed
81

82 83 84 85 86 87 88 89 90 91 92 93
(** 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
94 95
Hint Extern 1 (IntersectionWith _ (listset _)) =>
  eapply @listset_intersection_with : typeclass_instances.
96 97 98 99
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
100 101
Hint Extern 1 (Filter _ (listset _)) =>
  eapply @listset_filter : typeclass_instances.
102 103 104 105

Instance listset_ret: MRet listset := λ A x,
  {[ x ]}.
Instance listset_fmap: FMap listset := λ A B f l,
Robbert Krebbers's avatar
Robbert Krebbers committed
106 107 108
  match l with
  | Listset l' => Listset (f <$> l')
  end.
109
Instance listset_bind: MBind listset := λ A B f l,
Robbert Krebbers's avatar
Robbert Krebbers committed
110 111 112
  match l with
  | Listset l' => Listset (mbind (listset_car  f) l')
  end.
113 114 115
Instance listset_join: MJoin listset := λ A, mbind id.

Instance: CollectionMonad listset.
Robbert Krebbers's avatar
Robbert Krebbers committed
116 117
Proof.
  split.
118
  * intros. apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
  * intros ??? [?] ?. apply elem_of_list_bind.
120
  * intros. apply elem_of_list_ret.
Robbert Krebbers's avatar
Robbert Krebbers committed
121 122
  * intros ??? [?]. apply elem_of_list_fmap.
  * intros ? [?] ?.
123 124
    unfold mjoin, listset_join, elem_of, listset_elem_of.
    simpl. by rewrite elem_of_list_bind.
Robbert Krebbers's avatar
Robbert Krebbers committed
125
Qed.