fin_maps.v 12.3 KB
Newer Older
1
Require Export algebra.cmra prelude.gmap algebra.option.
Ralf Jung's avatar
Ralf Jung committed
2
Require Import algebra.functor.
3

4 5
Section cofe.
Context `{Countable K} {A : cofeT}.
6
Implicit Types m : gmap K A.
7

8
Instance map_dist : Dist (gmap K A) := λ n m1 m2,
9
   i, m1 !! i ={n}= m2 !! i.
10
Program Definition map_chain (c : chain (gmap K A))
11
  (k : K) : chain (option A) := {| chain_car n := c n !! k |}.
12 13
Next Obligation. by intros c k n i ?; apply (chain_cauchy c). Qed.
Instance map_compl : Compl (gmap K A) := λ c,
14
  map_imap (λ i _, compl (map_chain c i)) (c 1).
15
Definition map_cofe_mixin : CofeMixin (gmap K A).
16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31
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.
32 33 34
Canonical Structure mapC : cofeT := CofeT map_cofe_mixin.

Global Instance lookup_ne n k :
35
  Proper (dist n ==> dist n) (lookup k : gmap K A  option A).
36
Proof. by intros m1 m2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
37 38
Global Instance lookup_proper k :
  Proper (() ==> ()) (lookup k : gmap K A  option A) := _.
39
Global Instance insert_ne i n :
40
  Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
41 42 43 44
Proof.
  intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_equality;
    [by constructor|by apply lookup_ne].
Qed.
45
Global Instance singleton_ne i n :
46 47
  Proper (dist n ==> dist n) (singletonM i : A  gmap K A).
Proof. by intros ???; apply insert_ne. Qed.
48
Global Instance delete_ne i n :
49
  Proper (dist n ==> dist n) (delete (M:=gmap K A) i).
50 51 52 53
Proof.
  intros m m' ? j; destruct (decide (i = j)); simplify_map_equality;
    [by constructor|by apply lookup_ne].
Qed.
54

55
Instance map_empty_timeless : Timeless ( : gmap K A).
56 57 58 59
Proof.
  intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
  inversion_clear Hm; constructor.
Qed.
60
Global Instance map_lookup_timeless m i : Timeless m  Timeless (m !! i).
61 62
Proof.
  intros ? [x|] Hx; [|by symmetry; apply (timeless _)].
Robbert Krebbers's avatar
Robbert Krebbers committed
63 64 65
  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.
66
Qed.
67
Global Instance map_insert_timeless m i x :
68 69 70
  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
71 72
  { by apply (timeless _); rewrite -Hm lookup_insert. }
  by apply (timeless _); rewrite -Hm lookup_insert_ne.
73
Qed.
74
Global Instance map_singleton_timeless i x :
75
  Timeless x  Timeless ({[ i  x ]} : gmap K A) := _.
76
End cofe.
77

78
Arguments mapC _ {_ _} _.
79 80

(* CMRA *)
81 82 83 84 85 86 87
Section cmra.
Context `{Countable K} {A : cmraT}.

Instance map_op : Op (gmap K A) := merge op.
Instance map_unit : Unit (gmap K A) := fmap unit.
Instance map_validN : ValidN (gmap K A) := λ n m,  i, {n} (m!!i).
Instance map_minus : Minus (gmap K A) := merge minus.
88

89
Lemma lookup_op m1 m2 i : (m1  m2) !! i = m1 !! i  m2 !! i.
90
Proof. by apply lookup_merge. Qed.
91
Lemma lookup_minus m1 m2 i : (m1  m2) !! i = m1 !! i  m2 !! i.
92
Proof. by apply lookup_merge. Qed.
93
Lemma lookup_unit m i : unit m !! i = unit (m !! i).
94
Proof. by apply lookup_fmap. Qed.
95

96
Lemma map_included_spec (m1 m2 : gmap K A) : m1  m2   i, m1 !! i  m2 !! i.
97 98
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
  * by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
100
  * intros Hm; exists (m2  m1); intros i.
101
    by rewrite lookup_op lookup_minus cmra_op_minus'.
102
Qed.
103
Lemma map_includedN_spec (m1 m2 : gmap K A) n :
104 105 106
  m1 {n} m2   i, m1 !! i {n} m2 !! i.
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
  * by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
108
  * intros Hm; exists (m2  m1); intros i.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
    by rewrite lookup_op lookup_minus cmra_op_minus.
110
Qed.
111

112
Definition map_cmra_mixin : CMRAMixin (gmap K A).
113 114
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
115 116 117 118
  * 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).
119
  * by intros m i.
120 121 122 123 124
  * intros n m Hm i; apply cmra_validN_S, Hm.
  * 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 cmra_unit_l.
  * by intros m i; rewrite !lookup_unit cmra_unit_idempotent.
125
  * intros n x y; rewrite !map_includedN_spec; intros Hm i.
126 127
    by rewrite !lookup_unit; apply cmra_unit_preservingN.
  * intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
