Library iris.program_logic.stepshifts
From iris.program_logic Require Import ownership.
From iris.program_logic Require Export pviewshifts pstepshifts viewshifts invariants ghost_ownership.
From iris.proofmode Require Import pviewshifts pstepshifts invariants.
Import uPred.
Definition svs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
(□ (P -★ |={E1,E2}=>> Q))%I.
Arguments svs {_ _} _ _ _%I _%I.
Instance: Params (@vs) 4.
Notation "P ={ E1 , E2 }=>> Q" := (svs E1 E2 P%I Q%I)
(at level 99, E1,E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=>> Q") : uPred_scope.
Notation "P ={ E1 , E2 }=>> Q" := (Emp ⊢ (P ={E1,E2}=>> Q)%I)
(at level 99, E1, E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=>> Q") : C_scope.
Notation "P ={ E }=>> Q" := (P ={E,E}=>> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=>> Q") : uPred_scope.
Notation "P ={ E }=>> Q" := (Emp ⊢ (P ={E}=>> Q)%I)
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=>> Q") : C_scope.
Notation "P <={ E1 , E2 }=>> Q" := ((P ={E1,E2}=>> Q) ∧ (Q ={E2,E1}=>> P))%I
(at level 99, E1,E2 at level 50, Q at level 200,
format "P <={ E1 , E2 }=>> Q") : uPred_scope.
Notation "P <={ E1 , E2 }=>> Q" := (True ⊢ (P <={E1,E2}=>> Q)%I)
(at level 99, E1, E2 at level 50, Q at level 200,
format "P <={ E1 , E2 }=>> Q") : C_scope.
Notation "P <={ E }=>> Q" := (P <={E,E}=>> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P <={ E }=>> Q") : uPred_scope.
Notation "P <={ E }=>> Q" := (True ⊢ (P <={E}=>> Q)%I)
(at level 99, E at level 50, Q at level 200,
format "P <={ E }=>> Q") : C_scope.
Section svs.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q R : iProp Λ Σ.
Implicit Types N : namespace.
Lemma svs_alt E1 E2 P Q : (P ⊢ |={E1,E2}=>> Q) → P ={E1,E2}=>> Q.
Proof. iIntros (Hsvs). iIntros "_ ! ?". by iApply Hsvs. Qed.
Global Instance svs_ne E1 E2 n :
Proper (dist n ==> dist n ==> dist n) (@svs Λ Σ E1 E2).
Proof. solve_proper. Qed.
Global Instance svs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (@svs Λ Σ E1 E2).
Proof. apply ne_proper_2, _. Qed.
Lemma svs_mono E1 E2 P P' Q Q' :
(P ⊢ P') → (Q' ⊢ Q) → (P' ={E1,E2}=>> Q') ⊢ (P ={E1,E2}=>> Q).
Proof. by intros HP HQ; rewrite /svs -HP HQ. Qed.
Global Instance svs_mono' E1 E2 :
Proper (flip (⊢) ==> (⊢) ==> (⊢)) (@svs Λ Σ E1 E2).
Proof. solve_proper. Qed.
Lemma svs_false_elim E1 E2 P : False ={E1,E2}=>> P.
Proof. iIntros "_ ! []"; auto. Qed.
Lemma svs_vs E1 E2 E3 P Q R :
E2 ⊆ E1 ∪ E3 → ((P ={E1,E2}=>> Q) ★ ⧆(Q ={E2,E3}=> R)) ⊢ (P ={E1,E3}=>> R).
iIntros (?) "#[HsvsP HsvsQ] ! HP".
iPsvs ("HsvsP" with "HP"); first done.
rewrite affine_elim. iApply ("HsvsQ"). auto.
Qed.
Lemma vs_svs E1 E2 E3 P Q R :
E2 ⊆ E1 ∪ E3 → (⧆(P ={E1,E2}=> Q) ★ (Q ={E2,E3}=>> R)) ⊢ (P ={E1,E3}=>> R).
iIntros (?) "#[HsvsP HsvsQ] ! HP".
rewrite affine_elim. iSpecialize ("HsvsP" with " HP").
iApply pvs_psvs; eauto.
iPvs "HsvsP" as "HQ"; first set_solver.
iApply pvs_intro. iPsvs ("HsvsQ" with "HQ"); first set_solver.
iApply pvs_intro; auto.
Qed.
Lemma svs_vs' E P Q R : ((P ={E}=>> Q) ★ ⧆(Q ={E}=> R)) ⊢ (P ={E}=>> R).
Proof. apply svs_vs; set_solver. Qed.
Lemma vs_svs' E P Q R : (⧆(P ={E}=> Q) ★ (Q ={E}=>> R)) ⊢ (P ={E}=>> R).
Proof. apply vs_svs; set_solver. Qed.
Lemma svs_frame_l E1 E2 P Q R : (P ={E1,E2}=>> Q) ⊢ (⧆R ★ P ={E1,E2}=>> ⧆R ★ Q).
Proof. iIntros "#Hsvs ! [$ HP]". by iApply "Hsvs". Qed.
Lemma svs_frame_r E1 E2 P Q R : (P ={E1,E2}=>> Q) ⊢ (P ★ ⧆R ={E1,E2}=>> Q ★ ⧆R).
Proof. iIntros "#Hsvs ! [HP $]". by iApply "Hsvs". Qed.
Lemma svs_mask_frame E1 E2 Ef P Q :
Ef ⊥ E1 ∪ E2 → (P ={E1,E2}=>> Q) ⊢ (P ={E1 ∪ Ef,E2 ∪ Ef}=>> Q).
Proof.
iIntros (?) "#Hsvs ! HP". iApply psvs_mask_frame; auto. by iApply "Hsvs".
Qed.
Lemma svs_mask_frame' E Ef P Q : Ef ⊥ E → (P ={E}=>> Q) ⊢ (P ={E ∪ Ef}=>> Q).
Proof. intros; apply svs_mask_frame; set_solver. Qed.
Lemma svs_inv N E P Q R :
nclose N ⊆ E → (inv N R ★ (⧆▷ R ★ P ={E ∖ nclose N}=>> ⧆▷ R ★ Q)) ⊢ (P ={E}=>> Q).
Proof.
iIntros (?) "#[Hinv Hsvs] ! HP". iInv "Hinv" as "HR".
iApply "Hsvs".
iClear "Hinv".
iSplitL "HR"; auto.
Qed.
End svs.
Section svs_ghost.
Context `{i: inG Λ Σ A}.
Implicit Types a : A.
Implicit Types P Q R : iPropG Λ Σ.
Context (AltTriv: ∀ (gid': gid Σ) A, gid' ≠ (inG_id i) ∧
A = projT2 Σ gid' (iPreProp Λ (globalF Σ)) →
trivial_step A).
Lemma svs_stepP E a al φ :
a # al ~~>>: φ → owne a ★ ownle al ={E}=>> ∃ a' al', ⧆■ φ a' al' ★ owne a' ★ ownle al'.
Proof. intros. apply svs_alt. apply owne_stepP; auto. Qed.
End svs_ghost.
From iris.program_logic Require Export pviewshifts pstepshifts viewshifts invariants ghost_ownership.
From iris.proofmode Require Import pviewshifts pstepshifts invariants.
Import uPred.
Definition svs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
(□ (P -★ |={E1,E2}=>> Q))%I.
Arguments svs {_ _} _ _ _%I _%I.
Instance: Params (@vs) 4.
Notation "P ={ E1 , E2 }=>> Q" := (svs E1 E2 P%I Q%I)
(at level 99, E1,E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=>> Q") : uPred_scope.
Notation "P ={ E1 , E2 }=>> Q" := (Emp ⊢ (P ={E1,E2}=>> Q)%I)
(at level 99, E1, E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=>> Q") : C_scope.
Notation "P ={ E }=>> Q" := (P ={E,E}=>> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=>> Q") : uPred_scope.
Notation "P ={ E }=>> Q" := (Emp ⊢ (P ={E}=>> Q)%I)
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=>> Q") : C_scope.
Notation "P <={ E1 , E2 }=>> Q" := ((P ={E1,E2}=>> Q) ∧ (Q ={E2,E1}=>> P))%I
(at level 99, E1,E2 at level 50, Q at level 200,
format "P <={ E1 , E2 }=>> Q") : uPred_scope.
Notation "P <={ E1 , E2 }=>> Q" := (True ⊢ (P <={E1,E2}=>> Q)%I)
(at level 99, E1, E2 at level 50, Q at level 200,
format "P <={ E1 , E2 }=>> Q") : C_scope.
Notation "P <={ E }=>> Q" := (P <={E,E}=>> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P <={ E }=>> Q") : uPred_scope.
Notation "P <={ E }=>> Q" := (True ⊢ (P <={E}=>> Q)%I)
(at level 99, E at level 50, Q at level 200,
format "P <={ E }=>> Q") : C_scope.
Section svs.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q R : iProp Λ Σ.
Implicit Types N : namespace.
Lemma svs_alt E1 E2 P Q : (P ⊢ |={E1,E2}=>> Q) → P ={E1,E2}=>> Q.
Proof. iIntros (Hsvs). iIntros "_ ! ?". by iApply Hsvs. Qed.
Global Instance svs_ne E1 E2 n :
Proper (dist n ==> dist n ==> dist n) (@svs Λ Σ E1 E2).
Proof. solve_proper. Qed.
Global Instance svs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (@svs Λ Σ E1 E2).
Proof. apply ne_proper_2, _. Qed.
Lemma svs_mono E1 E2 P P' Q Q' :
(P ⊢ P') → (Q' ⊢ Q) → (P' ={E1,E2}=>> Q') ⊢ (P ={E1,E2}=>> Q).
Proof. by intros HP HQ; rewrite /svs -HP HQ. Qed.
Global Instance svs_mono' E1 E2 :
Proper (flip (⊢) ==> (⊢) ==> (⊢)) (@svs Λ Σ E1 E2).
Proof. solve_proper. Qed.
Lemma svs_false_elim E1 E2 P : False ={E1,E2}=>> P.
Proof. iIntros "_ ! []"; auto. Qed.
Lemma svs_vs E1 E2 E3 P Q R :
E2 ⊆ E1 ∪ E3 → ((P ={E1,E2}=>> Q) ★ ⧆(Q ={E2,E3}=> R)) ⊢ (P ={E1,E3}=>> R).
iIntros (?) "#[HsvsP HsvsQ] ! HP".
iPsvs ("HsvsP" with "HP"); first done.
rewrite affine_elim. iApply ("HsvsQ"). auto.
Qed.
Lemma vs_svs E1 E2 E3 P Q R :
E2 ⊆ E1 ∪ E3 → (⧆(P ={E1,E2}=> Q) ★ (Q ={E2,E3}=>> R)) ⊢ (P ={E1,E3}=>> R).
iIntros (?) "#[HsvsP HsvsQ] ! HP".
rewrite affine_elim. iSpecialize ("HsvsP" with " HP").
iApply pvs_psvs; eauto.
iPvs "HsvsP" as "HQ"; first set_solver.
iApply pvs_intro. iPsvs ("HsvsQ" with "HQ"); first set_solver.
iApply pvs_intro; auto.
Qed.
Lemma svs_vs' E P Q R : ((P ={E}=>> Q) ★ ⧆(Q ={E}=> R)) ⊢ (P ={E}=>> R).
Proof. apply svs_vs; set_solver. Qed.
Lemma vs_svs' E P Q R : (⧆(P ={E}=> Q) ★ (Q ={E}=>> R)) ⊢ (P ={E}=>> R).
Proof. apply vs_svs; set_solver. Qed.
Lemma svs_frame_l E1 E2 P Q R : (P ={E1,E2}=>> Q) ⊢ (⧆R ★ P ={E1,E2}=>> ⧆R ★ Q).
Proof. iIntros "#Hsvs ! [$ HP]". by iApply "Hsvs". Qed.
Lemma svs_frame_r E1 E2 P Q R : (P ={E1,E2}=>> Q) ⊢ (P ★ ⧆R ={E1,E2}=>> Q ★ ⧆R).
Proof. iIntros "#Hsvs ! [HP $]". by iApply "Hsvs". Qed.
Lemma svs_mask_frame E1 E2 Ef P Q :
Ef ⊥ E1 ∪ E2 → (P ={E1,E2}=>> Q) ⊢ (P ={E1 ∪ Ef,E2 ∪ Ef}=>> Q).
Proof.
iIntros (?) "#Hsvs ! HP". iApply psvs_mask_frame; auto. by iApply "Hsvs".
Qed.
Lemma svs_mask_frame' E Ef P Q : Ef ⊥ E → (P ={E}=>> Q) ⊢ (P ={E ∪ Ef}=>> Q).
Proof. intros; apply svs_mask_frame; set_solver. Qed.
Lemma svs_inv N E P Q R :
nclose N ⊆ E → (inv N R ★ (⧆▷ R ★ P ={E ∖ nclose N}=>> ⧆▷ R ★ Q)) ⊢ (P ={E}=>> Q).
Proof.
iIntros (?) "#[Hinv Hsvs] ! HP". iInv "Hinv" as "HR".
iApply "Hsvs".
iClear "Hinv".
iSplitL "HR"; auto.
Qed.
End svs.
Section svs_ghost.
Context `{i: inG Λ Σ A}.
Implicit Types a : A.
Implicit Types P Q R : iPropG Λ Σ.
Context (AltTriv: ∀ (gid': gid Σ) A, gid' ≠ (inG_id i) ∧
A = projT2 Σ gid' (iPreProp Λ (globalF Σ)) →
trivial_step A).
Lemma svs_stepP E a al φ :
a # al ~~>>: φ → owne a ★ ownle al ={E}=>> ∃ a' al', ⧆■ φ a' al' ★ owne a' ★ ownle al'.
Proof. intros. apply svs_alt. apply owne_stepP; auto. Qed.
End svs_ghost.