fin_maps.v 58 KB
Newer Older
1
(* Copyright (c) 2012-2013, Robbert Krebbers. *)
2
3
4
(* This file is distributed under the terms of the BSD license. *)
(** Finite maps associate data to keys. This file defines an interface for
finite maps and collects some theory on it. Most importantly, it proves useful
5
6
induction principles for finite maps and implements the tactic
[simplify_map_equality] to simplify goals involving finite maps. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
7
Require Import Permutation.
8
9
Require Export ars vector orders.

10
11
(** * Axiomatization of finite maps *)
(** We require Leibniz equality to be extensional on finite maps. This of
12
13
14
15
16
course limits the space of finite map implementations, but since we are mainly
interested in finite maps with numbers as indexes, we do not consider this to
be a serious limitation. The main application of finite maps is to implement
the memory, where extensionality of Leibniz equality is very important for a
convenient use in the assertions of our axiomatic semantics. *)
17

Robbert Krebbers's avatar
Robbert Krebbers committed
18
19
(** Finiteness is axiomatized by requiring that each map can be translated
to an association list. The translation to association lists is used to
20
prove well founded recursion on finite maps. *)
21

22
23
24
(** Finite map implementations are required to implement the [merge] function
which enables us to give a generic implementation of [union_with],
[intersection_with], and [difference_with]. *)
25

26
Class FinMapToList K A M := map_to_list: M  list (K * A).
Robbert Krebbers's avatar
Robbert Krebbers committed
27

28
Class FinMap K M `{!FMap M}
29
30
    `{ A, Lookup K A (M A)} `{ A, Empty (M A)} `{ A, PartialAlter K A (M A)}
    `{!Merge M} `{ A, FinMapToList K A (M A)}
31
    `{ i j : K, Decision (i = j)} := {
32
33
  map_eq {A} (m1 m2 : M A) : ( i, m1 !! i = m2 !! i)  m1 = m2;
  lookup_empty {A} i : ( : M A) !! i = None;
34
35
36
37
  lookup_partial_alter {A} f (m : M A) i :
    partial_alter f i m !! i = f (m !! i);
  lookup_partial_alter_ne {A} f (m : M A) i j :
    i  j  partial_alter f i m !! j = m !! j;
38
39
  lookup_fmap {A B} (f : A  B) (m : M A) i : (f <$> m) !! i = f <$> m !! i;
  map_to_list_nodup {A} (m : M A) : NoDup (map_to_list m);
40
41
42
43
44
  elem_of_map_to_list {A} (m : M A) i x :
    (i,x)  map_to_list m  m !! i = Some x;
  lookup_merge {A B C} (f : option A  option B  option C)
      `{!PropHolds (f None None = None)} m1 m2 i :
    merge f m1 m2 !! i = f (m1 !! i) (m2 !! i)
Robbert Krebbers's avatar
Robbert Krebbers committed
45
46
}.

47
48
49
(** * Derived operations *)
(** All of the following functions are defined in a generic way for arbitrary
finite map implementations. These generic implementations do not cause a
50
51
significant performance loss to make including them in the finite map interface
worthwhile. *)
52
53
54
55
56
Instance map_insert `{PartialAlter K A M} : Insert K A M :=
  λ i x, partial_alter (λ _, Some x) i.
Instance map_alter `{PartialAlter K A M} : Alter K A M :=
  λ f, partial_alter (fmap f).
Instance map_delete `{PartialAlter K A M} : Delete K M :=
57
  partial_alter (λ _, None).
58
Instance map_singleton `{PartialAlter K A M}
59
  `{Empty M} : Singleton (K * A) M := λ p, <[fst p:=snd p]>.
Robbert Krebbers's avatar
Robbert Krebbers committed
60

61
Definition map_of_list `{Insert K A M} `{Empty M}
62
  (l : list (K * A)) : M := insert_list l .
Robbert Krebbers's avatar
Robbert Krebbers committed
63

64
65
66
67
68
69
Instance map_union_with `{Merge M} {A} : UnionWith A (M A) :=
  λ f, merge (union_with f).
