From 0502f30bfaff2cd06b3efcd1522dbcadc9a11eec Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 18 Jun 2016 00:16:17 +0200
Subject: [PATCH] Remove lviewshifts.v and turn them into notations.

---
 _CoqProject                  |  1 -
 program_logic/ectx_lifting.v |  2 +-
 program_logic/invariants.v   |  2 +-
 program_logic/lifting.v      |  2 +-
 program_logic/lviewshifts.v  | 23 -----------------------
 program_logic/pviewshifts.v  |  7 +++++++
 tests/proofmode.v            |  2 +-
 7 files changed, 11 insertions(+), 28 deletions(-)
 delete mode 100644 program_logic/lviewshifts.v

diff --git a/_CoqProject b/_CoqProject
index 7aee7017a..d8f6edf73 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 fd0df37bf..ff70ca4dc 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 e4fe069c4..3037ced25 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 d2b80d543..37ac7b522 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 694d15330..000000000
--- 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 f045dc2c0..d5c21073b 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 9301a91b9..24edb16fc 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] |==>").
-- 
GitLab