gmap.v 10.5 KB
Newer Older
1
(* Copyright (c) 2012-2017, Coq-std++ developers. *)
2
3
4
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite maps and finite sets with keys of any countable
type. The implementation is based on [Pmap]s, radix-2 search trees. *)
5
From stdpp Require Export countable fin_maps fin_map_dom.
6
From stdpp Require Import pmap mapset set.
7
Set Default Proof Using "Type".
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

(** * The data structure *)
(** We pack a [Pmap] together with a proof that ensures that all keys correspond
to codes of actual elements of the countable type. *)
Definition gmap_wf `{Countable K} {A} : Pmap A  Prop :=
  map_Forall (λ p _, encode <$> decode p = Some p).
Record gmap K `{Countable K} A := GMap {
  gmap_car : Pmap A;
  gmap_prf : bool_decide (gmap_wf gmap_car)
}.
Arguments GMap {_ _ _ _} _ _.
Arguments gmap_car {_ _ _ _} _.
Lemma gmap_eq `{Countable K} {A} (m1 m2 : gmap K A) :
  m1 = m2  gmap_car m1 = gmap_car m2.
Proof.
23
  split; [by intros ->|intros]. destruct m1, m2; simplify_eq/=.
24
25
  f_equal; apply proof_irrel.
Qed.
26
Instance gmap_eq_eq `{Countable K, EqDecision A} : EqDecision (gmap K A).
27
Proof.
28
 refine (λ m1 m2, cast_if (decide (gmap_car m1 = gmap_car m2)));
29
30
31
32
  abstract (by rewrite gmap_eq).
Defined.

(** * Operations on the data structure *)
33
Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) := λ i m,
34
35
  let (m,_) := m in m !! encode i.
Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap  I.
36
Global Opaque gmap_empty.
37
38
39
40
Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A  option A) m i :
  gmap_wf m  gmap_wf (partial_alter f (encode i) m).
Proof.
  intros Hm p x. destruct (decide (encode i = p)) as [<-|?].
41
42
  - rewrite decode_encode; eauto.
  - rewrite lookup_partial_alter_ne by done. by apply Hm.
43
Qed.
44
45
Instance gmap_partial_alter `{Countable K} {A} :
    PartialAlter K A (gmap K A) := λ f i m,
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
  let (m,Hm) := m in GMap (partial_alter f (encode i) m)
    (bool_decide_pack _ (gmap_partial_alter_wf f m i
    (bool_decide_unpack _ Hm))).
Lemma gmap_fmap_wf `{Countable K} {A B} (f : A  B) m :
  gmap_wf m  gmap_wf (f <$> m).
Proof. intros ? p x. rewrite lookup_fmap, fmap_Some; intros (?&?&?); eauto. Qed.
Instance gmap_fmap `{Countable K} : FMap (gmap K) := λ A B f m,
  let (m,Hm) := m in GMap (f <$> m)
    (bool_decide_pack _ (gmap_fmap_wf f m (bool_decide_unpack _ Hm))).
Lemma gmap_omap_wf `{Countable K} {A B} (f : A  option B) m :
  gmap_wf m  gmap_wf (omap f m).