Robbert Krebbers's avatar
Robbert Krebbers committed
128
    by rewrite -lookup_op.
129
  * intros x y n; rewrite map_includedN_spec=> ? i.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
    by rewrite lookup_op lookup_minus cmra_op_minus.
131
Qed.
132
Definition map_cmra_extend_mixin : CMRAExtendMixin (gmap K A).
133 134 135
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
136
    by (by intros i; rewrite -lookup_op).
137 138 139
  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
140
    repeat split; intros i; rewrite /= ?lookup_op !lookup_imap.
141
  * destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor].
Robbert Krebbers's avatar
Robbert Krebbers committed
142
    rewrite -Hx; apply (proj2_sig (f i)).
143
  * destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [apply (proj2_sig (f i))|].
144
    pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
145
    by symmetry; apply option_op_positive_dist_l with (m2 !! i).
146 147
  * destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
    pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
148
    by symmetry; apply option_op_positive_dist_r with (m1 !! i).
149
Qed.
150 151
Canonical Structure mapRA : cmraT :=
  CMRAT map_cofe_mixin map_cmra_mixin map_cmra_extend_mixin.
152 153 154 155 156 157 158
Global Instance map_cmra_identity : CMRAIdentity mapRA.
Proof.
  split.
  * by intros ? n; rewrite lookup_empty.
  * by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
  * apply map_empty_timeless.
Qed.
159
End cmra.
160

161 162 163
Arguments mapRA _ {_ _} _.

