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

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

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

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

73 74 75 76 77 78 79 80 81 82
(* 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.

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

88 89 90 91 92 93
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
94

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
120 121 122 123 124
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.
125

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

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

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

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

159 160
Program Definition to_agree (a : A) : agree A :=
  {| agree_car := [a]; agree_not_nil := eq_refl |}.
161

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

Ralf Jung's avatar
Ralf Jung committed
169
Global Instance to_agree_injN n : Inj (dist n) (dist n) (to_agree).
170 171 172
Proof.
  move=> a b [_] /=. setoid_rewrite elem_of_list_singleton. naive_solver.
Qed.
Ralf Jung's avatar
Ralf Jung committed
173
Global Instance to_agree_inj : Inj () () (to_agree).
174
Proof. intros a b ?. apply equiv_dist=>n. by apply to_agree_injN, equiv_dist. Qed.
175

176
Lemma to_agree_uninjN n (x : agree A) : {n} x   a : A, to_agree a {n} x.
177
Proof.
178 179 180
  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
181 182
Qed.

183 184
Lemma to_agree_uninj (x : agree A) :  x   y : A, to_agree y  x.
Proof.
185 186 187
  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.
188 189
Qed.

190
Lemma agree_valid_includedN n x y : {n} y  x {n} y  x {n} y.
Ralf Jung's avatar
Ralf Jung committed
191
Proof.
192 193 194 195 196 197 198 199 200
  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+.
201 202
Qed.

203
Global Instance agree_cancelable x : Cancelable x.
204 205 206 207 208 209 210
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').
211
  { apply (inj to_agree), agree_op_invN. by rewrite EQx EQy. }
212
  assert (Hx'z' : x' {n} z').
213
  { apply (inj to_agree), agree_op_invN. by rewrite EQx EQz -Heq. }
214 215 216
  by rewrite -EQy -EQz -Hx'y' -Hx'z'.
Qed.

217
Lemma agree_op_inv x y :  (x  y)  x  y.
218 219 220
Proof.
  intros ?. apply equiv_dist=>n. by apply agree_op_invN, cmra_valid_validN.
Qed.
221
Lemma agree_op_inv' a b :  (to_agree a  to_agree b)  a  b.
222
Proof. by intros ?%agree_op_inv%(inj _). Qed.
223
Lemma agree_op_invL' `{!LeibnizEquiv A} a b :  (to_agree a  to_agree b)  a = b.
224 225
Proof. by intros ?%agree_op_inv'%leibniz_equiv. Qed.

226
(** Internalized properties *)
227
Lemma agree_equivI {M} a b : to_agree a  to_agree b  (a  b : uPred M).
228
Proof.
Ralf Jung's avatar
Ralf Jung committed
229 230 231
  uPred.unseal. do 2 split.
  - intros Hx. exact: to_agree_injN.
  - intros Hx. exact: to_agree_ne.
232
Qed.
233
Lemma agree_validI {M} x y :  (x  y)  (x  y : uPred M).
Ralf Jung's avatar
Ralf Jung committed
234
Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
235 236
End agree.

237
Instance: Params (@to_agree) 1.
238
Arguments agreeC : clear implicits.
239
Arguments agreeR : clear implicits.
240

241
Program Definition agree_map {A B} (f : A  B) (x : agree A) : agree B :=
242 243
  {| agree_car := f <$> agree_car x |}.
Next Obligation. by intros A B f [[|??] ?]. Qed.
244
Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
245
Proof. apply agree_eq. by rewrite /= list_fmap_id. Qed.
246 247
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).
248
Proof. apply agree_eq. by rewrite /= list_fmap_compose. Qed.
249

Robbert Krebbers's avatar
Robbert Krebbers committed
250
Section agree_map.
251
  Context {A B : ofeT} (f : A  B) `{Hf: NonExpansive f}.
252

253
  Instance agree_map_ne : NonExpansive (agree_map f).
254 255 256 257
  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
258
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
259
  Instance agree_map_proper : Proper (() ==> ()) (agree_map f) := ne_proper _.
Ralf Jung's avatar
Ralf Jung committed
260

261
  Lemma agree_map_ext (g : A  B) x :
262 263 264 265 266
    ( 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
267 268
  Qed.

269
  Global Instance agree_map_morphism : CmraMorphism (agree_map f).
270
  Proof using Hf.
Robbert Krebbers's avatar
Robbert Krebbers committed
271
    split; first apply _.
272 273 274
    - intros n x. rewrite !agree_validN_def=> Hv b b' /=.
      intros (a&->&?)%elem_of_list_fmap (a'&->&?)%elem_of_list_fmap.
      apply Hf; eauto.
275
    - done.
276 277
    - intros x y n; split=> b /=;
        rewrite !fmap_app; setoid_rewrite elem_of_app; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
278 279
  Qed.
End agree_map.
Robbert Krebbers's avatar
Robbert Krebbers committed
280

281 282
Definition agreeC_map {A B} (f : A -n> B) : agreeC A -n> agreeC B :=
  CofeMor (agree_map f : agreeC A  agreeC B).
283
Instance agreeC_map_ne A B : NonExpansive (@agreeC_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
284
Proof.
285 286
  intros n f g Hfg x; split=> b /=;
    setoid_rewrite elem_of_list_fmap; naive_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
287
Qed.
Ralf Jung's avatar
Ralf Jung committed
288

289 290 291 292
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)
|}.
293 294 295
Next Obligation.
  intros ? A1 A2 B1 B2 n ???; simpl. by apply agreeC_map_ne, cFunctor_ne.
Qed.
296 297
Next Obligation.
  intros F A B x; simpl. rewrite -{2}(agree_map_id x).
298
  apply (agree_map_ext _)=>y. by rewrite cFunctor_id.
299 300 301
Qed.
Next Obligation.
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -agree_map_compose.
302
  apply (agree_map_ext _)=>y; apply cFunctor_compose.
303
Qed.
304 305 306 307 308 309 310

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.