atomic.v 20.6 KB
Newer Older
1
2
From iris.bi Require Export bi updates laterable.
From iris.bi.lib Require Import fixpoint.
3
From stdpp Require Import coPset namespaces.
4
From iris.proofmode Require Import coq_tactics tactics reduction.
5
6
Set Default Proof Using "Type".

7
8
9
10
(** Conveniently split a conjunction on both assumption and conclusion. *)
Local Tactic Notation "iSplitWith" constr(H) :=
  iApply (bi.and_parallel with H); iSplit; iIntros H.

11
Section definition.
12
  Context `{BiFUpd PROP} {TA TB : tele}.
13
  Implicit Types
14
15
    (Eo Ei : coPset) (* outer/inner masks *)
    (α : TA  PROP) (* atomic pre-condition *)
16
    (P : PROP) (* abortion condition *)
17
18
    (β : TA  TB  PROP) (* atomic post-condition *)
    (Φ : TA  TB  PROP) (* post-condition *)
19
  .
20

Ralf Jung's avatar
Ralf Jung committed
21
22
23
  (** atomic_acc as the "introduction form" of atomic updates: An accessor
      that can be aborted back to [P]. *)
  Definition atomic_acc Eo Ei α P β Φ : PROP :=
24
25
    (|={Eo, Ei}=> .. x, α x 
          ((α x ={Ei, Eo}= P)  (.. y, β x y ={Ei, Eo}= Φ x y))
26
27
    )%I.

Ralf Jung's avatar
Ralf Jung committed
28
  Lemma atomic_acc_wand Eo Ei α P1 P2 β Φ1 Φ2 :
29
    ((P1 - P2)  (.. x y, Φ1 x y - Φ2 x y)) -
Ralf Jung's avatar
Ralf Jung committed
30
    (atomic_acc Eo Ei α P1 β Φ1 - atomic_acc Eo Ei α P2 β Φ2).
31
  Proof.
32
    iIntros "HP12 AS". iMod "AS" as (x) "[Hα Hclose]".
33
34
35
36
    iModIntro. iExists x. iFrame "Hα". iSplit.
    - iIntros "Hα". iDestruct "Hclose" as "[Hclose _]".
      iApply "HP12". iApply "Hclose". done.
    - iIntros (y) "Hβ". iDestruct "Hclose" as "[_ Hclose]".
37
      iApply "HP12". iApply "Hclose". done.
38
39
  Qed.

40
41
  Lemma atomic_acc_mask Eo Ed α P β Φ :
    atomic_acc Eo (EoEd) α P β Φ   E, Eo  E  atomic_acc E (EEd) α P β Φ.
42
43
44
45
46
47
48
49
50
51
52
53
  Proof.
    iSplit; last first.
    { iIntros "Hstep". iApply ("Hstep" with "[% //]"). }
    iIntros "Hstep" (E HE).
    iApply (fupd_mask_frame_acc with "Hstep"); first done.
    iIntros "Hstep". iDestruct "Hstep" as (x) "[Hα Hclose]".
    iIntros "!> Hclose'".
    iExists x. iFrame. iSplitWith "Hclose".
    - iIntros "Hα". iApply "Hclose'". iApply "Hclose". done.
    - iIntros (y) "Hβ". iApply "Hclose'". iApply "Hclose". done.
  Qed.

54
55
56
57
58
59
60
61
62
63
64
65
  Lemma atomic_acc_mask_weaken Eo1 Eo2 Ei α P β Φ :
    Eo1  Eo2 
    atomic_acc Eo1 Ei α P β Φ - atomic_acc Eo2 Ei α P β Φ.
  Proof.
    iIntros (HE) "Hstep".
    iMod fupd_intro_mask' as "Hclose1"; first done.
    iMod "Hstep" as (x) "[Hα Hclose2]". iIntros "!>". iExists x.
    iFrame. iSplitWith "Hclose2".
    - iIntros "Hα". iMod ("Hclose2" with "Hα") as "$". done.
    - iIntros (y) "Hβ". iMod ("Hclose2" with "Hβ") as "$". done.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
66
  (** atomic_update as a fixed-point of the equation
67
   AU = ∃ P. ▷ P ∗ □ (▷ P ==∗ α ∗ (α ==∗ AU) ∧ (β ==∗ Q))
Ralf Jung's avatar
Ralf Jung committed
68
69
      = ∃ P. ▷ P ∗ □ (▷ P -∗ atomic_acc α AU β Q)
  *)
70
  Context Eo Ei α β Φ.
71

72
  Definition atomic_update_pre (Ψ : ()  PROP) (_ : ()) : PROP :=
73
    ( (P : PROP),  P 
74
      ( P - atomic_acc Eo Ei α (Ψ ()) β Φ))%I.
75
76
77
78
79

  Local Instance atomic_update_pre_mono : BiMonoPred atomic_update_pre.
  Proof.
    constructor.
    - iIntros (P1 P2) "#HP12". iIntros ([]) "AU".
80
      iDestruct "AU" as (P) "[HP #AS]". iExists P. iFrame.
Ralf Jung's avatar
Ralf Jung committed
81
      iIntros "!# HP". iApply (atomic_acc_wand with "[HP12]"); last by iApply "AS".
82
      iSplit; last by eauto. iApply "HP12".
83
84
85
86
87
    - intros ??. solve_proper.
  Qed.

  Definition atomic_update_def :=
    bi_greatest_fixpoint atomic_update_pre ().
88

89
90
91
92
End definition.

(** Seal it *)
Definition atomic_update_aux : seal (@atomic_update_def). by eexists. Qed.
93
Definition atomic_update `{BiFUpd PROP} {TA TB : tele} := atomic_update_aux.(unseal) PROP _ TA TB.
94
95
96
Definition atomic_update_eq :
  @atomic_update = @atomic_update_def := atomic_update_aux.(seal_eq).

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
161
162
163
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
213
214
215
216
217
218
219
220
221
222
223
Arguments atomic_acc {PROP _ TA TB} Eo Ei _ _ _ _ : simpl never.
Arguments atomic_update {PROP _ TA TB} Eo Ei _ _ _ : simpl never.

