one_shot.v 11.8 KB
Newer Older
1
2
3
4
From iris.algebra Require Export cmra.
From iris.algebra Require Import upred.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _  !_ /.
Ralf Jung's avatar
Ralf Jung committed
5
6
Local Arguments cmra_validN _ _ !_ /.
Local Arguments cmra_valid _  !_ /.
7

Ralf Jung's avatar
Ralf Jung committed
8
(* TODO: Really, we should have sums, and then this should be just "excl unit + A". *)
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
Inductive one_shot {A : Type} :=
  | OneShotPending : one_shot
  | Shot : A  one_shot
  | OneShotUnit : one_shot
  | OneShotBot : one_shot.
Arguments one_shot _ : clear implicits.
Instance maybe_Shot {A} : Maybe (@Shot A) := λ x,
  match x with Shot a => Some a | _ => None end.
Instance: Params (@Shot) 1.

Section cofe.
Context {A : cofeT}.
Implicit Types a b : A.
Implicit Types x y : one_shot A.

(* Cofe *)
Inductive one_shot_equiv : Equiv (one_shot A) :=
  | OneShotPending_equiv : OneShotPending  OneShotPending
  | OneShot_equiv a b : a  b  Shot a  Shot b
  | OneShotUnit_equiv : OneShotUnit  OneShotUnit
  | OneShotBot_equiv : OneShotBot  OneShotBot.
Existing Instance one_shot_equiv.
Inductive one_shot_dist : Dist (one_shot A) :=
  | OneShotPending_dist n : OneShotPending {n} OneShotPending
  | OneShot_dist n a b : a {n} b  Shot a {n} Shot b
  | OneShotUnit_dist n : OneShotUnit {n} OneShotUnit
  | OneShotBot_dist n : OneShotBot {n} OneShotBot.
Existing Instance one_shot_dist.

Global Instance One_Shot_ne n : Proper (dist n ==> dist n) (@Shot A).
Proof. by constructor. Qed.
Global Instance One_Shot_proper : Proper (() ==> ()) (@Shot A).
Proof. by constructor. Qed.
Global Instance One_Shot_inj : Inj () () (@Shot A).
Proof. by inversion_clear 1. Qed.
Global Instance One_Shot_dist_inj n : Inj (dist n) (dist n) (@Shot A).
Proof. by inversion_clear 1. Qed.

Program Definition one_shot_chain (c : chain (one_shot A)) (a : A)
    (H : maybe Shot (c 0) = Some a) : chain A :=
  {| chain_car n := match c n return _ with Shot b => b | _ => a end |}.
Next Obligation.
  intros c a ? n i ?; simpl.
  destruct (c 0) eqn:?; simplify_eq/=.
  by feed inversion (chain_cauchy c n i).
Qed.
Instance one_shot_compl : Compl (one_shot A) := λ c,
  match Some_dec (maybe Shot (c 0)) with
  | inleft (exist a H) => Shot (compl (one_shot_chain c a H))
  | inright _ => c 0
  end.
Definition one_shot_cofe_mixin : CofeMixin (one_shot A).
Proof.
  split.
  - intros mx my; split.
    + by destruct 1; subst; constructor; try apply equiv_dist.
    + intros Hxy; feed inversion (Hxy 0); subst; constructor; try done.
      apply equiv_dist=> n; by feed inversion (Hxy n).
  - intros n; split.
    + by intros [|a| |]; constructor.
    + by destruct 1; constructor.
    + destruct 1; inversion_clear 1; constructor; etrans; eauto.
  - by inversion_clear 1; constructor; done || apply dist_S.
  - intros n c; unfold compl, one_shot_compl.
    destruct (Some_dec (maybe Shot (c 0))) as [[a Hx]|].
    { assert (c 0 = Shot a) by (by destruct (c 0); simplify_eq/=).
      assert ( b, c n = Shot b) as [y Hy].
      { feed inversion (chain_cauchy c 0 n);
          eauto with lia congruence f_equal. }
      rewrite Hy; constructor; auto.
      by rewrite (conv_compl n (one_shot_chain c a Hx)) /= Hy. }
    feed inversion (chain_cauchy c 0 n); first lia;
       constructor; destruct (c 0); simplify_eq/=.
