fin_maps.v 9.93 KB
Newer Older
1 2
Require Export modures.cmra prelude.gmap.
Require Import modures.option.
3 4

Section map.
5
Context `{Countable K}.
6 7

(* COFE *)
8
Global Instance map_dist `{Dist A} : Dist (gmap K A) := λ n m1 m2,
9
   i, m1 !! i ={n}= m2 !! i.
10
Program Definition map_chain `{Dist A} (c : chain (gmap K A))
11 12
  (k : K) : chain (option A) := {| chain_car n := c n !! k |}.
Next Obligation. by intros A ? c k n i ?; apply (chain_cauchy c). Qed.
13
Global Instance map_compl `{Cofe A} : Compl (gmap K A) := λ c,
14
  map_imap (λ i _, compl (map_chain c i)) (c 1).
15
Global Instance map_cofe `{Cofe A} : Cofe (gmap K A).
16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
Proof.
  split.
  * intros m1 m2; split.
    + by intros Hm n k; apply equiv_dist.
    + intros Hm k; apply equiv_dist; intros n; apply Hm.
  * intros n; split.
    + by intros m k.
    + by intros m1 m2 ? k.
    + by intros m1 m2 m3 ?? k; transitivity (m2 !! k).
  * by intros n m1 m2 ? k; apply dist_S.
  * by intros m1 m2 k.
  * intros c n k; unfold compl, map_compl; rewrite lookup_imap.
    destruct (decide (n = 0)) as [->|]; [constructor|].
    feed inversion (λ H, chain_cauchy c 1 n H k); simpl; auto with lia.
    by rewrite conv_compl; simpl; apply reflexive_eq.
Qed.
Global Instance lookup_ne `{Dist A} n k :
33
  Proper (dist n ==> dist n) (lookup k : gmap K A  option A).
34 35
Proof. by intros m1 m2. Qed.
Global Instance insert_ne `{Dist A} (i : K) n :
36
  Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
37 38 39 40
Proof.
  intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_equality;
    [by constructor|by apply lookup_ne].
Qed.
41 42 43
Global Instance singleton_ne `{Cofe A} (i : K) n :
  Proper (dist n ==> dist n) (singletonM i : A  gmap K A).
Proof. by intros ???; apply insert_ne. Qed.
44
Global Instance delete_ne `{Dist A} (i : K) n :
45
  Proper (dist n ==> dist n) (delete (M:=gmap K A) i).
46 47 48 49
Proof.
  intros m m' ? j; destruct (decide (i = j)); simplify_map_equality;
    [by constructor|by apply lookup_ne].
Qed.
50
Global Instance map_empty_timeless `{Dist A, Equiv A} : Timeless ( : gmap K A).
51 52 53 54
Proof.
  intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
  inversion_clear Hm; constructor.
Qed.
55
Global Instance map_lookup_timeless `{Cofe A} (m : gmap K A) i :
56 57 58
  Timeless m  Timeless (m !! i).
Proof.
  intros ? [x|] Hx; [|by symmetry; apply (timeless _)].
Robbert Krebbers's avatar
Robbert Krebbers committed
59 60 61
  assert (m ={1}= <[i:=x]> m)
    by (by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id).
  by rewrite (timeless m (<[i:=x]>m)) // lookup_insert.
62
Qed.
63
Global Instance map_ra_insert_timeless `{Cofe A} (m : gmap K A) i x :
64 65 66
  Timeless x  Timeless m  Timeless (<[i:=x]>m).
Proof.
  intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_equality.
Robbert Krebbers's avatar
Robbert Krebbers committed
67 68
  { by apply (timeless _); rewrite -Hm lookup_insert. }
  by apply (timeless _); rewrite -Hm lookup_insert_ne.
69 70
Qed.
Global Instance map_ra_singleton_timeless `{Cofe A} (i : K) (x : A) :
71
  Timeless x  Timeless ({[ i  x ]} : gmap K A) := _.
72
Global Instance map_fmap_ne `{Dist A, Dist B} (f : A  B) n :
73 74
  Proper (dist n ==> dist n) f 
  Proper (dist n ==> dist n) (fmap (M:=gmap K) f).
75
Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
76
Canonical Structure mapC (A : cofeT) : cofeT := CofeT (gmap K A).
77 78 79 80 81
Definition mapC_map {A B} (f: A -n> B) : mapC A -n> mapC B :=
  CofeMor (fmap f : mapC A  mapC B).
Global Instance mapC_map_ne {A B} n :
  Proper (dist n ==> dist n) (@mapC_map A B).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
  intros f g Hf m k; rewrite /= !lookup_fmap.
83 84 85 86
  destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
Qed.

