cmra_maps.v 11.4 KB
Newer Older
1
Require Export modures.cmra modures.cofe_maps.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
Require Import prelude.pmap prelude.natmap prelude.gmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
4

(** option *)
Robbert Krebbers's avatar
Robbert Krebbers committed
5
Instance option_valid `{Valid A} : Valid (option A) := λ mx,
Robbert Krebbers's avatar
Robbert Krebbers committed
6
  match mx with Some x =>  x | None => True end.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
Instance option_validN `{ValidN A} : ValidN (option A) := λ n mx,
Robbert Krebbers's avatar
Robbert Krebbers committed
8
  match mx with Some x => {n} x | None => True end.
Robbert Krebbers's avatar
Robbert Krebbers committed
9
10
11
12
Instance option_unit `{Unit A} : Unit (option A) := fmap unit.
Instance option_op `{Op A} : Op (option A) := union_with (λ x y, Some (x  y)).
Instance option_minus `{Minus A} : Minus (option A) :=
  difference_with (λ x y, Some (x  y)).
Robbert Krebbers's avatar
Robbert Krebbers committed
13
14
15
16
17
18
19
20
21
22
23
Lemma option_included `{CMRA A} mx my :
  mx  my  mx = None   x y, mx = Some x  my = Some y  x  y.
Proof.
  split.
  * intros [mz Hmz]; destruct mx as [x|]; [right|by left].
    destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
    destruct mz as [z|]; inversion_clear Hmz; split_ands; auto;
      setoid_subst; eauto using ra_included_l.
  * intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
    by exists (Some z); constructor.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
24
25
26
27
28
29
30
Lemma option_includedN `{CMRA A} n mx my :
  mx {n} my  n = 0  mx = None   x y, mx = Some x  my = Some y  x {n} y.
Proof.
  split.
  * intros [mz Hmz]; destruct n as [|n]; [by left|right].
    destruct mx as [x|]; [right|by left].
    destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
    destruct mz as [z|]; inversion_clear Hmz; split_ands; auto;
      cofe_subst; auto using cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
34
35
36
  * intros [->|[->|(x&y&->&->&z&Hz)]];
      try (by exists my; destruct my; constructor).
    by exists (Some z); constructor.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
37
38
39
40
41
42
43
44
45
Instance option_cmra `{CMRA A} : CMRA (option A).
Proof.
  split.
  * apply _.
  * by intros n [x|]; destruct 1; constructor;
      repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
  * by destruct 1; constructor; apply (_ : Proper (dist n ==> _) _).
  * destruct 1 as [[?|] [?|]| |]; unfold validN, option_validN; simpl;
     intros ?; auto using cmra_valid_0;
Robbert Krebbers's avatar
Robbert Krebbers committed
46
     eapply (_ : Proper (dist _ ==> impl) ({_})); eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
47
48
49
50
51
52
53
54
55
56
  * by destruct 1; inversion_clear 1; constructor;
      repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
  * intros [x|]; unfold validN, option_validN; auto using cmra_valid_0.
  * intros n [x|]; unfold validN, option_validN; auto using cmra_valid_S.
  * by intros [x|]; unfold valid, validN, option_validN, option_valid;
      auto using cmra_valid_validN.
  * intros [x|] [y|] [z|]; constructor; rewrite ?(associative _); auto.
  * intros [x|] [y|]; constructor; rewrite 1?(commutative _); auto.
  * by intros [x|]; constructor; rewrite cmra_unit_l.
  * by intros [x|]; constructor; rewrite cmra_unit_idempotent.
Robbert Krebbers's avatar
Robbert Krebbers committed
57
58
  * intros n mx my; rewrite !option_includedN;intros [|[->|(x&y&->&->&?)]];auto.
    do 2 right; exists (unit x), (unit y); eauto using cmra_unit_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
60
  * intros n [x|] [y|]; unfold validN, option_validN; simpl;
      eauto using cmra_valid_op_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
61
62
63
  * intros n mx my; rewrite option_includedN.
    intros [->|[->|(x&y&->&->&?)]]; [done|by destruct my|].
    by constructor; apply cmra_op_minus.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
66
Qed.
Instance option_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (option A).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
  intros n mx my1 my2; destruct (decide (n = 0)) as [->|].
