From 4e2dfc4e38baf49a3f9dbda2f453c5a848a2dc64 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Apr 2016 01:01:24 +0200
Subject: [PATCH] Get rid of overlapping notations for Par.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Par is now defined as an expression of type [∀ X, expr X] (instead of a
value) and we prove that it is stable under weakening and substitution.
---
 heap_lang/lib/assert.v   |  8 ++++----
 heap_lang/lib/par.v      | 18 ++++++++++--------
 heap_lang/substitution.v |  7 +++++++
 3 files changed, 21 insertions(+), 12 deletions(-)

diff --git a/heap_lang/lib/assert.v b/heap_lang/lib/assert.v
index 1f12a4ef0..0e810633f 100644
--- a/heap_lang/lib/assert.v
+++ b/heap_lang/lib/assert.v
@@ -4,12 +4,12 @@ From iris.heap_lang Require Import wp_tactics substitution notation.
 Definition Assert {X} (e : expr X) : expr X :=
   if: e then #() else #0 #0. (* #0 #0 is unsafe *)
 
+Instance do_wexpr_assert {X Y} (H : X `included` Y) e er :
+  WExpr H e er → WExpr H (Assert e) (Assert er) := _.
 Instance do_wsubst_assert {X Y} x es (H : X `included` x :: Y) e er :
-  WSubst x es H e er → WSubst x es H (Assert e) (Assert er) | 1.
+  WSubst x es H e er → WSubst x es H (Assert e) (Assert er).
 Proof. intros; red. by rewrite /Assert /wsubst -/wsubst; f_equal/=. Qed.
-Instance do_wexpr_assert {X Y} (H : X `included` Y) e er :
-  WExpr H e er → WExpr H (Assert e) (Assert er) | 1.
-Proof. intros; red. by rewrite /Assert /wexpr -/wexpr; f_equal/=. Qed.
+Typeclasses Opaque Assert.
 
 Lemma wp_assert {Σ} (Φ : val → iProp heap_lang Σ) :
   ▷ Φ #() ⊢ WP Assert #true {{ Φ }}.
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index 962e6c1e2..94df194bf 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -2,18 +2,20 @@ From iris.heap_lang Require Export spawn.
 From iris.heap_lang Require Import proofmode notation.
 Import uPred.
 
-Definition par : val :=
+Definition par {X} : expr X :=
   λ: "fs",
     let: "handle" := ^spawn (Fst '"fs") in
     let: "v2" := Snd '"fs" #() in
     let: "v1" := ^join '"handle" in
     Pair '"v1" '"v2".
-Notation Par e1 e2 := (^par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
-Notation ParV e1 e2 := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
-(* We want both par and par^ to print like this. *)
-Infix "||" := ParV : expr_scope.
+Notation Par e1 e2 := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
 Infix "||" := Par : expr_scope.
 
+Instance do_wexpr_assert {X Y} (H : X `included` Y) : WExpr H par par := _.
+Instance do_wsubst_assert {X Y} x es (H : X `included` x :: Y) :
+  WSubst x es H par par := do_wsubst_closed _ x es H _.
+Typeclasses Opaque par.
+
 Section proof.
 Context {Σ : gFunctors} `{!heapG Σ, !spawnG Σ}.
 Context (heapN N : namespace).
@@ -25,19 +27,19 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp) e (f1 f2 : val) (Φ : val → iProp) :
    ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
   ⊢ WP par e {{ Φ }}.
 Proof.
-  iIntros {??} "(#Hh&Hf1&Hf2&HΦ)". wp_value. wp_let. wp_proj.
+  iIntros {??} "(#Hh&Hf1&Hf2&HΦ)". rewrite /par. wp_value. wp_let. wp_proj.
   wp_apply spawn_spec; try wp_done. iFrame "Hf1 Hh".
   iIntros {l} "Hl". wp_let. wp_proj. wp_focus (f2 _).
   iApply wp_wand_l; iFrame "Hf2"; iIntros {v} "H2". wp_let.
   wp_apply join_spec; iFrame "Hl". iIntros {w} "H1".
-  iSpecialize "HΦ" "-"; first by iSplitL "H1". wp_let. by iPvsIntro.
+  iSpecialize "HΦ" "-"; first by iSplitL "H1". by wp_let.
 Qed.
 
 Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) :
   heapN ⊥ N →
   (heap_ctx heapN ★ WP e1 {{ Ψ1 }} ★ WP e2 {{ Ψ2 }} ★
    ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
-  ⊢ WP ParV e1 e2 {{ Φ }}.
+  ⊢ WP e1 || e2 {{ Φ }}.
 Proof.
   iIntros {?} "(#Hh&H1&H2&H)". iApply par_spec; auto.
   iFrame "Hh H". iSplitL "H1"; by wp_let.
diff --git a/heap_lang/substitution.v b/heap_lang/substitution.v
index 7dfaee028..e8da21dfe 100644
--- a/heap_lang/substitution.v
+++ b/heap_lang/substitution.v
@@ -85,6 +85,13 @@ Class WSubst {X Y} (x : string) (es : expr []) H (e : expr X) (er : expr Y) :=
   do_wsubst : wsubst x es H e = er.
 Hint Mode WSubst + + + + + + - : typeclass_instances.
 
+Lemma do_wsubst_closed (e: ∀ {X}, expr X) {X Y} x es (H : X `included` x :: Y) :
+  (∀ X, WExpr (included_nil X) e e) → WSubst x es H e e.
+Proof.
+  rewrite /WSubst /WExpr=> He. rewrite -(He X) wsubst_wexpr'.
+  by rewrite (wsubst_closed _ _ _ _ _ (included_nil _)); last set_solver.
+Qed.
+
 (* Variables *)
 Lemma do_wsubst_var_eq {X Y x es} {H : X `included` x :: Y} `{VarBound x X} er :
   WExpr (included_nil _) es er → WSubst x es H (Var x) er.
-- 
GitLab