agree.v 12.5 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 209 210 211 212 213
  move=> Hval [z Hy]; move: Hval; rewrite Hy.
  by move=> /agree_op_invN->; rewrite agree_idemp.
Qed.

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+.
214 215
Qed.

216
Global Instance agree_cancelable x : Cancelable x.
217 218 219 220 221 222 223
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').
224
  { apply (inj to_agree), agree_op_invN. by rewrite EQx EQy. }
225
  assert (Hx'z' : x' {n} z').
226
  { apply (inj to_agree), agree_op_invN. by rewrite EQx EQz -Heq. }
227 228 229
  by rewrite -EQy -EQz -Hx'y' -Hx'z'.
Qed.

230
Lemma agree_op_inv x y :  (x  y)  x  y.
231 232 233
Proof.
  intros ?. apply equiv_dist=>n. by apply agree_op_invN, cmra_valid_validN.
Qed.
234
Lemma agree_op_inv' a b :  (to_agree a  to_agree b)  a  b.
235
Proof. by intros ?%agree_op_inv%(inj to_agree). Qed.
236
Lemma agree_op_invL' `{!LeibnizEquiv A} a b :  (to_agree a  to_agree b)  a = b.
237 238
Proof. by intros ?%agree_op_inv'%leibniz_equiv. Qed.

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

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
251 252
End agree.

253
Instance: Params (@to_agree) 1 := {}.
254
Arguments agreeO : clear implicits.
255
Arguments agreeR : clear implicits.
256

257
Program Definition agree_map {A B} (f : A  B) (x : agree A) : agree B :=
258 259
  {| agree_car := f <$> agree_car x |}.
Next Obligation. by intros A B f [[|??] ?]. Qed.
260
Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
261
Proof. apply agree_eq. by rewrite /= list_fmap_id. Qed.
262 263
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).
264
Proof. apply agree_eq. by rewrite /= list_fmap_compose. Qed.
265 266 267
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.
268

Robbert Krebbers's avatar
Robbert Krebbers committed
269
Section agree_map.
270
  Context {A B : ofeT} (f : A  B) {Hf: NonExpansive f}.
271

272
  Instance agree_map_ne : NonExpansive (agree_map f).
273 274 275 276
  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
277
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
278
  Instance agree_map_proper : Proper (() ==> ()) (agree_map f) := ne_proper _.
Ralf Jung's avatar
Ralf Jung committed
279

280
  Lemma agree_map_ext (g : A  B) x :
281 282 283 284 285
    ( 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
286 287
  Qed.

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

300 301 302
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
303
Proof.
304 305
  intros n f g Hfg x; split=> b /=;
    setoid_rewrite elem_of_list_fmap; naive_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
306
Qed.
Ralf Jung's avatar
Ralf Jung committed
307

308 309 310
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)
311
|}.
312
Next Obligation.
313
  intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl. by apply agreeO_map_ne, oFunctor_ne.
314
Qed.
315
Next Obligation.
316
  intros F A ? B ? x; simpl. rewrite -{2}(agree_map_id x).
317
  apply (agree_map_ext _)=>y. by rewrite oFunctor_id.
318 319
Qed.
Next Obligation.
320
  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -agree_map_compose.
321
  apply (agree_map_ext _)=>y; apply oFunctor_compose.
322
Qed.
323 324

Instance agreeRF_contractive F :
325
  oFunctorContractive F  rFunctorContractive (agreeRF F).
326
Proof.
327
  intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl.
328
  by apply agreeO_map_ne, oFunctor_contractive.
329
Qed.