fin_maps.v 92.8 KB
Newer Older
1
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
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
induction principles for finite maps and implements the tactic
6
[simplify_map_eq] to simplify goals involving finite maps. *)
7
From Coq Require Import Permutation.
8
From stdpp Require Export relations orders vector fin_sets.
9 10
(* FIXME: This file needs a 'Proof Using' hint, but the default we use
   everywhere makes for lots of extra ssumptions. *)
11

12 13
(** * Axiomatization of finite maps *)
(** We require Leibniz equality to be extensional on finite maps. This of
14 15 16 17 18
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. *)
19

20 21
(** Finiteness is axiomatized by requiring that each map can be translated
to an association list. The translation to association lists is used to
22
prove well founded recursion on finite maps. *)
23

24 25 26
(** 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]. *)
27

28
Class FinMapToList K A M := map_to_list: M  list (K * A).
29 30
Hint Mode FinMapToList ! - - : typeclass_instances.
Hint Mode FinMapToList - - ! : typeclass_instances.
31

32 33
Class FinMap K M `{FMap M,  A, Lookup K A (M A),  A, Empty (M A),  A,
    PartialAlter K A (M A), OMap M, Merge M,  A, FinMapToList K A (M A),
34
    EqDecision K} := {
35 36
  map_eq {A} (m1 m2 : M A) : ( i, m1 !! i = m2 !! i)  m1 = m2;
  lookup_empty {A} i : ( : M A) !! i = None;
37 38 39 40
  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;
41
  lookup_fmap {A B} (f : A  B) (m : M A) i : (f <$> m) !! i = f <$> m !! i;
42
  NoDup_map_to_list {A} (m : M A) : NoDup (map_to_list m);
43 44
  elem_of_map_to_list {A} (m : M A) i x :
    (i,x)  map_to_list m  m !! i = Some x;
45 46 47 48
  lookup_omap {A B} (f : A  option B) (m : M A) i :
    omap f m !! i = m !! i = f; 
  lookup_merge {A B C} (f : option A  option B  option C)
      `{!DiagNone f} (m1 : M A) (m2 : M B) i :
49
    merge f m1 m2 !! i = f (m1 !! i) (m2 !! i)
Robbert Krebbers's avatar
Robbert Krebbers committed
50 51
}.

52 53 54
(** * 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
55 56
significant performance loss, which justifies including them in the finite map
interface as primitive operations. *)
57 58 59 60 61 62 63 64 65
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 :=
  partial_alter (λ _, None).
Instance map_singleton `{PartialAlter K A M, Empty M} :
  SingletonM K A M := λ i x, <[i:=x]> .

66
Definition list_to_map `{Insert K A M, Empty M} : list (K * A)  M :=
67
  fold_right (λ p, <[p.1:=p.2]>) .
68

69 70
Instance map_size `{FinMapToList K A M} : Size M := λ m, length (map_to_list m).

71
Definition map_to_set `{FinMapToList K A M,
72
    Singleton B C, Empty C, Union C} (f : K  A  B) (m : M) : C :=
73 74
  list_to_set (curry f <$> map_to_list m).