(* CMRA *)
87 88 89 90
Global Instance map_op `{Op A} : Op (gmap K A) := merge op.
Global Instance map_unit `{Unit A} : Unit (gmap K A) := fmap unit.
Global Instance map_valid `{Valid A} : Valid (gmap K A) := λ m,  i,  (m !! i).
Global Instance map_validN `{ValidN A} : ValidN (gmap K A) := λ n m,
91
   i, {n} (m!!i).
92
Global Instance map_minus `{Minus A} : Minus (gmap K A) := merge minus.
93 94 95 96 97 98
Lemma lookup_op `{Op A} m1 m2 i : (m1  m2) !! i = m1 !! i  m2 !! i.
Proof. by apply lookup_merge. Qed.
Lemma lookup_minus `{Minus A} m1 m2 i : (m1  m2) !! i = m1 !! i  m2 !! i.
Proof. by apply lookup_merge. Qed.
Lemma lookup_unit `{Unit A} m i : unit m !! i = unit (m !! i).
Proof. by apply lookup_fmap. Qed.
99
Lemma map_included_spec `{CMRA A} (m1 m2 : gmap K A) :
100 101 102
  m1  m2   i, m1 !! i  m2 !! i.
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
  * by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
104
  * intros Hm; exists (m2  m1); intros i.
Robbert Krebbers's avatar
Robbert Krebbers committed
105
    by rewrite lookup_op lookup_minus ra_op_minus.
106
Qed.
107
Lemma map_includedN_spec `{CMRA A} (m1 m2 : gmap K A) n :
108 109 110
  m1 {n} m2   i, m1 !! i {n} m2 !! i.
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
  * by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
112
  * intros Hm; exists (m2  m1); intros i.
Robbert Krebbers's avatar
Robbert Krebbers committed
113
    by rewrite lookup_op lookup_minus cmra_op_minus.
114
Qed.
115
Global Instance map_cmra `{CMRA A} : CMRA (gmap K A).
116 117 118
Proof.
  split.
  * apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
119 120 121 122
  * by intros n m1 m2 m3 Hm i; rewrite !lookup_op (Hm i).
  * by intros n m1 m2 Hm i; rewrite !lookup_unit (Hm i).
  * by intros n m1 m2 Hm ? i; rewrite -(Hm i).
  * by intros n m1 m1' Hm1 m2 m2' Hm2 i; rewrite !lookup_minus (Hm1 i) (Hm2 i).
123 124 125 126
  * by intros m i.
  * intros n m Hm i; apply cmra_valid_S, Hm.
  * intros m; split; [by intros Hm n i; apply cmra_valid_validN|].
    intros Hm i; apply cmra_valid_validN; intros n; apply Hm.
Robbert Krebbers's avatar
Robbert Krebbers committed
127 128 129 130
  * by intros m1 m2 m3 i; rewrite !lookup_op (associative _).
  * by intros m1 m2 i; rewrite !lookup_op (commutative _).
  * by intros m i; rewrite lookup_op !lookup_unit ra_unit_l.
  * by intros m i; rewrite !lookup_unit ra_unit_idempotent.
131 132 133
  * intros n x y; rewrite !map_includedN_spec; intros Hm i.
    by rewrite !lookup_unit; apply cmra_unit_preserving.
  * intros n m1 m2 Hm i; apply cmra_valid_op_l with (m2 !! i).
Robbert Krebbers's avatar
Robbert Krebbers committed
134
    by rewrite -lookup_op.
135
  * intros x y n; rewrite map_includedN_spec; intros ? i.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
    by rewrite lookup_op lookup_minus cmra_op_minus.
137
Qed.
138
Global Instance map_ra_empty `{RA A} : RAIdentity (gmap K A).
139 140 141
Proof.
  split.
  * by intros ?; rewrite lookup_empty.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
  * by intros m i; rewrite /= lookup_op lookup_empty; destruct (m !! i).
143
Qed.
144
Global Instance map_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (gmap K A).
145 146 147
Proof.
  intros n m m1 m2 Hm Hm12.
  assert ( i, m !! i ={n}= m1 !! i  m2 !! i) as Hm12'
Robbert Krebbers's avatar
Robbert Krebbers committed
148
    by (by intros i; rewrite -lookup_op).
