Commit 55a04c5f authored by Robbert Krebbers's avatar Robbert Krebbers

Change the level of view shifts so it is more like the implication.

It is now slightly below implication. In order to do this, I had to change
the notation from P ={E1,E2}=> Q to P >{E1,E2}=> Q because the prefer ={n
is already used at level 70 for the distance of the metric.
parent 28c4a0bf
......@@ -36,7 +36,7 @@ Proof.
by rewrite -wp_value; apply const_intro.
Qed.
Lemma ht_vs E P P' Q Q' e :
(P ={E}=> P' {{ P' }} e @ E {{ Q' }} v, Q' v ={E}=> Q v)
((P >{E}=> P') {{ P' }} e @ E {{ Q' }} v, Q' v >{E}=> Q v)
{{ P }} e @ E {{ Q }}.
Proof.
apply (always_intro' _ _), impl_intro_l.
......@@ -47,7 +47,7 @@ Proof.
Qed.
Lemma ht_atomic E1 E2 P P' Q Q' e :
E2 E1 atomic e
(P ={E1,E2}=> P' {{ P' }} e @ E2 {{ Q' }} v, Q' v ={E2,E1}=> Q v)
((P >{E1,E2}=> P') {{ P' }} e @ E2 {{ Q' }} v, Q' v >{E2,E1}=> Q v)
{{ P }} e @ E1 {{ Q }}.
Proof.
intros ??; apply (always_intro' _ _), impl_intro_l.
......
......@@ -20,8 +20,8 @@ Lemma ht_lift_step E1 E2
E1 E2 to_val e1 = None
reducible e1 σ1
( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
(P ={E2,E1}=> (ownP σ1 P') e2 σ2 ef,
( φ e2 σ2 ef ownP σ2 P') ={E1,E2}=> (Q1 e2 σ2 ef Q2 e2 σ2 ef)
((P >{E2,E1}=> ownP σ1 P') e2 σ2 ef,
( φ e2 σ2 ef ownP σ2 P' >{E1,E2}=> Q1 e2 σ2 ef Q2 e2 σ2 ef)
{{ Q1 e2 σ2 ef }} e2 @ E2 {{ R }}
{{ Q2 e2 σ2 ef }} ef ?@ coPset_all {{ λ _, True }})
{{ P }} e1 @ E2 {{ R }}.
......
......@@ -6,20 +6,22 @@ Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
( (P pvs E1 E2 Q))%I.
Arguments vs {_ _} _ _ _%I _%I.
Instance: Params (@vs) 4.
Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P%I Q%I)
(at level 69, E1 at level 1, format "P ={ E1 , E2 }=> Q") : uPred_scope.
Notation "P ={ E1 , E2 }=> Q" := (True vs E1 E2 P%I Q%I)
(at level 69, E1 at level 1, format "P ={ E1 , E2 }=> Q") : C_scope.
Notation "P ={ E }=> Q" := (vs E E P%I Q%I)
(at level 69, E at level 1, format "P ={ E }=> Q") : uPred_scope.
Notation "P ={ E }=> Q" := (True vs E E P%I Q%I)
(at level 69, E at level 1, format "P ={ E }=> Q") : C_scope.
Notation "P >{ E1 , E2 }=> Q" := (vs E1 E2 P%I Q%I)
(at level 199, E1 at level 1, E2 at level 1,
format "P >{ E1 , E2 }=> Q") : uPred_scope.
Notation "P >{ E1 , E2 }=> Q" := (True vs E1 E2 P%I Q%I)
(at level 199, E1 at level 1, E2 at level 1,
format "P >{ E1 , E2 }=> Q") : C_scope.
Notation "P >{ E }=> Q" := (vs E E P%I Q%I)
(at level 199, E at level 1, format "P >{ E }=> Q") : uPred_scope.
Notation "P >{ E }=> Q" := (True vs E E P%I Q%I)
(at level 199, E at level 1, format "P >{ E }=> Q") : C_scope.
Section vs.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q R : iProp Λ Σ.
Lemma vs_alt E1 E2 P Q : (P pvs E1 E2 Q) P ={E1,E2}=> Q.
Lemma vs_alt E1 E2 P Q : (P pvs E1 E2 Q) P >{E1,E2}=> Q.
Proof.
intros; rewrite -{1}always_const; apply always_intro, impl_intro_l.
by rewrite always_const (right_id _ _).
......@@ -33,73 +35,71 @@ Global Instance vs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (@vs Λ Σ
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.
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. by intros until 2; apply vs_mono. Qed.
Lemma vs_false_elim E1 E2 P : False ={E1,E2}=> P.
Lemma vs_false_elim E1 E2 P : False >{E1,E2}=> P.
Proof. apply vs_alt, False_elim. Qed.
Lemma vs_timeless E P : TimelessP P P ={E}=> P.
Lemma vs_timeless E P : TimelessP P P >{E}=> P.
Proof. by intros ?; apply vs_alt, pvs_timeless. Qed.
Lemma vs_transitive E1 E2 E3 P Q R :
E2 E1 E3 (P ={E1,E2}=> Q Q ={E2,E3}=> R) P ={E1,E3}=> R.
E2 E1 E3 ((P >{E1,E2}=> Q) (Q >{E2,E3}=> R)) (P >{E1,E3}=> R).
Proof.
intros; rewrite -always_and; apply always_intro, impl_intro_l.
rewrite always_and (associative _) (always_elim (P _)) impl_elim_r.
by rewrite pvs_impl_r; apply pvs_trans.
Qed.
Lemma vs_transitive' E P Q R : (P ={E}=> Q Q ={E}=> R) P ={E}=> R.
Lemma vs_transitive' E P Q R : ((P >{E}=> Q) (Q >{E}=> R)) (P >{E}=> R).
Proof. apply vs_transitive; solve_elem_of. Qed.
Lemma vs_reflexive E P : P ={E}=> P.
Lemma vs_reflexive E P : P >{E}=> P.
Proof. apply vs_alt, pvs_intro. Qed.
Lemma vs_impl E P Q : (P Q) P ={E}=> Q.
Lemma vs_impl E P Q : (P Q) (P >{E}=> Q).
Proof.
apply always_intro, impl_intro_l.
by rewrite always_elim impl_elim_r -pvs_intro.
Qed.
Lemma vs_frame_l E1 E2 P Q R : P ={E1,E2}=> Q (R P) ={E1,E2}=> (R Q).
Lemma vs_frame_l E1 E2 P Q R : (P >{E1,E2}=> Q) (R P >{E1,E2}=> R Q).
Proof.
apply always_intro, impl_intro_l.
rewrite -pvs_frame_l always_and_sep_r -always_wand_impl -(associative _).
by rewrite always_elim wand_elim_r.
Qed.
Lemma vs_frame_r E1 E2 P Q R : P ={E1,E2}=> Q (P R) ={E1,E2}=> (Q R).
Lemma vs_frame_r E1 E2 P Q R : (P >{E1,E2}=> Q) (P R >{E1,E2}=> Q R).
Proof. rewrite !(commutative _ _ R); apply vs_frame_l. Qed.
Lemma vs_mask_frame E1 E2 Ef P Q :
Ef (E1 E2) = P ={E1,E2}=> Q P ={E1 Ef,E2 Ef}=> Q.
Ef (E1 E2) = (P >{E1,E2}=> Q) (P >{E1 Ef,E2 Ef}=> Q).
Proof.
intros ?; apply always_intro, impl_intro_l; rewrite (pvs_mask_frame _ _ Ef)//.
by rewrite always_elim impl_elim_r.
Qed.
Lemma vs_mask_frame' E Ef P Q : Ef E = P ={E}=> Q P ={E Ef}=> Q.
Lemma vs_mask_frame' E Ef P Q : Ef E = (P >{E}=> Q) (P >{E Ef}=> Q).
Proof. intros; apply vs_mask_frame; solve_elem_of. Qed.
(* FIXME I really should not need parenthesis around the pre- and postcondition
of a view shift. *)
Lemma vs_open_close N E P Q R :
nclose N E
(inv N R (R P) ={E nclose N}=> (R Q)) P ={E}=> Q.
(inv N R ( R P >{E nclose N}=> R Q)) (P >{E}=> Q).
Proof.
intros HN. apply always_intro'; first by apply _. apply impl_intro_l.
intros; apply (always_intro' _ _), impl_intro_l.
rewrite associative (commutative _ P) -associative.
rewrite -pvs_open_close; first (apply and_mono; first done); last done.
rewrite -(pvs_open_close E N) //; apply and_mono; first done.
apply wand_intro_l.
(* Oh wow, this is annyoing... *)
rewrite always_and_sep_r' associative -always_and_sep_r'.
by rewrite /vs always_elim impl_elim_r.
Qed.
Lemma vs_alloc (N : namespace) P : P ={N}=> inv N P.
Lemma vs_alloc (N : namespace) P : P >{N}=> inv N P.
Proof. by intros; apply vs_alt, pvs_alloc. Qed.
End vs.
......@@ -109,16 +109,15 @@ Context {Λ : language} {Σ : gid → iFunctor} (i : gid) `{!InG Λ Σ i A}.
Implicit Types a : A.
Implicit Types P Q R : iProp Λ (globalC Σ).
Lemma vs_own_updateP E γ a (P : A Prop) :
a ~~>: P own i γ a ={E}=> ( a', P a' own i γ a').
Lemma vs_own_updateP E γ a φ :
a ~~>: φ own i γ a >{E}=> a', φ a' own i γ a'.
Proof. by intros; apply vs_alt, own_updateP. Qed.
Lemma vs_own_updateP_empty `{Empty A, !CMRAIdentity A}
E γ (P : A Prop) :
~~>: P True ={E}=> ( a', P a' own i γ a').
Lemma vs_own_updateP_empty `{Empty A, !CMRAIdentity A} E γ φ :
~~>: φ True >{E}=> a', φ a' own i γ a'.
Proof. by intros; eapply vs_alt, own_updateP_empty. Qed.
Lemma vs_update E γ a a' : a ~~> a' own i γ a ={E}=> own i γ a'.
Lemma vs_update E γ a a' : a ~~> a' own i γ a >{E}=> own i γ a'.
Proof. by intros; apply vs_alt, own_update. Qed.
End vs_ghost.
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