Commit 0502f30b authored by Robbert Krebbers's avatar Robbert Krebbers

Remove lviewshifts.v and turn them into notations.

parent 69eefa4c
Pipeline #1495 passed with stage
......@@ -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
......
......@@ -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.
......
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.
......
......@@ -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.
......
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. *)
......@@ -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 Λ Σ.
......
......@@ -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] |==>").
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment