agree.v 12.7 KB
Newer Older
1
From iris.algebra Require Export cmra.
Ralf Jung's avatar
Ralf Jung committed
2
From iris.algebra Require Import list.
3
From iris.base_logic Require Import base_logic.
Ralf Jung's avatar
Ralf Jung committed
4
5
6
7
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _  !_ /.
Local Arguments op _ _ _ !_ /.
Local Arguments pcore _ _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
8

9
(** Define an agreement construction such that Agree A is discrete when A is discrete.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
    Notice that this construction is NOT complete.  The following is due to Aleš:
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

Proposition: Ag(T) is not necessarily complete.
Proof.
  Let T be the set of binary streams (infinite sequences) with the usual
  ultrametric, measuring how far they agree.

  Let Aₙ be the set of all binary strings of length n. Thus for Aₙ to be a
  subset of T we have them continue as a stream of zeroes.

  Now Aₙ is a finite non-empty subset of T. Moreover {Aₙ} is a Cauchy sequence
  in the defined (Hausdorff) metric.

  However the limit (if it were to exist as an element of Ag(T)) would have to
  be the set of all binary streams, which is not exactly finite.

  Thus Ag(T) is not necessarily complete.
*)

29
30
(** Note that the projection [agree_car] is not non-expansive, so it cannot be
used in the logic. If you need to get a witness out, you should use the
31
32
lemma [to_agree_uninjN] instead. In general, [agree_car] should ONLY be used
internally in this file.  *)
33
Record agree (A : Type) : Type := {
34
35
  agree_car : list A;
  agree_not_nil : bool_decide (agree_car = []) = false
Robbert Krebbers's avatar
Robbert Krebbers committed
36
}.
Ralf Jung's avatar
Ralf Jung committed
37
Arguments agree_car {_} _.
38
39
Arguments agree_not_nil {_} _.
Local Coercion agree_car : agree >-> list.
Ralf Jung's avatar
Ralf Jung committed
40

41
42
43
Definition to_agree {A} (a : A) : agree A :=
  {| agree_car := [a]; agree_not_nil := eq_refl |}.

44
45
46
Lemma elem_of_agree {A} (x : agree A) :  a, a  agree_car x.
Proof. destruct x as [[|a ?] ?]; set_solver+. Qed.
Lemma agree_eq {A} (x y : agree A) : agree_car x = agree_car y  x = y.
Ralf Jung's avatar
Ralf Jung committed
47
Proof.
48
49
  destruct x as [a ?], y as [b ?]; simpl.
  intros ->; f_equal. apply (proof_irrel _).
Ralf Jung's avatar
Ralf Jung committed
50
51
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
52
Section agree.
53
Local Set Default Proof Using "Type".
54
Context {A : ofeT}.
55
56
Implicit Types a b : A.
Implicit Types x y : agree A.
Robbert Krebbers's avatar
Robbert Krebbers committed
57

58
(* OFE *)
59
Instance agree_dist : Dist (agree A) := λ n x y,
60
61
62
  ( a, a  agree_car x   b, b  agree_car y  a {n} b) 
  ( b, b  agree_car y   a, a  agree_car x  a {n} b).
Instance agree_equiv : Equiv (agree A) := λ x y,  n, x {n} y.
Ralf Jung's avatar
Ralf Jung committed
63

64
Definition agree_ofe_mixin : OfeMixin (agree A).
Robbert Krebbers's avatar
Robbert Krebbers committed
65
66
Proof.
  split.
