Library zoo.iris.bi.lib.atomic
From Ltac2 Require
Ltac2.
From stdpp Require Import
coPset
namespaces.
From iris.bi Require Export
bi
updates.
From iris.bi.lib Require Import
fixpoint_mono.
From iris.proofmode Require Import
coq_tactics
proofmode
reduction.
From iris.prelude Require Import
options.
Ltac2.
From stdpp Require Import
coPset
namespaces.
From iris.bi Require Export
bi
updates.
From iris.bi.lib Require Import
fixpoint_mono.
From iris.proofmode Require Import
coq_tactics
proofmode
reduction.
From iris.prelude Require Import
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 Types
(Eo Ei : coPset)
(α : TA → PROP)
(P : PROP)
(β : TA → TB → PROP)
(Φ : TA → TB → PROP)
.
iApply (bi.and_parallel with H); iSplit; iIntros H.
Section definition.
Context {PROP : bi} `{!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)).
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 β Φ.
|={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.
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.
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.
(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.
(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 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).
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 α β Φ) β Φ.
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).
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'.
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 β Φ).
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.
α 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 Types (α : 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.
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 :
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.
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.