(** Notation: Atomic updates *)
Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
  (atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
                 (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
                 Eo Ei
                 (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                       λ x1, .. (λ xn, α%I) ..)
                 (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                       λ x1, .. (λ xn,
                         tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
                         (λ y1, .. (λ yn, β%I) .. )
                        ) .. )
                 (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                       λ x1, .. (λ xn,
                         tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
                         (λ y1, .. (λ yn, Φ%I) .. )
                        ) .. )
  )
  (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
   format "'[   ' 'AU'  '<<'  ∀  x1  ..  xn ,  α  '>>'  '/' @  Eo ,  Ei  '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.

Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
  (atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
                 (TB:=TeleO)
                 Eo Ei
                 (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                       λ x1, .. (λ xn, α%I) ..)
                 (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                       λ x1, .. (λ xn, tele_app (TT:=TeleO) β%I) .. )
                 (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                       λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ%I) .. )
  )
  (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder,
   format "'[   ' 'AU'  '<<'  ∀  x1  ..  xn ,  α  '>>'  '/' @  Eo ,  Ei  '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.

Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
  (atomic_update (TA:=TeleO)
                 (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
                 Eo Ei
                 (tele_app (TT:=TeleO) α%I)
                 (tele_app (TT:=TeleO) $
                       tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
                                (λ y1, .. (λ yn, β%I) ..))
                 (tele_app (TT:=TeleO) $
                       tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
                                (λ y1, .. (λ yn, Φ%I) ..))
  )
  (at level 20, Eo, Ei, α, β, Φ at level 200, y1 binder, yn binder,
   format "'[   ' 'AU'  '<<'  α  '>>'  '/' @  Eo ,  Ei  '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.

Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
  (atomic_update (TA:=TeleO) (TB:=TeleO) Eo Ei
                 (tele_app (TT:=TeleO) α%I)
                 (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) β%I)
                 (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) Φ%I)
  )
  (at level 20, Eo, Ei, α, β, Φ at level 200,
   format "'[   ' 'AU'  '<<'  α  '>>'  '/' @  Eo ,  Ei  '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.

(** Notation: Atomic accessors *)
Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
  (atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
              (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
              Eo Ei
              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                    λ x1, .. (λ xn, α%I) ..)
              P%I
              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                    λ x1, .. (λ xn,
                      tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
                      (λ y1, .. (λ yn, β%I) .. )
                     ) .. )
              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                    λ x1, .. (λ xn,
                      tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
                      (λ y1, .. (λ yn, Φ%I) .. )
                     ) .. )
  )
  (at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
   format "'[     ' 'AACC'  '[   ' '<<'  ∀  x1  ..  xn ,  α  '/' ABORT  P  '>>'  ']' '/' @  Eo ,  Ei  '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.

Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
  (atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
              (TB:=TeleO)
              Eo Ei
              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                        λ x1, .. (λ xn, α%I) ..)
              P%I
              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                        λ x1, .. (λ xn, tele_app (TT:=TeleO) β%I) .. )
              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                        λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ%I) .. )
  )
  (at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder,
   format "'[     ' 'AACC'  '[   ' '<<'  ∀  x1  ..  xn ,  α  '/' ABORT  P  '>>'  ']' '/' @  Eo ,  Ei  '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.

Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
  (atomic_acc (TA:=TeleO)
              (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
              Eo Ei
              (tele_app (TT:=TeleO) α%I)
              P%I
              (tele_app (TT:=TeleO) $
                        tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
                        (λ y1, .. (λ yn, β%I) ..))
              (tele_app (TT:=TeleO) $
                        tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
                        (λ y1, .. (λ yn, Φ%I) ..))
  )
  (at level 20, Eo, Ei, α, P, β, Φ at level 200, y1 binder, yn binder,
   format "'[     ' 'AACC'  '[   ' '<<'  α  '/' ABORT  P  '>>'  ']' '/' @  Eo ,  Ei  '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.

Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
  (atomic_acc (TA:=TeleO)
              (TB:=TeleO)
              Eo Ei
              (tele_app (TT:=TeleO) α%I)
              P%I
                 (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) β%I)
                 (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) Φ%I)
  )
  (at level 20, Eo, Ei, α, P, β, Φ at level 200,
   format "'[     ' 'AACC'  '[   ' '<<'  α  '/' ABORT  P  '>>'  ']' '/' @  Eo ,  Ei  '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.

224
(** Lemmas about AU *)
225
Section lemmas.
226
227
  Context `{BiFUpd PROP} {TA TB : tele}.
  Implicit Types (α : TA  PROP) (β Φ : TA  TB  PROP) (P : PROP).
228
229

  Local Existing Instance atomic_update_pre_mono.
230

231
  Global Instance atomic_acc_ne Eo Ei n :
232
    Proper (
233
        pointwise_relation TA (dist n) ==>
234
        dist n ==>
235
236
        pointwise_relation TA (pointwise_relation TB (dist n)) ==>
        pointwise_relation TA (pointwise_relation TB (dist n)) ==>
237
        dist n
238
    ) (atomic_acc (PROP:=PROP) Eo Ei).
239
240
  Proof. solve_proper. Qed.

241
  Global Instance atomic_update_ne Eo Ei n :
242
    Proper (
243
244
245
        pointwise_relation TA (dist n) ==>
        pointwise_relation TA (pointwise_relation TB (dist n)) ==>
        pointwise_relation TA (pointwise_relation TB (dist n)) ==>
246
        dist n
247
    ) (atomic_update (PROP:=PROP) Eo Ei).
248
249
250
251
  Proof.
    rewrite atomic_update_eq /atomic_update_def /atomic_update_pre. solve_proper.
  Qed.

252
253
254
255
  (** The ellimination form: an atomic accessor *)
  Lemma aupd_aacc  Eo Ei α β Φ :
    atomic_update Eo Ei α β Φ -
    atomic_acc Eo Ei α (atomic_update Eo Ei α β Φ) β Φ.
256
  Proof using Type*.
257
    rewrite atomic_update_eq {1}/atomic_update_def /=. iIntros "HUpd".
258
    iPoseProof (greatest_fixpoint_unfold_1 with "HUpd") as "HUpd".
259
    iDestruct "HUpd" as (P) "(HP & Hshift)". by iApply "Hshift".
260
261
  Qed.

262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
  (* This lets you eliminate atomic updates with iMod. *)
  Global Instance elim_mod_aupd φ Eo Ei E α β Φ Q Q' :
    ( R, ElimModal φ false false (|={E,Ei}=> R) R Q Q') 
    ElimModal (φ  Eo  E) false false
              (atomic_update Eo Ei α β Φ)
              (.. x, α x 
                       (α x ={Ei,E}= atomic_update Eo Ei α β Φ) 
                       (.. y, β x y ={Ei,E}= Φ x y))
              Q Q'.
  Proof.
    intros ?. rewrite /ElimModal /= =>-[??]. iIntros "[AU Hcont]".
    iPoseProof (aupd_aacc with "AU") as "AC".
    iMod (atomic_acc_mask_weaken with "AC"); first done.
    iApply "Hcont". done.
  Qed.

278
279
  Global Instance aupd_laterable Eo Ei α β Φ :
    Laterable (atomic_update Eo Ei α β Φ).
280
281
282
283
284
285
286
  Proof.
    rewrite /Laterable atomic_update_eq {1}/atomic_update_def /=. iIntros "AU".
    iPoseProof (greatest_fixpoint_unfold_1 with "AU") as (P) "[HP #AS]".
    iExists P. iFrame. iIntros "!# HP !>".
    iApply greatest_fixpoint_unfold_2. iExists P. iFrame "#∗".
  Qed.

287
  Lemma aupd_intro P Q α β Eo Ei Φ :
288
    Affine P  Persistent P  Laterable Q 
289
290
    (P  Q - atomic_acc Eo Ei α Q β Φ) 
    P  Q - atomic_update Eo Ei α β Φ.
291
292
  Proof.
    rewrite atomic_update_eq {1}/atomic_update_def /=.
293
    iIntros (??? HAU) "[#HP HQ]".
294
295
    iApply (greatest_fixpoint_coind _ (λ _, Q)); last done. iIntros "!#" ([]) "HQ".
    iDestruct (laterable with "HQ") as (Q') "[HQ' #HQi]". iExists Q'. iFrame.
296
297
    iIntros "!# HQ'". iDestruct ("HQi" with "HQ'") as ">HQ {HQi}".
    iApply HAU. by iFrame.
298
  Qed.
299

300
301
302
303
  Lemma aacc_intro Eo Ei α P β Φ :
    Ei  Eo  (.. x, α x -
    ((α x ={Eo}= P)  (.. y, β x y ={Eo}= Φ x y)) -
    atomic_acc Eo Ei α P β Φ)%I.
304
  Proof.
305
    iIntros (? x) "Hα Hclose".
306
307
308
309
310
311
    iMod fupd_intro_mask' as "Hclose'"; last iModIntro; first set_solver.
    iExists x. iFrame. iSplitWith "Hclose".
    - iIntros "Hα". iMod "Hclose'" as "_". iApply "Hclose". done.
    - iIntros (y) "Hβ". iMod "Hclose'" as "_". iApply "Hclose". done.
  Qed.

312
  (* This lets you open invariants etc. when the goal is an atomic accessor. *)
Ralf Jung's avatar
Ralf Jung committed
313
  Global Instance elim_acc_aacc {X} E1 E2 Ei (α' β' : X  PROP) γ' α β Pas Φ :
314
    ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α' β' γ'
Ralf Jung's avatar
Ralf Jung committed
315
            (atomic_acc E1 Ei α Pas β Φ)
316
            (λ x', atomic_acc E2 Ei α (β' x'  (γ' x' -? Pas))%I β
317
318
                (λ.. x y, β' x'  (γ' x' -? Φ x y))
            )%I.
319
320
321
322
323
324
325
326
327
328
329
330
331
332
  Proof.
    rewrite /ElimAcc.
    (* FIXME: Is there any way to prevent maybe_wand from unfolding?
       It gets unfolded by env_cbv in the proofmode, ideally we'd like that
       to happen only if one argument is a constructor. *)
    iIntros "Hinner >Hacc". iDestruct "Hacc" as (x') "[Hα' Hclose]".
    iMod ("Hinner" with "Hα'") as (x) "[Hα Hclose']".
    iMod (fupd_intro_mask') as "Hclose''"; last iModIntro; first done.
    iExists x. iFrame. iSplitWith "Hclose'".
    - iIntros "Hα". iMod "Hclose''" as "_".
      iMod ("Hclose'" with "Hα") as "[Hβ' HPas]".
      iMod ("Hclose" with "Hβ'") as "Hγ'".
      iModIntro. destruct (γ' x'); iApply "HPas"; done.
    - iIntros (y) "Hβ". iMod "Hclose''" as "_".
333
334
      iMod ("Hclose'" with "Hβ") as "Hβ'".
      rewrite ->!tele_app_bind. iDestruct "Hβ'" as "[Hβ' HΦ]".
335
336
337
338
      iMod ("Hclose" with "Hβ'") as "Hγ'".
      iModIntro. destruct (γ' x'); iApply "HΦ"; done.
  Qed.

339
340
341
342
343
344
345
346
347
348
  (* Everything that fancy updates can eliminate without changing, atomic
  accessors can eliminate as well.  This is a forwarding instance needed becuase
  atomic_acc is becoming opaque. *)
  Global Instance elim_modal_acc p q φ P P' Eo Ei α Pas β Φ :
    ( Q, ElimModal φ p q P P' (|={Eo,Ei}=> Q) (|={Eo,Ei}=> Q)) 
    ElimModal φ p q P P'
              (atomic_acc Eo Ei α Pas β Φ)
              (atomic_acc Eo Ei α Pas β Φ).
  Proof. intros Helim. apply Helim. Qed.

349
  Lemma aacc_aacc {TA' TB' : tele} E1 E1' E2 E3
350
        α P β Φ
351
352
353
354
355
356
        (α' : TA'  PROP) P' (β' Φ' : TA'  TB'  PROP) :
    E1'  E1 
    atomic_acc E1' E2 α P β Φ -
    (.. x, α x - atomic_acc E2 E3 α' (α x  (P ={E1}= P')) β'
            (λ.. x' y', (α x  (P ={E1}= Φ' x' y'))
                     .. y, β x y  (Φ x y ={E1}= Φ' x' y'))) -
Ralf Jung's avatar
Ralf Jung committed
357
    atomic_acc E1 E3 α' P' β' Φ'.
358
  Proof.
359
360
    iIntros (?) "Hupd Hstep".
    iMod (atomic_acc_mask_weaken with "Hupd") as (x) "[Hα Hclose]"; first done.
361
362
363
364
365
366
367
    iMod ("Hstep" with "Hα") as (x') "[Hα' Hclose']".
    iModIntro. iExists x'. iFrame "Hα'". iSplit.
    - iIntros "Hα'". iDestruct "Hclose'" as "[Hclose' _]".
      iMod ("Hclose'" with "Hα'") as "[Hα Hupd]".
      iDestruct "Hclose" as "[Hclose _]".
      iMod ("Hclose" with "Hα"). iApply "Hupd". auto.
    - iIntros (y') "Hβ'". iDestruct "Hclose'" as "[_ Hclose']".
368
369
      iMod ("Hclose'" with "Hβ'") as "Hres".
      rewrite ->!tele_app_bind. iDestruct "Hres" as "[[Hα HΦ']|Hcont]".
370
371
372
373
374
375
376
377
378
379
380
      + (* Abort the step we are eliminating *)
        iDestruct "Hclose" as "[Hclose _]".
        iMod ("Hclose" with "Hα") as "HP".
        iApply "HΦ'". done.
      + (* Complete the step we are eliminating *)
        iDestruct "Hclose" as "[_ Hclose]".
        iDestruct "Hcont" as (y) "[Hβ HΦ']".
        iMod ("Hclose" with "Hβ") as "HΦ".
        iApply "HΦ'". done.
  Qed.

381
  Lemma aacc_aupd {TA' TB' : tele} E1 E1' E2 E3
382
        α β Φ
383
384
385
386
387
388
389
        (α' : TA'  PROP) P' (β' Φ' : TA'  TB'  PROP) :
    E1'  E1 
    atomic_update E1' E2 α β Φ -
    (.. x, α x - atomic_acc E2 E3 α' (α x  (atomic_update E1' E2 α β Φ ={E1}= P')) β'
            (λ.. x' y', (α x  (atomic_update E1' E2 α β Φ ={E1}= Φ' x' y'))
                     .. y, β x y  (Φ x y ={E1}= Φ' x' y'))) -
    atomic_acc E1 E3 α' P' β' Φ'.
390
  Proof.
391
392
    iIntros (?) "Hupd Hstep". iApply (aacc_aacc with "[Hupd] Hstep"); first done.
    iApply aupd_aacc; done.
393
394
  Qed.

395
  Lemma aacc_aupd_commit {TA' TB' : tele} E1 E1' E2 E3
396
        α β Φ
397
398
399
400
401
402
        (α' : TA'  PROP) P' (β' Φ' : TA'  TB'  PROP) :
    E1'  E1 
    atomic_update E1' E2 α β Φ -
    (.. x, α x - atomic_acc E2 E3 α' (α x  (atomic_update E1' E2 α β Φ ={E1}= P')) β'
            (λ.. x' y', .. y, β x y  (Φ x y ={E1}= Φ' x' y'))) -
    atomic_acc E1 E3 α' P' β' Φ'.
403
  Proof.
Ralf Jung's avatar
Ralf Jung committed
404
405
    iIntros (?) "Hupd Hstep". iApply (aacc_aupd with "Hupd"); first done.
    iIntros (x) "Hα". iApply atomic_acc_wand; last first.
406
    { iApply "Hstep". done. }
407
    iSplit; first by eauto. iIntros (??) "?". rewrite ->!tele_app_bind. by iRight.
408
409
  Qed.

410
  Lemma aacc_aupd_abort {TA' TB' : tele} E1 E1' E2 E3
411
        α β Φ
412
413
414
415
416
417
        (α' : TA'  PROP) P' (β' Φ' : TA'  TB'  PROP) :
    E1'  E1 
    atomic_update E1' E2 α β Φ -
    (.. x, α x - atomic_acc E2 E3 α' (α x  (atomic_update E1' E2 α β Φ ={E1}= P')) β'
            (λ.. x' y', α x  (atomic_update E1' E2 α β Φ ={E1}= Φ' x' y'))) -
    atomic_acc E1 E3 α' P' β' Φ'.
418
  Proof.
Ralf Jung's avatar
Ralf Jung committed
419
420
    iIntros (?) "Hupd Hstep". iApply (aacc_aupd with "Hupd"); first done.
    iIntros (x) "Hα". iApply atomic_acc_wand; last first.
421
    { iApply "Hstep". done. }
422
    iSplit; first by eauto. iIntros (??) "?". rewrite ->!tele_app_bind. by iLeft.
423
424
  Qed.

425
End lemmas.
426
427
428

(** ProofMode support for atomic updates *)
Section proof_mode.
429
430
  Context `{BiFUpd PROP} {TA TB : tele}.
  Implicit Types (α : TA  PROP) (β Φ : TA  TB  PROP) (P : PROP).
431

432
  Lemma tac_aupd_intro Γp Γs n α β Eo Ei Φ P :
433
434
435
    Timeless (PROP:=PROP) emp 
    TCForall Laterable (env_to_list Γs) 
    P = prop_of_env Γs 
436
437
    envs_entails (Envs Γp Γs n) (atomic_acc Eo Ei α P β Φ) 
    envs_entails (Envs Γp Γs n) (atomic_update Eo Ei α β Φ).
438
  Proof.
Ralf Jung's avatar
Ralf Jung committed
439
    intros ? HΓs ->. rewrite envs_entails_eq of_envs_eq' /atomic_acc /=.
440
    setoid_rewrite prop_of_env_sound =>HAU.
441
    apply aupd_intro; [apply _..|]. done.
Ralf Jung's avatar
Ralf Jung committed
442
  Qed.
443
444
445
446
447
448
End proof_mode.

(** Now the coq-level tactics *)

Tactic Notation "iAuIntro" :=
  iStartProof; eapply tac_aupd_intro; [
449
450
    iSolveTC || fail "iAuIntro: emp is not timeless"
  | iSolveTC || fail "iAuIntro: not all spatial assumptions are laterable"
451
  | (* P = ...: make the P pretty *) pm_reflexivity
452
  | (* the new proof mode goal *) ].
453
454
455
456
457
458
459
Tactic Notation "iAaccIntro" "with" constr(sel) :=
  iStartProof; lazymatch goal with
  | |- environments.envs_entails _ (@atomic_acc ?PROP ?H ?TA ?TB ?Eo ?Ei ?α ?P ?β ?Φ) =>
    iApply (@aacc_intro PROP H TA TB Eo Ei α P β Φ with sel);
    first try solve_ndisj; last iSplit
  | _ => fail "iAAccIntro: Goal is not an atomic accessor"
  end.
460
461
462

(* From here on, prevent TC search from implicitly unfolding these. *)
Typeclasses Opaque atomic_acc atomic_update.