Instance map_intersection_with `{Merge M} {A} : IntersectionWith A (M A) :=
  λ f, merge (intersection_with f).
Instance map_difference_with `{Merge M} {A} : DifferenceWith A (M A) :=
  λ f, merge (difference_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
70

71
72
(** The relation [intersection_forall R] on finite maps describes that the
relation [R] holds for each pair in the intersection. *)
73
Definition map_forall `{Lookup K A M} (P : K  A  Prop) : M  Prop :=
Robbert Krebbers's avatar
Robbert Krebbers committed
74
  λ m,  i x, m !! i = Some x  P i x.
75
Definition map_intersection_forall `{Lookup K A M}
Robbert Krebbers's avatar
Robbert Krebbers committed
76
77
    (R : relation A) : relation M := λ m1 m2,
   i x1 x2, m1 !! i = Some x1  m2 !! i = Some x2  R x1 x2.
78
79
Instance map_disjoint `{ A, Lookup K A (M A)} : Disjoint (M A) :=
  λ A, map_intersection_forall (λ _ _, False).
Robbert Krebbers's avatar
Robbert Krebbers committed
80
81
82
83
84

(** The union of two finite maps only has a meaningful definition for maps
that are disjoint. However, as working with partial functions is inconvenient
in Coq, we define the union as a total function. In case both finite maps
have a value at the same index, we take the value of the first map. *)
85
Instance map_union `{Merge M} {A} : Union (M A) := union_with (λ x _, Some x).
86
87
88
Instance map_intersection `{Merge M} {A} : Intersection (M A) :=
  intersection_with (λ x _, Some x).

89
90
(** The difference operation removes all values from the first map whose
index contains a value in the second map as well. *)
91
Instance map_difference `{Merge M} {A} : Difference (M A) :=
92
  difference_with (λ _ _, None).
Robbert Krebbers's avatar
Robbert Krebbers committed
93

94
95
96
97
98
99
100
101
(** * Theorems *)
Section theorems.
Context `{FinMap K M}.

Global Instance map_subseteq {A} : SubsetEq (M A) := λ m1 m2,
   i x, m1 !! i = Some x  m2 !! i = Some x.
Global Instance: BoundedPreOrder (M A).
Proof. split; [firstorder |]. intros m i x. by rewrite lookup_empty. Qed.
102
Global Instance : PartialOrder (@subseteq (M A) _).
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
Proof.
  split; [apply _ |].
  intros ????. apply map_eq. intros i. apply option_eq. naive_solver.
Qed.

Lemma lookup_weaken {A} (m1 m2 : M A) i x :
  m1 !! i = Some x  m1  m2  m2 !! i = Some x.
Proof. auto. Qed.
Lemma lookup_weaken_is_Some {A} (m1 m2 : M A) i :
  is_Some (m1 !! i)  m1  m2  is_Some (m2 !! i).
Proof. inversion 1. eauto using lookup_weaken. Qed.
Lemma lookup_weaken_None {A} (m1 m2 : M A) i :
  m2 !! i = None  m1  m2  m1 !! i = None.
Proof.
  rewrite eq_None_not_Some. intros Hm2 Hm1m2.
  specialize (Hm1m2 i). destruct (m1 !! i); naive_solver.
Qed.

Lemma lookup_weaken_inv {A} (m1 m2 : M A) i x y :
122
123
  m1 !! i = Some x  m1  m2  m2 !! i = Some y  x = y.
Proof. intros Hm1 ? Hm2. eapply lookup_weaken in Hm1; eauto. congruence. Qed.
124
125
126
127
128
129
130
131
132
133
134
135
136
137

Lemma lookup_ne {A} (m : M A) i j : m !! i  m !! j  i  j.
Proof. congruence. Qed.
Lemma map_empty {A} (m : M A) : ( i, m !! i = None)  m = .
Proof. intros Hm. apply map_eq. intros. by rewrite Hm, lookup_empty. Qed.
Lemma lookup_empty_is_Some {A} i : ¬is_Some (( : M A) !! i).
Proof. rewrite lookup_empty. by inversion 1. Qed.
Lemma lookup_empty_Some {A} i (x : A) : ¬ !! i = Some x.
Proof. by rewrite lookup_empty. Qed.

Lemma map_subset_empty {A} (m : M A) : m  .
Proof. intros [? []]. intros i x. by rewrite lookup_empty. Qed.

(** ** Properties of the [partial_alter] operation *)
138
139
140
141
142
143
144
145
Lemma partial_alter_ext {A} (f g : option A  option A) (m : M A) i :
  ( x, m !! i = x  f x = g x)  partial_alter f i m = partial_alter g i m.
Proof.
  intros Hfg. apply map_eq. intros j. destruct (decide (i = j)); subst.
  * rewrite !lookup_partial_alter. by apply Hfg.
  * by rewrite !lookup_partial_alter_ne.
Qed.
Lemma partial_alter_compose {A} f g (m : M A) i:
146
147
148
149
150
151
  partial_alter (f  g) i m = partial_alter f i (partial_alter g i m).
Proof.
  intros. apply map_eq. intros ii. case (decide (i = ii)).
  * intros. subst. by rewrite !lookup_partial_alter.
  * intros. by rewrite !lookup_partial_alter_ne.
Qed.
152
Lemma partial_alter_commute {A} f g (m : M A) i j :
153
  i  j  partial_alter f i (partial_alter g j m) =
154
155
    partial_alter g j (partial_alter f i m).
Proof.
156
  intros. apply map_eq. intros jj. destruct (decide (jj = j)).
157
158
159
160
161
162
163
164
165
166
  * subst. by rewrite lookup_partial_alter_ne,
      !lookup_partial_alter, lookup_partial_alter_ne.
  * destruct (decide (jj = i)).
    + subst. by rewrite lookup_partial_alter,
       !lookup_partial_alter_ne, lookup_partial_alter by congruence.
    + by rewrite !lookup_partial_alter_ne by congruence.
Qed.
Lemma partial_alter_self_alt {A} (m : M A) i x :
  x = m !! i  partial_alter (λ _, x) i m = m.
Proof.
167
  intros. apply map_eq. intros ii. destruct (decide (i = ii)).
168
169
170
  * subst. by rewrite lookup_partial_alter.
  * by rewrite lookup_partial_alter_ne.
Qed.
171
Lemma partial_alter_self {A} (m : M A) i : partial_alter (λ _, m !! i) i m = m.
172
173
Proof. by apply partial_alter_self_alt. Qed.

174
Lemma partial_alter_subseteq {A} f (m : M A) i :
175
176
  m !! i = None  m  partial_alter f i m.
Proof. intros Hi j x Hj. rewrite lookup_partial_alter_ne; congruence. Qed.
177
Lemma partial_alter_subset {A} f (m : M A) i :
178
  m !! i = None  is_Some (f (m !! i))  m  partial_alter f i m.
179
180
181
182
183
184
185
186
187
Proof.
  intros Hi Hfi. split.
  * by apply partial_alter_subseteq.
  * inversion Hfi as [x Hx]. intros Hm.
    apply (Some_ne_None x). rewrite <-(Hm i x); [done|].
    by rewrite lookup_partial_alter.
Qed.

(** ** Properties of the [alter] operation *)
188
189
190
191
Lemma alter_ext {A} (f g : A  A) (m : M A) i :
  ( x, m !! i = Some x  f x = g x)  alter f i m = alter g i m.
Proof. intro. apply partial_alter_ext. intros [x|] ?; simpl; f_equal; auto. Qed.

192
Lemma lookup_alter {A} (f : A  A) m i : alter f i m !! i = f <$> m !! i.
193
Proof. apply lookup_partial_alter. Qed.
194
Lemma lookup_alter_ne {A} (f : A  A) m i j : i  j  alter f i m !! j = m !! j.
195
196
Proof. apply lookup_partial_alter_ne. Qed.

197
198
199
200
201
202
203
204
205
206
207
Lemma alter_compose {A} (f g : A  A) (m : M A) i:
  alter (f  g) i m = alter f i (alter g i m).
Proof.
  unfold alter, map_alter. rewrite <-partial_alter_compose.
  apply partial_alter_ext. by intros [?|].
Qed.

Lemma alter_commute {A} (f g : A  A) (m : M A) i j :
  i  j  alter f i (alter g j m) = alter g j (alter f i m).
Proof. apply partial_alter_commute. Qed.

208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
Lemma lookup_alter_Some {A} (f : A  A) m i j y :
  alter f i m !! j = Some y 
    (i = j   x, m !! j = Some x  y = f x)  (i  j  m !! j = Some y).
Proof.
  destruct (decide (i = j)); subst.
  * rewrite lookup_alter. naive_solver (simplify_option_equality; eauto).
  * rewrite lookup_alter_ne by done. naive_solver.
Qed.
Lemma lookup_alter_None {A} (f : A  A) m i j :
  alter f i m !! j = None  m !! j = None.
Proof.
  destruct (decide (i = j)); subst.
  * by rewrite lookup_alter, fmap_None.
  * by rewrite lookup_alter_ne.
Qed.

224
Lemma alter_None {A} (f : A  A) m i : m !! i = None  alter f i m = m.
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
Proof.
  intros Hi. apply map_eq. intros j. destruct (decide (i = j)); subst.
  * by rewrite lookup_alter, !Hi.
  * by rewrite lookup_alter_ne.
Qed.

(** ** Properties of the [delete] operation *)
Lemma lookup_delete {A} (m : M A) i : delete i m !! i = None.
Proof. apply lookup_partial_alter. Qed.
Lemma lookup_delete_ne {A} (m : M A) i j : i  j  delete i m !! j = m !! j.
Proof. apply lookup_partial_alter_ne. Qed.

Lemma lookup_delete_Some {A} (m : M A) i j y :
  delete i m !! j = Some y  i  j  m !! j = Some y.
Proof.
  split.
  * destruct (decide (i = j)); subst;
      rewrite ?lookup_delete, ?lookup_delete_ne; intuition congruence.
  * intros [??]. by rewrite lookup_delete_ne.
Qed.
Lemma lookup_delete_None {A} (m : M A) i j :
  delete i m !! j = None  i = j  m !! j = None.
Proof.
  destruct (decide (i = j)).
  * subst. rewrite lookup_delete. tauto.
  * rewrite lookup_delete_ne; tauto.
Qed.

Lemma delete_empty {A} i : delete i ( : M A) = .
Proof. rewrite <-(partial_alter_self ) at 2. by rewrite lookup_empty. Qed.
255
Lemma delete_singleton {A} i (x : A) : delete i {[i, x]} = .
256
257
258
259
260
261
262
263
Proof. setoid_rewrite <-partial_alter_compose. apply delete_empty. Qed.
Lemma delete_commute {A} (m : M A) i j :
  delete i (delete j m) = delete j (delete i m).
Proof. destruct (decide (i = j)). by subst. by apply partial_alter_commute. Qed.
Lemma delete_insert_ne {A} (m : M A) i j x :
  i  j  delete i (<[j:=x]>m) = <[j:=x]>(delete i m).
Proof. intro. by apply partial_alter_commute. Qed.

264
Lemma delete_notin {A} (m : M A) i : m !! i = None  delete i m = m.
265
Proof.
266
  intros. apply map_eq. intros j. destruct (decide (i = j)).
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
  * subst. by rewrite lookup_delete.
  * by apply lookup_delete_ne.
Qed.

Lemma delete_partial_alter {A} (m : M A) i f :
  m !! i = None  delete i (partial_alter f i m) = m.
Proof.
  intros. unfold delete, map_delete. rewrite <-partial_alter_compose.
  unfold compose. by apply partial_alter_self_alt.
Qed.
Lemma delete_insert {A} (m : M A) i x :
  m !! i = None  delete i (<[i:=x]>m) = m.
Proof. apply delete_partial_alter. Qed.
Lemma insert_delete {A} (m : M A) i x :
  m !! i = Some x  <[i:=x]>(delete i m) = m.
Proof.
  intros Hmi. unfold delete, map_delete, insert, map_insert.
  rewrite <-partial_alter_compose. unfold compose. rewrite <-Hmi.
  by apply partial_alter_self_alt.
Qed.

288
Lemma delete_subseteq {A} (m : M A) i : delete i m  m.
289
290
Proof. intros j x. rewrite lookup_delete_Some. tauto. Qed.
Lemma delete_subseteq_compat {A} (m1 m2 : M A) i :
291
  m1  m2  delete i m1  delete i m2.
292
Proof. intros ? j x. rewrite !lookup_delete_Some. intuition eauto. Qed.
293
Lemma delete_subset_alt {A} (m : M A) i x : m !! i = Some x  delete i m  m.
294
295
296
297
298
299
Proof.
  split.
  * apply delete_subseteq.
  * intros Hi. apply (None_ne_Some x).
    by rewrite <-(lookup_delete m i), (Hi i x).
Qed.
300
Lemma delete_subset {A} (m : M A) i : is_Some (m !! i)  delete i m  m.
301
302
303
304
305
Proof. inversion 1. eauto using delete_subset_alt. Qed.

(** ** Properties of the [insert] operation *)
Lemma lookup_insert {A} (m : M A) i x : <[i:=x]>m !! i = Some x.
Proof. unfold insert. apply lookup_partial_alter. Qed.
306
Lemma lookup_insert_rev {A}  (m : M A) i x y : <[i:=x]>m !! i = Some y  x = y.
307
Proof. rewrite lookup_insert. congruence. Qed.
308
Lemma lookup_insert_ne {A} (m : M A) i j x : i  j  <[i:=x]>m !! j = m !! j.
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
Proof. unfold insert. apply lookup_partial_alter_ne. Qed.
Lemma insert_commute {A} (m : M A) i j x y :
  i  j  <[i:=x]>(<[j:=y]>m) = <[j:=y]>(<[i:=x]>m).
Proof. apply partial_alter_commute. Qed.

Lemma lookup_insert_Some {A} (m : M A) i j x y :
  <[i:=x]>m !! j = Some y  (i = j  x = y)  (i  j  m !! j = Some y).
Proof.
  split.
  * destruct (decide (i = j)); subst;
      rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
  * intros [[??]|[??]].
    + subst. apply lookup_insert.
    + by rewrite lookup_insert_ne.
Qed.
Lemma lookup_insert_None {A} (m : M A) i j x :
  <[i:=x]>m !! j = None  m !! j = None  i  j.
Proof.
  split.
  * destruct (decide (i = j)); subst;
      rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
  * intros [??]. by rewrite lookup_insert_ne.
Qed.

333
Lemma insert_subseteq {A} (m : M A) i x : m !! i = None  m  <[i:=x]>m.
334
Proof. apply partial_alter_subseteq. Qed.
335
Lemma insert_subset {A} (m : M A) i x : m !! i = None  m  <[i:=x]>m.
336
337
Proof. intro. apply partial_alter_subset; eauto. Qed.
Lemma insert_subseteq_r {A} (m1 m2 : M A) i x :
338
  m1 !! i = None  m1  m2  m1  <[i:=x]>m2.
339
340
341
342
343
344
345
Proof.
  intros ?? j ?. destruct (decide (j = i)); subst.
  * congruence.
  * rewrite lookup_insert_ne; auto.
Qed.

Lemma insert_delete_subseteq {A} (m1 m2 : M A) i x :
346
  m1 !! i = None  <[i:=x]> m1  m2  m1  delete i m2.
347
348
349
350
351
352
353
Proof.
  intros Hi Hix j y Hj. destruct (decide (i = j)); subst.
  * congruence.
  * rewrite lookup_delete_ne by done. apply Hix.
    by rewrite lookup_insert_ne by done.
Qed.
Lemma delete_insert_subseteq {A} (m1 m2 : M A) i x :
354
  m1 !! i = Some x  delete i m1  m2  m1  <[i:=x]> m2.
355
356
357
Proof.
  intros Hix Hi j y Hj. destruct (decide (i = j)); subst.
  * rewrite lookup_insert. congruence.
358
  * rewrite lookup_insert_ne by done. apply Hi. by rewrite lookup_delete_ne.
359
360
361
Qed.

Lemma insert_delete_subset {A} (m1 m2 : M A) i x :
362
  m1 !! i = None  <[i:=x]> m1  m2  m1  delete i m2.
363
364
365
366
367
368
369
370
Proof.
  intros ? [Hm12 Hm21]. split.
  * eauto using insert_delete_subseteq.
  * contradict Hm21. apply delete_insert_subseteq; auto.
    apply Hm12. by rewrite lookup_insert.
Qed.

Lemma insert_subset_inv {A} (m1 m2 : M A) i x :
371
  m1 !! i = None  <[i:=x]> m1  m2 
372
373
374
   m2', m2 = <[i:=x]>m2'  m1  m2'  m2' !! i = None.
Proof.
  intros Hi Hm1m2. exists (delete i m2). split_ands.
375
  * rewrite insert_delete. done. eapply lookup_weaken, strict_include; eauto.
376
377
378
379
380
381
382
    by rewrite lookup_insert.
  * eauto using insert_delete_subset.
  * by rewrite lookup_delete.
Qed.

(** ** Properties of the singleton maps *)
Lemma lookup_singleton_Some {A} i j (x y : A) :
383
  {[i, x]} !! j = Some y  i = j  x = y.
384
385
Proof.
  unfold singleton, map_singleton.
386
  rewrite lookup_insert_Some, lookup_empty. simpl. intuition congruence.
387
Qed.
388
Lemma lookup_singleton_None {A} i j (x : A) : {[i, x]} !! j = None  i  j.
389
390
391
392
Proof.
  unfold singleton, map_singleton.
  rewrite lookup_insert_None, lookup_empty. simpl. tauto.
Qed.
393
Lemma lookup_singleton {A} i (x : A) : {[i, x]} !! i = Some x.
394
Proof. by rewrite lookup_singleton_Some. Qed.
395
Lemma lookup_singleton_ne {A} i j (x : A) : i  j  {[i, x]} !! j = None.
396
397
Proof. by rewrite lookup_singleton_None. Qed.

398
Lemma insert_singleton {A} i (x y : A) : <[i:=y]>{[i, x]} = {[i, y]}.
399
400
401
402
Proof.
  unfold singleton, map_singleton, insert, map_insert.
  by rewrite <-partial_alter_compose.
Qed.
403
Lemma alter_singleton {A} (f : A  A) i x : alter f i {[i,x]} = {[i, f x]}.
404
405
406
407
408
409
Proof.
  intros. apply map_eq. intros i'. destruct (decide (i = i')); subst.
  * by rewrite lookup_alter, !lookup_singleton.
  * by rewrite lookup_alter_ne, !lookup_singleton_ne.
Qed.
Lemma alter_singleton_ne {A} (f : A  A) i j x :
410
  i  j  alter f i {[j,x]} = {[j,x]}.
411
412
413
414
415
416
417
418
Proof.
  intros. apply map_eq. intros i'. destruct (decide (i = i')); subst.
  * by rewrite lookup_alter, lookup_singleton_ne.
  * by rewrite lookup_alter_ne.
Qed.

(** ** Properties of conversion to lists *)
Lemma map_to_list_unique {A} (m : M A) i x y :
419
  (i,x)  map_to_list m  (i,y)  map_to_list m  x = y.
420
Proof. rewrite !elem_of_map_to_list. congruence. Qed.
421
422
Lemma map_to_list_key_nodup {A} (m : M A) : NoDup (fst <$> map_to_list m).
Proof. eauto using NoDup_fmap_fst, map_to_list_unique, map_to_list_nodup. Qed.
423
424

Lemma elem_of_map_of_list_1 {A} (l : list (K * A)) i x :
425
  NoDup (fst <$> l)  (i,x)  l  map_of_list l !! i = Some x.
426
427
428
429
430
431
432
433
434
435
436
Proof.
  induction l as [|[j y] l IH]; simpl.
  { by rewrite elem_of_nil. }
  rewrite NoDup_cons, elem_of_cons, elem_of_list_fmap.
  intros [Hl ?] [?|?]; simplify_equality.
  { by rewrite lookup_insert. }
  destruct (decide (i = j)); simplify_equality.
  * destruct Hl. by exists (j,x).
  * rewrite lookup_insert_ne; auto.
Qed.
Lemma elem_of_map_of_list_2 {A} (l : list (K * A)) i x :
437
  map_of_list l !! i = Some x  (i,x)  l.
438
439
440
441
442
443
444
445
Proof.
  induction l as [|[j y] l IH]; simpl.
  { by rewrite lookup_empty. }
  rewrite elem_of_cons. destruct (decide (i = j)); simplify_equality.
  * rewrite lookup_insert; intuition congruence.
  * rewrite lookup_insert_ne; intuition congruence.
Qed.
Lemma elem_of_map_of_list {A} (l : list (K * A)) i x :
446
447
  NoDup (fst <$> l)  (i,x)  l  map_of_list l !! i = Some x.
Proof. split; auto using elem_of_map_of_list_1, elem_of_map_of_list_2. Qed.
448
449

Lemma not_elem_of_map_of_list_1 {A} (l : list (K * A)) i :
450
  i  fst <$> l  map_of_list l !! i = None.
451
Proof.
452
  rewrite elem_of_list_fmap, eq_None_not_Some.
453
454
455
456
  intros Hi [x ?]. destruct Hi. exists (i,x). simpl.
  auto using elem_of_map_of_list_2.
Qed.
Lemma not_elem_of_map_of_list_2 {A} (l : list (K * A)) i :
457
  map_of_list l !! i = None  i  fst <$> l.
458
459
460
461
462
463
464
465
466
467
Proof.
  induction l as [|[j y] l IH]; simpl.
  { rewrite elem_of_nil. tauto. }
  rewrite elem_of_cons. destruct (decide (i = j)); simplify_equality.
  * by rewrite lookup_insert.
  * by rewrite lookup_insert_ne; intuition.
Qed.
Lemma not_elem_of_map_of_list {A} (l : list (K * A)) i :
  i  fst <$> l  map_of_list l !! i = None.
Proof.
468
  split; auto using not_elem_of_map_of_list_1, not_elem_of_map_of_list_2.
469
470
471
Qed.

Lemma map_of_list_proper {A} (l1 l2 : list (K * A)) :
472
  NoDup (fst <$> l1)  l1  l2  map_of_list l1 = map_of_list l2.
473
474
475
476
477
Proof.
  intros ? Hperm. apply map_eq. intros i. apply option_eq. intros x.
  by rewrite <-!elem_of_map_of_list; rewrite <-?Hperm.
Qed.
Lemma map_of_list_inj {A} (l1 l2 : list (K * A)) :
478
479
  NoDup (fst <$> l1)  NoDup (fst <$> l2) 
  map_of_list l1 = map_of_list l2  l1  l2.
480
Proof.
481
  intros ?? Hl1l2. apply NoDup_Permutation; auto using (fmap_nodup_1 fst).
482
483
  intros [i x]. by rewrite !elem_of_map_of_list, Hl1l2.
Qed.
484
Lemma map_of_to_list {A} (m : M A) : map_of_list (map_to_list m) = m.
485
486
487
488
489
490
Proof.
  apply map_eq. intros i. apply option_eq. intros x.
  by rewrite <-elem_of_map_of_list, elem_of_map_to_list
    by auto using map_to_list_key_nodup.
Qed.
Lemma map_to_of_list {A} (l : list (K * A)) :
491
492
  NoDup (fst <$> l)  map_to_list (map_of_list l)  l.
Proof. auto using map_of_list_inj, map_to_list_key_nodup, map_of_to_list. Qed.
493
Lemma map_to_list_inj {A} (m1 m2 : M A) :
494
  map_to_list m1  map_to_list m2  m1 = m2.
495
Proof.
496
  intros. rewrite <-(map_of_to_list m1), <-(map_of_to_list m2).
497
498
499
  auto using map_of_list_proper, map_to_list_key_nodup.
Qed.

500
Lemma map_to_list_empty {A} : map_to_list  = @nil (K * A).
501
502
503
504
505
Proof.
  apply elem_of_nil_inv. intros [i x].
  rewrite elem_of_map_to_list. apply lookup_empty_Some.
Qed.
Lemma map_to_list_insert {A} (m : M A) i x :
506
  m !! i = None  map_to_list (<[i:=x]>m)  (i,x) :: map_to_list m.
507
508
509
510
Proof.
  intros. apply map_of_list_inj; simpl.
  * apply map_to_list_key_nodup.
  * constructor; auto using map_to_list_key_nodup.
511
    rewrite elem_of_list_fmap. intros [[??] [? Hlookup]]; subst; simpl in *.
512
513
514
515
    rewrite elem_of_map_to_list in Hlookup. congruence.
  * by rewrite !map_of_to_list.
Qed.

516
Lemma map_of_list_nil {A} : map_of_list (@nil (K * A)) = .
517
518
519
520
521
Proof. done. Qed.
Lemma map_of_list_cons {A} (l : list (K * A)) i x :
  map_of_list ((i, x) :: l) = <[i:=x]>(map_of_list l).
Proof. done. Qed.

522
Lemma map_to_list_empty_inv_alt {A}  (m : M A) : map_to_list m  []  m = .
523
Proof. rewrite <-map_to_list_empty. apply map_to_list_inj. Qed.
524
Lemma map_to_list_empty_inv {A} (m : M A) : map_to_list m = []  m = .
525
526
527
Proof. intros Hm. apply map_to_list_empty_inv_alt. by rewrite Hm. Qed.

Lemma map_to_list_insert_inv {A} (m : M A) l i x :
528
  map_to_list m  (i,x) :: l  m = <[i:=x]>(map_of_list l).
529
530
531
532
533
534
535
536
537
538
539
Proof.
  intros Hperm. apply map_to_list_inj.
  assert (NoDup (fst <$> (i, x) :: l)) as Hnodup.
  { rewrite <-Hperm. auto using map_to_list_key_nodup. }
  simpl in Hnodup. rewrite NoDup_cons in Hnodup. destruct Hnodup.
  rewrite Hperm, map_to_list_insert, map_to_of_list;
    auto using not_elem_of_map_of_list_1.
Qed.

(** * Induction principles *)
Lemma map_ind {A} (P : M A  Prop) :
540
  P   ( i x m, m !! i = None  P m  P (<[i:=x]>m))   m, P m.
541
542
Proof.
  intros Hemp Hins.
543
  cut ( l, NoDup (fst <$> l)   m, map_to_list m  l  P m).
544
545
546
547
548
549
550
551
552
553
554
  { intros help m.
    apply (help (map_to_list m)); auto using map_to_list_key_nodup. }
  induction l as [|[i x] l IH]; intros Hnodup m Hml.
  { apply map_to_list_empty_inv_alt in Hml. by subst. }
  inversion_clear Hnodup.
  apply map_to_list_insert_inv in Hml. subst. apply Hins.
  * by apply not_elem_of_map_of_list_1.
  * apply IH; auto using map_to_of_list.
Qed.

Lemma map_to_list_length {A} (m1 m2 : M A) :
555
  m1  m2  length (map_to_list m1) < length (map_to_list m2).
556
557
558
559
560
561
562
563
564
565
566
Proof.
  revert m2. induction m1 as [|i x m ? IH] using map_ind.
  { intros m2 Hm2. rewrite map_to_list_empty. simpl.
    apply neq_0_lt. intros Hlen. symmetry in Hlen.
    apply nil_length, map_to_list_empty_inv in Hlen.
    rewrite Hlen in Hm2. destruct (irreflexivity ()  Hm2). }
  intros m2 Hm2.
  destruct (insert_subset_inv m m2 i x) as (m2'&?&?&?); auto; subst.
  rewrite !map_to_list_insert; simpl; auto with arith.
Qed.

567
Lemma map_wf {A} : wf (strict (@subseteq (M A) _)).
568
569
570
571
572
573
574
575
576
577
Proof.
  apply (wf_projected (<) (length  map_to_list)).
  * by apply map_to_list_length.
  * by apply lt_wf.
Qed.

(** ** Properties of the [map_forall] predicate *)
Section map_forall.
Context {A} (P : K  A  Prop).

578
Lemma map_forall_to_list m : map_forall P m  Forall (curry P) (map_to_list m).
579
580
Proof.
  rewrite Forall_forall. split.
581
582
  * intros Hforall [i x]. rewrite elem_of_map_to_list. by apply (Hforall i x).
  * intros Hforall i x. rewrite <-elem_of_map_to_list. by apply (Hforall (i,x)).
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
Qed.

Context `{ i x, Decision (P i x)}.
Global Instance map_forall_dec m : Decision (map_forall P m).
Proof.
  refine (cast_if (decide (Forall (curry P) (map_to_list m))));
    by rewrite map_forall_to_list.
Defined.

Lemma map_not_forall (m : M A) :
  ¬map_forall P m   i x, m !! i = Some x  ¬P i x.
Proof.
  split.
  * rewrite map_forall_to_list. intros Hm.
    apply (not_Forall_Exists _), Exists_exists in Hm.
    destruct Hm as ([i x]&?&?). exists i x. by rewrite <-elem_of_map_to_list.
  * intros (i&x&?&?) Hm. specialize (Hm i x). tauto.
Qed.
End map_forall.

(** ** Properties of the [merge] operation *)
Lemma merge_Some {A B C} (f : option A  option B  option C)
    `{!PropHolds (f None None = None)} m1 m2 m :
  ( i, m !! i = f (m1 !! i) (m2 !! i))  merge f m1 m2 = m.
Proof.
  split; [| intro; subst; apply (lookup_merge _) ].
609
  intros Hlookup. apply map_eq. intros. rewrite Hlookup. apply (lookup_merge _).
610
611
612
613
614
615
616
617
Qed.

Section merge.
Context {A} (f : option A  option A  option A).

Global Instance: LeftId (=) None f  LeftId (=)  (merge f).
Proof.
  intros ??. apply map_eq. intros.
618
  by rewrite !(lookup_merge f), lookup_empty, (left_id_L None f).
619
620
621
622
Qed.
Global Instance: RightId (=) None f  RightId (=)  (merge f).
Proof.
  intros ??. apply map_eq. intros.
623
  by rewrite !(lookup_merge f), lookup_empty, (right_id_L None f).
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
Qed.

Context `{!PropHolds (f None None = None)}.

Lemma merge_commutative m1 m2 :
  ( i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) 
  merge f m1 m2 = merge f m2 m1.
Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
Global Instance: Commutative (=) f  Commutative (=) (merge f).
Proof.
  intros ???. apply merge_commutative. intros. by apply (commutative f).
Qed.
Lemma merge_associative m1 m2 m3 :
  ( i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) =
        f (f (m1 !! i) (m2 !! i)) (m3 !! i)) 
  merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3.
Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
Global Instance: Associative (=) f  Associative (=) (merge f).
Proof.
643
  intros ????. apply merge_associative. intros. by apply (associative_L f).
