Restore program_logic/viewshifts.

_CoqProject

@@ -70,6 +70,7 @@ program_logic/ownership.v
 program_logic/weakestpre.v
 program_logic/pviewshifts.v
 program_logic/hoare.v
+program_logic/viewshifts.v
 program_logic/language.v
 program_logic/ectx_language.v
 program_logic/ectxi_language.v

program_logic/hoare.v

-From iris.program_logic Require Export weakestpre. (* viewshifts *)
+From iris.program_logic Require Export weakestpre viewshifts.
 From iris.proofmode Require Import weakestpre.
 
 Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
@@ -59,7 +59,7 @@ Lemma ht_val E v : {{ True }} of_val v @ E {{ v', v = v' }}.
 Proof. iIntros "!# _". by iApply wp_value'. Qed.
 
 Lemma ht_vs E P P' Φ Φ' e :
-  □ (P ={E}=★ P') ∧ {{ P' }} e @ E {{ Φ' }} ∧ □ (∀ v, Φ' v ={E}=★ Φ v)
+  (P ={E}=> P') ∧ {{ P' }} e @ E {{ Φ' }} ∧ (∀ v, Φ' v ={E}=> Φ v)
   ⊢ {{ P }} e @ E {{ Φ }}.
 Proof.
   iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iVs ("Hvs" with "HP") as "HP".
@@ -69,7 +69,7 @@ Qed.
 
 Lemma ht_atomic E1 E2 P P' Φ Φ' e :
   atomic e →
-  □ (P ={E1,E2}=★ P') ∧ {{ P' }} e @ E2 {{ Φ' }} ∧ □ (∀ v, Φ' v ={E2,E1}=★ Φ v)
+  (P ={E1,E2}=> P') ∧ {{ P' }} e @ E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
   ⊢ {{ P }} e @ E1 {{ Φ }}.
 Proof.
   iIntros (?) "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ E2); auto.
@@ -104,7 +104,7 @@ Proof. iIntros "#Hwp !# [HP $]". by iApply "Hwp". Qed.
 
 Lemma ht_frame_step_l E1 E2 P R1 R2 e Φ :
   to_val e = None → E2 ⊆ E1 →
-  □ (R1 ={E1,E2}=★ ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ E2 {{ Φ }}
+  (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ E2 {{ Φ }}
   ⊢ {{ R1 ★ P }} e @ E1 {{ λ v, R2 ★ Φ v }}.
 Proof.
   iIntros (??) "[#Hvs #Hwp] !# [HR HP]".
@@ -114,7 +114,7 @@ Qed.
 
 Lemma ht_frame_step_r E1 E2 P R1 R2 e Φ :
   to_val e = None → E2 ⊆ E1 →
-  □ (R1 ={E1,E2}=★ ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ E2 {{ Φ }}
+  (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ E2 {{ Φ }}
   ⊢ {{ P ★ R1 }} e @ E1 {{ λ v, Φ v ★ R2 }}.
 Proof.
   iIntros (??) "[#Hvs #Hwp] !# [HP HR]".

program_logic/viewshifts.v

+From iris.program_logic Require Export pviewshifts.
+From iris.proofmode Require Import pviewshifts invariants.
+
+Definition vs `{irisG Λ Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
+  (□ (P → |={E1,E2}=> Q))%I.
+Arguments vs {_ _ _} _ _ _%I _%I.
+Instance: Params (@vs) 5.
+Notation "P ={ E1 , E2 }=> Q" := (vs 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 ={ E }=> Q" := (P ={E,E}=> Q)%I
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }=>  Q") : uPred_scope.
+
+Section vs.
+Context `{irisG Λ Σ}.
+Implicit Types P Q R : iProp Σ.
+Implicit Types N : namespace.
+
+Global Instance vs_ne E1 E2 n: Proper (dist n ==> dist n ==> dist n) (vs E1 E2).
+Proof. solve_proper. Qed.
+
+Global Instance vs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (vs E1 E2).
+Proof. apply ne_proper_2, _. Qed.
+
+Lemma vs_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 /vs -HP HQ. Qed.
+
+Global Instance vs_mono' E1 E2 : Proper (flip (⊢) ==> (⊢) ==> (⊢)) (vs E1 E2).
+Proof. solve_proper. Qed.
+
+Lemma vs_false_elim E1 E2 P : False ={E1,E2}=> P.
+Proof. iIntros "[]". Qed.
+Lemma vs_timeless E P : TimelessP P → ▷ P ={E}=> P.
+Proof. by iIntros (?) "> ?". Qed.
+
+Lemma vs_transitive E1 E2 E3 P Q R :
+  (P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R) ⊢ P ={E1,E3}=> R.
+Proof.
+  iIntros "#[HvsP HvsQ] !# HP".
+  iVs ("HvsP" with "HP") as "HQ". by iApply "HvsQ".
+Qed.
+
+Lemma vs_reflexive E P : P ={E}=> P.
+Proof. by iIntros "HP". Qed.
+
+Lemma vs_impl E P Q : □ (P → Q) ⊢ P ={E}=> Q.
+Proof. iIntros "#HPQ !# HP". by iApply "HPQ". Qed.
+
+Lemma vs_frame_l E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ R ★ P ={E1,E2}=> R ★ Q.
+Proof. iIntros "#Hvs !# [$ HP]". by iApply "Hvs". Qed.
+
+Lemma vs_frame_r E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ P ★ R ={E1,E2}=> Q ★ R.
+Proof. iIntros "#Hvs !# [HP $]". by iApply "Hvs". Qed.
+
+Lemma vs_mask_frame_r E1 E2 Ef P Q :
+  E1 ⊥ Ef → (P ={E1,E2}=> Q) ⊢ P ={E1 ∪ Ef,E2 ∪ Ef}=> Q.
+Proof.
+  iIntros (?) "#Hvs !# HP". iApply pvs_mask_frame_r; auto. by iApply "Hvs".
+Qed.
+
+Lemma vs_inv N E P Q R :
+  nclose N ⊆ E → inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q) ⊢ P ={E}=> Q.
+Proof.
+  iIntros (?) "#[? Hvs] !# HP". iInv N as "HR" "Hclose".
+  iVs ("Hvs" with "[HR HP]") as "[? $]"; first by iFrame.
+  by iApply "Hclose".
+Qed.
+
+Lemma vs_alloc N P : ▷ P ={N}=> inv N P.
+Proof. iIntros "HP". by iApply inv_alloc. Qed.
+End vs.