atomic.v 19 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
  Global Instance aupd_laterable Eo Ei α β Φ :
    Laterable (atomic_update Eo Ei α β Φ).
264 265 266 267 268 269 270
  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.

271
  Lemma aupd_intro P Q α β Eo Ei Φ :
272
    Affine P  Persistent P  Laterable Q 
273 274
    (P  Q - atomic_acc Eo Ei α Q β Φ) 
    P  Q - atomic_update Eo Ei α β Φ.
275 276
  Proof.
    rewrite atomic_update_eq {1}/atomic_update_def /=.
277
    iIntros (??? HAU) "[#HP HQ]".
278 279
    iApply (greatest_fixpoint_coind _ (λ _, Q)); last done. iIntros "!#" ([]) "HQ".
    iDestruct (laterable with "HQ") as (Q') "[HQ' #HQi]". iExists Q'. iFrame.
280 281
    iIntros "!# HQ'". iDestruct ("HQi" with "HQ'") as ">HQ {HQi}".
    iApply HAU. by iFrame.
282
  Qed.
283

284 285 286 287
  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.
288
  Proof.
289
    iIntros (? x) "Hα Hclose".
290 291 292 293 294 295
    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.

Ralf Jung's avatar
Ralf Jung committed
296
  Global Instance elim_acc_aacc {X} E1 E2 Ei (α' β' : X  PROP) γ' α β Pas Φ :
297
    ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α' β' γ'
Ralf Jung's avatar
Ralf Jung committed
298
            (atomic_acc E1 Ei α Pas β Φ)
299
            (λ x', atomic_acc E2 Ei α (β' x'  (γ' x' -? Pas))%I β
300 301
                (λ.. x y, β' x'  (γ' x' -? Φ x y))
            )%I.
302 303 304 305 306 307 308 309 310 311 312 313 314 315
  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 "_".
316 317
      iMod ("Hclose'" with "Hβ") as "Hβ'".
      rewrite ->!tele_app_bind. iDestruct "Hβ'" as "[Hβ' HΦ]".
318 319 320 321
      iMod ("Hclose" with "Hβ'") as "Hγ'".
      iModIntro. destruct (γ' x'); iApply "HΦ"; done.
  Qed.

322
  Lemma aacc_aacc {TA' TB' : tele} E1 E1' E2 E3
323
        α P β Φ
324 325 326 327 328 329
        (α' : 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
330
    atomic_acc E1 E3 α' P' β' Φ'.
331
  Proof.
332 333
    iIntros (?) "Hupd Hstep".
    iMod (atomic_acc_mask_weaken with "Hupd") as (x) "[Hα Hclose]"; first done.
334 335 336 337 338 339 340
    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']".
341 342
      iMod ("Hclose'" with "Hβ'") as "Hres".
      rewrite ->!tele_app_bind. iDestruct "Hres" as "[[Hα HΦ']|Hcont]".
343 344 345 346 347 348 349 350 351 352 353
      + (* 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.

354
  Lemma aacc_aupd {TA' TB' : tele} E1 E1' E2 E3
355
        α β Φ
356 357 358 359 360 361 362
        (α' : 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' β' Φ'.
363
  Proof.
364 365
    iIntros (?) "Hupd Hstep". iApply (aacc_aacc with "[Hupd] Hstep"); first done.
    iApply aupd_aacc; done.
366 367
  Qed.

368
  Lemma aacc_aupd_commit {TA' TB' : tele} E1 E1' E2 E3
369
        α β Φ
370 371 372 373 374 375
        (α' : 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' β' Φ'.
376
  Proof.
Ralf Jung's avatar
Ralf Jung committed
377 378
    iIntros (?) "Hupd Hstep". iApply (aacc_aupd with "Hupd"); first done.
    iIntros (x) "Hα". iApply atomic_acc_wand; last first.
379
    { iApply "Hstep". done. }
380
    iSplit; first by eauto. iIntros (??) "?". rewrite ->!tele_app_bind. by iRight.
381 382
  Qed.

383
  Lemma aacc_aupd_abort {TA' TB' : tele} E1 E1' E2 E3
384
        α β Φ
385 386 387 388 389 390
        (α' : 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' β' Φ'.
391
  Proof.
Ralf Jung's avatar
Ralf Jung committed
392 393
    iIntros (?) "Hupd Hstep". iApply (aacc_aupd with "Hupd"); first done.
    iIntros (x) "Hα". iApply atomic_acc_wand; last first.
394
    { iApply "Hstep". done. }
395
    iSplit; first by eauto. iIntros (??) "?". rewrite ->!tele_app_bind. by iLeft.
396 397
  Qed.

398
End lemmas.
399 400 401

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

405
  Lemma tac_aupd_intro Γp Γs n α β Eo Ei Φ P :
406 407 408
    Timeless (PROP:=PROP) emp 
    TCForall Laterable (env_to_list Γs) 
    P = prop_of_env Γs 
409 410
    envs_entails (Envs Γp Γs n) (atomic_acc Eo Ei α P β Φ) 
    envs_entails (Envs Γp Γs n) (atomic_update Eo Ei α β Φ).
411
  Proof.
Ralf Jung's avatar
Ralf Jung committed
412
    intros ? HΓs ->. rewrite envs_entails_eq of_envs_eq' /atomic_acc /=.
413
    setoid_rewrite prop_of_env_sound =>HAU.
414
    apply aupd_intro; [apply _..|]. done.
Ralf Jung's avatar
Ralf Jung committed
415
  Qed.
416 417 418 419 420 421
End proof_mode.

(** Now the coq-level tactics *)

Tactic Notation "iAuIntro" :=
  iStartProof; eapply tac_aupd_intro; [
422 423
    iSolveTC || fail "iAuIntro: emp is not timeless"
  | iSolveTC || fail "iAuIntro: not all spatial assumptions are laterable"
424
  | (* P = ...: make the P pretty *) pm_reflexivity
425
  | (* the new proof mode goal *) ].