644
645
Qed.
Lemma merge_idempotent m1 :
646
  ( i, f (m1 !! i) (m1 !! i) = m1 !! i)  merge f m1 m1 = m1.
647
648
Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
Global Instance: Idempotent (=) f  Idempotent (=) (merge f).
649
Proof. intros ??. apply merge_idempotent. intros. by apply (idempotent f). Qed.
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699

Lemma partial_alter_merge (g g1 g2 : option A  option A) m1 m2 i :
  g (f (m1 !! i) (m2 !! i)) = f (g1 (m1 !! i)) (g2 (m2 !! i)) 
  partial_alter g i (merge f m1 m2) =
    merge f (partial_alter g1 i m1) (partial_alter g2 i m2).
Proof.
  intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
  * by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
  * by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
Qed.
Lemma partial_alter_merge_l (g g1 : option A  option A) m1 m2 i :
  g (f (m1 !! i) (m2 !! i)) = f (g1 (m1 !! i)) (m2 !! i) 
  partial_alter g i (merge f m1 m2) = merge f (partial_alter g1 i m1) m2.
Proof.
  intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
  * by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
  * by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
Qed.
Lemma partial_alter_merge_r (g g2 : option A  option A) m1 m2 i :
  g (f (m1 !! i) (m2 !! i)) = f (m1 !! i) (g2 (m2 !! i)) 
  partial_alter g i (merge f m1 m2) = merge f m1 (partial_alter g2 i m2).