Robbert Krebbers's avatar
Robbert Krebbers committed
68
69
70
  { by exists (mx, None); repeat constructor; destruct mx; constructor. }
  destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx';
    try (by exfalso; inversion Hx'; auto).
Robbert Krebbers's avatar
Robbert Krebbers committed
71
  * destruct (cmra_extend_op n x y1 y2) as ([z1 z2]&?&?&?); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
73
74
75
76
77
    { by inversion_clear Hx'. }
    by exists (Some z1, Some z2); repeat constructor.
  * by exists (Some x,None); inversion Hx'; repeat constructor.
  * by exists (None,Some x); inversion Hx'; repeat constructor.
  * exists (None,None); repeat constructor.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
79
80
81
82
Instance None_valid_timeless `{Valid A, ValidN A} : ValidTimeless (@None A).
Proof. done. Qed.
Instance Some_valid_timeless `{Valid A, ValidN A} x :
  ValidTimeless x  ValidTimeless (Some x).
Proof. by intros ? y; apply (valid_timeless x). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
83
Instance option_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A  B)
Robbert Krebbers's avatar
Robbert Krebbers committed
84
  `{!CMRAMonotone f} : CMRAMonotone (fmap f : option A  option B).
Robbert Krebbers's avatar
Robbert Krebbers committed
85
86
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
87
88
  * intros n mx my; rewrite !option_includedN.
    intros [->|[->|(x&y&->&->&?)]]; simpl; eauto 10 using @includedN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
89
90
91
  * by intros n [x|] ?;
      unfold validN, option_validN; simpl; try apply validN_preserving.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
92
93
94
95
96

(** fin maps *)
Section map.
  Context `{FinMap K M}.
  Existing Instances map_dist map_compl map_cofe.
97
98
99
100
101
102
  Global Instance map_op `{Op A} : Op (M A) := merge op.
  Global Instance map_unit `{Unit A} : Unit (M A) := fmap unit.
  Global Instance map_valid `{Valid A} : Valid (M A) := λ m,  i,  (m !! i).
  Global Instance map_validN `{ValidN A} : ValidN (M A) := λ n m,
     i, {n} (m!!i).
  Global Instance map_minus `{Minus A} : Minus (M A) := merge minus.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
104
105
106
107
108
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
  Lemma map_included_spec `{CMRA A} (m1 m2 : M A) :
    m1  m2   i, m1 !! i  m2 !! i.
  Proof.
    split.
    * intros [m Hm]; intros i; exists (m !! i). by rewrite <-lookup_op, Hm.
    * intros Hm; exists (m2  m1); intros i.
      by rewrite lookup_op, lookup_minus, ra_op_minus.
  Qed.
  Lemma map_includedN_spec `{CMRA A} (m1 m2 : M A) n :
    m1 {n} m2   i, m1 !! i {n} m2 !! i.
  Proof.
    split.
    * intros [m Hm]; intros i; exists (m !! i). by rewrite <-lookup_op, Hm.
    * intros Hm; exists (m2  m1); intros i.
      by rewrite lookup_op, lookup_minus, cmra_op_minus.
  Qed.
125
  Global Instance map_cmra `{CMRA A} : CMRA (M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
126
127
128
129
130
131
132
133
  Proof.
    split.
    * apply _.
    * 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).
    * intros n m1 m1' Hm1 m2 m2' Hm2 i.
      by rewrite !lookup_minus, (Hm1 i), (Hm2 i).
Robbert Krebbers's avatar
Robbert Krebbers committed
134
    * by intros m i.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
136
137
138
139
140
141
    * 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.
    * 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
    * intros n x y; rewrite !map_includedN_spec; intros Hm i.
      by rewrite !lookup_unit; apply cmra_unit_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
145
    * intros n m1 m2 Hm i; apply cmra_valid_op_l with (m2 !! i).
      by rewrite <-lookup_op.
Robbert Krebbers's avatar
Robbert Krebbers committed
146
147
    * intros x y n; rewrite map_includedN_spec; intros ? i.
      by rewrite lookup_op, lookup_minus, cmra_op_minus by done.
Robbert Krebbers's avatar
Robbert Krebbers committed
148
  Qed.
149
  Global Instance map_ra_empty `{RA A} : RAEmpty (M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
150
151
152
153
154
  Proof.
    split.
    * by intros ?; rewrite lookup_empty.
    * by intros m i; simpl; rewrite lookup_op, lookup_empty; destruct (m !! i).
  Qed.
155
  Global Instance map_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
156
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
    intros n m m1 m2 Hm Hm12.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
159
    assert ( i, m !! i ={n}= m1 !! i  m2 !! i) as Hm12'
      by (by intros i; rewrite <-lookup_op).
Robbert Krebbers's avatar
Robbert Krebbers committed
160
    set (f i := cmra_extend_op n (m !! i) (m1 !! i) (m2 !! i) (Hm i) (Hm12' i)).
Robbert Krebbers's avatar
Robbert Krebbers committed
161
162
163
164
165
166
167
168
169
170
171
172
    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);
      repeat split; simpl; intros i; rewrite ?lookup_op, !lookup_imap.
    * destruct (m !! i) as [x|] eqn:Hx; simpl; [|constructor].
      rewrite <-Hx; apply (proj2_sig (f i)).
    * 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
  Global Instance map_empty_valid_timeless `{Valid A, ValidN A} :
    ValidTimeless ( : M A).
  Proof. by intros ??; rewrite lookup_empty. Qed.
  Global Instance map_ra_insert_valid_timeless `{Valid A,ValidN A} (m: M A) i x:
    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_timeless `{Valid A, ValidN A} (i : K) x :
    ValidTimeless x  ValidTimeless ({[ i, x ]} : M A).
  Proof.
    intros ?; apply (map_ra_insert_valid_timeless _ _ _ _ _); simpl.
    by rewrite lookup_empty.
  Qed.
192
193
194
195
196
197
  Lemma map_insert_valid `{ValidN A} (m : M A) n i x :
    {n} x  {n} m  {n} (<[i:=x]>m).
  Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed.
  Lemma map_insert_op `{Op A} (m1 m2 : M A) i x :
    m2 !! i = None   <[i:=x]>(m1  m2) = <[i:=x]>m1  m2.
  Proof. by intros Hi; apply (insert_merge_l _); rewrite Hi. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
198
  Definition mapRA (A : cmraT) : cmraT := CMRAT (M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
199
200
  Global Instance map_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A  B)
    `{!CMRAMonotone f} : CMRAMonotone (fmap f : M A  M B).
Robbert Krebbers's avatar
Robbert Krebbers committed
201
202
  Proof.
    split.
Robbert Krebbers's avatar
Robbert Krebbers committed
203
204
    * intros m1 m2 n; rewrite !map_includedN_spec; intros Hm i.
      by rewrite !lookup_fmap; apply includedN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
205
206
    * by intros n m ? i; rewrite lookup_fmap; apply validN_preserving.
  Qed.
207
  Hint Resolve (map_fmap_ne (M:=M)) : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
208
209
210
211
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
212
  Global Instance mapRA_map_monotone {A B : cmraT} (f : A -n> B)
Robbert Krebbers's avatar
Robbert Krebbers committed
213
    `{!CMRAMonotone f} : CMRAMonotone (mapRA_map f) := _.
Robbert Krebbers's avatar
Robbert Krebbers committed
214
215
216
End map.
Arguments mapRA {_} _ {_ _ _ _ _ _ _ _ _} _.

217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
Section map_dom.
  Context `{FinMapDom K M D, Fresh K D, !FreshSpec K D}.
  Lemma map_dom_op `{Op A} (m1 m2: M A) : dom D (m1  m2)  dom D m1  dom D m2.
  Proof.
    apply elem_of_equiv; intros i; rewrite elem_of_union, !elem_of_dom.
    unfold is_Some; setoid_rewrite lookup_op.
    destruct (m1 !! i), (m2 !! i); naive_solver.
  Qed.
  Lemma map_update_alloc `{CMRA A} (m : M A) x :
     x  m : λ m',  i, m' = <[i:=x]>m  m !! i = None.
  Proof.
    intros ? mf n Hm. set (i := fresh (dom D (m  mf))).
    assert (i  dom D m  i  dom D mf) as [??].
    { rewrite <-not_elem_of_union, <-map_dom_op; apply is_fresh. }
    exists (<[i:=x]>m); split; [exists i; split; [done|]|].
    * by apply not_elem_of_dom.
    * rewrite <-map_insert_op by (by apply not_elem_of_dom).
      by apply map_insert_valid; [apply cmra_valid_validN|].
  Qed.
End map_dom.

Robbert Krebbers's avatar
Robbert Krebbers committed
238
Canonical Structure natmapRA := mapRA natmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
239
240
Definition natmapRA_map {A B : cmraT}
  (f : A -n> B) : natmapRA A -n> natmapRA B := mapRA_map f.
Robbert Krebbers's avatar
Robbert Krebbers committed
241
Canonical Structure PmapRA := mapRA Pmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
242
243
Definition PmapRA_map {A B : cmraT}
  (f : A -n> B) : PmapRA A -n> PmapRA B := mapRA_map f.
Robbert Krebbers's avatar
Robbert Krebbers committed
244
245
246
Canonical Structure gmapRA K `{Countable K} := mapRA (gmap K).
Definition gmapRA_map `{Countable K} {A B : cmraT}
  (f : A -n> B) : gmapRA K A -n> gmapRA K B := mapRA_map f.