fin_maps.v 57.2 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
138
139
140
141
142
143
144
145

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 *)
Lemma partial_alter_compose {A} (m : M A) i f g :
  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.
Lemma partial_alter_commute {A} (m : M A) i j f g :
146
  i  j  partial_alter f i (partial_alter g j m) =
147
148
    partial_alter g j (partial_alter f i m).
Proof.
149
  intros. apply map_eq. intros jj. destruct (decide (jj = j)).
150
151
152
153
154
155
156
157
158
159
  * 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.
160
  intros. apply map_eq. intros ii. destruct (decide (i = ii)).
161
162
163
  * subst. by rewrite lookup_partial_alter.
  * by rewrite lookup_partial_alter_ne.
Qed.
164
Lemma partial_alter_self {A} (m : M A) i : partial_alter (λ _, m !! i) i m = m.
165
166
167
Proof. by apply partial_alter_self_alt. Qed.

Lemma partial_alter_subseteq {A} (m : M A) i f :
168
169
  m !! i = None  m  partial_alter f i m.
Proof. intros Hi j x Hj. rewrite lookup_partial_alter_ne; congruence. Qed.
170
Lemma partial_alter_subset {A} (m : M A) i f :
171
  m !! i = None  is_Some (f (m !! i))  m  partial_alter f i m.
172
173
174
175
176
177
178
179
180
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 *)
181
Lemma lookup_alter {A} (f : A  A) m i : alter f i m !! i = f <$> m !! i.
182
Proof. apply lookup_partial_alter. Qed.
183
Lemma lookup_alter_ne {A} (f : A  A) m i j : i  j  alter f i m !! j = m !! j.
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
Proof. apply lookup_partial_alter_ne. Qed.

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.

202
Lemma alter_None {A} (f : A  A) m i : m !! i = None  alter f i m = m.
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
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.
233
Lemma delete_singleton {A} i (x : A) : delete i {[i, x]} = .
234
235
236
237
238
239
240
241
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.

242
Lemma delete_notin {A} (m : M A) i : m !! i = None  delete i m = m.
243
Proof.
244
  intros. apply map_eq. intros j. destruct (decide (i = j)).
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
  * 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.

266
Lemma delete_subseteq {A} (m : M A) i : delete i m  m.
267
268
Proof. intros j x. rewrite lookup_delete_Some. tauto. Qed.
Lemma delete_subseteq_compat {A} (m1 m2 : M A) i :
269
  m1  m2  delete i m1  delete i m2.
270
Proof. intros ? j x. rewrite !lookup_delete_Some. intuition eauto. Qed.
271
Lemma delete_subset_alt {A} (m : M A) i x : m !! i = Some x  delete i m  m.
272
273
274
275
276
277
Proof.
  split.
  * apply delete_subseteq.
  * intros Hi. apply (None_ne_Some x).
    by rewrite <-(lookup_delete m i), (Hi i x).
Qed.
278
Lemma delete_subset {A} (m : M A) i : is_Some (m !! i)  delete i m  m.
279
280
281
282
283
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.
284
Lemma lookup_insert_rev {A}  (m : M A) i x y : <[i:=x]>m !! i = Some y  x = y.
285
Proof. rewrite lookup_insert. congruence. Qed.
286
Lemma lookup_insert_ne {A} (m : M A) i j x : i  j  <[i:=x]>m !! j = m !! j.
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
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.

311
Lemma insert_subseteq {A} (m : M A) i x : m !! i = None  m  <[i:=x]>m.
312
Proof. apply partial_alter_subseteq. Qed.
313
Lemma insert_subset {A} (m : M A) i x : m !! i = None  m  <[i:=x]>m.
314
315
Proof. intro. apply partial_alter_subset; eauto. Qed.
Lemma insert_subseteq_r {A} (m1 m2 : M A) i x :
316
  m1 !! i = None  m1  m2  m1  <[i:=x]>m2.
317
318
319
320
321
322
323
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 :
324
  m1 !! i = None  <[i:=x]> m1  m2  m1  delete i m2.
325
326
327
328
329
330
331
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 :
332
  m1 !! i = Some x  delete i m1  m2  m1  <[i:=x]> m2.
333
334
335
Proof.
  intros Hix Hi j y Hj. destruct (decide (i = j)); subst.
  * rewrite lookup_insert. congruence.
