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

Ralf Jung's avatar
Ralf Jung committed
10
(* TODO: Really, we should have sums, and then this should be just "excl unit + A". *)
Robbert Krebbers's avatar
Robbert Krebbers committed
11
12
13
14
15
16
17
18
Inductive one_shot (A : Type) :=
  | OneShotPending : one_shot A
  | Shot : A  one_shot A
  | OneShotBot : one_shot A.
Arguments OneShotPending {_}.
Arguments Shot {_} _.
Arguments OneShotBot {_}.

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
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
  | 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
  | 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.

49
Program Definition one_shot_chain (c : chain (one_shot A)) (a : A) : chain A :=
50
  {| chain_car n := match c n return _ with Shot b => b | _ => a end |}.
51
Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
52
Instance one_shot_compl : Compl (one_shot A) := λ c,
53
  match c 0 with Shot a => Shot (compl (one_shot_chain c a)) | x => x end.
54
55
56
57
58
59
60
61
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
    + by intros [|a|]; constructor.
63
64
65
    + by destruct 1; constructor.
    + destruct 1; inversion_clear 1; constructor; etrans; eauto.
  - by inversion_clear 1; constructor; done || apply dist_S.
66
67
68
  - intros n c; rewrite /compl /one_shot_compl.
    feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
    rewrite (conv_compl n (one_shot_chain c _)) /=. destruct (c n); naive_solver.
69
Qed.
70
Canonical Structure one_shotC : cofeT := CofeT (one_shot A) one_shot_cofe_mixin.
71
72
73
74
75
76
77
78
79
80
81
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.
End cofe.

Arguments one_shotC : clear implicits.

Ralf Jung's avatar
Ralf Jung committed
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
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
(* 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)
  | 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
  | OneShotBot => False
  end.
Instance one_shot_validN : ValidN (one_shot A) := λ n x,
  match x with
  | OneShotPending => True
  | Shot a => {n} a
  | OneShotBot => False
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
125
Instance one_shot_pcore : PCore (one_shot A) := λ x,
Ralf Jung's avatar
Ralf Jung committed
126
  match x with
Robbert Krebbers's avatar
Robbert Krebbers committed
127
128
129
  | OneShotPending => None
  | Shot a => Shot <$> pcore a
  | OneShotBot => Some OneShotBot
Ralf Jung's avatar
Ralf Jung committed
130
131
132
133
134
135
136
137
138
  end.
Instance one_shot_op : Op (one_shot A) := λ x y,
  match x, y with
  | Shot a, Shot b => Shot (a  b)
  | _, _ => OneShotBot
  end.

Lemma Shot_op a b : Shot a  Shot b = Shot (a  b).
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
139

Robbert Krebbers's avatar
Robbert Krebbers committed
140
141
Lemma one_shot_included x y :
  x  y  y = OneShotBot   a b, x = Shot a  y = Shot b  a  b.
Ralf Jung's avatar
Ralf Jung committed
142
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
144
145
146
147
148
149
150
  split.
  - intros [z Hy]; destruct x as [|a|], z as [|b|]; inversion_clear Hy; auto.
    right; eexists _, _; split_and!; eauto.
    setoid_subst; eauto using cmra_included_l.
  - intros [->|(a&b&->&->&c&?)].
    + destruct x; exists OneShotBot; constructor.
    + exists (Shot c); by constructor.
Qed.
Ralf Jung's avatar
Ralf Jung committed
151

152
Lemma one_shot_cmra_mixin : CMRAMixin (one_shot A).
Ralf Jung's avatar
Ralf Jung committed
153
154
155
Proof.
  split.
  - intros n []; destruct 1; constructor; by cofe_subst. 