Proof.
  intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
  * by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
  * by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
Qed.

Lemma insert_merge_l m1 m2 i x :
  f (Some x) (m2 !! i) = Some x 
  <[i:=x]>(merge f m1 m2) = merge f (<[i:=x]>m1) m2.
Proof.
  intros. unfold insert, map_insert, alter, map_alter.
  by apply partial_alter_merge_l.
Qed.
Lemma insert_merge_r m1 m2 i x :
  f (m1 !! i) (Some x) = Some x 
  <[i:=x]>(merge f m1 m2) = merge f m1 (<[i:=x]>m2).
Proof.
  intros. unfold insert, map_insert, alter, map_alter.
  by apply partial_alter_merge_r.
Qed.
End merge.

(** ** Properties on the [map_intersection_forall] relation *)
Section intersection_forall.
Context {A} (R : relation A).

Global Instance map_intersection_forall_sym:
  Symmetric R  Symmetric (map_intersection_forall R).
Proof. firstorder auto. Qed.
700
Lemma map_intersection_forall_empty_l (m : M A) : map_intersection_forall R  m.
701
Proof. intros ???. by rewrite lookup_empty. Qed.
702
Lemma map_intersection_forall_empty_r (m : M A) : map_intersection_forall R m .
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
Proof. intros ???. by rewrite lookup_empty. Qed.

