listset.v 3.42 KB
Newer Older
1
(* Copyright (c) 2012-2017, Coq-std++ developers. *)
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
From stdpp Require Export collections list.
6
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
7

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

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

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

22
Global Instance: SimpleCollection A (listset A).
23
Proof.
24
  split.
25 26 27
  - by apply not_elem_of_nil.
  - by apply elem_of_list_singleton.
  - intros [?] [?]. apply elem_of_app.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
29 30
Lemma listset_empty_alt X : X    listset_car X = [].
Proof.
31
  destruct X as [l]; split; [|by intros; simplify_eq/=].
32 33
  rewrite elem_of_equiv_empty; intros Hl.
  destruct l as [|x l]; [done|]. feed inversion (Hl x). left.
Robbert Krebbers's avatar
Robbert Krebbers committed
34 35 36 37 38 39
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
40

41
Context `{!EqDecision A}.
Robbert Krebbers's avatar
Robbert Krebbers committed
42

43
Instance listset_intersection: Intersection (listset A) := λ l k,
44
  let (l') := l in let (k') := k in Listset (list_intersection l' k').
45
Instance listset_difference: Difference (listset A) := λ l k,
46
  let (l') := l in let (k') := k in Listset (list_difference l' k').
Robbert Krebbers's avatar
Robbert Krebbers committed
47

48
Instance: Collection A (listset A).
49
Proof.
50
  split.
51 52 53
  - apply _.
  - intros [?] [?]. apply elem_of_list_intersection.
  - intros [?] [?]. apply elem_of_list_difference.
54
Qed.
55
Instance listset_elems: Elements A (listset A) := remove_dups  listset_car.
56
Global Instance: FinCollection A (listset A).
Robbert Krebbers's avatar
Robbert Krebbers committed
57 58
Proof.
  split.
59 60 61
  - apply _.
  - intros. apply elem_of_remove_dups.
  - intros. apply NoDup_remove_dups.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
Qed.
63
End listset.
Robbert Krebbers's avatar
Robbert Krebbers committed
64

65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81
(** 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.

82
Instance listset_ret: MRet listset := λ A x, {[ x ]}.
83
Instance listset_fmap: FMap listset := λ A B f l,
84
  let (l') := l in Listset (f <$> l').
85
Instance listset_bind: MBind listset := λ A B f l,
86
  let (l') := l in Listset (mbind (listset_car  f) l').
87 88 89
Instance listset_join: MJoin listset := λ A, mbind id.

Instance: CollectionMonad listset.
Robbert Krebbers's avatar
Robbert Krebbers committed
90 91
Proof.
  split.
92 93 94 95 96
  - 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.
97
    simpl. by rewrite elem_of_list_bind.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
Qed.