Definition set_to_map `{Elements B C, Insert K A M, Empty M}
75
    (f : B  K * A) (X : C) : M :=
76
  list_to_map (f <$> elements X).
Robbert Krebbers's avatar
Robbert Krebbers committed
77

78 79 80 81 82 83
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
84

85 86 87
(** Higher precedence to make sure it's not used for other types with a [Lookup]
instance, such as lists. *)
Instance map_equiv `{ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 20 :=
88
  λ m1 m2,  i, m1 !! i  m2 !! i.
Robbert Krebbers's avatar
Robbert Krebbers committed
89

90
Definition map_Forall `{Lookup K A M} (P : K  A  Prop) : M  Prop :=
91
  λ m,  i x, m !! i = Some x  P i x.
Ralf Jung's avatar
Ralf Jung committed
92

93
Definition map_relation `{ A, Lookup K A (M A)} {A B} (R : A  B  Prop)
Robbert Krebbers's avatar
Robbert Krebbers committed
94 95
    (P : A  Prop) (Q : B  Prop) (m1 : M A) (m2 : M B) : Prop :=  i,
  option_relation R P Q (m1 !! i) (m2 !! i).
96
Definition map_included `{ A, Lookup K A (M A)} {A}
Robbert Krebbers's avatar
Robbert Krebbers committed
97
  (R : relation A) : relation (M A) := map_relation R (λ _, False) (λ _, True).
98
Definition map_disjoint `{ A, Lookup K A (M A)} {A} : relation (M A) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
99
  map_relation (λ _ _, False) (λ _, True) (λ _, True).
100
Infix "##ₘ" := map_disjoint (at level 70) : stdpp_scope.
101
Hint Extern 0 (_ ## _) => symmetry; eassumption : core.
102 103
Notation "( m ##ₘ.)" := (map_disjoint m) (only parsing) : stdpp_scope.
Notation "(.##ₘ m )" := (λ m2, m2 ## m) (only parsing) : stdpp_scope.
104
Instance map_subseteq `{ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
105
  map_included (=).
106 107 108 109 110

(** 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. *)
111
Instance map_union `{Merge M} {A} : Union (M A) := union_with (λ x _, Some x).
112 113 114
Instance map_intersection `{Merge M} {A} : Intersection (M A) :=
  intersection_with (λ x _, Some x).

115 116
(** The difference operation removes all values from the first map whose
index contains a value in the second map as well. *)
117
Instance map_difference `{Merge M} {A} : Difference (M A) :=
118
  difference_with (λ _ _, None).
119

120 121
(** A stronger variant of map that allows the mapped function to use the index
of the elements. Implemented by conversion to lists, so not very efficient. *)
122 123
Definition map_imap `{ A, Insert K A (M A),  A, Empty (M A),
     A, FinMapToList K A (M A)} {A B} (f : K  A  option B) (m : M A) : M B :=
124
  list_to_map (omap (λ ix, (fst ix,) <$> curry f ix) (map_to_list m)).
125

126 127 128 129 130 131 132
(* The zip operation on maps combines two maps key-wise. The keys of resulting
map correspond to the keys that are in both maps. *)
Definition map_zip_with `{Merge M} {A B C} (f : A  B  C) : M A  M B  M C :=
  merge (λ mx my,
    match mx, my with Some x, Some y => Some (f x y) | _, _ => None end).
Notation map_zip := (map_zip_with pair).

133 134 135 136 137
(* Folds a function [f] over a map. The order in which the function is called
is unspecified. *)
Definition map_fold `{FinMapToList K A M} {B}
  (f : K  A  B  B) (b : B) : M  B := foldr (curry f) b  map_to_list.

138
Instance map_filter `{FinMapToList K A M, Insert K A M, Empty M} : Filter (K * A) M :=
139 140
  λ P _, map_fold (λ k v m, if decide (P (k,v)) then <[k := v]>m else m) .

141 142 143 144 145 146
Fixpoint map_seq `{Insert nat A M, Empty M} (start : nat) (xs : list A) : M :=
  match xs with
  | [] => 
  | x :: xs => <[start:=x]> (map_seq (S start) xs)
  end.

147 148 149 150
(** * Theorems *)
Section theorems.
Context `{FinMap K M}.

Robbert Krebbers's avatar
Robbert Krebbers committed
151 152
(** ** Setoids *)
Section setoid.
153
  Context `{Equiv A}.
154

155 156 157 158
  Lemma map_equiv_lookup_l (m1 m2 : M A) i x :
    m1  m2  m1 !! i = Some x   y, m2 !! i = Some y  x  y.
  Proof. generalize (equiv_Some_inv_l (m1 !! i) (m2 !! i) x); naive_solver. Qed.

159
  Global Instance map_equivalence : Equivalence (@{A})  Equivalence (@{M A}).
Robbert Krebbers's avatar
Robbert Krebbers committed
160 161
  Proof.
    split.
162 163
    - by intros m i.
    - by intros m1 m2 ? i.
164
    - by intros m1 m2 m3 ?? i; trans (m2 !! i).
Robbert Krebbers's avatar
Robbert Krebbers committed
165
  Qed.
166
  Global Instance lookup_proper (i : K) : Proper ((@{M A}) ==> ()) (lookup i).
Robbert Krebbers's avatar
Robbert Krebbers committed
167 168
  Proof. by intros m1 m2 Hm. Qed.
  Global Instance partial_alter_proper :
169
    Proper ((() ==> ()) ==> (=) ==> () ==> (@{M A})) partial_alter.
Robbert Krebbers's avatar
Robbert Krebbers committed
170 171 172 173 174 175
  Proof.
    by intros f1 f2 Hf i ? <- m1 m2 Hm j; destruct (decide (i = j)) as [->|];
      rewrite ?lookup_partial_alter, ?lookup_partial_alter_ne by done;
      try apply Hf; apply lookup_proper.
  Qed.
  Global Instance insert_proper (i : K) :
176
    Proper (() ==> () ==> (@{M A})) (insert i).
Robbert Krebbers's avatar
Robbert Krebbers committed
177
  Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed.
178
  Global Instance singleton_proper k : Proper (() ==> (@{M A})) (singletonM k).
179 180 181 182
  Proof.
    intros ???; apply insert_proper; [done|].
    intros ?. rewrite lookup_empty; constructor.
  Qed.
183
  Global Instance delete_proper (i : K) : Proper (() ==> (@{M A})) (delete i).
Robbert Krebbers's avatar
Robbert Krebbers committed
184 185
  Proof. by apply partial_alter_proper; [constructor|]. Qed.
  Global Instance alter_proper :
186
    Proper ((() ==> ()) ==> (=) ==> () ==> (@{M A})) alter.
Robbert Krebbers's avatar
Robbert Krebbers committed
187 188 189 190
  Proof.
    intros ?? Hf; apply partial_alter_proper.
    by destruct 1; constructor; apply Hf.
  Qed.
191 192
  Lemma merge_ext `{Equiv B, Equiv C} (f g : option A  option B  option C)
      `{!DiagNone f, !DiagNone g} :
Robbert Krebbers's avatar
Robbert Krebbers committed
193
    (() ==> () ==> ())%signature f g 
194
    (() ==> () ==> (@{M _}))%signature (merge f) (merge g).
Robbert Krebbers's avatar
Robbert Krebbers committed
195 196 197 198
  Proof.
    by intros Hf ?? Hm1 ?? Hm2 i; rewrite !lookup_merge by done; apply Hf.
  Qed.
  Global Instance union_with_proper :
199
    Proper ((() ==> () ==> ()) ==> () ==> () ==>(@{M A})) union_with.
Robbert Krebbers's avatar
Robbert Krebbers committed
200 201 202
  Proof.
    intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
    by do 2 destruct 1; first [apply Hf | constructor].
203
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
204
  Global Instance map_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (M A).
205
  Proof. intros m1 m2 Hm; apply map_eq; intros i. apply leibniz_equiv, Hm. Qed.
206 207
  Lemma map_equiv_empty (m : M A) : m    m = .
  Proof.
208 209 210
    split; [intros Hm; apply map_eq; intros i|intros ->].
    - generalize (Hm i). by rewrite lookup_empty, equiv_None.
    - intros ?. rewrite lookup_empty; constructor.
211
  Qed.
212
  Global Instance map_fmap_proper `{Equiv B} (f : A  B) :
213
    Proper (() ==> ()) f  Proper (() ==> (@{M _})) (fmap f).
214 215 216
  Proof.
    intros ? m m' ? k; rewrite !lookup_fmap. by apply option_fmap_proper.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
217 218 219
End setoid.

(** ** General properties *)
220 221 222 223 224
Lemma map_eq_iff {A} (m1 m2 : M A) : m1 = m2   i, m1 !! i = m2 !! i.
Proof. split. by intros ->. apply map_eq. Qed.
Lemma map_subseteq_spec {A} (m1 m2 : M A) :
  m1  m2   i x, m1 !! i = Some x  m2 !! i = Some x.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
  unfold subseteq, map_subseteq, map_relation. split; intros Hm i;
226 227
    specialize (Hm i); destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
228
Global Instance map_included_preorder {A} (R : relation A) :
229
  PreOrder R  PreOrder (map_included R : relation (M A)).
230
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
231
  split; [intros m i; by destruct (m !! i); simpl|].
232
  intros m1 m2 m3 Hm12 Hm23 i; specialize (Hm12 i); specialize (Hm23 i).
233
  destruct (m1 !! i), (m2 !! i), (m3 !! i); simplify_eq/=;
234
    done || etrans; eauto.
235
Qed.
236
Global Instance map_subseteq_po : PartialOrder (@{M A}).
237
Proof.
238 239 240
  split; [apply _|].
  intros m1 m2; rewrite !map_subseteq_spec.
  intros; apply map_eq; intros i; apply option_eq; naive_solver.
241 242 243
Qed.
Lemma lookup_weaken {A} (m1 m2 : M A) i x :
  m1 !! i = Some x  m1  m2  m2 !! i = Some x.
244
Proof. rewrite !map_subseteq_spec. auto. Qed.
245 246 247 248 249 250
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.
251 252
  rewrite map_subseteq_spec, !eq_None_not_Some.
  intros Hm2 Hm [??]; destruct Hm2; eauto.
253 254
Qed.
Lemma lookup_weaken_inv {A} (m1 m2 : M A) i x y :
255 256
  m1 !! i = Some x  m1  m2  m2 !! i = Some y  x = y.
Proof. intros Hm1 ? Hm2. eapply lookup_weaken in Hm1; eauto. congruence. Qed.
257 258 259 260 261 262
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.
263
Lemma lookup_empty_Some {A} i (x : A) : ¬( : M A) !! i = Some x.
264 265
Proof. by rewrite lookup_empty. Qed.
Lemma map_subset_empty {A} (m : M A) : m  .
266 267 268
Proof.
  intros [_ []]. rewrite map_subseteq_spec. intros ??. by rewrite lookup_empty.
Qed.
269 270
Lemma map_fmap_empty {A B} (f : A  B) : f <$> ( : M A) = .
Proof. by apply map_eq; intros i; rewrite lookup_fmap, !lookup_empty. Qed.
271 272 273 274 275
Lemma map_fmap_empty_inv {A B} (f : A  B) m : f <$> m =   m = .
Proof.
  intros Hm. apply map_eq; intros i. generalize (f_equal (lookup i) Hm).
  by rewrite lookup_fmap, !lookup_empty, fmap_None.
Qed.
276

277 278 279 280 281
Lemma map_subset_alt {A} (m1 m2 : M A) :
  m1  m2  m1  m2   i, m1 !! i = None  is_Some (m2 !! i).
Proof.
  rewrite strict_spec_alt. split.
  - intros [? Heq]; split; [done|].
282
    destruct (decide (Exists (λ ix, m1 !! ix.1 = None) (map_to_list m2)))
283 284 285 286 287 288 289 290 291 292
      as [[[i x] [?%elem_of_map_to_list ?]]%Exists_exists
         |Hm%(not_Exists_Forall _)]; [eauto|].
    destruct Heq; apply (anti_symm _), map_subseteq_spec; [done|intros i x Hi].
    assert (is_Some (m1 !! i)) as [x' ?].
    { by apply not_eq_None_Some,
        (proj1 (Forall_forall _ _) Hm (i,x)), elem_of_map_to_list. }
    by rewrite <-(lookup_weaken_inv m1 m2 i x' x).
  - intros [? (i&?&x&?)]; split; [done|]. congruence.
Qed.

293
(** ** Properties of the [partial_alter] operation *)
294 295 296
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.
297 298
  intros. apply map_eq; intros j. by destruct (decide (i = j)) as [->|?];
    rewrite ?lookup_partial_alter, ?lookup_partial_alter_ne; auto.
299 300
Qed.
Lemma partial_alter_compose {A} f g (m : M A) i:
301 302
  partial_alter (f  g) i m = partial_alter f i (partial_alter g i m).
Proof.
303 304
  intros. apply map_eq. intros ii. by destruct (decide (i = ii)) as [->|?];
    rewrite ?lookup_partial_alter, ?lookup_partial_alter_ne.
305
Qed.
306
Lemma partial_alter_commute {A} f g (m : M A) i j :
307
  i  j  partial_alter f i (partial_alter g j m) =
308 309
    partial_alter g j (partial_alter f i m).
Proof.
310 311 312 313
  intros. apply map_eq; intros jj. destruct (decide (jj = j)) as [->|?].
  { by rewrite lookup_partial_alter_ne,
      !lookup_partial_alter, lookup_partial_alter_ne. }
  destruct (decide (jj = i)) as [->|?].
314
  - by rewrite lookup_partial_alter,
315
     !lookup_partial_alter_ne, lookup_partial_alter by congruence.
316
  - by rewrite !lookup_partial_alter_ne by congruence.
317 318 319 320
Qed.
Lemma partial_alter_self_alt {A} (m : M A) i x :
  x = m !! i  partial_alter (λ _, x) i m = m.
Proof.
321 322
  intros. apply map_eq. intros ii. by destruct (decide (i = ii)) as [->|];
    rewrite ?lookup_partial_alter, ?lookup_partial_alter_ne.
323
Qed.
324
Lemma partial_alter_self {A} (m : M A) i : partial_alter (λ _, m !! i) i m = m.
325
Proof. by apply partial_alter_self_alt. Qed.
326
Lemma partial_alter_subseteq {A} f (m : M A) i :
327
  m !! i = None  m  partial_alter f i m.
328 329 330 331
Proof.
  rewrite map_subseteq_spec. intros Hi j x Hj.
  rewrite lookup_partial_alter_ne; congruence.
Qed.
332
Lemma partial_alter_subset {A} f (m : M A) i :
333
  m !! i = None  is_Some (f (m !! i))  m  partial_alter f i m.
334
Proof.
335 336
  intros Hi Hfi. apply map_subset_alt; split; [by apply partial_alter_subseteq|].
  exists i. by rewrite lookup_partial_alter.
337 338 339
Qed.

(** ** Properties of the [alter] operation *)
340
Lemma lookup_alter {A} (f : A  A) (m : M A) i : alter f i m !! i = f <$> m !! i.
341
Proof. unfold alter. apply lookup_partial_alter. Qed.
342 343
Lemma lookup_alter_ne {A} (f : A  A) (m : M A) i j :
  i  j  alter f i m !! j = m !! j.
344
Proof. unfold alter. apply lookup_partial_alter_ne. Qed.
345 346 347
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|] ?; f_equal/=; auto. Qed.
348 349 350 351 352 353 354 355 356
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.
357
Lemma lookup_alter_Some {A} (f : A  A) (m : M A) i j y :
358 359 360
  alter f i m !! j = Some y 
    (i = j   x, m !! j = Some x  y = f x)  (i  j  m !! j = Some y).
Proof.
361
  destruct (decide (i = j)) as [->|?].
362
  - rewrite lookup_alter. naive_solver (simplify_option_eq; eauto).
363
  - rewrite lookup_alter_ne by done. naive_solver.
364
Qed.
365
Lemma lookup_alter_None {A} (f : A  A) (m : M A) i j :
366 367
  alter f i m !! j = None  m !! j = None.
Proof.
368 369
  by destruct (decide (i = j)) as [->|?];
    rewrite ?lookup_alter, ?fmap_None, ?lookup_alter_ne.
370
Qed.
371
Lemma lookup_alter_is_Some {A} (f : A  A) (m : M A) i j :
372 373
  is_Some (alter f i m !! j)  is_Some (m !! j).
Proof. by rewrite <-!not_eq_None_Some, lookup_alter_None. Qed.
374
Lemma alter_id {A} (f : A  A) (m : M A) i :
Robbert Krebbers's avatar
Robbert Krebbers committed
375
  ( x, m !! i = Some x  f x = x)  alter f i m = m.
376
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
377
  intros Hi; apply map_eq; intros j; destruct (decide (i = j)) as [->|?].
378
  { rewrite lookup_alter; destruct (m !! j); f_equal/=; auto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
379
  by rewrite lookup_alter_ne by done.
380
Qed.
381 382 383 384 385 386 387 388 389 390 391 392
Lemma alter_mono {A} f (m1 m2 : M A) i : m1  m2  alter f i m1  alter f i m2.
Proof.
  rewrite !map_subseteq_spec. intros ? j x.
  rewrite !lookup_alter_Some. naive_solver.
Qed.
Lemma alter_strict_mono {A} f (m1 m2 : M A) i :
  m1  m2  alter f i m1  alter f i m2.
Proof.
  rewrite !map_subset_alt.
  intros [? (j&?&?)]; split; auto using alter_mono.
  exists j. by rewrite lookup_alter_None, lookup_alter_is_Some.
Qed.
393 394 395 396 397 398 399 400 401 402

(** ** 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.
403
  - destruct (decide (i = j)) as [->|?];
404
      rewrite ?lookup_delete, ?lookup_delete_ne; intuition congruence.
405
  - intros [??]. by rewrite lookup_delete_ne.
406
Qed.
407 408 409
Lemma lookup_delete_is_Some {A} (m : M A) i j :
  is_Some (delete i m !! j)  i  j  is_Some (m !! j).
Proof. unfold is_Some; setoid_rewrite lookup_delete_Some; naive_solver. Qed.
410 411 412
Lemma lookup_delete_None {A} (m : M A) i j :
  delete i m !! j = None  i = j  m !! j = None.
Proof.
413 414
  destruct (decide (i = j)) as [->|?];
    rewrite ?lookup_delete, ?lookup_delete_ne; tauto.
415 416 417 418 419 420 421 422 423
Qed.
Lemma delete_empty {A} i : delete i ( : M A) = .
Proof. rewrite <-(partial_alter_self ) at 2. by rewrite lookup_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.
424
Lemma delete_notin {A} (m : M A) i : m !! i = None  delete i m = m.
425
Proof.
426 427
  intros. apply map_eq. intros j. by destruct (decide (i = j)) as [->|?];
    rewrite ?lookup_delete, ?lookup_delete_ne.
428
Qed.
429 430 431
Lemma delete_idemp {A} (m : M A) i :
  delete i (delete i m) = delete i m.
Proof. by setoid_rewrite <-partial_alter_compose. Qed.
432 433 434 435 436 437 438 439 440
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.
441 442 443
Lemma delete_insert_delete {A} (m : M A) i x :
  delete i (<[i:=x]>m) = delete i m.
Proof. by setoid_rewrite <-partial_alter_compose. Qed.
444 445
Lemma insert_delete {A} (m : M A) i x : <[i:=x]>(delete i m) = <[i:=x]> m.
Proof. symmetry; apply (partial_alter_compose (λ _, Some x)). Qed.
446
Lemma delete_subseteq {A} (m : M A) i : delete i m  m.
447 448 449
Proof.
  rewrite !map_subseteq_spec. intros j x. rewrite lookup_delete_Some. tauto.
Qed.
450
Lemma delete_subset {A} (m : M A) i : is_Some (m !! i)  delete i m  m.
451
Proof.
452 453
  intros [x ?]; apply map_subset_alt; split; [apply delete_subseteq|].
  exists i. rewrite lookup_delete; eauto.
454
Qed.
455
Lemma delete_mono {A} (m1 m2 : M A) i : m1  m2  delete i m1  delete i m2.
456
Proof.
457 458
  rewrite !map_subseteq_spec. intros ? j x.
  rewrite !lookup_delete_Some. intuition eauto.
459 460 461 462 463
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.
464
Lemma lookup_insert_rev {A}  (m : M A) i x y : <[i:=x]>m !! i = Some y  x = y.
465
Proof. rewrite lookup_insert. congruence. Qed.
466
Lemma lookup_insert_ne {A} (m : M A) i j x : i  j  <[i:=x]>m !! j = m !! j.
467
Proof. unfold insert. apply lookup_partial_alter_ne. Qed.
468 469
Lemma insert_insert {A} (m : M A) i x y : <[i:=x]>(<[i:=y]>m) = <[i:=x]>m.
Proof. unfold insert, map_insert. by rewrite <-partial_alter_compose. Qed.
470 471 472 473 474 475 476
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.
477
  - destruct (decide (i = j)) as [->|?];
478
      rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
479
  - intros [[-> ->]|[??]]; [apply lookup_insert|]. by rewrite lookup_insert_ne.
480
Qed.
481 482 483
Lemma lookup_insert_is_Some {A} (m : M A) i j x :
  is_Some (<[i:=x]>m !! j)  i = j  i  j  is_Some (m !! j).
Proof. unfold is_Some; setoid_rewrite lookup_insert_Some; naive_solver. Qed.
484 485 486
Lemma lookup_insert_is_Some' {A} (m : M A) i j x :
  is_Some (<[i:=x]>m !! j)  i = j  is_Some (m !! j).
Proof. rewrite lookup_insert_is_Some. destruct (decide (i=j)); naive_solver. Qed.
487 488 489
Lemma lookup_insert_None {A} (m : M A) i j x :
  <[i:=x]>m !! j = None  m !! j = None  i  j.
Proof.
490 491 492
  split; [|by intros [??]; rewrite lookup_insert_ne].
  destruct (decide (i = j)) as [->|];
    rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
493
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
494
Lemma insert_id {A} (m : M A) i x : m !! i = Some x  <[i:=x]>m = m.
495 496 497 498 499 500 501 502
Proof.
  intros; apply map_eq; intros j; destruct (decide (i = j)) as [->|];
    by rewrite ?lookup_insert, ?lookup_insert_ne by done.
Qed.
Lemma insert_included {A} R `{!Reflexive R} (m : M A) i x :
  ( y, m !! i = Some y  R y x)  map_included R m (<[i:=x]>m).
Proof.
  intros ? j; destruct (decide (i = j)) as [->|].
503 504
  - rewrite lookup_insert. destruct (m !! j); simpl; eauto.
  - rewrite lookup_insert_ne by done. by destruct (m !! j); simpl.
505
Qed.
506
Lemma insert_empty {A} i (x : A) : <[i:=x]>( : M A) = {[i := x]}.
507 508 509 510 511 512
Proof. done. Qed.
Lemma insert_non_empty {A} (m : M A) i x : <[i:=x]>m  .
Proof.
  intros Hi%(f_equal (!! i)). by rewrite lookup_insert, lookup_empty in Hi.
Qed.

513
Lemma insert_subseteq {A} (m : M A) i x : m !! i = None  m  <[i:=x]>m.
514
Proof. apply partial_alter_subseteq. Qed.
515
Lemma insert_subset {A} (m : M A) i x : m !! i = None  m  <[i:=x]>m.
516
Proof. intro. apply partial_alter_subset; eauto. Qed.
517 518 519 520 521
Lemma insert_mono {A} (m1 m2 : M A) i x : m1  m2  <[i:=x]> m1  <[i:=x]>m2.
Proof.
  rewrite !map_subseteq_spec.
  intros Hm j y. rewrite !lookup_insert_Some. naive_solver.
Qed.
522
Lemma insert_subseteq_r {A} (m1 m2 : M A) i x :
523
  m1 !! i = None  m1  m2  m1  <[i:=x]>m2.
524
Proof.
525
  intros. trans (<[i:=x]> m1); eauto using insert_subseteq, insert_mono.
526
Qed.
527

528
Lemma insert_delete_subseteq {A} (m1 m2 : M A) i x :
529
  m1 !! i = None  <[i:=x]> m1  m2  m1  delete i m2.
530
Proof.
531 532 533 534
  rewrite !map_subseteq_spec. intros Hi Hix j y Hj.
  destruct (decide (i = j)) as [->|]; [congruence|].
  rewrite lookup_delete_ne by done.
  apply Hix; by rewrite lookup_insert_ne by done.
535 536
Qed.
Lemma delete_insert_subseteq {A} (m1 m2 : M A) i x :
537
  m1 !! i = Some x  delete i m1  m2  m1  <[i:=x]> m2.
538
Proof.
539 540
  rewrite !map_subseteq_spec.
  intros Hix Hi j y Hj. destruct (decide (i = j)) as [->|?].
541 542
  - rewrite lookup_insert. congruence.
  - rewrite lookup_insert_ne by done. apply Hi. by rewrite lookup_delete_ne.
543 544
Qed.
Lemma insert_delete_subset {A} (m1 m2 : M A) i x :
545
  m1 !! i = None  <[i:=x]> m1  m2  m1  delete i m2.
546
Proof.
547 548 549
  intros ? [Hm12 Hm21]; split; [eauto using insert_delete_subseteq|].
  contradict Hm21. apply delete_insert_subseteq; auto.
  eapply lookup_weaken, Hm12. by rewrite lookup_insert.
550 551
Qed.
Lemma insert_subset_inv {A} (m1 m2 : M A) i x :
552
  m1 !! i = None  <[i:=x]> m1  m2 
553 554
   m2', m2 = <[i:=x]>m2'  m1  m2'  m2' !! i = None.
Proof.
555
  intros Hi Hm1m2. exists (delete i m2). split_and?.
556 557
  - rewrite insert_delete, insert_id. done.
    eapply lookup_weaken, strict_include; eauto. by rewrite lookup_insert.
558 559
  - eauto using insert_delete_subset.
  - by rewrite lookup_delete.
560 561 562 563
Qed.

(** ** Properties of the singleton maps *)
Lemma lookup_singleton_Some {A} i j (x y : A) :
564
  ({[i := x]} : M A) !! j = Some y  i = j  x = y.
565
Proof.
566
  rewrite <-insert_empty,lookup_insert_Some, lookup_empty; intuition congruence.
567
Qed.
568 569
Lemma lookup_singleton_None {A} i j (x : A) :
  ({[i := x]} : M A) !! j = None  i  j.
570
Proof. rewrite <-insert_empty,lookup_insert_None, lookup_empty; tauto. Qed.
571
Lemma lookup_singleton {A} i (x : A) : ({[i := x]} : M A) !! i = Some x.
572
Proof. by rewrite lookup_singleton_Some. Qed.
573 574
Lemma lookup_singleton_ne {A} i j (x : A) :
  i  j  ({[i := x]} : M A) !! j = None.
575
Proof. by rewrite lookup_singleton_None. Qed.
576
Lemma map_non_empty_singleton {A} i (x : A) : {[i := x]}  ( : M A).
577 578 579 580
Proof.
  intros Hix. apply (f_equal (!! i)) in Hix.
  by rewrite lookup_empty, lookup_singleton in Hix.
Qed.
581
Lemma insert_singleton {A} i (x y : A) : <[i:=y]>({[i := x]} : M A) = {[i := y]}.
582
Proof.
583
  unfold singletonM, map_singleton, insert, map_insert.
584 585
  by rewrite <-partial_alter_compose.
Qed.
586 587
Lemma alter_singleton {A} (f : A  A) i x :
  alter f i ({[i := x]} : M A) = {[i := f x]}.
588
Proof.
589
  intros. apply map_eq. intros i'. destruct (decide (i = i')) as [->|?].
590 591
  - by rewrite lookup_alter, !lookup_singleton.
  - by rewrite lookup_alter_ne, !lookup_singleton_ne.
592 593
Qed.
Lemma alter_singleton_ne {A} (f : A  A) i j x :
594
  i  j  alter f i ({[j := x]} : M A) = {[j := x]}.
595
Proof.
596 597
  intros. apply map_eq; intros i'. by destruct (decide (i = i')) as [->|?];
    rewrite ?lookup_alter, ?lookup_singleton_ne, ?lookup_alter_ne by done.
598
Qed.
599
Lemma singleton_non_empty {A} i (x : A) : {[i:=x]}  ( : M A).
600
Proof. apply insert_non_empty. Qed.
601
Lemma delete_singleton {A} i (x : A) : delete i {[i := x]} = ( : M A).
602
Proof. setoid_rewrite <-partial_alter_compose. apply delete_empty. Qed.
603
Lemma delete_singleton_ne {A} i j (x : A) :
604
  i  j  delete i ({[j := x]} : M A) = {[j := x]}.
605
Proof. intro. apply delete_notin. by apply lookup_singleton_ne. Qed.
606

607 608 609 610 611
(** ** Properties of the map operations *)
Lemma fmap_empty {A B} (f : A  B) : f <$>  = .
Proof. apply map_empty; intros i. by rewrite lookup_fmap, lookup_empty. Qed.
Lemma omap_empty {A B} (f : A  option B) : omap f  = .
Proof. apply map_empty; intros i. by rewrite lookup_omap, lookup_empty. Qed.
612 613 614
Lemma fmap_insert {A B} (f: A  B) m i x: f <$> <[i:=x]>m = <[i:=f x]>(f <$> m).
Proof.
  apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
615 616
  - by rewrite lookup_fmap, !lookup_insert.
  - by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
617
Qed.
618 619 620 621 622 623
Lemma fmap_delete {A B} (f: A  B) m i: f <$> delete i m = delete i (f <$> m).
Proof.
  apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
  - by rewrite lookup_fmap, !lookup_delete.
  - by rewrite lookup_fmap, !lookup_delete_ne, lookup_fmap by done.
Qed.
624 625 626 627
Lemma omap_insert {A B} (f : A  option B) m i x y :
  f x = Some y  omap f (<[i:=x]>m) = <[i:=y]>(omap f m).
Proof.
  intros; apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
628 629
  - by rewrite lookup_omap, !lookup_insert.
  - by rewrite lookup_omap, !lookup_insert_ne, lookup_omap by done.
630
Qed.
631
Lemma map_fmap_singleton {A B} (f : A  B) i x : f <$> {[i := x]} = {[i := f x]}.
632 633 634
Proof.
  by unfold singletonM, map_singleton; rewrite fmap_insert, map_fmap_empty.
Qed.
635
Lemma omap_singleton {A B} (f : A  option B) i x y :
636
  f x = Some y  omap f {[ i := x ]} = {[ i := y ]}.
637
Proof.
638 639
  intros. unfold singletonM, map_singleton.
  by erewrite omap_insert, omap_empty by eauto.
640
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
641 642 643
Lemma map_fmap_id {A} (m : M A) : id <$> m = m.
Proof. apply map_eq; intros i; by rewrite lookup_fmap, option_fmap_id. Qed.
Lemma map_fmap_compose {A B C} (f : A  B) (g : B  C) (m : M A) :
644
  g  f <$> m = g <$> (f <$> m).
Robbert Krebbers's avatar
Robbert Krebbers committed
645
Proof. apply map_eq; intros i; by rewrite !lookup_fmap,option_fmap_compose. Qed.
646
Lemma map_fmap_equiv_ext `{Equiv A, Equiv B} (f1 f2 : A  B) (m : M A) :
647 648 649 650 651
  ( i x, m !! i = Some x  f1 x  f2 x)  f1 <$> m  f2 <$> m.
Proof.
  intros Hi i; rewrite !lookup_fmap.
  destruct (m !! i) eqn:?; constructor; eauto.
Qed.
652
Lemma map_fmap_ext {A B} (f1 f2 : A  B) (m : M A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
653 654 655 656 657
  ( i x, m !! i = Some x  f1 x = f2 x)  f1 <$> m = f2 <$> m.
Proof.
  intros Hi; apply map_eq; intros i; rewrite !lookup_fmap.
  by destruct (m !! i) eqn:?; simpl; erewrite ?Hi by eauto.
Qed.
658
Lemma omap_ext {A B} (f1 f2 : A  option B) (m : M A) :
659 660 661 662 663
  ( i x, m !! i = Some x  f1 x = f2 x)  omap f1 m = omap f2 m.
Proof.
  intros Hi; apply map_eq; intros i; rewrite !lookup_omap.
  by destruct (m !! i) eqn:?; simpl; erewrite ?Hi by eauto.
Qed.
664

665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684
Lemma map_fmap_mono {A B} (f : A  B) (m1 m2 : M A) :
  m1  m2  f <$> m1  f <$> m2.
Proof.
  rewrite !map_subseteq_spec; intros Hm i x.
  rewrite !lookup_fmap, !fmap_Some. naive_solver.
Qed.
Lemma map_fmap_strict_mono {A B} (f : A  B) (m1 m2 : M A) :
  m1  m2  f <$> m1  f <$> m2.
Proof.
  rewrite !map_subset_alt.
  intros [? (j&?&?)]; split; auto using map_fmap_mono.
  exists j. by rewrite !lookup_fmap, fmap_None, fmap_is_Some.
Qed.
Lemma map_omap_mono {A B} (f : A  option B) (m1 m2 : M A) :
  m1  m2  omap f m1  omap f m2.
Proof.
  rewrite !map_subseteq_spec; intros Hm i x.
  rewrite !lookup_omap, !bind_Some. naive_solver.
Qed.

685
(** ** Properties of conversion to lists *)
686 687 688
Lemma elem_of_map_to_list' {A} (m : M A) ix :
  ix  map_to_list m  m !! ix.1 = Some (ix.2).
Proof. destruct ix as [i x]. apply elem_of_map_to_list. Qed.
689
Lemma map_to_list_unique {A} (m : M A) i x y :
690
  (i,x)  map_to_list m  (i,y)  map_to_list m  x = y.
691
Proof. rewrite !elem_of_map_to_list. congruence. Qed.
692
Lemma NoDup_fst_map_to_list {A} (m : M A) : NoDup ((map_to_list m).*1).
693
Proof. eauto using NoDup_fmap_fst, map_to_list_unique, NoDup_map_to_list. Qed.
694 695
Lemma elem_of_list_to_map_1' {A} (l : list (K * A)) i x :
  ( y, (i,y)  l  x = y)  (i,x)  l  (list_to_map l : M A) !! i = Some x.
696 697 698
Proof.
  induction l as [|[j y] l IH]; csimpl; [by rewrite elem_of_nil|].
  setoid_rewrite elem_of_cons.
699
  intros Hdup [?|?]; simplify_eq; [by rewrite lookup_insert|].
700
  destruct (decide (i = j)) as [->|].
701
  - rewrite lookup_insert; f_equal; eauto using eq_sym.
702
  - rewrite lookup_insert_ne by done; eauto.
703
Qed.
704 705
Lemma elem_of_list_to_map_1 {A} (l : list (K * A)) i x :
  NoDup (l.*1)  (i,x)  l  (list_to_map l : M A) !! i = Some x.
706
Proof.
707
  intros ? Hx; apply elem_of_list_to_map_1'; eauto using NoDup_fmap_fst.
708
  intros y; revert Hx. rewrite !elem_of_list_lookup; intros [i' Hi'] [j' Hj'].
709
  cut (i' = j'); [naive_solver|]. apply NoDup_lookup with (l.*1) i;
710
    by rewrite ?list_lookup_fmap, ?Hi', ?Hj'.
711
Qed.
712 713
Lemma elem_of_list_to_map_2 {A} (l : list (K * A)) i x :
  (list_to_map l : M A) !! i = Some x  (i,x)  l.
714
Proof.
715 716 717
  induction l as [|[j y] l IH]; simpl; [by rewrite lookup_empty|].
  rewrite elem_of_cons. destruct (decide (i = j)) as [->|];
    rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
718
Qed.
719
Lemma elem_of_list_to_map' {A} (l : list (K * A)) i x :
720
  ( x', (i,x)  l  (i,x')  l  x = x') 
721 722 723 724 725
  (i,x)  l  (list_to_map l : M A) !! i = Some x.
Proof. split; auto using elem_of_list_to_map_1', elem_of_list_to_map_2. Qed.
Lemma elem_of_list_to_map {A} (l : list (K * A)) i x :
  NoDup (l.*1)  (i,x)  l  (list_to_map l : M A) !! i = Some x.
Proof. split; auto using elem_of_list_to_map_1, elem_of_list_to_map_2. Qed.
726

727 728
Lemma not_elem_of_list_to_map_1 {A} (l : list (K * A)) i :
  i  l.*1  (list_to_map l : M A) !! i = None.
729
Proof.
730
  rewrite elem_of_list_fmap, eq_None_not_Some. intros Hi [x ?]; destruct Hi.
731
  exists (i,x); simpl; auto using elem_of_list_to_map_2.
732
Qed.
733 734
Lemma not_elem_of_list_to_map_2 {A} (l : list (K * A)) i :
  (list_to_map l : M A) !! i = None  i  l.*1.
735
Proof.
736
  induction l as [|[j y] l IH]; csimpl; [rewrite elem_of_nil; tauto|].
737
  rewrite elem_of_cons. destruct (decide (i = j)); simplify_eq.
738 739
  - by rewrite lookup_insert.
  - by rewrite lookup_insert_ne; intuition.
740
Qed.
741 742 743 744 745
Lemma not_elem_of_list_to_map {A} (l : list (K * A)) i :
  i  l.*1  (list_to_map l : M A) !! i = None.
Proof. red; auto using not_elem_of_list_to_map_1,not_elem_of_list_to_map_2. Qed.
Lemma list_to_map_proper {A} (l1 l2 : list (K * A)) :
  NoDup (l1.*1)  l1 ≡ₚ l2  (list_to_map l1 : M A) = list_to_map l2.
746 747
Proof.
  intros ? Hperm. apply map_eq. intros i. apply option_eq. intros x.
748
  by rewrite <-!elem_of_list_to_map; rewrite <-?Hperm.
749
Qed.
750
Lemma list_to_map_inj {A} (l1 l2 : list (K * A)) :
751
  NoDup (l1.*1)  NoDup (l2.*1) 
752
  (list_to_map l1 : M A) = list_to_map l2  l1 ≡ₚ l2.
753
Proof.
754
  intros ?? Hl1l2. apply NoDup_Permutation; auto using (NoDup_fmap_1 fst).
755
  intros [i x]. by rewrite !elem_of_list_to_map, Hl1l2.
756
Qed.
757
Lemma list_to_map_to_list {A} (m : M A) : list_to_map (map_to_list m) = m.
758 759
Proof.
  apply map_eq. intros i. apply option_eq. intros x.
760
  by rewrite <-elem_of_list_to_map, elem_of_map_to_list
761
    by auto using NoDup_fst_map_to_list.
762
Qed.
763 764 765
Lemma map_to_list_to_map {A} (l : list (K * A)) :
  NoDup (l.*1)  map_to_list (list_to_map l) ≡ₚ l.
Proof. auto using list_to_map_inj, NoDup_fst_map_to_list, list_to_map_to_list. Qed.
766
Lemma map_to_list_inj {A} (m1 m2 : M A) :
767
  map_to_list m1 ≡ₚ map_to_list m2  m1 = m2.
768
Proof.
769 770
  intros. rewrite <-(list_to_map_to_list m1), <-(list_to_map_to_list m2).
  auto using list_to_map_proper, NoDup_fst_map_to_list.
771
Qed.
772 773
Lemma list_to_map_flip {A} (m1 : M A) l2 :
  map_to_list m1 ≡ₚ l2  m1 = list_to_map l2.
774
Proof.
775 776
  intros. rewrite <-(list_to_map_to_list m1).
  auto using list_to_map_proper, NoDup_fst_map_to_list.
777
Qed.
778

779
Lemma list_to_map_nil {A} : list_to_map [] = ( : M A).
780
Proof. done. Qed.
781 782
Lemma list_to_map_cons {A} (l : list (K * A)) i x :
  list_to_map ((i, x) :: l) = <[i:=x]>(list_to_map l : M A).
783
Proof. done. Qed.
784 785
Lemma list_to_map_fmap {A B} (f : A  B) l :
  list_to_map (prod_map id f <$> l) = f <$> (list_to_map l : M A).
786 787
Proof.
  induction l as [|[i x] l IH]; csimpl; rewrite ?fmap_empty; auto.
788
  rewrite <-list_to_map_cons; simpl. by rewrite IH, <-fmap_insert.
789 790
Qed.

791
Lemma map_to_list_empty {A} : map_to_list  = @nil (K * A).
792 793 794 795 796
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 :
797
  m !! i = None  map_to_list (<[i:=x]>m) ≡ₚ (i,x) :: map_to_list m.
798
Proof.
799
  intros. apply list_to_map_inj; csimpl.
800 801
  - apply NoDup_fst_map_to_list.