Qed.
Canonical Structure one_shotC : cofeT := CofeT one_shot_cofe_mixin.
Global Instance one_shot_discrete : Discrete A  Discrete one_shotC.
Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed.
Global Instance one_shot_leibniz : LeibnizEquiv A  LeibnizEquiv (one_shot A).
Proof. by destruct 2; f_equal; done || apply leibniz_equiv. Qed.

Global Instance Shot_timeless (a : A) : Timeless a  Timeless (Shot a).
Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed.
Global Instance OneShotUnit_timeless : Timeless (@OneShotUnit A).
Proof. by inversion_clear 1; constructor. Qed.
End cofe.

Arguments one_shotC : clear implicits.

Ralf Jung's avatar
Ralf Jung committed
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
(* Functor on COFEs *)
Definition one_shot_map {A B} (f : A  B) (x : one_shot A) : one_shot B :=
  match x with
  | OneShotPending => OneShotPending
  | Shot a => Shot (f a)
  | OneShotUnit => OneShotUnit
  | OneShotBot => OneShotBot
  end.
Instance: Params (@one_shot_map) 2.

Lemma one_shot_map_id {A} (x : one_shot A) : one_shot_map id x = x.
Proof. by destruct x. Qed.
Lemma one_shot_map_compose {A B C} (f : A  B) (g : B  C) (x : one_shot A) :
  one_shot_map (g  f) x = one_shot_map g (one_shot_map f x).
Proof. by destruct x. Qed.
Lemma one_shot_map_ext {A B : cofeT} (f g : A  B) x :
  ( x, f x  g x)  one_shot_map f x  one_shot_map g x.
Proof. by destruct x; constructor. Qed.
Instance one_shot_map_cmra_ne {A B : cofeT} n :
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@one_shot_map A B).
Proof. intros f f' Hf; destruct 1; constructor; by try apply Hf. Qed.
Definition one_shotC_map {A B} (f : A -n> B) : one_shotC A -n> one_shotC B :=
  CofeMor (one_shot_map f).
Instance one_shotC_map_ne A B n : Proper (dist n ==> dist n) (@one_shotC_map A B).
Proof. intros f f' Hf []; constructor; by try apply Hf. Qed.

Section cmra.
Context {A : cmraT}.
Implicit Types a b : A.
Implicit Types x y : one_shot A.

(* CMRA *)
Instance one_shot_valid : Valid (one_shot A) := λ x,
  match x with
  | OneShotPending => True
  | Shot a =>  a
  | OneShotUnit => True
  | OneShotBot => False
  end.
Instance one_shot_validN : ValidN (one_shot A) := λ n x,
  match x with
  | OneShotPending => True
  | Shot a => {n} a
  | OneShotUnit => True
  | OneShotBot => False
  end.
Global Instance one_shot_empty : Empty (one_shot A) := OneShotUnit.
Instance one_shot_core : Core (one_shot A) := λ x,
  match x with
  | Shot a => Shot (core a)
  | OneShotBot => OneShotBot
  | _ => 
  end.
Instance one_shot_op : Op (one_shot A) := λ x y,
  match x, y with
  | Shot a, Shot b => Shot (a  b)
  | Shot a, OneShotUnit | OneShotUnit, Shot a => Shot a
  | OneShotUnit, OneShotPending | OneShotPending, OneShotUnit => OneShotPending
  | OneShotUnit, OneShotUnit => OneShotUnit
  | _, _ => OneShotBot
  end.

Lemma Shot_op a b : Shot a  Shot b = Shot (a  b).
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
162
163
Lemma Shot_core a : core (Shot a) = Shot (core a).
Proof. done. Qed.