Lemma map_intersection_forall_alt (m1 m2 : M A) :
  map_intersection_forall R m1 m2 
    map_forall (λ _, curry R) (merge (λ x y,
      match x, y with
      | Some x, Some y => Some (x,y)
      | _, _ => None
      end) m1 m2).
Proof.
  split.
  * intros Hm12 i [x y]. rewrite lookup_merge by done. intros.
    destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simplify_equality.
    eapply Hm12; eauto.
  * intros Hm12 i x y ??. apply (Hm12 i (x,y)).
    rewrite lookup_merge by done. by simplify_option_equality.
Qed.

(** Due to the finiteness of finite maps, we can extract a witness if the
relation does not hold. *)
Lemma map_not_intersection_forall `{ x y, Decision (R x y)} (m1 m2 : M A) :
  ¬map_intersection_forall R m1 m2
      i x1 x2, m1 !! i = Some x1  m2 !! i = Some x2  ¬R x1 x2.
Proof.
  split.
  * rewrite map_intersection_forall_alt, (map_not_forall _).
    intros (i & [x y] & Hm12 & ?). rewrite lookup_merge in Hm12 by done.
    exists i x y. by destruct (m1 !! i), (m2 !! i); simplify_equality.
  * intros (i & x1 & x2 & Hx1 & Hx2 & Hx1x2) Hm12.
    by apply Hx1x2, (Hm12 i x1 x2).
Qed.
End intersection_forall.

(** ** Properties on the disjoint maps *)
Lemma map_disjoint_alt {A} (m1 m2 : M A) :
  m1  m2   i, m1 !! i = None  m2 !! i = None.
Proof.
  split; intros Hm1m2 i; specialize (Hm1m2 i);
    destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
Lemma map_not_disjoint {A} (m1 m2 : M A) :
  ¬m1  m2   i x1 x2, m1 !! i = Some x1  m2 !! i = Some x2.
Proof.
746
  unfold disjoint, map_disjoint. rewrite map_not_intersection_forall.
747
748
749
750
751
752
753
754
755
756
757
758
  * naive_solver.
  * right. auto.
Qed.

Global Instance: Symmetric (@disjoint (M A) _).
Proof. intro. apply map_intersection_forall_sym. auto. Qed.
Lemma map_disjoint_empty_l {A} (m : M A) :   m.
Proof. apply map_intersection_forall_empty_l. Qed.
Lemma map_disjoint_empty_r {A} (m : M A) : m  .
Proof. apply map_intersection_forall_empty_r. Qed.

Lemma map_disjoint_weaken {A} (m1 m1' m2 m2' : M A) :
759
  m1'  m2'  m1  m1'  m2  m2'  m1  m2.
760
761
762
763
764
765
766
767
768
769
770
771
Proof.
  intros Hdisjoint Hm1 Hm2 i x1 x2 Hx1 Hx2.
  destruct (Hdisjoint i x1 x2); auto.
Qed.
Lemma map_disjoint_weaken_l {A} (m1 m1' m2  : M A) :
  m1'  m2  m1  m1'  m1  m2.
Proof. eauto using map_disjoint_weaken. Qed.
Lemma map_disjoint_weaken_r {A} (m1 m2 m2' : M A) :
  m1  m2'  m2  m2'  m1  m2.
Proof. eauto using map_disjoint_weaken. Qed.

Lemma map_disjoint_Some_l {A} (m1 m2 : M A) i x:
772
  m1  m2  m1 !! i = Some x  m2 !! i = None.
773
Proof.
774
  intros Hdisjoint ?. rewrite eq_None_not_Some.
775
776
777
  intros [x2 ?]. by apply (Hdisjoint i x x2).
Qed.
Lemma map_disjoint_Some_r {A} (m1 m2 : M A) i x:
778
  m1  m2  m2 !! i = Some x  m1 !! i = None.
779
780
Proof. rewrite (symmetry_iff ()). apply map_disjoint_Some_l. Qed.

781
Lemma map_disjoint_singleton_l {A} (m : M A) i x : {[i, x]}  m  m !! i = None.
782
783
Proof.
  split.
784
  * intro. apply (map_disjoint_Some_l {[i, x]} _ _ x);
785
786
787
788
789
790
      auto using lookup_singleton.
  * intros ? j y1 y2. destruct (decide (i = j)); subst.
    + rewrite lookup_singleton. intuition congruence.
    + by rewrite lookup_singleton_ne.
Qed.
Lemma map_disjoint_singleton_r {A} (m : M A) i x :
791
  m  {[i, x]}  m !! i = None.
792
793
794
Proof. by rewrite (symmetry_iff ()), map_disjoint_singleton_l. Qed.

Lemma map_disjoint_singleton_l_2 {A} (m : M A) i x :
795
  m !! i = None  {[i, x]}  m.
796
797
Proof. by rewrite map_disjoint_singleton_l. Qed.
Lemma map_disjoint_singleton_r_2 {A} (m : M A) i x :
798
  m !! i = None  m  {[i, x]}.
799
800
Proof. by rewrite map_disjoint_singleton_r. Qed.

801
Lemma map_disjoint_delete_l {A} (m1 m2 : M A) i : m1  m2  delete i m1  m2.
802
803
804
805
806
Proof.
  rewrite !map_disjoint_alt.
  intros Hdisjoint j. destruct (Hdisjoint j); auto.
  rewrite lookup_delete_None. tauto.
Qed.
807
Lemma map_disjoint_delete_r {A} (m1 m2 : M A) i : m1  m2  m1  delete i m2.
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
Proof. symmetry. by apply map_disjoint_delete_l. Qed.

(** ** Properties of the [union_with] operation *)
Section union_with.
Context {A} (f : A  A  option A).

Lemma lookup_union_with m1 m2 i z :
  union_with f m1 m2 !! i = z 
    (m1 !! i = None  m2 !! i = None  z = None) 
    ( x, m1 !! i = Some x  m2 !! i = None  z = Some x) 
    ( y, m1 !! i = None  m2 !! i = Some y  z = Some y) 
    ( x y, m1 !! i = Some x  m2 !! i = Some y  z = f x y).
Proof.
  unfold union_with, map_union_with. rewrite (lookup_merge _).
  destruct (m1 !! i), (m2 !! i); compute; naive_solver.
Qed.
Lemma lookup_union_with_Some m1 m2 i z :
  union_with f m1 m2 !! i = Some z 
    (m1 !! i = Some z  m2 !! i = None) 
    (m1 !! i = None  m2 !! i = Some z) 
    ( x y, m1 !! i = Some x  m2 !! i = Some y  f x y = Some z).
Proof. rewrite lookup_union_with. naive_solver. Qed.
Lemma lookup_union_with_None m1 m2 i :
  union_with f m1 m2 !! i = None 
    (m1 !! i = None  m2 !! i = None) 
    ( x y, m1 !! i = Some x  m2 !! i = Some y  f x y = None).
Proof. rewrite lookup_union_with. naive_solver. Qed.

Lemma lookup_union_with_Some_lr m1 m2 i x y z :
837
  m1 !! i = Some x  m2 !! i = Some y  f x y = Some z 
838
839
840
  union_with f m1 m2 !! i = Some z.
Proof. rewrite lookup_union_with. naive_solver. Qed.
Lemma lookup_union_with_Some_l m1 m2 i x :
841
  m1 !! i = Some x  m2 !! i = None  union_with f m1 m2 !! i = Some x.
842
843
Proof. rewrite lookup_union_with. naive_solver. Qed.
Lemma lookup_union_with_Some_r m1 m2 i y :
844
  m1 !! i = None  m2 !! i = Some y  union_with f m1 m2 !! i = Some y.
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
Proof. rewrite lookup_union_with. naive_solver. Qed.

Global Instance: LeftId (@eq (M A))  (union_with f).
Proof. unfold union_with, map_union_with. apply _. Qed.
Global Instance: RightId (@eq (M A))  (union_with f).
Proof. unfold union_with, map_union_with. apply _. Qed.

Lemma union_with_commutative m1 m2 :
  ( i x y, m1 !! i = Some x  m2 !! i = Some y  f x y = f y x) 
  union_with f m1 m2 = union_with f m2 m1.
Proof.
  intros. apply (merge_commutative _). intros i.
  destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto.
Qed.
Global Instance: Commutative (=) f  Commutative (@eq (M A)) (union_with f).
Proof. intros ???. apply union_with_commutative. eauto. Qed.

Lemma union_with_idempotent m :
863
  ( i x, m !! i = Some x  f x x = Some x)  union_with f m m = m.
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
Proof.
  intros. apply (merge_idempotent _). intros i.
  destruct (m !! i) eqn:?; simpl; eauto.
Qed.

Lemma alter_union_with (g : A  A) m1 m2 i :
  ( x y, m1 !! i = Some x  m2 !! i = Some y  g <$> f x y = f (g x) (g y)) 
  alter g i (union_with f m1 m2) =
    union_with f (alter g i m1) (alter g i m2).
Proof.
  intros. apply (partial_alter_merge _).
  destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto.
Qed.
Lemma alter_union_with_l (g : A  A) m1 m2 i :
  ( x y, m1 !! i = Some x  m2 !! i = Some y  g <$> f x y = f (g x) y) 
  ( y, m1 !! i = None  m2 !! i = Some y  g y = y) 
  alter g i (union_with f m1 m2) = union_with f (alter g i m1) m2.
Proof.
  intros. apply (partial_alter_merge_l _).
  destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto using f_equal.
Qed.
Lemma alter_union_with_r (g : A  A) m1 m2 i :
  ( x y, m1 !! i = Some x  m2 !! i = Some y  g <$> f x y = f x (g y)) 
  ( x, m1 !! i = Some x  m2 !! i = None  g x = x) 
  alter g i (union_with f m1 m2) = union_with f m1 (alter g i m2).
Proof.
  intros. apply (partial_alter_merge_r _).
  destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto using f_equal.
Qed.

Lemma delete_union_with m1 m2 i :
  delete i (union_with f m1 m2) = union_with f (delete i m1) (delete i m2).
Proof. by apply (partial_alter_merge _). Qed.

Lemma delete_list_union_with (m1 m2 : M A) is :
  delete_list is (union_with f m1 m2) =
    union_with f (delete_list is m1) (delete_list is m2).
Proof. induction is; simpl. done. by rewrite IHis, delete_union_with. Qed.

Lemma insert_union_with m1 m2 i x :
  ( x, f x x = Some x) 
  <[i:=x]>(union_with f m1 m2) = union_with f (<[i:=x]>m1) (<[i:=x]>m2).
Proof. intros. apply (partial_alter_merge _). simpl. auto. Qed.
Lemma insert_union_with_l m1 m2 i x :
908
  m2 !! i = None  <[i:=x]>(union_with f m1 m2) = union_with f (<[i:=x]>m1) m2.
909
910
911
912
913
Proof.
  intros Hm2. unfold union_with, map_union_with.
  rewrite (insert_merge_l _). done. by rewrite Hm2.
Qed.
Lemma insert_union_with_r m1 m2 i x :
914
  m1 !! i = None  <[i:=x]>(union_with f m1 m2) = union_with f m1 (<[i:=x]>m2).
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
Proof.
  intros Hm1. unfold union_with, map_union_with.
  rewrite (insert_merge_r _). done. by rewrite Hm1.
Qed.
End union_with.

(** ** Properties of the [union] operation *)
Global Instance: LeftId (@eq (M A))  () := _.
Global Instance: RightId (@eq (M A))  () := _.
Global Instance: Associative (@eq (M A)) ().
Proof.
  intros A m1 m2 m3. unfold union, map_union, union_with, map_union_with.
  apply (merge_associative _). intros i.
  by destruct (m1 !! i), (m2 !! i), (m3 !! i).
Qed.
Global Instance: Idempotent (@eq (M A)) ().
Proof. intros A ?. by apply union_with_idempotent. Qed.

Lemma lookup_union_Some_raw {A} (m1 m2 : M A) i x :
  (m1  m2) !! i = Some x 
    m1 !! i = Some x  (m1 !! i = None  m2 !! i = Some x).
Proof.
937
  unfold union, map_union, union_with, map_union_with. rewrite (lookup_merge _).
938
939
940
941
942
  destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
Qed.
Lemma lookup_union_None {A} (m1 m2 : M A) i :
  (m1  m2) !! i = None  m1 !! i = None  m2 !! i = None.
Proof.
943
  unfold union, map_union, union_with, map_union_with. rewrite (lookup_merge _).
944
945
946
947
  destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
Qed.

Lemma lookup_union_Some {A} (m1 m2 : M A) i x :
948
  m1  m2  (m1  m2) !! i = Some x  m1 !! i = Some x  m2 !! i = Some x.
949
950
951
952
953
954
Proof.
  intros Hdisjoint. rewrite lookup_union_Some_raw.
  intuition eauto using map_disjoint_Some_r.
Qed.

Lemma lookup_union_Some_l {A} (m1 m2 : M A) i x :
955
  m1 !! i = Some x  (m1  m2) !! i = Some x.
956
957
Proof. intro. rewrite lookup_union_Some_raw; intuition. Qed.
Lemma lookup_union_Some_r {A} (m1 m2 : M A) i x :
958
  m1  m2  m2 !! i = Some x  (m1  m2) !! i = Some x.
959
960
Proof. intro. rewrite lookup_union_Some; intuition. Qed.

961
Lemma map_union_commutative {A} (m1 m2 : M A) : m1  m2  m1  m2 = m2  m1.
962
963
964
965
966
967
Proof.
  intros Hdisjoint. apply (merge_commutative (union_with (λ x _, Some x))).
  intros i. specialize (Hdisjoint i).
  destruct (m1 !! i), (m2 !! i); compute; naive_solver.
Qed.

968
Lemma map_subseteq_union {A} (m1 m2 : M A) : m1  m2  m1  m2 = m2.
969
Proof.
Robbert Krebbers's avatar