Proof. intros ? p x; rewrite lookup_omap, bind_Some; intros (?&?&?); eauto. Qed.
Instance gmap_omap `{Countable K} : OMap (gmap K) := λ A B f m,
  let (m,Hm) := m in GMap (omap f m)
    (bool_decide_pack _ (gmap_omap_wf f m (bool_decide_unpack _ Hm))).
Lemma gmap_merge_wf `{Countable K} {A B C}
    (f : option A  option B  option C) m1 m2 :
  let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
  gmap_wf m1  gmap_wf m2  gmap_wf (merge f' m1 m2).
Proof.
  intros f' Hm1 Hm2 p z; rewrite lookup_merge by done; intros.
  destruct (m1 !! _) eqn:?, (m2 !! _) eqn:?; naive_solver.
Qed.
Instance gmap_merge `{Countable K} : Merge (gmap K) := λ A B C f m1 m2,
  let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
  let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
  GMap (merge f' m1 m2) (bool_decide_pack _ (gmap_merge_wf f _ _
    (bool_decide_unpack _ Hm1) (bool_decide_unpack _ Hm2))).
74
Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ m,
75
76
77
78
79
80
81
  let (m,_) := m in omap (λ ix : positive * A,
    let (i,x) := ix in (,x) <$> decode i) (map_to_list m).

(** * Instantiation of the finite map interface *)
Instance gmap_finmap `{Countable K} : FinMap K (gmap K).
Proof.
  split.
82
  - unfold lookup; intros A [m1 Hm1] [m2 Hm2] Hm.
83
84
85
86
    apply gmap_eq, map_eq; intros i; simpl in *.
    apply bool_decide_unpack in Hm1; apply bool_decide_unpack in Hm2.
    apply option_eq; intros x; split; intros Hi.
    + pose proof (Hm1 i x Hi); simpl in *.
87
      by destruct (decode i); simplify_eq/=; rewrite <-Hm.
88
    + pose proof (Hm2 i x Hi); simpl in *.
89
      by destruct (decode i); simplify_eq/=; rewrite Hm.
90
91
92
  - done.
  - intros A f [m Hm] i; apply (lookup_partial_alter f m).
  - intros A f [m Hm] i j Hs; apply (lookup_partial_alter_ne f m).
93
    by contradict Hs; apply (inj encode).
94
95
  - intros A B f [m Hm] i; apply (lookup_fmap f m).
  - intros A [m Hm]; unfold map_to_list; simpl.
96
97
    apply bool_decide_unpack, map_Forall_to_list in Hm; revert Hm.
    induction (NoDup_map_to_list m) as [|[p x] l Hpx];
98
99
100
      inversion 1 as [|??? Hm']; simplify_eq/=; [by constructor|].
    destruct (decode p) as [i|] eqn:?; simplify_eq/=; constructor; eauto.
    rewrite elem_of_list_omap; intros ([p' x']&?&?); simplify_eq/=.
101
    feed pose proof (proj1 (Forall_forall _ _) Hm' (p',x')); simpl in *; auto.
102
    by destruct (decode p') as [i'|]; simplify_eq/=.
103
  - intros A [m Hm] i x; unfold map_to_list, lookup; simpl.
104
105
106
    apply bool_decide_unpack in Hm; rewrite elem_of_list_omap; split.
    + intros ([p' x']&Hp'&?); apply elem_of_map_to_list in Hp'.
      feed pose proof (Hm p' x'); simpl in *; auto.
107
      by destruct (decode p') as [i'|] eqn:?; simplify_eq/=.
108
109
    + intros; exists (encode i,x); simpl.
      by rewrite elem_of_map_to_list, decode_encode.
110
111
  - intros A B f [m Hm] i; apply (lookup_omap f m).
  - intros A B C f ? [m1 Hm1] [m2 Hm2] i; unfold merge, lookup; simpl.
112
113
114
115
    set (f' o1 o2 := match o1, o2 with None,None => None | _, _ => f o1 o2 end).
    by rewrite lookup_merge by done; destruct (m1 !! _), (m2 !! _).
Qed.

116
117
118
119
120
121
122
123
124
125
Program Instance gmap_countable
    `{Countable K, Countable A} : Countable (gmap K A) := {
  encode m := encode (map_to_list m : list (K * A));
  decode p := map_of_list <$> decode p
}.
Next Obligation.
  intros K ?? A ?? m; simpl. rewrite decode_encode; simpl.
  by rewrite map_of_to_list.
Qed.

126
127
128
129
130
131
132
(** * Curry and uncurry *)
Definition gmap_curry `{Countable K1, Countable K2} {A} :
    gmap K1 (gmap K2 A)  gmap (K1 * K2) A :=
  map_fold (λ i1 m' macc,
    map_fold (λ i2 x, <[(i1,i2):=x]>) macc m') .
Definition gmap_uncurry `{Countable K1, Countable K2} {A} :
    gmap (K1 * K2) A  gmap K1 (gmap K2 A) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
133
  map_fold (λ ii x, let '(i1,i2) := ii in
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
    partial_alter (Some  <[i2:=x]>  from_option id ) i1) .

Section curry_uncurry.
  Context `{Countable K1, Countable K2} {A : Type}.

  Lemma lookup_gmap_curry (m : gmap K1 (gmap K2 A)) i j :
    gmap_curry m !! (i,j) = m !! i = (!! j).
  Proof.
    apply (map_fold_ind (λ mr m, mr !! (i,j) = m !! i = (!! j))).
    { by rewrite !lookup_empty. }
    clear m; intros i' m2 m m12 Hi' IH.
    apply (map_fold_ind (λ m2r m2, m2r !! (i,j) = <[i':=m2]> m !! i = (!! j))).
    { rewrite IH. destruct (decide (i' = i)) as [->|].
      - rewrite lookup_insert, Hi'; simpl; by rewrite lookup_empty.
      - by rewrite lookup_insert_ne by done. }
    intros j' y m2' m12' Hj' IH'. destruct (decide (i = i')) as [->|].
    - rewrite lookup_insert; simpl. destruct (decide (j = j')) as [->|].
      + by rewrite !lookup_insert.
      + by rewrite !lookup_insert_ne, IH', lookup_insert by congruence.
    - by rewrite !lookup_insert_ne, IH', lookup_insert_ne by congruence.
  Qed.

  Lemma lookup_gmap_uncurry (m : gmap (K1 * K2) A) i j :
    gmap_uncurry m !! i = (!! j) = m !! (i, j).
  Proof.
    apply (map_fold_ind (λ mr m, mr !! i = (!! j) = m !! (i, j))).
    { by rewrite !lookup_empty. }
    clear m; intros [i' j'] x m12 mr Hij' IH.
    destruct (decide (i = i')) as [->|].
    - rewrite lookup_partial_alter. destruct (decide (j = j')) as [->|].
      + destruct (mr !! i'); simpl; by rewrite !lookup_insert.
      + destruct (mr !! i'); simpl; by rewrite !lookup_insert_ne by congruence.
    - by rewrite lookup_partial_alter_ne, lookup_insert_ne by congruence.
  Qed.

  Lemma gmap_curry_uncurry (m : gmap (K1 * K2) A) :
    gmap_curry (gmap_uncurry m) = m.
  Proof.
   apply map_eq; intros [i j]. by rewrite lookup_gmap_curry, lookup_gmap_uncurry.
  Qed.
End curry_uncurry.

176
177
(** * Finite sets *)
Notation gset K := (mapset (gmap K)).
178
Instance gset_dom `{Countable K} {A} : Dom (gmap K A) (gset K) := mapset_dom.
179
180
Instance gset_dom_spec `{Countable K} :
  FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
181

Robbert Krebbers's avatar
Robbert Krebbers committed
182
183
184
185
Definition of_gset `{Countable A} (X : gset A) : set A := mkSet (λ x, x  X).
Lemma elem_of_of_gset `{Countable A} (X : gset A) x : x  of_gset X  x  X.
Proof. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
Definition to_gmap `{Countable K} {A} (x : A) (X : gset K) : gmap K A :=
  (λ _, x) <$> mapset_car X.

Lemma lookup_to_gmap `{Countable K} {A} (x : A) (X : gset K) i :
  to_gmap x X !! i = guard (i  X); Some x.
Proof.
  destruct X as [X]; unfold to_gmap, elem_of, mapset_elem_of; simpl.
  rewrite lookup_fmap.
  case_option_guard; destruct (X !! i) as [[]|]; naive_solver.
Qed.
Lemma lookup_to_gmap_Some `{Countable K} {A} (x : A) (X : gset K) i y :
  to_gmap x X !! i = Some y  i  X  x = y.
Proof. rewrite lookup_to_gmap. simplify_option_eq; naive_solver. Qed.
Lemma lookup_to_gmap_None `{Countable K} {A} (x : A) (X : gset K) i :
  to_gmap x X !! i = None  i  X.
Proof. rewrite lookup_to_gmap. simplify_option_eq; naive_solver. Qed.

Lemma to_gmap_empty `{Countable K} {A} (x : A) : to_gmap x  = .
Proof. apply fmap_empty. Qed.
Lemma to_gmap_union_singleton `{Countable K} {A} (x : A) i Y :
  to_gmap x ({[ i ]}  Y) = <[i:=x]>(to_gmap x Y).
Proof.
  apply map_eq; intros j; apply option_eq; intros y.
  rewrite lookup_insert_Some, !lookup_to_gmap_Some, elem_of_union,
    elem_of_singleton; destruct (decide (i = j)); intuition.
Qed.

213
214
215
216
217
218
Lemma fmap_to_gmap `{Countable K} {A B} (f : A  B) (X : gset K) (x : A) :
  f <$> to_gmap x X = to_gmap (f x) X.
Proof.
  apply map_eq; intros j. rewrite lookup_fmap, !lookup_to_gmap.
  by simplify_option_eq.
Qed.
219
220
221
222
223
224
225
226
227
Lemma to_gmap_dom `{Countable K} {A B} (m : gmap K A) (y : B) :
  to_gmap y (dom _ m) = const y <$> m.
Proof.
  apply map_eq; intros j. rewrite lookup_fmap, lookup_to_gmap.
  destruct (m !! j) as [x|] eqn:?.
  - by rewrite option_guard_True by (rewrite elem_of_dom; eauto).
  - by rewrite option_guard_False by (rewrite not_elem_of_dom; eauto).
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
228
229
230
231
232
233
(** * Fresh elements *)
(* This is pretty ad-hoc and just for the case of [gset positive]. We need a
notion of countable non-finite types to generalize this. *)
Instance gset_positive_fresh : Fresh positive (gset positive) := λ X,
  let 'Mapset (GMap m _) := X in fresh (dom _ m).
Instance gset_positive_fresh_spec : FreshSpec positive (gset positive).
234
235
Proof.
  split.
236
237
238
  - apply _.
  - by intros X Y; rewrite <-elem_of_equiv_L; intros ->.
  - intros [[m Hm]]; unfold fresh; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
239
    by intros ?; apply (is_fresh (dom Pset m)), elem_of_dom_2 with ().
240
Qed.