fin_maps.v 10.6 KB
Newer Older
1
Require Export algebra.cmra prelude.gmap algebra.option.
2

3
4
Section cofe.
Context `{Countable K} {A : cofeT}.
5
6

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

Global Instance lookup_ne n k :
34
  Proper (dist n ==> dist n) (lookup k : gmap K A  option A).
35
Proof. by intros m1 m2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
36
37
Global Instance lookup_proper k :
  Proper (() ==> ()) (lookup k : gmap K A  option A) := _.
38
Global Instance insert_ne (i : K) n :
39
  Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
40
41
42
43
Proof.
  intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_equality;
    [by constructor|by apply lookup_ne].
Qed.
44
Global Instance singleton_ne (i : K) n :
45
46
  Proper (dist n ==> dist n) (singletonM i : A  gmap K A).
Proof. by intros ???; apply insert_ne. Qed.
47
Global Instance delete_ne (i : K) n :
48
  Proper (dist n ==> dist n) (delete (M:=gmap K A) i).
49
50
51
52
Proof.
  intros m m' ? j; destruct (decide (i = j)); simplify_map_equality;
    [by constructor|by apply lookup_ne].
Qed.
53
Instance map_empty_timeless : Timeless ( : gmap K A).
54
55
56
57
Proof.
  intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
  inversion_clear Hm; constructor.
Qed.
58
Global Instance map_lookup_timeless (m : gmap K A) i :
59
60
61
  Timeless m  Timeless (m !! i).
Proof.
  intros ? [x|] Hx; [|by symmetry; apply (timeless _)].
Robbert Krebbers's avatar
Robbert Krebbers committed
62
63
64
  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.
65
Qed.
66
Global Instance map_ra_insert_timeless (m : gmap K A) i x :
67
68
69
  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
70
71
  { by apply (timeless _); rewrite -Hm lookup_insert. }
  by apply (timeless _); rewrite -Hm lookup_insert_ne.
72
Qed.
73
Global Instance map_ra_singleton_timeless (i : K) (x : A) :
74
  Timeless x  Timeless ({[ i  x ]} : gmap K A) := _.
75
76
End cofe.
Arguments mapC _ {_ _} _.
77
78

(* CMRA *)
79
80
81
82
83
84
85
86
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.
Lemma lookup_op m1 m2 i : (m1  m2) !! i = m1 !! i  m2 !! i.
87
Proof. by apply lookup_merge. Qed.
88
Lemma lookup_minus m1 m2 i : (m1  m2) !! i = m1 !! i  m2 !! i.
89
Proof. by apply lookup_merge. Qed.
90
Lemma lookup_unit m i : unit m !! i = unit (m !! i).
91
Proof. by apply lookup_fmap. Qed.
92
Lemma map_included_spec (m1 m2 : gmap K A) : m1  m2   i, m1 !! i  m2 !! i.
93
94
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
  * by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
96
  * intros Hm; exists (m2  m1); intros i.
97
    by rewrite lookup_op lookup_minus cmra_op_minus'.
98
Qed.
99
Lemma map_includedN_spec (m1 m2 : gmap K A) n :
100
101
102
  m1 {n} m2   i, m1 !! i {n} 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 cmra_op_minus.
106
Qed.
107
Definition map_cmra_mixin : CMRAMixin (gmap K A).
108
109
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
111
112
113
  * 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).
114
  * by intros m i.
115
116
117
118
119
  * 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.
120
  * intros n x y; rewrite !map_includedN_spec; intros Hm i.
121
122
    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
123
    by rewrite -lookup_op.
124
  * intros x y n; rewrite map_includedN_spec=> ? i.
Robbert Krebbers's avatar
Robbert Krebbers committed
125
    by rewrite lookup_op lookup_minus cmra_op_minus.
126
Qed.
127
Definition map_cmra_extend_mixin : CMRAExtendMixin (gmap K A).
128
129
130
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
131
    by (by intros i; rewrite -lookup_op).
132
133
134
  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
135
    repeat split; intros i; rewrite /= ?lookup_op !lookup_imap.
136
  * destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor].
Robbert Krebbers's avatar
Robbert Krebbers committed
137
    rewrite -Hx; apply (proj2_sig (f i)).
138
  * destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [apply (proj2_sig (f i))|].
139
    pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
140
    by symmetry; apply option_op_positive_dist_l with (m2 !! i).
141
142
  * destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
    pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
143
    by symmetry; apply option_op_positive_dist_r with (m1 !! i).
144
Qed.
145
146
Canonical Structure mapRA : cmraT :=
  CMRAT map_cofe_mixin map_cmra_mixin map_cmra_extend_mixin.
147
148
149
150
151
152
153
154
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.

155
156
157
158
159
End cmra.
Arguments mapRA _ {_ _} _.

Section properties.
Context `{Countable K} {A: cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
Implicit Types m : gmap K A.
161

Robbert Krebbers's avatar
Robbert Krebbers committed
162
163
164
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).
165
Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
Lemma map_insert_op m1 m2 i x :
167
  m2 !! i = None  <[i:=x]>(m1  m2) = <[i:=x]>m1  m2.