149 150 151
  set (f i := cmra_extend_op n (m !! i) (m1 !! i) (m2 !! i) (Hm i) (Hm12' i)).
  set (f_proj i := proj1_sig (f i)).
  exists (map_imap (λ i _, (f_proj i).1) m, map_imap (λ i _, (f_proj i).2) m);
Robbert Krebbers's avatar
Robbert Krebbers committed
152
    repeat split; intros i; rewrite /= ?lookup_op !lookup_imap.
153
  * destruct (m !! i) as [x|] eqn:Hx; simpl; [|constructor].
Robbert Krebbers's avatar
Robbert Krebbers committed
154
    rewrite -Hx; apply (proj2_sig (f i)).
155 156 157 158 159 160 161 162
  * destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
    pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
    by destruct (m1 !! i), (m2 !! i); inversion_clear Hm12''.
  * destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
    pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
    by destruct (m1 !! i), (m2 !! i); inversion_clear Hm12''.
Qed.
Global Instance map_empty_valid_timeless `{Valid A, ValidN A} :
163
  ValidTimeless ( : gmap K A).
164
Proof. by intros ??; rewrite lookup_empty. Qed.
165 166
Global Instance map_ra_insert_valid_timeless `{Valid A, ValidN A}
    (m : gmap K A) i x:
167 168 169 170 171 172 173 174 175 176
  ValidTimeless x  ValidTimeless m  m !! i = None 
  ValidTimeless (<[i:=x]>m).
Proof.
  intros ?? Hi Hm j; destruct (decide (i = j)); simplify_map_equality.
  { specialize (Hm j); simplify_map_equality. by apply (valid_timeless _). }
  generalize j; clear dependent j; rapply (valid_timeless m).
  intros j; destruct (decide (i = j)); simplify_map_equality;[by rewrite Hi|].
  by specialize (Hm j); simplify_map_equality.
Qed.
Global Instance map_ra_singleton_valid_timeless `{Valid A, ValidN A} (i : K) x :
177
  ValidTimeless x  ValidTimeless ({[ i  x ]} : gmap K A).
178
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
179
  intros ?; apply (map_ra_insert_valid_timeless _ _ _ _ _).
180 181
  by rewrite lookup_empty.
Qed.
182
Lemma map_insert_valid `{ValidN A} (m : gmap K A) n i x :
183 184
  {n} x  {n} m  {n} (<[i:=x]>m).
Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed.
185
Lemma map_insert_op `{Op A} (m1 m2 : gmap K A) i x :
186 187
  m2 !! i = None   <[i:=x]>(m1  m2) = <[i:=x]>m1  m2.
Proof. by intros Hi; apply (insert_merge_l _); rewrite Hi. Qed.
188 189 190 191
Lemma map_singleton_op `{Op A} (i : K) (x y : A) :
  ({[ i  x  y ]} : gmap K A) = {[ i  x ]}  {[ i  y ]}.
Proof. by apply symmetry, merge_singleton. Qed.

192
Canonical Structure mapRA (A : cmraT) : cmraT := CMRAT (gmap K A).
193
Global Instance map_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A  B)
194
  `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A  gmap K B).
195 196 197 198 199 200 201 202 203 204 205 206 207
Proof.
  split.
  * intros m1 m2 n; rewrite !map_includedN_spec; intros Hm i.
    by rewrite !lookup_fmap; apply includedN_preserving.
  * by intros n m ? i; rewrite lookup_fmap; apply validN_preserving.
Qed.
Definition mapRA_map {A B : cmraT} (f : A -n> B) : mapRA A -n> mapRA B :=
  CofeMor (fmap f : mapRA A  mapRA B).
Global Instance mapRA_map_ne {A B} n :
  Proper (dist n ==> dist n) (@mapRA_map A B) := mapC_map_ne n.
Global Instance mapRA_map_monotone {A B : cmraT} (f : A -n> B)
  `{!CMRAMonotone f} : CMRAMonotone (mapRA_map f) := _.

208
Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
209

210 211 212
Lemma map_dom_op `{Op A} (m1 m2 : gmap K A) :
  dom (gset K) (m1  m2)  dom _ m1  dom _ m2.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
213
  apply elem_of_equiv; intros i; rewrite elem_of_union !elem_of_dom.
214 215 216 217 218 219 220 221
  unfold is_Some; setoid_rewrite lookup_op.
  destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
Lemma map_update_alloc `{CMRA A} (m : gmap K A) x :
   x  m : λ m',  i, m' = <[i:=x]>m  m !! i = None.
Proof.
  intros ? mf n Hm. set (i := fresh (dom (gset K) (m  mf))).
  assert (i  dom (gset K) m  i  dom (gset K) mf) as [??].
Robbert Krebbers's avatar
Robbert Krebbers committed
222
  { rewrite -not_elem_of_union -map_dom_op; apply is_fresh. }
223 224
  exists (<[i:=x]>m); split; [exists i; split; [done|]|].
  * by apply not_elem_of_dom.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
  * rewrite -map_insert_op; last by apply not_elem_of_dom.
226 227 228 229 230
    by apply map_insert_valid; [apply cmra_valid_validN|].
Qed.
End map.
Arguments mapC _ {_ _} _.
Arguments mapRA _ {_ _} _.