fin_maps.v 97.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

Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 :=
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Tej Chajed's avatar
Tej Chajed committed
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 (=).
Robbert Krebbers's avatar
Robbert Krebbers committed
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).
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 220 221 222 223
  Global Instance map_zip_with_proper `{Equiv B, Equiv C} (f : A  B  C) :
    Proper (() ==> () ==> ()) f 
    Proper (() ==> () ==> ()) (map_zip_with (M:=M) f).
  Proof.
    intros Hf m1 m1' Hm1 m2 m2' Hm2. apply merge_ext; try done.
    destruct 1; destruct 1; repeat f_equiv; constructor || done.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
224 225 226
End setoid.

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

284 285 286 287 288
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|].
Robbert Krebbers's avatar
Robbert Krebbers committed
289
    destruct (decide (Exists (λ ix, m1 !! ix.1 = None) (map_to_list m2)))
290 291 292 293 294 295 296 297 298 299
      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.

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

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

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

520
Lemma insert_subseteq {A} (m : M A) i x : m !! i = None  m  <[i:=x]>m.
521
Proof. apply partial_alter_subseteq. Qed.
522
Lemma insert_subset {A} (m : M A) i x : m !! i = None  m  <[i:=x]>m.
523
Proof. intro. apply partial_alter_subset; eauto. Qed.
524 525 526 527 528
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.
529
Lemma insert_subseteq_r {A} (m1 m2 : M A) i x :
530
  m1 !! i = None  m1  m2  m1  <[i:=x]>m2.
531
Proof.
532
  intros. trans (<[i:=x]> m1); eauto using insert_subseteq, insert_mono.
533
Qed.
534

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

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

614 615 616 617 618
(** ** 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.
619 620 621
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 [->|].
622 623
  - by rewrite lookup_fmap, !lookup_insert.
  - by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
624
Qed.
625 626 627 628 629 630
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.
631 632 633 634
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 [->|].
635 636
  - by rewrite lookup_omap, !lookup_insert.
  - by rewrite lookup_omap, !lookup_insert_ne, lookup_omap by done.
637
Qed.
638
Lemma map_fmap_singleton {A B} (f : A  B) i x : f <$> {[i := x]} = {[i := f x]}.
639 640 641
Proof.
  by unfold singletonM, map_singleton; rewrite fmap_insert, map_fmap_empty.
Qed.
642
Lemma omap_singleton {A B} (f : A  option B) i x y :
643
  f x = Some y  omap f {[ i := x ]} = {[ i := y ]}.
644
Proof.
645 646
  intros. unfold singletonM, map_singleton.
  by erewrite omap_insert, omap_empty by eauto.
647
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
648 649 650
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) :
651
  g  f <$> m = g <$> (f <$> m).
Robbert Krebbers's avatar
Robbert Krebbers committed
652
Proof. apply map_eq; intros i; by rewrite !lookup_fmap,option_fmap_compose. Qed.
653
Lemma map_fmap_equiv_ext {A} `{Equiv B} (f1 f2 : A  B) (m : M A) :
654 655 656 657 658
  ( 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.
659
Lemma map_fmap_ext {A B} (f1 f2 : A  B) (m : M A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
660 661 662 663 664
  ( i x, m !! i = Some x  f1 x = f2 x)  f1 <$> m = f2