Section properties.
164
Context `{Countable K} {A : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
Implicit Types m : gmap K A.
166 167
Implicit Types i : K.
Implicit Types a : A.
168

Robbert Krebbers's avatar
Robbert Krebbers committed
169 170 171
Lemma map_lookup_validN n m i x : {n} m  m !! i ={n}= Some x  {n} x.
Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed.
Lemma map_insert_validN n m i x : {n} x  {n} m  {n} (<[i:=x]>m).
172
Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed.
173 174 175 176 177
Lemma map_singleton_validN n i x : {n} ({[ i  x ]} : gmap K A)  {n} x.
Proof.
  split; [|by intros; apply map_insert_validN, cmra_empty_valid].
  by move=>/(_ i); simplify_map_equality.
Qed.
178

Robbert Krebbers's avatar
Robbert Krebbers committed
179
Lemma map_insert_op m1 m2 i x :
180
  m2 !! i = None  <[i:=x]>(m1  m2) = <[i:=x]>m1  m2.
181 182 183 184 185 186 187
Proof. by intros Hi; apply (insert_merge_l _ m1 m2); rewrite Hi. Qed.
Lemma map_unit_singleton (i : K) (x : A) :
  unit ({[ i  x ]} : gmap K A) = {[ i  unit x ]}.
Proof. apply map_fmap_singleton. Qed.
Lemma map_op_singleton (i : K) (x y : A) :
  {[ i  x ]}  {[ i  y ]} = ({[ i  x  y ]} : gmap K A).
Proof. by apply (merge_singleton _ _ _ x y). Qed.
188

Robbert Krebbers's avatar
Robbert Krebbers committed
189 190 191 192 193 194 195
Lemma singleton_includedN n m i x :
  {[ i  x ]} {n} m   y, m !! i ={n}= Some y  x  y.
  (* not m !! i = Some y ∧ x ≼{n} y to deal with n = 0 *)
Proof.
  split.
  * move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton=> Hm.
    destruct (m' !! i) as [y|];
196
      [exists (x  y)|exists x]; eauto using cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
197 198 199 200 201
  * intros (y&Hi&?); rewrite map_includedN_spec=>j.
    destruct (decide (i = j)); simplify_map_equality.
    + by rewrite Hi; apply Some_Some_includedN, cmra_included_includedN.
    + apply None_includedN.
Qed.
202
Lemma map_dom_op m1 m2 : dom (gset K) (m1  m2)  dom _ m1  dom _ m2.
203
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
204
  apply elem_of_equiv; intros i; rewrite elem_of_union !elem_of_dom.
205 206 207
  unfold is_Some; setoid_rewrite lookup_op.
  destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
208

209
Lemma map_insert_updateP (P : A  Prop) (Q : gmap K A  Prop) m i x :
210
  x ~~>: P  ( y, P y  Q (<[i:=y]>m))  <[i:=x]>m ~~>: Q.
211 212 213 214 215 216 217 218
Proof.
  intros Hx%option_updateP' HP mf n Hm.
  destruct (Hx (mf !! i) n) as ([y|]&?&?); try done.
  { by generalize (Hm i); rewrite lookup_op; simplify_map_equality. }
  exists (<[i:=y]> m); split; first by auto.
  intros j; move: (Hm j)=>{Hm}; rewrite !lookup_op=>Hm.
  destruct (decide (i = j)); simplify_map_equality'; auto.
Qed.
219
Lemma map_insert_updateP' (P : A  Prop) m i x :
220
  x ~~>: P  <[i:=x]>m ~~>: λ m',  y, m' = <[i:=y]>m  P y.
221
Proof. eauto using map_insert_updateP. Qed.
222
Lemma map_insert_update m i x y : x ~~> y  <[i:=x]>m ~~> <[i:=y]>m.
223
Proof.
224
  rewrite !cmra_update_updateP; eauto using map_insert_updateP with subst.
225 226
Qed.

227 228 229 230
Lemma map_singleton_updateP (P : A  Prop) (Q : gmap K A  Prop) i x :
  x ~~>: P  ( y, P y  Q {[ i  y ]})  {[ i  x ]} ~~>: Q.
Proof. apply map_insert_updateP. Qed.
Lemma map_singleton_updateP' (P : A  Prop) i x :
231
  x ~~>: P  {[ i  x ]} ~~>: λ m,  y, m = {[ i  y ]}  P y.
232
Proof. apply map_insert_updateP'. Qed.
233
Lemma map_singleton_update i (x y : A) : x ~~> y  {[ i  x ]} ~~> {[ i  y ]}.
234
Proof. apply map_insert_update. Qed.
235

236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255
Lemma map_singleton_updateP_empty `{Empty A, !CMRAIdentity A}
      (P : A  Prop) (Q : gmap K A  Prop) i :
   ~~>: P  ( y, P y  Q {[ i  y ]})   ~~>: Q.
  Proof.
    intros Hx HQ gf n Hg.
    destruct (Hx (default  (gf !! i) id) n) as (y&?&Hy).
    { move:(Hg i). rewrite !left_id. case _: (gf !! i); first done.
      intros. apply cmra_empty_valid. }
    exists {[ i  y]}. split; first by apply HQ.
    intros i'. rewrite lookup_op.
    destruct (decide (i' = i)).
    - subst i'. rewrite lookup_singleton. move:Hy.
      case _: (gf !! i); first done.
      by rewrite right_id.
    - move:(Hg i'). rewrite lookup_singleton_ne // !left_id. done.
Qed.
Lemma map_singleton_updateP_empty' `{Empty A, !CMRAIdentity A} (P : A  Prop) i :
   ~~>: P   ~~>: λ m,  y, m = {[ i  y ]}  P y.
Proof. eauto using map_singleton_updateP_empty. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
256
Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
257
Lemma map_updateP_alloc (Q : gmap K A  Prop) m x :
258
   x  ( i, m !! i = None  Q (<[i:=x]>m))  m ~~>: Q.
259
Proof.
260
  intros ? HQ mf n Hm. set (i := fresh (dom (gset K) (m  mf))).
261
  assert (i  dom (gset K) m  i  dom (gset K) mf) as [??].
Robbert Krebbers's avatar
Robbert Krebbers committed
262
  { rewrite -not_elem_of_union -map_dom_op; apply is_fresh. }
263 264 265
  exists (<[i:=x]>m); split; first by apply HQ, not_elem_of_dom.
  rewrite -map_insert_op; last by apply not_elem_of_dom.
  by apply map_insert_validN; [apply cmra_valid_validN|].
266
Qed.
267
Lemma map_updateP_alloc' m x :
268
   x  m ~~>: λ m',  i, m' = <[i:=x]>m  m !! i = None.
269
Proof. eauto using map_updateP_alloc. Qed.
270 271
End properties.

272
(** Functor *)
273 274 275 276 277 278 279 280 281 282 283
Instance map_fmap_ne `{Countable K} {A B : cofeT} (f : A  B) n :
  Proper (dist n ==> dist n) f  Proper (dist n ==>dist n) (fmap (M:=gmap K) f).
Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
Instance map_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A  B)
  `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A  gmap K B).
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.
284 285 286 287 288 289 290 291
Definition mapC_map `{Countable K} {A B} (f: A -n> B) : mapC K A -n> mapC K B :=
  CofeMor (fmap f : mapC K A  mapC K B).
Instance mapC_map_ne `{Countable K} {A B} n :
  Proper (dist n ==> dist n) (@mapC_map K _ _ A B).
Proof.
  intros f g Hf m k; rewrite /= !lookup_fmap.
  destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
Qed.
Ralf Jung's avatar
Ralf Jung committed
292 293 294 295 296 297 298 299 300 301 302 303 304 305 306

Program Definition mapF K `{Countable K} (Σ : iFunctor) : iFunctor := {|
  ifunctor_car := mapRA K  Σ; ifunctor_map A B := mapC_map  ifunctor_map Σ
|}.
Next Obligation.
  by intros K ?? Σ A B n f g Hfg; apply mapC_map_ne, ifunctor_map_ne.
Qed.
Next Obligation.
  intros K ?? Σ A x. rewrite /= -{2}(map_fmap_id x).
  apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_id.
Qed.
Next Obligation.
  intros K ?? Σ A B C f g x. rewrite /= -map_fmap_compose.
  apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_compose.
Qed.