Library iris.bi.lib.atomic

From stdpp Require Import coPset namespaces.
From iris.bi Require Export bi updates laterable.
From iris.bi.lib Require Import fixpoint.
From iris.proofmode Require Import coq_tactics tactics reduction.
Set Default Proof Using "Type".

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

Section definition.
  Context `{BiFUpd PROP} {TA TB : tele}.
  Implicit Types
    (Eo Ei : coPset)
    (α : TA PROP)
    (P : PROP)
    (β : TA TB PROP)
    (Φ : TA TB PROP)
  .

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 :=
    (|={Eo, Ei}=> .. x, α x
          ((α x ={Ei, Eo}=∗ P) (.. y, β x y ={Ei, Eo}=∗ Φ x y))
    )%I.

  Lemma atomic_acc_wand Eo Ei α P1 P2 β Φ1 Φ2 :
    ((P1 -∗ P2) (.. x y, Φ1 x y -∗ Φ2 x y)) -∗
    (atomic_acc Eo Ei α P1 β Φ1 -∗ atomic_acc Eo Ei α P2 β Φ2).
  Proof.
    iIntros "HP12 AS". iMod "AS" as (x) "[Hα Hclose]".
    iModIntro. iExists x. iFrame "Hα". iSplit.
    - iIntros "Hα". iDestruct "Hclose" as "[Hclose _]".
      iApply "HP12". iApply "Hclose". done.
    - iIntros (y) "Hβ". iDestruct "Hclose" as "[_ Hclose]".
      iApply "HP12". iApply "Hclose". done.
  Qed.

  Lemma atomic_acc_mask Eo Ed α P β Φ :
    atomic_acc Eo (EoEd) α P β Φ ⊣⊢ E, Eo E atomic_acc E (EEd) α P β Φ.
  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.

  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.

atomic_update as a fixed-point of the equation AU = make_laterable
  Context Eo Ei α β Φ.

  Definition atomic_update_pre (Ψ : () PROP) (_ : ()) : PROP :=
    make_laterable $ atomic_acc Eo Ei α (Ψ ()) β Φ.

  Local Instance atomic_update_pre_mono : BiMonoPred atomic_update_pre.
  Proof.
    constructor.
    - iIntros (P1 P2) "#HP12". iIntros ([]) "AU".
      iApply (make_laterable_wand with "[] AU").
      iIntros "!> AA". iApply (atomic_acc_wand with "[HP12] AA").
      iSplit; last by eauto. iApply "HP12".
    - intros ??. solve_proper.
  Qed.

  Definition atomic_update_def :=
    bi_greatest_fixpoint atomic_update_pre ().

End definition.

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

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.

Lemmas about AU
Section lemmas.
  Context `{BiFUpd PROP} {TA TB : tele}.
  Implicit Types (α : TA PROP) (β Φ : TA TB PROP) (P : PROP).

  Local Existing Instance atomic_update_pre_mono.

  Global Instance atomic_acc_ne Eo Ei n :
    Proper (
        pointwise_relation TA (dist n) ==>
        dist n ==>
        pointwise_relation TA (pointwise_relation TB (dist n)) ==>
        pointwise_relation TA (pointwise_relation TB (dist n)) ==>
        dist n
    ) (atomic_acc (PROP:=PROP) Eo Ei).
  Proof. solve_proper. Qed.

  Global Instance atomic_update_ne Eo Ei n :
    Proper (
        pointwise_relation TA (dist n) ==>
        pointwise_relation TA (pointwise_relation TB (dist n)) ==>
        pointwise_relation TA (pointwise_relation TB (dist n)) ==>
        dist n
    ) (atomic_update (PROP:=PROP) Eo Ei).
  Proof.
    rewrite atomic_update_eq /atomic_update_def /atomic_update_pre. solve_proper.
  Qed.

  Lemma atomic_update_mask_weaken Eo1 Eo2 Ei α β Φ :
    Eo1 Eo2
    atomic_update Eo1 Ei α β Φ -∗ atomic_update Eo2 Ei α β Φ.
  Proof.
    rewrite atomic_update_eq {2}/atomic_update_def /=.
    iIntros (Heo) "HAU".
    iApply (greatest_fixpoint_coind _ (λ _, atomic_update_def Eo1 Ei α β Φ)); last done.
    iIntros "!> *". rewrite {1}/atomic_update_def /= greatest_fixpoint_unfold.
    iApply make_laterable_wand. iIntros "!>".
    iApply atomic_acc_mask_weaken. done.
  Qed.

