listset.v 2.98 KB
Newer Older
1
(* Copyright (c) 2012-2019, 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 sets 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 {_} _ : assert.
Arguments Listset {_} _ : assert.
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 18
Global Instance listset_elem_of: ElemOf A (listset A) := λ x l, x  listset_car l.
Global Instance listset_empty: Empty (listset A) := Listset [].
Global Instance listset_singleton: Singleton A (listset A) := λ x, Listset [x].
Global 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 listset_simple_set : SemiSet 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.
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.
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 42 43 44 45 46
Context `{Aeq : !EqDecision A}.

Global Instance listset_elem_of_dec : RelDecision (@{listset A}).
Proof using Aeq.
  refine (λ x X, cast_if (decide (x  listset_car X))); done.
Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
47

48
Global Instance listset_intersection: Intersection (listset A) := λ l k,
49
  let (l') := l in let (k') := k in Listset (list_intersection l' k').
50
Global Instance listset_difference: Difference (listset A) := λ l k,
51
  let (l') := l in let (k') := k in Listset (list_difference l' k').
Robbert Krebbers's avatar
Robbert Krebbers committed
52

53
Instance listset_set: Set_ A (listset A).
54
Proof.
55
  split.
56 57 58
  - apply _.
  - intros [?] [?]. apply elem_of_list_intersection.
  - intros [?] [?]. apply elem_of_list_difference.
59
Qed.
60 61
Global Instance listset_elements: Elements A (listset A) :=
  remove_dups  listset_car.
62
Global Instance listset_fin_set : FinSet A (listset A).
Robbert Krebbers's avatar
Robbert Krebbers committed
63 64
Proof.
  split.
65 66 67
  - apply _.
  - intros. apply elem_of_remove_dups.
  - intros. apply NoDup_remove_dups.
Robbert Krebbers's avatar
Robbert Krebbers committed
68
Qed.
69
End listset.
Robbert Krebbers's avatar
Robbert Krebbers committed
70

71
Instance listset_ret: MRet listset := λ A x, {[ x ]}.
72
Instance listset_fmap: FMap listset := λ A B f l,
73
  let (l') := l in Listset (f <$> l').
74
Instance listset_bind: MBind listset := λ A B f l,
75
  let (l') := l in Listset (mbind (listset_car  f) l').
76 77
Instance listset_join: MJoin listset := λ A, mbind id.

78
Instance listset_set_monad : MonadSet listset.
Robbert Krebbers's avatar
Robbert Krebbers committed
79 80
Proof.
  split.
81 82 83 84 85
  - 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.
86
    simpl. by rewrite elem_of_list_bind.
Robbert Krebbers's avatar
Robbert Krebbers committed
87
Qed.