agree.v 12.6 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
Import stdpp.list. (* Make sure we use those names. FIXME: remove when we drop Coq 8.9 support. *)
Ralf Jung's avatar
Ralf Jung committed
5 6 7 8
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _  !_ /.
Local Arguments op _ _ _ !_ /.
Local Arguments pcore _ _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
9

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

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

30 31
(** 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
32 33
lemma [to_agree_uninjN] instead. In general, [agree_car] should ONLY be used
internally in this file.  *)
34
Record agree (A : Type) : Type := {
35 36
  agree_car : list A;
  agree_not_nil : bool_decide (agree_car = []) = false
Robbert Krebbers's avatar
Robbert Krebbers committed
37
}.
Ralf Jung's avatar
Ralf Jung committed
38
Arguments agree_car {_} _.
39 40
Arguments agree_not_nil {_} _.
Local Coercion agree_car : agree >-> list.
Ralf Jung's avatar
Ralf Jung committed
41

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

45 46 47
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
48
Proof.
49 50
  destruct x as [a ?], y as [b ?]; simpl.
  intros ->; f_equal. apply (proof_irrel _).
Ralf Jung's avatar
Ralf Jung committed
51 52
Qed.

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

59
(* OFE *)
60
Instance agree_dist : Dist (agree A) := λ n x y,
61 62 63
  ( 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
64

65
Definition agree_ofe_mixin : OfeMixin (agree A).
Robbert Krebbers's avatar
Robbert Krebbers committed
66 67
Proof.
  split.
68 69 70 71 72 73 74 75 76 77
  - 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
78
Qed.
79
Canonical Structure agreeO := OfeT (agree A) agree_ofe_mixin.
80

81 82 83 84 85 86 87 88 89 90
(* 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.

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

96 97 98 99 100 101
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
102

103 104 105
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) _).
106
Proof.
107
  intros x y z n; split=> a /=; repeat setoid_rewrite elem_of_app; naive_solver.
108
Qed.
109 110 111 112
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
113
Proof.
114 115
  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
116
Qed.
117 118
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
119

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

Robbert Krebbers's avatar
Robbert Krebbers committed
128 129 130 131 132
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.
133

Ralf Jung's avatar
Ralf Jung committed
134 135
Lemma agree_op_invN n (x1 x2 : agree A) : {n} (x1  x2)  x1 {n} x2.
Proof.
136 137 138
  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.
139 140
Qed.

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

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

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

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

174 175 176 177 178 179 180 181 182
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
183
Global Instance to_agree_injN n : Inj (dist n) (dist n) (to_agree).
184 185 186
Proof.
  move=> a b [_] /=. setoid_rewrite elem_of_list_singleton. naive_solver.
Qed.
Ralf Jung's avatar
Ralf Jung committed
187
Global Instance to_agree_inj : Inj () () (to_agree).
188
Proof. intros a b ?. apply equiv_dist=>n. by apply (inj to_agree), equiv_dist. Qed.
189

190
Lemma to_agree_uninjN n x : {n} x   a, to_agree a {n} x.
191
Proof.
192 193 194
  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
195 196
Qed.

197
Lemma to_agree_uninj x :  x   a, to_agree a  x.
198
Proof.
199 200 201
  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.
202 203
Qed.

204
Lemma agree_valid_includedN n x y : {n} y  x {n} y  x {n} y.
Ralf Jung's avatar
Ralf Jung committed
205
Proof.
206 207 208 209 210 211 212 213 214
  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+.
215 216
Qed.

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

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

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

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

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

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

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

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

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

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

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

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

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