The ellimination form: an atomic accessor
  Lemma aupd_aacc Eo Ei α β Φ :
    atomic_update Eo Ei α β Φ -∗
    atomic_acc Eo Ei α (atomic_update Eo Ei α β Φ) β Φ.
  Proof using Type×.
    rewrite atomic_update_eq {1}/atomic_update_def /=. iIntros "HUpd".
    iPoseProof (greatest_fixpoint_unfold_1 with "HUpd") as "HUpd".
    iApply make_laterable_elim. done.
  Qed.

  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.

  Global Instance aupd_laterable Eo Ei α β Φ :
    Laterable (atomic_update Eo Ei α β Φ).
  Proof.
    rewrite atomic_update_eq {1}/atomic_update_def greatest_fixpoint_unfold.
    apply _.
  Qed.

  Lemma aupd_intro P Q α β Eo Ei Φ :
    Affine P Persistent P Laterable Q
    (P Q -∗ atomic_acc Eo Ei α Q β Φ)
    P Q -∗ atomic_update Eo Ei α β Φ.
  Proof.
    rewrite atomic_update_eq {1}/atomic_update_def /=.
    iIntros (??? HAU) "[#HP HQ]".
    iApply (greatest_fixpoint_coind _ (λ _, Q)); last done. iIntros "!>" ([]) "HQ".
    iApply (make_laterable_intro Q with "[] HQ"). iIntros "!> >HQ".
    iApply HAU. by iFrame.
  Qed.

  Lemma aacc_intro Eo Ei α P β Φ :
    Ei Eo (.. x, α x -∗
    ((α x ={Eo}=∗ P) (.. y, β x y ={Eo}=∗ Φ x y)) -∗
    atomic_acc Eo Ei α P β Φ).
  Proof.
    iIntros (? x) "Hα Hclose".
    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.

  Global Instance elim_acc_aacc {X} E1 E2 Ei (α' β' : X PROP) γ' α β Pas Φ :
    ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α' β' γ'
            (atomic_acc E1 Ei α Pas β Φ)
            (λ x', atomic_acc E2 Ei α (β' x' (γ' x' -∗? Pas))%I β
                (λ.. x y, β' x' (γ' x' -∗? Φ x y))
            )%I.
  Proof.
    rewrite /ElimAcc.
    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 "_".
      iMod ("Hclose'" with "Hβ") as "Hβ'".
      rewrite ->!tele_app_bind. iDestruct "Hβ'" as "[Hβ' HΦ]".
      iMod ("Hclose" with "Hβ'") as "Hγ'".
      iModIntro. destruct (γ' x'); iApply "HΦ"; done.
  Qed.

  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.

  Lemma aacc_aacc {TA' TB' : tele} E1 E1' E2 E3
        α P β Φ
        (α' : 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'))) -∗
    atomic_acc E1 E3 α' P' β' Φ'.
  Proof.
    iIntros (?) "Hupd Hstep".
    iMod (atomic_acc_mask_weaken with "Hupd") as (x) "[Hα Hclose]"; first done.
    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']".
      iMod ("Hclose'" with "Hβ'") as "Hres".
      rewrite ->!tele_app_bind. iDestruct "Hres" as "[[Hα HΦ']|Hcont]".
      +
        iDestruct "Hclose" as "[Hclose _]".
        iMod ("Hclose" with "Hα") as "HP".
        iApply "HΦ'". done.
      +
        iDestruct "Hclose" as "[_ Hclose]".
        iDestruct "Hcont" as (y) "[Hβ HΦ']".
        iMod ("Hclose" with "Hβ") as "HΦ".
        iApply "HΦ'". done.
  Qed.

  Lemma aacc_aupd {TA' TB' : tele} E1 E1' E2 E3
        α β Φ
        (α' : 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' β' Φ'.
  Proof.
    iIntros (?) "Hupd Hstep". iApply (aacc_aacc with "[Hupd] Hstep"); first done.
    iApply aupd_aacc; done.
  Qed.

  Lemma aacc_aupd_commit {TA' TB' : tele} E1 E1' E2 E3
        α β Φ
        (α' : 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' β' Φ'.
  Proof.
    iIntros (?) "Hupd Hstep". iApply (aacc_aupd with "Hupd"); first done.
    iIntros (x) "Hα". iApply atomic_acc_wand; last first.
    { iApply "Hstep". done. }
    
    iSplit; first by eauto. iIntros (??) "?". rewrite ->!tele_app_bind. by iRight.
  Qed.

  Lemma aacc_aupd_abort {TA' TB' : tele} E1 E1' E2 E3
        α β Φ
        (α' : 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' β' Φ'.
  Proof.
    iIntros (?) "Hupd Hstep". iApply (aacc_aupd with "Hupd"); first done.
    iIntros (x) "Hα". iApply atomic_acc_wand; last first.
    { iApply "Hstep". done. }
    
    iSplit; first by eauto. iIntros (??) "?". rewrite ->!tele_app_bind. by iLeft.
  Qed.

End lemmas.

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

  Lemma tac_aupd_intro Γp Γs n α β Eo Ei Φ P :
    Timeless (PROP:=PROP) emp
    TCForall Laterable (env_to_list Γs)
    P = env_to_prop Γs
    envs_entails (Envs Γp Γs n) (atomic_acc Eo Ei α P β Φ)
    envs_entails (Envs Γp Γs n) (atomic_update Eo Ei α β Φ).
  Proof.
    intros ? HΓs →. rewrite envs_entails_eq of_envs_eq' /atomic_acc /=.
    setoid_rewrite env_to_prop_soundHAU.
    apply aupd_intro; [apply _..|]. done.
  Qed.
End proof_mode.

Now the coq-level tactics

Tactic Notation "iAuIntro" :=
  iStartProof; eapply tac_aupd_intro; [
    iSolveTC || fail "iAuIntro: emp is not timeless"
  | iSolveTC || fail "iAuIntro: not all spatial assumptions are laterable"
  | pm_reflexivity
  | ].
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.

Typeclasses Opaque atomic_acc atomic_update.