Library zoo.iris.bi.lib.atomic

Require Ltac2.Ltac2.

Require Import stdpp.coPset.
Require Import stdpp.namespaces.

Require Export iris.bi.bi.
Require Export iris.bi.updates.
Require Import iris.bi.lib.fixpoint_mono.
Require Import iris.proofmode.coq_tactics.
Require Import iris.proofmode.proofmode.
Require Import iris.proofmode.reduction.
Require Import iris.prelude.options.

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 {PROP : bi} `{!BiFUpd PROP} {TA TB : tele}.
  Implicit Type
    (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)).

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

  Lemma atomic_accｰmask Eo Ed α P β Φ :
    atomic_acc Eo (Eo∖Ed) α P β Φ ⊣⊢ ∀ E, ⌜Eo ⊆ E⌝ → atomic_acc E (E∖Ed) α P β Φ.

  Lemma atomic_accｰmaskｰweaken Eo1 Eo2 Ei α P β Φ :
    Eo1 ⊆ Eo2 →
    atomic_acc Eo1 Ei α P β Φ -∗ atomic_acc Eo2 Ei α P β Φ.

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

  Definition atomic_update۰pre (Ψ : () → PROP) (_ : ()) : PROP :=
    atomic_acc Eo Ei α (Ψ ()) β Φ.

  Local Instance atomic_update۰preｰmono : BiMonoPred atomic_update۰pre.

  Local Definition atomic_update۰def :=
    bi_greatest_fixpoint atomic_update۰pre ().

End definition.

Seal it
Local Definition atomic_update۰aux : seal (@atomic_update۰def).
Definition atomic_update := atomic_update۰aux.(unseal).
Global Arguments atomic_update {PROP _ TA TB}.
Local Definition atomic_updateｰunseal :
  @atomic_update = _ := atomic_update۰aux.(seal_eq).

Global Arguments atomic_acc {PROP _ TA TB} Eo Ei _ _ _ _ : simpl never.
Global Arguments atomic_update {PROP _ TA TB} Eo Ei _ _ _ : simpl never.

Notation: Atomic updates We avoid ''/'' since those can also reasonably be infix operators (and in fact Autosubst uses the latter).
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 $ λ x1, .. (λ xn, α%I) ..)
                 (tele_app $ λ x1, .. (λ xn,
                         tele_app (λ y1, .. (λ yn, β%I) .. )
                        ) .. )
                 (tele_app $ λ x1, .. (λ xn,
                         tele_app (λ y1, .. (λ yn, Φ%I) .. )
                        ) .. )
  )
  (at level 0, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
   format "'[hv ' '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 $ λ x1, .. (λ xn, α%I) ..)
                 (tele_app $ λ x1, .. (λ xn, tele_app β%I) .. )
                 (tele_app $ λ x1, .. (λ xn, tele_app Φ%I) .. )
  )
  (at level 0, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder,
   format "'[hv ' '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 α%I)
                 (tele_app $ tele_app (λ y1, .. (λ yn, β%I) ..))
                 (tele_app $ tele_app (λ y1, .. (λ yn, Φ%I) ..))
  )
  (at level 0, Eo, Ei, α, β, Φ at level 200, y1 binder, yn binder,
   format "'[hv ' 'AU' '<{' '[' α ']' '}>' '/' @ '[' Eo , '/' Ei ']' '/' '<{' '[' ∀∀ y1 .. yn , '/' β , '/' COMM Φ ']' '}>' ']'") : bi_scope.

Notation "'AU' '<{' α '}>' @ Eo , Ei '<{' β , 'COMM' Φ '}>'" :=
  (atomic_update (TA:=TeleO) (TB:=TeleO)
                 Eo Ei
                 (tele_app α%I)
                 (tele_app $ tele_app β%I)
                 (tele_app $ tele_app Φ%I)
  )
  (at level 0, Eo, Ei, α, β, Φ at level 200,
   format "'[hv ' '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 $ λ x1, .. (λ xn, α%I) ..)
              P%I
              (tele_app $ λ x1, .. (λ xn,
                      tele_app (λ y1, .. (λ yn, β%I) .. )
                     ) .. )
              (tele_app $ λ x1, .. (λ xn,
                      tele_app (λ y1, .. (λ yn, Φ%I) .. )
                     ) .. )
  )
  (at level 0, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
   format "'[hv ' '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 $ λ x1, .. (λ xn, α%I) ..)
              P%I
              (tele_app $ λ x1, .. (λ xn, tele_app β%I) .. )
              (tele_app $ λ x1, .. (λ xn, tele_app Φ%I) .. )
  )
  (at level 0, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder,
   format "'[hv ' '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 α%I)
              P%I
              (tele_app $ tele_app (λ y1, .. (λ yn, β%I) ..))
              (tele_app $ tele_app (λ y1, .. (λ yn, Φ%I) ..))
  )
  (at level 0, Eo, Ei, α, P, β, Φ at level 200, y1 binder, yn binder,
   format "'[hv ' '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 α%I)
              P%I
              (tele_app $ tele_app β%I)
              (tele_app $ tele_app Φ%I)
  )
  (at level 0, Eo, Ei, α, P, β, Φ at level 200,
   format "'[hv ' 'AACC' '<{' '[' α , '/' ABORT P ']' '}>' '/' @ '[' Eo , '/' Ei ']' '/' '<{' '[' β , '/' COMM Φ ']' '}>' ']'") : bi_scope.

Lemmas about AU
Section lemmas.
  Context `{BiFUpd PROP} {TA TB : tele}.
  Implicit Type (α : 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).

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

  Lemma atomic_updateｰmaskｰweaken Eo1 Eo2 Ei α β Φ :
    Eo1 ⊆ Eo2 →
    atomic_update Eo1 Ei α β Φ -∗ atomic_update Eo2 Ei α β Φ.

  Local Lemma aupdｰunfold Eo Ei α β Φ :
    atomic_update Eo Ei α β Φ ⊣⊢
    atomic_acc Eo Ei α (atomic_update Eo Ei α β Φ) β Φ.