Ralf Jung's avatar
Ralf Jung committed
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
Lemma Shot_incl a b : Shot a  Shot b  a  b.
Proof.
  split; intros [c H].
  - destruct c; inversion_clear H; first by eexists.
    by rewrite (_ : b  a).
  - exists (Shot c). constructor. done.
Qed. 

Definition one_shot_cmra_mixin : CMRAMixin (one_shot A).
Proof.
  split.
  - intros n []; destruct 1; constructor; by cofe_subst. 
  - intros ? [|a| |] [|b| |] H; inversion_clear H; constructor; by f_equiv.
  - intros ? [|a| |] [|b| |] H; inversion_clear H; cofe_subst; done.
  - intros [|a| |]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O.
  - intros n [|a| |]; simpl; auto using cmra_validN_S.
  - intros [|a1| |] [|a2| |] [|a3| |]; constructor; by rewrite ?assoc.
  - intros [|a1| |] [|a2| |]; constructor; by rewrite 1?comm.
  - intros [|a| |]; constructor; []. exact: cmra_core_l.
  - intros [|a| |]; constructor; []. exact: cmra_core_idemp.
  - intros [|a1| |] [|a2| |]; simpl;
      try solve [ by exists OneShotUnit; constructor
                | by exists OneShotBot; constructor
                | by intros [[|a3| |] H]; inversion_clear H ].
    + intros H%Shot_incl. apply Shot_incl, cmra_core_preserving. done.
    + intros _. exists (Shot (core a2)). by constructor.
  - intros n [|a1| |] [|a2| |]; simpl; eauto using cmra_validN_op_l; done.
  - intros n [|a| |] y1 y2 Hx Hx'; last 2 first.
    + by exists (, ); destruct y1, y2; inversion_clear Hx'.
    + by exists (OneShotBot, OneShotBot); destruct y1, y2; inversion_clear Hx'.
    + destruct y1, y2; try (exfalso; by inversion_clear Hx').
      * by exists (OneShotPending, OneShotUnit).
      * by exists (OneShotUnit, OneShotPending).
    +  destruct y1 as [|b1 | |], y2 as [|b2| |]; try (exfalso; by inversion_clear Hx').
       * apply (inj Shot) in Hx'.
         destruct (cmra_extend n a b1 b2) as ([z1 z2]&?&?&?); auto.
         exists (Shot z1, Shot z2). by repeat constructor.
       * exists (Shot a, ). inversion_clear Hx'. by repeat constructor.
       * exists (, Shot a). inversion_clear Hx'. by repeat constructor.
Qed.
Canonical Structure one_shotR : cmraT := CMRAT one_shot_cofe_mixin one_shot_cmra_mixin.
Global Instance one_shot_cmra_unit : CMRAUnit one_shotR.
Proof. split. done. by intros []. apply _. Qed.
Global Instance one_shot_cmra_discrete : CMRADiscrete A  CMRADiscrete one_shotR.
Proof.
  split; first apply _.
  intros [|a| |]; simpl; auto using cmra_discrete_valid.
Qed.

213
214
215
Global Instance Shot_persistent a : Persistent a  Persistent (Shot a).
Proof. by constructor. Qed.

Ralf Jung's avatar
Ralf Jung committed
216
Lemma one_shot_validN_inv_l n y : {n} (OneShotPending  y)  y = .
217
Proof. by destruct y; inversion_clear 1. Qed.
Ralf Jung's avatar
Ralf Jung committed
218
219
220
Lemma one_shot_valid_inv_l y :  (OneShotPending  y)  y = .
Proof. intros. by apply one_shot_validN_inv_l with 0, cmra_valid_validN. Qed.
Lemma one_shot_bot_largest y : y  OneShotBot.
221
Proof. destruct y; exists OneShotBot; constructor. Qed.
Ralf Jung's avatar
Ralf Jung committed
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253

(** Internalized properties *)
Lemma one_shot_equivI {M} (x y : one_shot A) :
  (x  y)  (match x, y with
               | OneShotPending, OneShotPending => True
               | Shot a, Shot b => a  b
               | OneShotUnit, OneShotUnit => True
               | OneShotBot, OneShotBot => True
               | _, _ => False
               end : uPred M).
Proof.
  uPred.unseal; do 2 split; first by destruct 1.
  by destruct x, y; try destruct 1; try constructor.
Qed.
Lemma one_shot_validI {M} (x : one_shot A) :
  ( x)  (match x with
            | Shot a =>  a 
            | OneShotBot => False
            | _ => True
            end : uPred M).
Proof. uPred.unseal. by destruct x. Qed.

(** Updates *)
Lemma one_shot_update_shoot (a : A) :  a  OneShotPending ~~> Shot a.
Proof.
  move=> ? n y /one_shot_validN_inv_l ->. by apply cmra_valid_validN.
Qed.
Lemma one_shot_update (a1 a2 : A) : a1 ~~> a2  Shot a1 ~~> Shot a2.
Proof.
  intros Ha n [|b| |] ?; simpl; auto.
  apply cmra_validN_op_l with (core a1), Ha. by rewrite cmra_core_r.
Qed.
Ralf Jung's avatar
Ralf Jung committed
254
255
256
257
258
259
260
Lemma one_shot_updateP (P : A  Prop) (Q : one_shot A  Prop) a :
  a ~~>: P  ( b, P b  Q (Shot b))  Shot a ~~>: Q.
Proof.
  intros Hx HP n mf Hm. destruct mf as [|b| |]; try by destruct Hm.
  - destruct (Hx n b) as (c&?&?); try done.
    exists (Shot c). auto.
  - destruct (Hx n (core a)) as (c&?&?); try done.
261
262
    { by rewrite cmra_core_r. }
    exists (Shot c). split; simpl; eauto using cmra_validN_op_l.
Ralf Jung's avatar
Ralf Jung committed
263
264
265
266
Qed.
Lemma one_shot_updateP' (P : A  Prop) a :
  a ~~>: P  Shot a ~~>: λ m',  b, m' = Shot b  P b.
Proof. eauto using one_shot_updateP. Qed.
Ralf Jung's avatar
Ralf Jung committed
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306

End cmra.

Arguments one_shotR : clear implicits.

(* Functor *)
Instance one_shot_map_cmra_monotone {A B : cmraT} (f : A  B) :
  CMRAMonotone f  CMRAMonotone (one_shot_map f).
Proof.
  split; try apply _.
  - intros n [|a| |]; simpl; auto using validN_preserving.
  - intros [|a1| |] [|a2| |] [[|a3| |] Hx];
      inversion Hx; setoid_subst; try apply cmra_unit_least;
        try apply one_shot_bot_largest; auto; [].
    destruct (included_preserving f a1 (a1  a3)) as [b ?].
    { by apply cmra_included_l. }
    by exists (Shot b); constructor.
Qed.

Program Definition one_shotRF (F : rFunctor) : rFunctor := {|
  rFunctor_car A B := one_shotR (rFunctor_car F A B);
  rFunctor_map A1 A2 B1 B2 fg := one_shotC_map (rFunctor_map F fg)
|}.
Next Obligation.
  by intros F A1 A2 B1 B2 n f g Hfg; apply one_shotC_map_ne, rFunctor_ne.
Qed.
Next Obligation.
  intros F A B x. rewrite /= -{2}(one_shot_map_id x).
  apply one_shot_map_ext=>y; apply rFunctor_id.
Qed.
Next Obligation.
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -one_shot_map_compose.
  apply one_shot_map_ext=>y; apply rFunctor_compose.
Qed.

Instance one_shotRF_contractive F :
  rFunctorContractive F  rFunctorContractive (one_shotRF F).
Proof.
  by intros ? A1 A2 B1 B2 n f g Hfg; apply one_shotC_map_ne, rFunctor_contractive.
Qed.