From 55a04c5f2f750704b2c8b566e13e5fa79cde4931 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 10 Feb 2016 01:16:32 +0100
Subject: [PATCH] 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.
---
 program_logic/hoare.v         |  4 +--
 program_logic/hoare_lifting.v |  4 +--
 program_logic/viewshifts.v    | 63 +++++++++++++++++------------------
 3 files changed, 35 insertions(+), 36 deletions(-)

diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index c3c44ac3a..ec2e3edf4 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -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.
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index 74afe875c..aa72735a1 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -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 }}.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 08f8db3bc..f238f45c5 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -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.
-- 
GitLab