mapset.v 5.75 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files gives an implementation of finite sets using finite maps with
elements of the unit type. Since maps enjoy extensional equality, the
constructed finite sets do so as well. *)
6
From iris.prelude Require Export fin_map_dom.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
9
10
11
12
13
14
15
16
17
18
19

Record mapset (M : Type  Type) : Type :=
  Mapset { mapset_car: M (unit : Type) }.
Arguments Mapset {_} _.
Arguments mapset_car {_} _.

Section mapset.
Context `{FinMap K M}.

Instance mapset_elem_of: ElemOf K (mapset M) := λ x X,
  mapset_car X !! x = Some ().
Instance mapset_empty: Empty (mapset M) := Mapset .
Instance mapset_singleton: Singleton K (mapset M) := λ x,
20
  Mapset {[ x := () ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
Instance mapset_union: Union (mapset M) := λ X1 X2,
  let (m1) := X1 in let (m2) := X2 in Mapset (m1  m2).
Instance mapset_intersection: Intersection (mapset M) := λ X1 X2,
  let (m1) := X1 in let (m2) := X2 in Mapset (m1  m2).
Instance mapset_difference: Difference (mapset M) := λ X1 X2,
  let (m1) := X1 in let (m2) := X2 in Mapset (m1  m2).
Instance mapset_elems: Elements K (mapset M) := λ X,
  let (m) := X in (map_to_list m).*1.

Lemma mapset_eq (X1 X2 : mapset M) : X1 = X2   x, x  X1  x  X2.
Proof.
  split; [by intros ->|].
  destruct X1 as [m1], X2 as [m2]. simpl. intros E.
  f_equal. apply map_eq. intros i. apply option_eq. intros []. by apply E.
Qed.

Instance: Collection K (mapset M).
Proof.
  split; [split | | ].
40
  - unfold empty, elem_of, mapset_empty, mapset_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
    simpl. intros. by simpl_map.
42
  - unfold singleton, elem_of, mapset_singleton, mapset_elem_of.
43
    simpl. by split; intros; simplify_map_eq.
44
  - unfold union, elem_of, mapset_union, mapset_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
46
    intros [m1] [m2] ?. simpl. rewrite lookup_union_Some_raw.
    destruct (m1 !! x) as [[]|]; tauto.
47
  - unfold intersection, elem_of, mapset_intersection, mapset_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
49
50
51
    intros [m1] [m2] ?. simpl. rewrite lookup_intersection_Some.
    assert (is_Some (m2 !! x)  m2 !! x = Some ()).
    { split; eauto. by intros [[] ?]. }
    naive_solver.
52
  - unfold difference, elem_of, mapset_difference, mapset_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
53
54
55
    intros [m1] [m2] ?. simpl. rewrite lookup_difference_Some.
    destruct (m2 !! x) as [[]|]; intuition congruence.
Qed.
56
57
Global Instance: LeibnizEquiv (mapset M).
Proof. intros ??. apply mapset_eq. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
58
59
60
Global Instance: FinCollection K (mapset M).
Proof.
  split.
61
62
  - apply _.
  - unfold elements, elem_of at 2, mapset_elems, mapset_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
64
65
    intros [m] x. simpl. rewrite elem_of_list_fmap. split.
    + intros ([y []] &?& Hy). subst. by rewrite <-elem_of_map_to_list.
    + intros. exists (x, ()). by rewrite elem_of_map_to_list.
66
  - unfold elements, mapset_elems. intros [m]. simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
68
69
    apply NoDup_fst_map_to_list.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
70
Section deciders.
71
72
  Context `{EqDecision (M unit)}.
  Global Instance mapset_eq_dec : EqDecision (mapset M) | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
  Proof.
74
75
   refine (λ X1 X2,
    match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end);
Robbert Krebbers's avatar
Robbert Krebbers committed
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
    abstract congruence.
  Defined.
  Global Instance mapset_equiv_dec (X1 X2 : mapset M) : Decision (X1  X2) | 1.
  Proof. refine (cast_if (decide (X1 = X2))); abstract (by fold_leibniz). Defined.
  Global Instance mapset_elem_of_dec x (X : mapset M) : Decision (x  X) | 1.
  Proof. solve_decision. Defined.
  Global Instance mapset_disjoint_dec (X1 X2 : mapset M) : Decision (X1  X2).
  Proof.
   refine (cast_if (decide (X1  X2 = )));
    abstract (by rewrite disjoint_intersection_L).
  Defined.
  Global Instance mapset_subseteq_dec (X1 X2 : mapset M) : Decision (X1  X2).
  Proof.
   refine (cast_if (decide (X1  X2 = X2)));
    abstract (by rewrite subseteq_union_L).
  Defined.
End deciders.

Robbert Krebbers's avatar
Robbert Krebbers committed
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
Definition mapset_map_with {A B} (f : bool  A  option B)
    (X : mapset M) : M A  M B :=
  let (mX) := X in merge (λ x y,
    match x, y with
    | Some _, Some a => f true a | None, Some a => f false a | _, None => None
    end) mX.
Definition mapset_dom_with {A} (f : A  bool) (m : M A) : mapset M :=
  Mapset $ merge (λ x _,
    match x with
    | Some a => if f a then Some () else None | None => None
    end) m (@empty (M A) _).

Lemma lookup_mapset_map_with {A B} (f : bool  A  option B) X m i :
  mapset_map_with f X m !! i = m !! i = f (bool_decide (i  X)).
Proof.
  destruct X as [mX]. unfold mapset_map_with, elem_of, mapset_elem_of.
  rewrite lookup_merge by done. simpl.
  by case_bool_decide; destruct (mX !! i) as [[]|], (m !! i).
Qed.
Lemma elem_of_mapset_dom_with {A} (f : A  bool) m i :
  i  mapset_dom_with f m   x, m !! i = Some x  f x.
Proof.
  unfold mapset_dom_with, elem_of, mapset_elem_of.
  simpl. rewrite lookup_merge by done. destruct (m !! i) as [a|].
118
119
  - destruct (Is_true_reflect (f a)); naive_solver.
  - naive_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
Qed.
Instance mapset_dom {A} : Dom (M A) (mapset M) := mapset_dom_with (λ _, true).
Instance mapset_dom_spec: FinMapDom K M (mapset M).
Proof.
  split; try apply _. intros. unfold dom, mapset_dom, is_Some.
  rewrite elem_of_mapset_dom_with; naive_solver.
Qed.
End mapset.

(** These instances are declared using [Hint Extern] to avoid too
eager type class search. *)
Hint Extern 1 (ElemOf _ (mapset _)) =>
  eapply @mapset_elem_of : typeclass_instances.
Hint Extern 1 (Empty (mapset _)) =>
  eapply @mapset_empty : typeclass_instances.
Hint Extern 1 (Singleton _ (mapset _)) =>
  eapply @mapset_singleton : typeclass_instances.
Hint Extern 1 (Union (mapset _)) =>
  eapply @mapset_union : typeclass_instances.
Hint Extern 1 (Intersection (mapset _)) =>
  eapply @mapset_intersection : typeclass_instances.
Hint Extern 1 (Difference (mapset _)) =>
  eapply @mapset_difference : typeclass_instances.
Hint Extern 1 (Elements _ (mapset _)) =>
  eapply @mapset_elems : typeclass_instances.
Arguments mapset_eq_dec _ _ _ _ : simpl never.