336
  * rewrite lookup_insert_ne by done. apply Hi. by rewrite lookup_delete_ne.
337
338
339
Qed.

Lemma insert_delete_subset {A} (m1 m2 : M A) i x :
340
  m1 !! i = None  <[i:=x]> m1  m2  m1  delete i m2.
341
342
343
344
345
346
347
348
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 :
349
  m1 !! i = None  <[i:=x]> m1  m2 
350
351
352
   m2', m2 = <[i:=x]>m2'  m1  m2'  m2' !! i = None.
Proof.
  intros Hi Hm1m2. exists (delete i m2). split_ands.
353
  * rewrite insert_delete. done. eapply lookup_weaken, subset_subseteq; eauto.
354
355
356
357
358
359
360
    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) :
361
  {[i, x]} !! j = Some y  i = j  x = y.
362
363
Proof.
  unfold singleton, map_singleton.
364
  rewrite lookup_insert_Some, lookup_empty. simpl. intuition congruence.
365
Qed.
366
Lemma lookup_singleton_None {A} i j (x : A) : {[i, x]} !! j = None  i  j.
367
368
369
370
Proof.
  unfold singleton, map_singleton.
  rewrite lookup_insert_None, lookup_empty. simpl. tauto.
Qed.
371
Lemma lookup_singleton {A} i (x : A) : {[i, x]} !! i = Some x.
372
Proof. by rewrite lookup_singleton_Some. Qed.
373
Lemma lookup_singleton_ne {A} i j (x : A) : i  j  {[i, x]} !! j = None.
374
375
Proof. by rewrite lookup_singleton_None. Qed.

376
Lemma insert_singleton {A} i (x y : A) : <[i:=y]>{[i, x]} = {[i, y]}.
377
378
379
380
Proof.
  unfold singleton, map_singleton, insert, map_insert.
  by rewrite <-partial_alter_compose.
Qed.
381
Lemma alter_singleton {A} (f : A  A) i x : alter f i {[i,x]} = {[i, f x]}.
382
383
384
385
386
387
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 :
388
  i  j  alter f i {[j,x]} = {[j,x]}.
389
390
391
392
393
394
395
396
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 :
397
  (i,x)  map_to_list m  (i,y)  map_to_list m  x = y.
398
Proof. rewrite !elem_of_map_to_list. congruence. Qed.
399
400
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.
401
402

Lemma elem_of_map_of_list_1 {A} (l : list (K * A)) i x :
403
  NoDup (fst <$> l)  (i,x)  l  map_of_list l !! i = Some x.
404
405
406
407
408
409
410
411
412
413
414
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 :
415
  map_of_list l !! i = Some x  (i,x)  l.
416
417
418
419
420
421
422
423
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 :
424
425
  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.
426
427

Lemma not_elem_of_map_of_list_1 {A} (l : list (K * A)) i :
428
  i  fst <$> l  map_of_list l !! i = None.
429
430
431
432
433
434
Proof.
  rewrite elem_of_list_fmap, eq_None_not_Some, is_Some_alt.
  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 :
435
  map_of_list l !! i = None  i  fst <$> l.
436
437
438
439
440
441
442
443
444
445
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.
446
  split; auto using not_elem_of_map_of_list_1, not_elem_of_map_of_list_2.
447
448
449
Qed.

Lemma map_of_list_proper {A} (l1 l2 : list (K * A)) :
450
  NoDup (fst <$> l1)  l1  l2  map_of_list l1 = map_of_list l2.
451
452
453
454
455
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)) :
456
457
  NoDup (fst <$> l1)  NoDup (fst <$> l2) 
  map_of_list l1 = map_of_list l2  l1  l2.
458
Proof.
459
  intros ?? Hl1l2. apply NoDup_Permutation; auto using (NoDup_fmap_1 fst).
460
461
  intros [i x]. by rewrite !elem_of_map_of_list, Hl1l2.
Qed.
462
Lemma map_of_to_list {A} (m : M A) : map_of_list (map_to_list m) = m.
463
464
465
466
467
468
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)) :
469
470
  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.
471
Lemma map_to_list_inj {A} (m1 m2 : M A) :
472
  map_to_list m1  map_to_list m2  m1 = m2.
473
Proof.
474
  intros. rewrite <-(map_of_to_list m1), <-(map_of_to_list m2).
475
476
477
  auto using map_of_list_proper, map_to_list_key_nodup.
Qed.