The elimination form: an atomic accessor
  Lemma aupdｰaacc Eo Ei α β Φ :
    atomic_update Eo Ei α β Φ ⊢
    atomic_acc Eo Ei α (atomic_update Eo Ei α β Φ) β Φ.

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

The introduction lemma for atomic_update. This should usually not be used directly; use the iAuIntro tactic instead.
  Local Lemma aupdｰintro P Q α β Eo Ei Φ :
    Absorbing P → Persistent P →
    (P ∧ Q ⊢ atomic_acc Eo Ei α Q β Φ) →
    P ∧ Q ⊢ atomic_update Eo Ei α β Φ.

  Lemma aaccｰintro Eo Ei α P β Φ x :
    Ei ⊆ Eo →
    α x -∗
    ( α x ={Eo}=∗ P)
    ∧ (∀.. y : TB, β x y ={Eo}=∗ Φ x y
    ) -∗
    atomic_acc Eo Ei α P β Φ.

  Global Instance elim_accｰaacc {X} E1 E2 Ei (α' β' : X → PROP) γ' α β Pas Φ :
    ElimAcc (X:=X) True (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.

  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 β Φ).

Lemmas for directly proving one atomic accessor in terms of another (or an atomic update). These are only really useful when the atomic accessor you are trying to prove exactly corresponds to an atomic update/accessor you have as an assumption -- which is not very common.
  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' β' Φ'.

  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' β' Φ'.

  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' β' Φ'.

  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' β' Φ'.

End lemmas.

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

  Lemma tacｰaupdｰintro Γp Γs n α β Eo Ei Φ P :
    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 α β Φ).
End proof_mode.

Now the Rocq-level tactics


Tactic Notation "iAuIntro" :=
  match goal with
  | |- envs_entails (Envs ?Γp ?Γs _) (atomic_update _ _ _ _ ?Φ) ⇒
      notypeclasses refine (tacｰaupdｰintro Γp Γs _ _ _ _ _ Φ _ _ _); [
         pm_reflexivity
      | ]
  end.

Module iAaccIntro.
  Import Ltac2.

  Ltac2 Type error :=
    [ Invalid_telescope
    | Too_many_witnesses
    ].

  Ltac2 error_to_string err :=
    match err with
    | Invalid_telescope ⇒
        "invalid telescope"
    | Too_many_witnesses ⇒
        "too many witnesses"
    end.
  Ltac2 error err :=
    let err := error_to_string err in
    let err := String.app "iAaccIntro: " err in
    Control.throw_invalid_argument err.

  Ltac2 rec extra_witnesses xs tele :=
    lazy_match! tele with
    | TeleO ⇒
        'TargO
    | TeleS ?tele ⇒
        match Constr.Unsafe.kind tele with
        | Constr.Unsafe.Lambda bdr tele ⇒
            let ty := Constr.Binder.type bdr in
            let ty := Constr.Unsafe.substnl xs 0 ty in
            let x := '?[?witness] in
            let xs := extra_witnesses (x :: xs) tele in
            Constr.Unsafe.make (Constr.Unsafe.App '@TeleArgCons [|ty; '_; x; xs|])
        | _ ⇒
            '?[?witnesses]
        end
    | _ ⇒
        '?[?witnesses]
    end.

  Ltac2 rec witnesses' xs1 tele xs2 :=
    match xs2 with
    | [] ⇒
        extra_witnesses xs1 tele
    | x :: xs2 ⇒
        lazy_match! tele with
        | TeleO ⇒
            error Too_many_witnesses
        | TeleS ?tele ⇒
            match Constr.Unsafe.kind tele with
            | Constr.Unsafe.Lambda bdr tele ⇒
                let ty := Constr.Binder.type bdr in
                let ty := Constr.Unsafe.substnl xs1 0 ty in
                let x :=
                  Constr.Pretype.pretype
                    Constr.Pretype.Flags.open_constr_flags_with_tc
                    Constr.Pretype.expected_without_type_constraint
                    preterm:($preterm:x : $ty)
                in
                let xs2 := witnesses' (x :: xs1) tele xs2 in
                Constr.Unsafe.make (Constr.Unsafe.App '@TeleArgCons [|ty; '_; x; xs2|])
            | _ ⇒
                error Invalid_telescope
            end
        | _ ⇒
            error Invalid_telescope
        end
    end.
  Ltac2 witnesses tele xs :=
    witnesses' [] tele xs.
End iAaccIntro.

Tactic Notation "iAaccIntro" uconstr_list_sep(xs, ",") "with" constr(H) :=
  iStartProof;
  lazymatch goal with
  | |- envs_entails _ (@atomic_acc _ _ ?tele _ ?Eo ?Ei ?α ?P ?β ?Φ) ⇒
      let go := ltac2val:(tele xs |-
        let tele := Option.get (Ltac1.to_constr tele) in
        let xs := Option.get (Ltac1.to_list xs) in
        let xs := List.map (fun x ⇒ Option.get (Ltac1.to_preterm x)) xs in
        let xs := iAaccIntro.witnesses tele xs in
        Ltac1.of_constr xs
      ) in
      let xs := go tele xs in
      iApply (aaccｰintro Eo Ei α P β Φ xs with H);
        first try solve_ndisj;
        last iSplit
  | _ ⇒
      fail "iAaccIntro: goal is not an atomic accessor"
  end.

Global Typeclasses Opaque atomic_acc atomic_update.