diff --git a/_CoqProject b/_CoqProject index 7aee7017a3478832b589b8aa0fb00000601809a1..d8f6edf734d3b3bbc0a8e3fe50ffad6105f4dd9b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -68,7 +68,6 @@ program_logic/ownership.v program_logic/weakestpre.v program_logic/weakestpre_fix.v program_logic/pviewshifts.v -program_logic/lviewshifts.v program_logic/resources.v program_logic/hoare.v program_logic/language.v diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v index fd0df37bf038959a9b6477045989508107f797e3..ff70ca4dcfa6ed49a17c6a9306856fe91403b34d 100644 --- a/program_logic/ectx_lifting.v +++ b/program_logic/ectx_lifting.v @@ -23,7 +23,7 @@ Lemma wp_lift_head_step E1 E2 head_reducible e1 σ1 → (∀ e2 σ2 ef, head_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) → (|={E1,E2}=> ▷ ownP σ1 ★ ▷ ∀ e2 σ2 ef, - (■ φ e2 σ2 ef ∧ ownP σ2) -★ |={E2,E1}=> WP e2 @ E1 {{ Φ }} ★ wp_fork ef) + (■ φ e2 σ2 ef ∧ ownP σ2) ={E2,E1}=★ WP e2 @ E1 {{ Φ }} ★ wp_fork ef) ⊢ WP e1 @ E1 {{ Φ }}. Proof. eauto using wp_lift_step. Qed. diff --git a/program_logic/invariants.v b/program_logic/invariants.v index e4fe069c490e1ba13656a5e7b8696887ac2c7db2..3037ced25dbb01b82e39d3b45851d264d8c93997 100644 --- a/program_logic/invariants.v +++ b/program_logic/invariants.v @@ -1,5 +1,5 @@ From iris.program_logic Require Import ownership. -From iris.program_logic Require Export namespaces lviewshifts. +From iris.program_logic Require Export namespaces. From iris.proofmode Require Import pviewshifts. Import uPred. diff --git a/program_logic/lifting.v b/program_logic/lifting.v index d2b80d543ab41b0252bbad79061d6f29f011da1a..37ac7b5220e6121f310756e3751f2d5affd7cd8c 100644 --- a/program_logic/lifting.v +++ b/program_logic/lifting.v @@ -23,7 +23,7 @@ Lemma wp_lift_step E1 E2 reducible e1 σ1 → (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) → (|={E1,E2}=> ▷ ownP σ1 ★ ▷ ∀ e2 σ2 ef, - (■ φ e2 σ2 ef ∧ ownP σ2) -★ |={E2,E1}=> WP e2 @ E1 {{ Φ }} ★ wp_fork ef) + (■ φ e2 σ2 ef ∧ ownP σ2) ={E2,E1}=★ WP e2 @ E1 {{ Φ }} ★ wp_fork ef) ⊢ WP e1 @ E1 {{ Φ }}. Proof. intros ? He Hsafe Hstep. rewrite pvs_eq wp_eq. diff --git a/program_logic/lviewshifts.v b/program_logic/lviewshifts.v deleted file mode 100644 index 694d153301647d44c33e8086be1f5fdcacb679df..0000000000000000000000000000000000000000 --- a/program_logic/lviewshifts.v +++ /dev/null @@ -1,23 +0,0 @@ -From iris.program_logic Require Export pviewshifts. -Import uPred. - -(* Some notation for linear view shifts. *) - -Definition lvs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ := - (P -★ |={E1,E2}=> Q)%I. -Arguments lvs {_ _} _ _ _%I _%I. -Instance: Params (@lvs) 4. -Notation "P ={ E1 , E2 }=★ Q" := (lvs 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" := (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. - -(* TODO: Also prove some lemmas. *) diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v index f045dc2c0199cc3d795f572ff61e9f020ec373ff..d5c21073b24e497e669d843412521f1d9dab191e 100644 --- a/program_logic/pviewshifts.v +++ b/program_logic/pviewshifts.v @@ -45,6 +45,13 @@ Notation "P ={ E1 , E2 }=> Q" := (P ⊢ |={E1,E2}=> Q) Notation "P ={ E }=> Q" := (P ⊢ |={E}=> Q) (at level 99, E at level 50, Q at level 200, only parsing) : C_scope. +Notation "P ={ E1 , E2 }=★ Q" := (P -★ |={E1,E2}=> 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 pvs. Context {Λ : language} {Σ : iFunctor}. Implicit Types P Q : iProp Λ Σ. diff --git a/tests/proofmode.v b/tests/proofmode.v index 9301a91b987e1e340358babde4dc32b288316388..24edb16fcc2af18a56fd0b6b817f4243e06c26e5 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -97,7 +97,7 @@ Section iris. Lemma demo_8 N E P Q R : nclose N ⊆ E → - (True -★ P -★ inv N Q -★ True -★ R) ⊢ P -★ ▷ Q -★ |={E}=> R. + (True -★ P -★ inv N Q -★ True -★ R) ⊢ P -★ ▷ Q ={E}=★ R. Proof. iIntros {?} "H HP HQ". iApply ("H" with "[#] HP |==>[HQ] |==>").