mapset.v 5.48 KB
Newer Older
1
2
3
(** 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. *)
Janno's avatar
Janno committed
4
From stdpp Require Export countable fin_map_dom.
5
(* FIXME: This file needs a 'Proof Using' hint. *)
6

Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
Record mapset (M : Type  Type) : Type :=
  Mapset { mapset_car: M (unit : Type) }.
9
10
Arguments Mapset {_} _ : assert.
Arguments mapset_car {_} _ : assert.
11
12
13
14

Section mapset.
Context `{FinMap K M}.

15
Global Instance mapset_elem_of: ElemOf K (mapset M) := λ x X,
16
  mapset_car X !! x = Some ().
17
18
Global Instance mapset_empty: Empty (mapset M) := Mapset .
Global Instance mapset_singleton: Singleton K (mapset M) := λ x,
19
  Mapset {[ x := () ]}.
20
Global Instance mapset_union: Union (mapset M) := λ X1 X2,
21
  let (m1) := X1 in let (m2) := X2 in Mapset (m1  m2).
22
Global Instance mapset_intersection: Intersection (mapset M) := λ X1 X2,
23
  let (m1) := X1 in let (m2) := X2 in Mapset (m1  m2).
24
Global Instance mapset_difference: Difference (mapset M) := λ X1 X2,
25
  let (m1) := X1 in let (m2) := X2 in Mapset (m1  m2).
26
Global Instance mapset_elements: Elements K (mapset M) := λ X,
27
  let (m) := X in (map_to_list m).*1.
28

Robbert Krebbers's avatar
Robbert Krebbers committed
29
Lemma mapset_eq (X1 X2 : mapset M) : X1 = X2   x, x  X1  x  X2.
30
Proof.
31
  split; [by intros ->|].
32
33
  destruct X1 as [m1], X2 as [m2]. simpl. intros E.
  f_equal. apply map_eq. intros i. apply option_eq. intros []. by apply E.
34
35
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
69
Section deciders.
70
71
  Context `{EqDecision (M unit)}.
  Global Instance mapset_eq_dec : EqDecision (mapset M) | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
  Proof.
73
74
   refine (λ X1 X2,
    match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end);
Robbert Krebbers's avatar
Robbert Krebbers committed
75
76
    abstract congruence.
  Defined.
77
  Global Program Instance mapset_countable `{Countable (M ())} : Countable (mapset M) :=
Janno's avatar
Janno committed
78
79
    inj_countable mapset_car (Some  Mapset) _.
  Next Obligation. by intros ? ? []. Qed.
80
  Global Instance mapset_equiv_dec : RelDecision (@{mapset M}) | 1.
81
  Proof. refine (λ X1 X2, cast_if (decide (X1 = X2))); abstract (by fold_leibniz). Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
  Global Instance mapset_elem_of_dec : RelDecision (@{mapset M}) | 1.
83
  Proof. refine (λ x X, cast_if (decide (mapset_car X !! x = Some ()))); done. Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
  Global Instance mapset_disjoint_dec : RelDecision (##@{mapset M}).
Robbert Krebbers's avatar
Robbert Krebbers committed
85
  Proof.
86
   refine (λ X1 X2, cast_if (decide (X1  X2 = )));
Robbert Krebbers's avatar
Robbert Krebbers committed
87
88
    abstract (by rewrite disjoint_intersection_L).
  Defined.
89
  Global Instance mapset_subseteq_dec : RelDecision (@{mapset M}).
Robbert Krebbers's avatar
Robbert Krebbers committed
90
  Proof.
91
   refine (λ X1 X2, cast_if (decide (X1  X2 = X2)));
Robbert Krebbers's avatar
Robbert Krebbers committed
92
93
94
95
    abstract (by rewrite subseteq_union_L).
  Defined.
End deciders.

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

108
109
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)).
110
111
112
113
114
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.
115
Lemma elem_of_mapset_dom_with {A} (f : A  bool) m i :
116
117
118
  i  mapset_dom_with f m   x, m !! i = Some x  f x.
Proof.
  unfold mapset_dom_with, elem_of, mapset_elem_of.
119
  simpl. rewrite lookup_merge by done. destruct (m !! i) as [a|].
120
121
  - destruct (Is_true_reflect (f a)); naive_solver.
  - naive_solver.
122
Qed.
123
Instance mapset_dom {A} : Dom (M A) (mapset M) := mapset_dom_with (λ _, true).
Robbert Krebbers's avatar
Robbert Krebbers committed
124
Instance mapset_dom_spec: FinMapDom K M (mapset M).
125
Proof.
126
127
  split; try apply _. intros. unfold dom, mapset_dom, is_Some.
  rewrite elem_of_mapset_dom_with; naive_solver.
128
129
130
Qed.
End mapset.

131
132
133
134
(** [mapset_elem_of] internally contains an equality; make sure that tactics do
not unfold it and try to unify [∈] against goals with [=]. *)
Opaque mapset_elem_of.

135
Arguments mapset_eq_dec : simpl never.