478
Lemma map_to_list_empty {A} : map_to_list  = @nil (K * A).
479
480
481
482
483
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 :
484
  m !! i = None  map_to_list (<[i:=x]>m)  (i,x) :: map_to_list m.
485
486
487
488
Proof.
  intros. apply map_of_list_inj; simpl.
  * apply map_to_list_key_nodup.
  * constructor; auto using map_to_list_key_nodup.
489
    rewrite elem_of_list_fmap. intros [[??] [? Hlookup]]; subst; simpl in *.
490
491
492
493
    rewrite elem_of_map_to_list in Hlookup. congruence.
  * by rewrite !map_of_to_list.
Qed.

494
Lemma map_of_list_nil {A} : map_of_list (@nil (K * A)) = .
495
496
497
498
499
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.

500
Lemma map_to_list_empty_inv_alt {A}  (m : M A) : map_to_list m  []  m = .
501
Proof. rewrite <-map_to_list_empty. apply map_to_list_inj. Qed.
502
Lemma map_to_list_empty_inv {A} (m : M A) : map_to_list m = []  m = .
503
504
505
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 :
506
  map_to_list m  (i,x) :: l  m = <[i:=x]>(map_of_list l).
507
508
509
510
511
512
513
514
515
516
517
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) :
518
  P   ( i x m, m !! i = None  P m  P (<[i:=x]>m))   m, P m.
519
520
Proof.
  intros Hemp Hins.
521
  cut ( l, NoDup (fst <$> l)   m, map_to_list m  l  P m).
522
523
524
525
526
527
528
529
530
531
532
  { 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) :
533
  m1  m2  length (map_to_list m1) < length (map_to_list m2).
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
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.

Lemma map_wf {A} : wf (@subset (M A) _).
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).

556
Lemma map_forall_to_list m : map_forall P m  Forall (curry P) (map_to_list m).
557
558
Proof.
  rewrite Forall_forall. split.
559
560
  * 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)).
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
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 _) ].
587
  intros Hlookup. apply map_eq. intros. rewrite Hlookup. apply (lookup_merge _).
588
589
590
591
592
593
594
595
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.
596
  by rewrite !(lookup_merge f), lookup_empty, (left_id_L None f).
597
598
599
600
Qed.
Global Instance: RightId (=) None f  RightId (=)  (merge f).
Proof.
  intros ??. apply map_eq. intros.
601
  by rewrite !(lookup_merge f), lookup_empty, (right_id_L None f).
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
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.
621
  intros ????. apply merge_associative. intros. by apply (associative_L f).
622
623
Qed.
Lemma merge_idempotent m1 :
624
  ( i, f (m1 !! i) (m1 !! i) = m1 !! i)  merge f m1 m1 = m1.
625
626
Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
Global Instance: Idempotent (=) f  Idempotent (=) (merge f).
627
Proof. intros ??. apply merge_idempotent. intros. by apply (idempotent f). Qed.
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
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

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.
678
Lemma map_intersection_forall_empty_l (m : M A) : map_intersection_forall R  m.
679
Proof. intros ???. by rewrite lookup_empty. Qed.
680
Lemma map_intersection_forall_empty_r (m : M A) : map_intersection_forall R m .
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
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.
724
  unfold disjoint, map_disjoint. rewrite map_not_intersection_forall.
725
726
727
728
729
730
731
732
733
734
735
736
  * 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) :
737
  m1'  m2'  m1  m1'  m2  m2'  m1  m2.
738
739
740
741
742
743
744
745
746
747
748
749
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:
750
  m1  m2  m1 !! i = Some x  m2 !! i = None.
751
752
753
754
755
Proof.
  intros Hdisjoint ?. rewrite eq_None_not_Some, is_Some_alt.
  intros [x2 ?]. by apply (Hdisjoint i x x2).
Qed.
Lemma map_disjoint_Some_r {A} (m1 m2 : M A) i x:
756
  m1  m2  m2 !! i = Some x  m1 !! i = None.
757
758
Proof. rewrite (symmetry_iff ()). apply map_disjoint_Some_l. Qed.

759
Lemma map_disjoint_singleton_l {A} (m : M A) i x : {[i, x]}  m  m !! i = None.
760
761
Proof.
  split.
762
  * intro. apply (map_disjoint_Some_l {[i, x]} _ _ x);
763
764
765
766
767
768
      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 :
769
  m  {[i, x]}  m !! i = None.
