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

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

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

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

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

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

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

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

94 95 96 97 98 99
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
100

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

252
Instance: Params (@to_agree) 1.
253
Arguments agreeC : clear implicits.
254
Arguments agreeR : clear implicits.
255

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

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

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

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

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

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

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

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.