From 92d5d562073a47e6107545babe2d30f4f02262e3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 5 Mar 2016 13:39:50 +0100
Subject: [PATCH] define parallel composition and state its spec

---
 _CoqProject     |  1 +
 heap_lang/par.v | 23 +++++++++++++++++++++++
 2 files changed, 24 insertions(+)
 create mode 100644 heap_lang/par.v

diff --git a/_CoqProject b/_CoqProject
index 152f62db8..7c4d0a636 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -82,6 +82,7 @@ heap_lang/derived.v
 heap_lang/heap.v
 heap_lang/notation.v
 heap_lang/spawn.v
+heap_lang/par.v
 heap_lang/tests.v
 heap_lang/substitution.v
 barrier/barrier.v
diff --git a/heap_lang/par.v b/heap_lang/par.v
new file mode 100644
index 000000000..3bbdda8c5
--- /dev/null
+++ b/heap_lang/par.v
@@ -0,0 +1,23 @@
+From heap_lang Require Export heap.
+From heap_lang Require Import spawn notation.
+
+Definition par : val :=
+  λ: "f1" "f2", let: "handle" := ^spawn '"f1" in
+                let: "v2" := '"f2" #() in
+                let: "v1" := ^join '"handle" in
+                Pair '"v1" '"v2".
+Notation Par e1 e2 := (^par (λ: <>, e1)%V (λ: <>, e2)%V)%E.
+
+Section proof.
+Context {Σ : rFunctorG} `{!heapG Σ, !spawnG Σ}.
+Context (heapN N : namespace).
+Local Notation iProp := (iPropG heap_lang Σ).
+
+Lemma par_spec (Ψ1 Ψ2 : val → iProp) (f1 f2 : val) (Φ : val → iProp) :
+  (#> f1 #() {{ Ψ1 }} ★ #> f2 #() {{ Ψ2 }} ★
+   ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ Φ (PairV v1 v2))
+  ⊑ #> par f1 f2 {{ Φ }}.
+Proof.
+Abort.
+
+End proof.
\ No newline at end of file
-- 
GitLab