agree.v 11.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
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 := Agree {
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
34
Arguments Agree {_} _ _.
Arguments agree_car {_} _.
35
36
Arguments agree_not_nil {_} _.
Local Coercion agree_car : agree >-> list.
Ralf Jung's avatar
Ralf Jung committed
37

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

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

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

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

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

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

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

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
147
148
Global Instance agree_total : CMRATotal agreeR.
Proof. rewrite /CMRATotal; eauto. Qed.
149
Global Instance agree_persistent (x : agree A) : Persistent x.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
Proof. by constructor. Qed.
151

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.