168
169
170
171
172
173
174
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
175
176
177
178
179
180
181
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|];
182
      [exists (x  y)|exists x]; eauto using cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
183
184
185
186
187
  * 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.
188
Lemma map_dom_op m1 m2 : dom (gset K) (m1  m2)  dom _ m1  dom _ m2.
189
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
190
  apply elem_of_equiv; intros i; rewrite elem_of_union !elem_of_dom.
191
192
193
  unfold is_Some; setoid_rewrite lookup_op.
  destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
194

195
Lemma map_insert_updateP (P : A  Prop) (Q : gmap K A  Prop) m i x :
196
  x ~~>: P  ( y, P y  Q (<[i:=y]>m))  <[i:=x]>m ~~>: Q.
197
198
199
200
201
202
203
204
205
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.
Lemma map_insert_updateP' (P : A  Prop) (Q : gmap K A  Prop) m i x :
206
  x ~~>: P  <[i:=x]>m ~~>: λ m',  y, m' = <[i:=y]>m  P y.
207
Proof. eauto using map_insert_updateP. Qed.
208
Lemma map_insert_update m i x y : x ~~> y  <[i:=x]>m ~~> <[i:=y]>m.
209
210
211
212
Proof.
  rewrite !cmra_update_updateP; eauto using map_insert_updateP with congruence.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
213
Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
214
Lemma map_updateP_alloc (Q : gmap K A  Prop) m x :
215
   x  ( i, m !! i = None  Q (<[i:=x]>m))  m ~~>: Q.
216
Proof.
217
  intros ? HQ mf n Hm. set (i := fresh (dom (gset K) (m  mf))).
218
  assert (i  dom (gset K) m  i  dom (gset K) mf) as [??].
Robbert Krebbers's avatar
Robbert Krebbers committed
219
  { rewrite -not_elem_of_union -map_dom_op; apply is_fresh. }
220
221
222
  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|].
223
Qed.
224
Lemma map_updateP_alloc' m x :
225
   x  m ~~>: λ m',  i, m' = <[i:=x]>m  m !! i = None.
226
Proof. eauto using map_updateP_alloc. Qed.
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
End properties.

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.
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.

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.
Definition mapRA_map `{Countable K} {A B : cmraT} (f : A -n> B) :
  mapRA K A -n> mapRA K B := CofeMor (fmap f : mapRA K A  mapRA K B).
Instance mapRA_map_ne `{Countable K} {A B} n :
  Proper (dist n ==> dist n) (@mapRA_map K _ _ A B) := mapC_map_ne n.
Instance mapRA_map_monotone `{Countable K} {A B : cmraT} (f : A -n> B)
  `{!CMRAMonotone f} : CMRAMonotone (mapRA_map f) := _.