agree.v 12.2 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 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
(** Define an agreement construction such that Agree A is discrete when A is discrete.
    Notice that this construction is NOT complete.  The fullowing is due to Aleš:

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
Record agree (A : Type) : Type := {
30 31
  agree_car : list A;
  agree_not_nil : bool_decide (agree_car = []) = false
Robbert Krebbers's avatar
Robbert Krebbers committed
32
}.
Ralf Jung's avatar
Ralf Jung committed
33
Arguments agree_car {_} _.
34 35
Arguments agree_not_nil {_} _.
Local Coercion agree_car : agree >-> list.
Ralf Jung's avatar
Ralf Jung committed
36

37 38 39
Definition to_agree {A} (a : A) : agree A :=
  {| agree_car := [a]; agree_not_nil := eq_refl |}.

40 41 42
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
43
Proof.
44 45
  destruct x as [a ?], y as [b ?]; simpl.
  intros ->; f_equal. apply (proof_irrel _).
Ralf Jung's avatar
Ralf Jung committed
46 47
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
48
Section agree.
49
Local Set Default Proof Using "Type".
50
Context {A : ofeT}.
51 52
Implicit Types a b : A.
Implicit Types x y : agree A.
Robbert Krebbers's avatar
Robbert Krebbers committed
53

54
(* OFE *)
55
Instance agree_dist : Dist (agree A) := λ n x y,
56 57 58
  ( 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
59

60
Definition agree_ofe_mixin : OfeMixin (agree A).
Robbert Krebbers's avatar
Robbert Krebbers committed
61 62
Proof.
  split.
63 64 65 66 67 68 69 70 71 72
  - 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
73
Qed.
74 75
Canonical Structure agreeC := OfeT (agree A) agree_ofe_mixin.

76 77 78 79 80 81 82 83 84 85
(* 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.

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

91 92 93 94 95 96
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
97

98 99 100
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) _).
101
Proof.
102
  intros x y z n; split=> a /=; repeat setoid_rewrite elem_of_app; naive_solver.
103
Qed.
104 105 106 107
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
108
Proof.
109 110
  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
111
Qed.
112 113
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
114

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

Robbert Krebbers's avatar
Robbert Krebbers committed
123 124 125 126 127
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.
128

Ralf Jung's avatar
Ralf Jung committed
129 130
Lemma agree_op_invN n (x1 x2 : agree A) : {n} (x1  x2)  x1 {n} x2.
Proof.
131 132 133
  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.
134 135
Qed.

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

149 150
Global Instance agree_cmra_total : CmraTotal agreeR.
Proof. rewrite /CmraTotal; eauto. Qed.
151
Global Instance agree_core_id (x : agree A) : CoreId x.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
Proof. by constructor. Qed.
153

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

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

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

185
Lemma to_agree_uninjN n x : {n} x   a, to_agree a {n} x.
186
Proof.
187 188 189
  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
190 191
Qed.

192
Lemma to_agree_uninj x :  x   a, to_agree a  x.
193
Proof.
194 195 196
  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.
197 198
Qed.

199
Lemma agree_valid_includedN n x y : {n} y  x {n} y  x {n} y.
Ralf Jung's avatar
Ralf Jung committed
200
Proof.
201 202 203 204 205 206 207 208 209
  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+.
210 211
Qed.

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

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

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

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
247 248
End agree.

249
Instance: Params (@to_agree) 1.
250
Arguments agreeC : clear implicits.
251
Arguments agreeR : clear implicits.
252

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

Robbert Krebbers's avatar
Robbert Krebbers committed
265
Section agree_map.
266
  Context {A B : ofeT} (f : A  B) `{Hf: NonExpansive f}.
267

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

276
  Lemma agree_map_ext (g : A  B) x :
277 278 279 280 281
    ( 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
282 283
  Qed.

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

296 297
Definition agreeC_map {A B} (f : A -n> B) : agreeC A -n> agreeC B :=
  CofeMor (agree_map f : agreeC A  agreeC B).
298
Instance agreeC_map_ne A B : NonExpansive (@agreeC_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
299
Proof.
300 301
  intros n f g Hfg x; split=> b /=;
    setoid_rewrite elem_of_list_fmap; naive_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
302
Qed.
Ralf Jung's avatar
Ralf Jung committed
303

304 305 306 307
Program Definition agreeRF (F : cFunctor) : rFunctor := {|
  rFunctor_car A B := agreeR (cFunctor_car F A B);
  rFunctor_map A1 A2 B1 B2 fg := agreeC_map (cFunctor_map F fg)
|}.
308 309 310
Next Obligation.
  intros ? A1 A2 B1 B2 n ???; simpl. by apply agreeC_map_ne, cFunctor_ne.
Qed.
311 312
Next Obligation.
  intros F A B x; simpl. rewrite -{2}(agree_map_id x).
313
  apply (agree_map_ext _)=>y. by rewrite cFunctor_id.
314 315 316
Qed.
Next Obligation.
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -agree_map_compose.
317
  apply (agree_map_ext _)=>y; apply cFunctor_compose.
318
Qed.
319 320 321 322 323 324 325

Instance agreeRF_contractive F :
  cFunctorContractive F  rFunctorContractive (agreeRF F).
Proof.
  intros ? A1 A2 B1 B2 n ???; simpl.
  by apply agreeC_map_ne, cFunctor_contractive.
Qed.