listset.v 3.39 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 iris.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
  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: Collection A (listset A).
Proof.
  split.
49
50
51
  - apply _.
  - intros [?] [?]. apply elem_of_list_intersection.
  - intros [?] [?]. apply elem_of_list_difference.
Robbert Krebbers's avatar
Robbert Krebbers committed
52
53
54
55
56
Qed.
Instance listset_elems: Elements A (listset A) := remove_dups  listset_car.
Global Instance: FinCollection A (listset A).
Proof.
  split.
57
58
59
  - apply _.
  - intros. apply elem_of_remove_dups.
  - intros. apply NoDup_remove_dups.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
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 (Difference (listset _)) =>
  eapply @listset_difference : typeclass_instances.
Hint Extern 1 (Elements _ (listset _)) =>
  eapply @listset_elems : 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.
90
91
92
93
94
  - 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
95
96
    simpl. by rewrite elem_of_list_bind.
Qed.