770
771
772
Proof. by rewrite (symmetry_iff ()), map_disjoint_singleton_l. Qed.

Lemma map_disjoint_singleton_l_2 {A} (m : M A) i x :
773
  m !! i = None  {[i, x]}  m.
774
775
Proof. by rewrite map_disjoint_singleton_l. Qed.
Lemma map_disjoint_singleton_r_2 {A} (m : M A) i x :
776
  m !! i = None  m  {[i, x]}.
777
778
Proof. by rewrite map_disjoint_singleton_r. Qed.

779
Lemma map_disjoint_delete_l {A} (m1 m2 : M A) i : m1  m2  delete i m1  m2.
780
781
782
783
784
Proof.
  rewrite !map_disjoint_alt.
  intros Hdisjoint j. destruct (Hdisjoint j); auto.
  rewrite lookup_delete_None. tauto.
Qed.
785
Lemma map_disjoint_delete_r {A} (m1 m2 : M A) i : m1  m2  m1  delete i m2.
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
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 :
815
  m1 !! i = Some x  m2 !! i = Some y  f x y = Some z 
816
817
818
  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 :
819
  m1 !! i = Some x  m2 !! i = None  union_with f m1 m2 !! i = Some x.
820
821
Proof. rewrite lookup_union_with. naive_solver. Qed.
Lemma lookup_union_with_Some_r m1 m2 i y :
822
  m1 !! i = None  m2 !! i = Some y  union_with f m1 m2 !! i = Some y.
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
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 :
841
  ( i x, m !! i = Some x  f x x = Some x)  union_with f m m = m.
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
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 :
886
  m2 !! i = None  <[i:=x]>(union_with f m1 m2) = union_with f (<[i:=x]>m1) m2.
887
888
889
890
891
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 :
892
  m1 !! i = None  <[i:=x]>(union_with f m1 m2) = union_with f m1 (<[i:=x]>m2).
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
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.
915
  unfold union, map_union, union_with, map_union_with. rewrite (lookup_merge _).
916
917
918
919
920
  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.
921
  unfold union, map_union, union_with, map_union_with. rewrite (lookup_merge _).
922
923
924
925
  destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
Qed.

Lemma lookup_union_Some {A} (m1 m2 : M A) i x :
926
  m1  m2  (m1  m2) !! i = Some x  m1 !! i = Some x  m2 !! i = Some x.
927
928
929
930
931
932
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 :
933
  m1 !! i = Some x  (m1  m2) !! i = Some x.
934
935
Proof. intro. rewrite lookup_union_Some_raw; intuition. Qed.
Lemma lookup_union_Some_r {A} (m1 m2 : M A) i x :
936
  m1  m2  m2 !! i = Some x  (m1  m2) !! i = Some x.
937
938
Proof. intro. rewrite lookup_union_Some; intuition. Qed.

939
Lemma map_union_commutative {A} (m1 m2 : M A) : m1  m2  m1  m2 = m2  m1.
940
941
942
943
944
945
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.

946
Lemma map_subseteq_union {A} (m1 m2 : M A) : m1  m2  m1  m2 = m2.
947
Proof.
948
  intros Hm1m2. apply map_eq. intros i. apply option_eq. intros x.
949
  rewrite lookup_union_Some_raw. split; [by intuition |].
950
  intros Hm2. specialize (Hm1m2 i). destruct (m1 !! i) as [y|]; [| by auto].
951
952
953
  rewrite (Hm1m2 y eq_refl) in Hm2. intuition congruence.
Qed.

954
Lemma map_union_subseteq_l {A} (m1 m2 : M A) : m1  m1  m2.
955
Proof. intros ? i x. rewrite lookup_union_Some_raw. intuition. Qed.
956
Lemma map_union_subseteq_r {A} (m1 m2 : M A) : m1  m2  m2  m1  m2.
957
Proof.
958
  intros. rewrite map_union_commutative by done. by apply map_union_subseteq_l.
959
960
Qed.

961
Lemma map_union_subseteq_l_alt {A} (m1 m2 m3 : M A) : m1  m2  m1  m2  m3.
962
963
Proof. intros. transitivity m2; auto using map_union_subseteq_l. Qed.
Lemma map_union_subseteq_r_alt {A} (m1 m2 m3 : M A) :
964
  m2  m3  m1  m3  m1  m2  m3.
965
966
Proof. intros.