mapset.v 5.8 KB
Newer Older
1
(* Copyright (c) 2012-2017, Robbert Krebbers. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
2
3
4
5
(* 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.
7
(* FIXME: This file needs a 'Proof Using' hint. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
8
9
10
11
12
13
14
15
16
17
18
19
20

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,
21
  Mapset {[ x := () ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
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 | | ].
41
  - unfold empty, elem_of, mapset_empty, mapset_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
42
    simpl. intros. by simpl_map.
43
  - unfold singleton, elem_of, mapset_singleton, mapset_elem_of.
44
    simpl. by split; intros; simplify_map_eq.
45
  - unfold union, elem_of, mapset_union, mapset_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
47
    intros [m1] [m2] ?. simpl. rewrite lookup_union_Some_raw.
    destruct (m1 !! x) as [[]|]; tauto.
48
  - unfold intersection, elem_of, mapset_intersection, mapset_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
49
50
51
52
    intros [m1] [m2] ?. simpl. rewrite lookup_intersection_Some.
    assert (is_Some (m2 !! x)  m2 !! x = Some ()).
    { split; eauto. by intros [[] ?]. }
    naive_solver.
53
  - unfold difference, elem_of, mapset_difference, mapset_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
54
55
56
    intros [m1] [m2] ?. simpl. rewrite lookup_difference_Some.
    destruct (m2 !! x) as [[]|]; intuition congruence.
Qed.
57
58
Global Instance: LeibnizEquiv (mapset M).
Proof. intros ??. apply mapset_eq. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
60
61
Global Instance: FinCollection K (mapset M).
Proof.
  split.
62
63
  - apply _.
  - unfold elements, elem_of at 2, mapset_elems, mapset_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
66
    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.
67
  - unfold elements, mapset_elems. intros [m]. simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
68
69
70
    apply NoDup_fst_map_to_list.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
71
Section deciders.
72
73
  Context `{EqDecision (M unit)}.
  Global Instance mapset_eq_dec : EqDecision (mapset M) | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
  Proof.
75
76
   refine (λ X1 X2,
    match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end);
Robbert Krebbers's avatar
Robbert Krebbers committed
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
    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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
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|].
119
120
  - destruct (Is_true_reflect (f a)); naive_solver.
  - naive_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
146
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.