67
68
69
70
71
72
73
74
75
76
  - done.
  - intros n; split; rewrite /dist /agree_dist.
    + intros x; split; eauto.
    + intros x y [??]. naive_solver eauto.
    + intros x y z [H1 H1'] [H2 H2']; split.
      * intros a ?. destruct (H1 a) as (b&?&?); auto.
        destruct (H2 b) as (c&?&?); eauto. by exists c; split; last etrans.
      * intros a ?. destruct (H2' a) as (b&?&?); auto.
        destruct (H1' b) as (c&?&?); eauto. by exists c; split; last etrans.
  - intros n x y [??]; split; naive_solver eauto using dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
Qed.
78
Canonical Structure agreeO := OfeT (agree A) agree_ofe_mixin.
79

80
81
82
83
84
85
86
87
88
89
(* CMRA *)
(* agree_validN is carefully written such that, when applied to a singleton, it
is convertible to True. This makes working with agreement much more pleasant. *)
Instance agree_validN : ValidN (agree A) := λ n x,
  match agree_car x with
  | [a] => True
  | _ =>  a b, a  agree_car x  b  agree_car x  a {n} b
  end.
Instance agree_valid : Valid (agree A) := λ x,  n, {n} x.

90
Program Instance agree_op : Op (agree A) := λ x y,
91
  {| agree_car := agree_car x ++ agree_car y |}.
92
Next Obligation. by intros [[|??]] y. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
Instance agree_pcore : PCore (agree A) := Some.
94

95
96
97
98
99
100
Lemma agree_validN_def n x :
  {n} x   a b, a  agree_car x  b  agree_car x  a {n} b.
Proof.
  rewrite /validN /agree_validN. destruct (agree_car _) as [|? [|??]]; auto.
  setoid_rewrite elem_of_list_singleton; naive_solver.
Qed.
Ralf Jung's avatar
Ralf Jung committed
101

102
103
104
Instance agree_comm : Comm () (@op (agree A) _).
Proof. intros x y n; split=> a /=; setoid_rewrite elem_of_app; naive_solver. Qed.
Instance agree_assoc : Assoc () (@op (agree A) _).
105
Proof.
106
  intros x y z n; split=> a /=; repeat setoid_rewrite elem_of_app; naive_solver.
107
Qed.
108
109
110
111
Lemma agree_idemp (x : agree A) : x  x  x.
Proof. intros n; split=> a /=; setoid_rewrite elem_of_app; naive_solver. Qed.

Instance agree_validN_ne n : Proper (dist n ==> impl) (@validN (agree A) _ n).
Ralf Jung's avatar
Ralf Jung committed
112
Proof.
113
114
  intros x y [H H']; rewrite /impl !agree_validN_def; intros Hv a b Ha Hb.
  destruct (H' a) as (a'&?&<-); auto. destruct (H' b) as (b'&?&<-); auto.
Ralf Jung's avatar
Ralf Jung committed
115
Qed.
116
117
Instance agree_validN_proper n : Proper (equiv ==> iff) (@validN (agree A) _ n).
Proof. move=> x y /equiv_dist H. by split; rewrite (H n). Qed.
Ralf Jung's avatar
Ralf Jung committed
118

119
Instance agree_op_ne' x : NonExpansive (op x).
Robbert Krebbers's avatar
Robbert Krebbers committed
120
Proof.
121
  intros n y1 y2 [H H']; split=> a /=; setoid_rewrite elem_of_app; naive_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
Qed.
123
Instance agree_op_ne : NonExpansive2 (@op (agree A) _).
124
Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed.
125
Instance agree_op_proper : Proper (() ==> () ==> ()) op := ne_proper_2 _.
126

Robbert Krebbers's avatar
Robbert Krebbers committed
127
128
129
130
131
Lemma agree_included (x y : agree A) : x  y  y  x  y.
Proof.
  split; [|by intros ?; exists y].
  by intros [z Hz]; rewrite Hz assoc agree_idemp.
Qed.
132

Ralf Jung's avatar
Ralf Jung committed
133
134
Lemma agree_op_invN n (x1 x2 : agree A) : {n} (x1  x2)  x1 {n} x2.
Proof.
135
136
137
  rewrite agree_validN_def /=. setoid_rewrite elem_of_app=> Hv; split=> a Ha.
  - destruct (elem_of_agree x2); naive_solver.
  - destruct (elem_of_agree x1); naive_solver.
138
139
Qed.

140
Definition agree_cmra_mixin : CmraMixin (agree A).
Robbert Krebbers's avatar
Robbert Krebbers committed
141
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
  apply cmra_total_mixin; try apply _ || by eauto.
143
  - intros n x; rewrite !agree_validN_def; eauto using dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
  - intros x. apply agree_idemp.
145
146
  - intros n x y; rewrite !agree_validN_def /=.
    setoid_rewrite elem_of_app; naive_solver.
147
  - intros n x y1 y2 Hval Hx; exists x, x; simpl; split.
148
    + by rewrite agree_idemp.
Ralf Jung's avatar
Ralf Jung committed
149
    + by move: Hval; rewrite Hx; move=> /agree_op_invN->; rewrite agree_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
Qed.
151
Canonical Structure agreeR : cmraT := CmraT (agree A) agree_cmra_mixin.
152

153
154
Global Instance agree_cmra_total : CmraTotal agreeR.
Proof. rewrite /CmraTotal; eauto. Qed.
155
Global Instance agree_core_id (x : agree A) : CoreId x.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
Proof. by constructor. Qed.
157

158
Global Instance agree_cmra_discrete : OfeDiscrete A  CmraDiscrete agreeR.
Ralf Jung's avatar
Ralf Jung committed
159
160
Proof.
  intros HD. split.
161
  - intros x y [H H'] n; split=> a; setoid_rewrite <-(discrete_iff_0 _ _); auto.
162
  - intros x; rewrite agree_validN_def=> Hv n. apply agree_validN_def=> a b ??.
163
    apply discrete_iff_0; auto.
Ralf Jung's avatar
Ralf Jung committed
164
165
Qed.

166
Global Instance to_agree_ne : NonExpansive to_agree.
Ralf Jung's avatar
Ralf Jung committed
167
Proof.
168
169
  intros n a1 a2 Hx; split=> b /=;
    setoid_rewrite elem_of_list_singleton; naive_solver.
Ralf Jung's avatar
Ralf Jung committed
170
Qed.
171
Global Instance to_agree_proper : Proper (() ==> ()) to_agree := ne_proper _.
172

173
174
175
176
177
178
179
180
181
Global Instance to_agree_discrete a : Discrete a  Discrete (to_agree a).
Proof.
  intros ? y [H H'] n; split.
  - intros a' ->%elem_of_list_singleton. destruct (H a) as [b ?]; first by left.
    exists b. by rewrite -discrete_iff_0.
  - intros b Hb. destruct (H' b) as (b'&->%elem_of_list_singleton&?); auto.
    exists a. by rewrite elem_of_list_singleton -discrete_iff_0.
Qed.

Ralf Jung's avatar
Ralf Jung committed
182
Global Instance to_agree_injN n : Inj (dist n) (dist n) (to_agree).
183
184
185
Proof.
  move=> a b [_] /=. setoid_rewrite elem_of_list_singleton. naive_solver.
Qed.
Ralf Jung's avatar
Ralf Jung committed
186
Global Instance to_agree_inj : Inj () () (to_agree).
187
Proof. intros a b ?. apply equiv_dist=>n. by apply (inj to_agree), equiv_dist. Qed.
188

189
Lemma to_agree_uninjN n x : {n} x   a, to_agree a {n} x.
190
Proof.
191
192
193
  rewrite agree_validN_def=> Hv.
  destruct (elem_of_agree x) as [a ?].
  exists a; split=> b /=; setoid_rewrite elem_of_list_singleton; naive_solver.
Ralf Jung's avatar
Ralf Jung committed
194
195
Qed.

196
Lemma to_agree_uninj x :  x   a, to_agree a  x.
197
Proof.
198
199
200
  rewrite /valid /agree_valid; setoid_rewrite agree_validN_def.
  destruct (elem_of_agree x) as [a ?].
  exists a; split=> b /=; setoid_rewrite elem_of_list_singleton; naive_solver.
201
202
Qed.

203
Lemma agree_valid_includedN n x y : {n} y  x {n} y  x {n} y.
Ralf Jung's avatar
Ralf Jung committed
204
Proof.
205
206
207
208
  move=> Hval [z Hy]; move: Hval; rewrite Hy.
  by move=> /agree_op_invN->; rewrite agree_idemp.
Qed.

209
Lemma to_agree_includedN n a b : to_agree a {n} to_agree b  a {n} b.
210
Proof.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
211
  split; last by intros ->. intros [x [_ Hincl]].
212
213
214
  by destruct (Hincl a) as (? & ->%elem_of_list_singleton & ?); first set_solver+.
Qed.

215
216
217
218
219
Lemma to_agree_included a b : to_agree a  to_agree b  a  b.
Proof.
  split; last by intros ->.
  intros (x & Heq). apply equiv_dist=>n. destruct (Heq n) as [_ Hincl].
  by destruct (Hincl a) as (? & ->%elem_of_list_singleton & ?); first set_solver+.
220
221
Qed.

222
Global Instance agree_cancelable x : Cancelable x.
223
224
225
226
227
228
229
Proof.
  intros n y z Hv Heq.
  destruct (to_agree_uninjN n x) as [x' EQx]; first by eapply cmra_validN_op_l.
  destruct (to_agree_uninjN n y) as [y' EQy]; first by eapply cmra_validN_op_r.
  destruct (to_agree_uninjN n z) as [z' EQz].
  { eapply (cmra_validN_op_r n x z). by rewrite -Heq. }
  assert (Hx'y' : x' {n} y').
230
  { apply (inj to_agree), agree_op_invN. by rewrite EQx EQy. }
231
  assert (Hx'z' : x' {n} z').
232
  { apply (inj to_agree), agree_op_invN. by rewrite EQx EQz -Heq. }
233
234
235
  by rewrite -EQy -EQz -Hx'y' -Hx'z'.
Qed.

236
Lemma agree_op_inv x y :  (x  y)  x  y.
237
238
239
Proof.
  intros ?. apply equiv_dist=>n. by apply agree_op_invN, cmra_valid_validN.
Qed.
240
Lemma agree_op_inv' a b :  (to_agree a  to_agree b)  a  b.
241
Proof. by intros ?%agree_op_inv%(inj to_agree). Qed.
242
Lemma agree_op_invL' `{!LeibnizEquiv A} a b :  (to_agree a  to_agree b)  a = b.
243
244
Proof. by intros ?%agree_op_inv'%leibniz_equiv. Qed.

245
(** Internalized properties *)
246
Lemma agree_equivI {M} a b : to_agree a  to_agree b @{uPredI M} (a  b).
247
Proof.
Ralf Jung's avatar
Ralf Jung committed
248
  uPred.unseal. do 2 split.
249
  - intros Hx. exact: (inj to_agree).
Ralf Jung's avatar
Ralf Jung committed
250
  - intros Hx. exact: to_agree_ne.
251
Qed.
252
Lemma agree_validI {M} x y :  (x  y) @{uPredI M} x  y.
Ralf Jung's avatar
Ralf Jung committed
253
Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed.
254
255
256

Lemma to_agree_uninjI {M} x :  x @{uPredI M}  a, to_agree a  x.
Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
257
258
End agree.

259
Instance: Params (@to_agree) 1 := {}.
260
Arguments agreeO : clear implicits.
261
Arguments agreeR : clear implicits.
262

263
Program Definition agree_map {A B} (f : A  B) (x : agree A) : agree B :=
264
265
  {| agree_car := f <$> agree_car x |}.
Next Obligation. by intros A B f [[|??] ?]. Qed.
266
Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
267
Proof. apply agree_eq. by rewrite /= list_fmap_id. Qed.
268
269
Lemma agree_map_compose {A B C} (f : A  B) (g : B  C) (x : agree A) :
  agree_map (g  f) x = agree_map g (agree_map f x).
270
Proof. apply agree_eq. by rewrite /= list_fmap_compose. Qed.
271
272
273
Lemma agree_map_to_agree {A B} (f : A  B) (x : A) :
  agree_map f (to_agree x) = to_agree (f x).
Proof. by apply agree_eq. Qed.
274

Robbert Krebbers's avatar
Robbert Krebbers committed
275
Section agree_map.
276
  Context {A B : ofeT} (f : A  B) {Hf: NonExpansive f}.
277

278
  Instance agree_map_ne : NonExpansive (agree_map f).
279
280
281
282
  Proof.
    intros n x y [H H']; split=> b /=; setoid_rewrite elem_of_list_fmap.
    - intros (a&->&?). destruct (H a) as (a'&?&?); auto. naive_solver.
    - intros (a&->&?). destruct (H' a) as (a'&?&?); auto. naive_solver.
Ralf Jung's avatar
Ralf Jung committed
283
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
284
  Instance agree_map_proper : Proper (() ==> ()) (agree_map f) := ne_proper _.
Ralf Jung's avatar
Ralf Jung committed
285

286
  Lemma agree_map_ext (g : A  B) x :
287
288
289
290
291
    ( a, f a  g a)  agree_map f x  agree_map g x.
  Proof using Hf.
    intros Hfg n; split=> b /=; setoid_rewrite elem_of_list_fmap.
    - intros (a&->&?). exists (g a). rewrite Hfg; eauto.
    - intros (a&->&?). exists (f a). rewrite -Hfg; eauto.
Ralf Jung's avatar
Ralf Jung committed
292
293
  Qed.

294
  Global Instance agree_map_morphism : CmraMorphism (agree_map f).
295
  Proof using Hf.
Robbert Krebbers's avatar
Robbert Krebbers committed
296
    split; first apply _.
297
298
299
    - intros n x. rewrite !agree_validN_def=> Hv b b' /=.
      intros (a&->&?)%elem_of_list_fmap (a'&->&?)%elem_of_list_fmap.
      apply Hf; eauto.
300
    - done.
301
302
    - intros x y n; split=> b /=;
        rewrite !fmap_app; setoid_rewrite elem_of_app; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
303
304
  Qed.
End agree_map.
Robbert Krebbers's avatar
Robbert Krebbers committed
305

306
307
308
Definition agreeO_map {A B} (f : A -n> B) : agreeO A -n> agreeO B :=
  OfeMor (agree_map f : agreeO A  agreeO B).
Instance agreeO_map_ne A B : NonExpansive (@agreeO_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
309
Proof.
310
311
  intros n f g Hfg x; split=> b /=;
    setoid_rewrite elem_of_list_fmap; naive_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
312
Qed.
Ralf Jung's avatar
Ralf Jung committed
313

314
315
316
Program Definition agreeRF (F : oFunctor) : rFunctor := {|
  rFunctor_car A _ B _ := agreeR (oFunctor_car F A B);
  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := agreeO_map (oFunctor_map F fg)
317
|}.
318
Next Obligation.
319
  intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl. by apply agreeO_map_ne, oFunctor_map_ne.
320
Qed.
321
Next Obligation.
322
  intros F A ? B ? x; simpl. rewrite -{2}(agree_map_id x).
323
  apply (agree_map_ext _)=>y. by rewrite oFunctor_map_id.
324
325
Qed.
Next Obligation.
326
  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -agree_map_compose.
327
  apply (agree_map_ext _)=>y; apply oFunctor_map_compose.
328
Qed.
329
330

Instance agreeRF_contractive F :
331
  oFunctorContractive F  rFunctorContractive (agreeRF F).
332
Proof.
333
  intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl.
334
  by apply agreeO_map_ne, oFunctor_map_contractive.
335
Qed.