Robbert Krebbers's avatar
Robbert Krebbers committed
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
  - intros ???? [n|n a b Hab|n] [=]; subst; eauto.
    destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
    destruct (cmra_pcore_ne n a b ca) as (cb&->&?); auto.
    exists (Shot cb); by repeat constructor.
  - 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|] ? [=]; subst; auto.
    destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
    constructor; eauto using cmra_pcore_l.
  - intros [|a|] ? [=]; subst; auto.
    destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
    feed inversion (cmra_pcore_idemp a ca); repeat constructor; auto.
  - intros x y ? [->|(a&b&->&->&?)]%one_shot_included [=].
    { exists OneShotBot. rewrite one_shot_included; eauto. }
    destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
    destruct (cmra_pcore_preserving a b ca) as (cb&->&?); auto.
    exists (Shot cb). rewrite one_shot_included; eauto 10.
  - intros n [|a1|] [|a2|]; simpl; eauto using cmra_validN_op_l; done.
  - intros n [|a|] y1 y2 Hx Hx'.
    + destruct y1, y2; exfalso; by inversion_clear Hx'.
    + 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.
Ralf Jung's avatar
Ralf Jung committed
183
184
    + by exists (OneShotBot, OneShotBot); destruct y1, y2; inversion_clear Hx'.
Qed.
185
Canonical Structure one_shotR :=
186
  CMRAT (one_shot A) one_shot_cofe_mixin one_shot_cmra_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
187

Ralf Jung's avatar
Ralf Jung committed
188
189
190
Global Instance one_shot_cmra_discrete : CMRADiscrete A  CMRADiscrete one_shotR.
Proof.
  split; first apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
  intros [|a|]; simpl; auto using cmra_discrete_valid.
Ralf Jung's avatar
Ralf Jung committed
192
193
Qed.

194
Global Instance Shot_persistent a : Persistent a  Persistent (Shot a).
Robbert Krebbers's avatar
Robbert Krebbers committed
195
Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed.
Ralf Jung's avatar
Ralf Jung committed
196
197
198

(** Internalized properties *)
Lemma one_shot_equivI {M} (x y : one_shot A) :
199
200
201
202
203
204
  x  y  (match x, y with
            | OneShotPending, OneShotPending => True
            | Shot a, Shot b => a  b
            | OneShotBot, OneShotBot => True
            | _, _ => False
            end : uPred M).
Ralf Jung's avatar
Ralf Jung committed
205
206
207
208
209
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) :
210
211
212
213
214
   x  (match x with
          | Shot a =>  a 
          | OneShotBot => False
          | _ => True
          end : uPred M).
Ralf Jung's avatar
Ralf Jung committed
215
216
217
218
Proof. uPred.unseal. by destruct x. Qed.

(** Updates *)
Lemma one_shot_update_shoot (a : A) :  a  OneShotPending ~~> Shot a.
Robbert Krebbers's avatar
Robbert Krebbers committed
219
Proof. move=> ? n [y|] //= ?. by apply cmra_valid_validN. Qed.
Ralf Jung's avatar
Ralf Jung committed
220
221
Lemma one_shot_update (a1 a2 : A) : a1 ~~> a2  Shot a1 ~~> Shot a2.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
222
223
224
  intros Ha n [[|b|]|] ?; simpl in *; auto.
  - by apply (Ha n (Some b)).
  - by apply (Ha n None).
Ralf Jung's avatar
Ralf Jung committed
225
Qed.
Ralf Jung's avatar
Ralf Jung committed
226
227
228
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
229
230
231
  intros Hx HP n mf Hm. destruct mf as [[|b|]|]; try by destruct Hm.
  - destruct (Hx n (Some b)) as (c&?&?); naive_solver.
  - destruct (Hx n None) as (c&?&?); naive_solver eauto using cmra_validN_op_l.
Ralf Jung's avatar
Ralf Jung committed
232
233
234
235
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
236
237
238
239
240
241
242
243
244
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 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
245
246
247
  - intros n [|a|]; simpl; auto using validN_preserving.
  - intros x y; rewrite !one_shot_included.
    intros [->|(a&b&->&->&?)]; simpl; eauto 10 using included_preserving.
Ralf Jung's avatar
Ralf Jung committed
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
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.