1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
|
(** 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. *)
From stdpp Require Export countable fin_map_dom.
From stdpp Require Import options.
(* FIXME: This file needs a 'Proof Using' hint, but they need to be set
locally (or things moved out of sections) as no default works well enough. *)
Unset Default Proof Using.
(** Given a type of maps [M : Type → Type], we construct sets as [M ()], i.e.,
maps with unit values. To avoid unnecessary universe constraints, we first
define [mapset' Munit] with [Munit : Type] as a record, and then [mapset M] with
[M : Type → Type] as a notation. See [tests/universes.v] for a test case that
fails otherwise. *)
Record mapset' (Munit : Type) : Type :=
Mapset { mapset_car: Munit }.
Notation mapset M := (mapset' (M unit)).
Global Arguments Mapset {_} _ : assert.
Global Arguments mapset_car {_} _ : assert.
Section mapset.
Context `{FinMap K M}.
Global Instance mapset_elem_of: ElemOf K (mapset M) := λ x X,
mapset_car X !! x = Some ().
Global Instance mapset_empty: Empty (mapset M) := Mapset ∅.
Global Instance mapset_singleton: Singleton K (mapset M) := λ x,
Mapset {[ x := () ]}.
Global Instance mapset_union: Union (mapset M) := λ X1 X2,
let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∪ m2).
Global Instance mapset_intersection: Intersection (mapset M) := λ X1 X2,
let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∩ m2).
Global Instance mapset_difference: Difference (mapset M) := λ X1 X2,
let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∖ m2).
Global Instance mapset_elements: 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.
Local Instance mapset_set: Set_ K (mapset M).
Proof.
split; [split | | ].
- unfold empty, elem_of, mapset_empty, mapset_elem_of.
simpl. intros. by simpl_map.
- unfold singleton, elem_of, mapset_singleton, mapset_elem_of.
simpl. by split; intros; simplify_map_eq.
- unfold union, elem_of, mapset_union, mapset_elem_of.
intros [m1] [m2] x. simpl. rewrite lookup_union_Some_raw.
destruct (m1 !! x) as [[]|]; tauto.
- unfold intersection, elem_of, mapset_intersection, mapset_elem_of.
intros [m1] [m2] x. simpl. rewrite lookup_intersection_Some.
assert (is_Some (m2 !! x) ↔ m2 !! x = Some ()).
{ split; eauto. by intros [[] ?]. }
naive_solver.
- unfold difference, elem_of, mapset_difference, mapset_elem_of.
intros [m1] [m2] x. simpl. rewrite lookup_difference_Some.
destruct (m2 !! x) as [[]|]; intuition congruence.
Qed.
Global Instance mapset_leibniz : LeibnizEquiv (mapset M).
Proof. intros ??. apply mapset_eq. Qed.
Global Instance mapset_fin_set : FinSet K (mapset M).
Proof.
split.
- apply _.
- unfold elements, elem_of at 2, mapset_elements, mapset_elem_of.
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.
- unfold elements, mapset_elements. intros [m]. simpl.
apply NoDup_fst_map_to_list.
Qed.
Section deciders.
Context `{EqDecision (M unit)}.
Global Instance mapset_eq_dec : EqDecision (mapset M) | 1.
Proof.
refine (λ X1 X2,
match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end);
abstract congruence.
Defined.
Global Program Instance mapset_countable `{Countable (M ())} : Countable (mapset M) :=
inj_countable mapset_car (Some ∘ Mapset) _.
Next Obligation. by intros ? ? []. Qed.
Global Instance mapset_equiv_dec : RelDecision (≡@{mapset M}) | 1.
Proof. refine (λ X1 X2, cast_if (decide (X1 = X2))); abstract (by fold_leibniz). Defined.
Global Instance mapset_elem_of_dec : RelDecision (∈@{mapset M}) | 1.
Proof. refine (λ x X, cast_if (decide (mapset_car X !! x = Some ()))); done. Defined.
Global Instance mapset_disjoint_dec : RelDecision (##@{mapset M}).
Proof.
refine (λ X1 X2, cast_if (decide (X1 ∩ X2 = ∅)));
abstract (by rewrite disjoint_intersection_L).
Defined.
Global Instance mapset_subseteq_dec : RelDecision (⊆@{mapset M}).
Proof.
refine (λ X1 X2, cast_if (decide (X1 ∪ X2 = X2)));
abstract (by rewrite subseteq_union_L).
Defined.
End deciders.
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 $ omap (λ a, if f a then Some () else None) m.
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_omap. destruct (m !! i) as [a|]; simpl.
- destruct (Is_true_reflect (f a)); naive_solver.
- naive_solver.
Qed.
Local Instance mapset_dom {A} : Dom (M A) (mapset M) := λ m,
Mapset $ fmap (λ _, ()) m.
Local Instance mapset_dom_spec: FinMapDom K M (mapset M).
Proof.
split; try apply _. intros A m i.
unfold dom, mapset_dom, is_Some, elem_of, mapset_elem_of; simpl.
rewrite lookup_fmap. destruct (m !! i); naive_solver.
Qed.
End mapset.
Global Arguments mapset_eq_dec : simpl never.
|
