fin_maps.v 57.1 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
Proof.
430
  rewrite elem_of_list_fmap, eq_None_not_Some.
431 432 433 434
  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
Proof.
752
  intros Hdisjoint ?. rewrite eq_None_not_Some.
753 754 755
  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