From 8d0e07efba91877e3e05aba43cecd8600f2bafcc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 15 Mar 2016 09:59:37 +0100
Subject: [PATCH] add the code of the join-existentials example

---
 _CoqProject                      | 1 +
 examples/joining_extistentials.v | 7 +++++++
 heap_lang/lang.v                 | 8 ++++++--
 heap_lang/notation.v             | 1 +
 4 files changed, 15 insertions(+), 2 deletions(-)
 create mode 100644 examples/joining_extistentials.v

diff --git a/_CoqProject b/_CoqProject
index fc1fc44d4..8fce989b5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -95,3 +95,4 @@ barrier/specification.v
 barrier/protocol.v
 barrier/proof.v
 barrier/client.v
+examples/joining_existentials.v
diff --git a/examples/joining_extistentials.v b/examples/joining_extistentials.v
new file mode 100644
index 000000000..f5fd98f89
--- /dev/null
+++ b/examples/joining_extistentials.v
@@ -0,0 +1,7 @@
+From iris.program_logic Require Import saved_one_shot.
+From iris.barrier Require Import proof specification.
+From iris.heap_lang Require Import notation par.
+
+Definition client (eM eW1 eW2 : expr []) : expr [] :=
+  (let: "b" := newbarrier #() in (^^eM ;; ^signal '"b") ||
+                              ((^wait '"b" ;; ^^eW1) || (^wait '"b" ;; ^^eW2))).
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index b8af35558..b72e354de 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -228,6 +228,10 @@ Program Fixpoint wexpr {X Y} (H : X `included` Y) (e : expr X) : expr Y :=
   end.
 Solve Obligations with set_solver.
 
+Program Definition wexpr' {X} (e : expr []) : expr X :=
+  wexpr _ e.
+Solve Obligations with set_solver.
+
 Definition of_val' {X} (v : val) : expr X := wexpr (included_nil _) (of_val v).
 
 Lemma wsubst_rec_true_prf {X Y x} (H : X `included` x :: Y) {f y}
@@ -242,7 +246,7 @@ Proof. move: Hfy=>/not_and_l [/dec_stable|/dec_stable]; set_solver. Qed.
 Program Fixpoint wsubst {X Y} (x : string) (es : expr [])
     (H : X `included` x :: Y) (e : expr X)  : expr Y :=
   match e return expr Y with
-  | Var y _ => if decide (x = y) then wexpr _ es else @Var _ y _
+  | Var y _ => if decide (x = y) then wexpr' es else @Var _ y _
   | Rec f y e =>
      Rec f y $ match decide (BNamed x ≠ f ∧ BNamed x ≠ y) return _ with
                | left Hfy => wsubst x es (wsubst_rec_true_prf H Hfy) e
@@ -390,7 +394,7 @@ Lemma wexpr_wsubst X Y Z x es (H1: X `included` x::Y) (H2: Y `included` Z) H3 e:
 Proof.
   revert Y Z H1 H2 H3.
   induction e; intros; repeat (case_decide || simplify_eq/=);
-    auto using var_proof_irrel, wexpr_wexpr with f_equal.
+    unfold wexpr'; auto using var_proof_irrel, wexpr_wexpr with f_equal.
 Qed.
 Lemma wsubst_wexpr X Y Z x es (H1: X `included` Y) (H2: Y `included` x::Z) H3 e:
   wsubst x es H2 (wexpr H1 e) = wsubst x es H3 e.
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 7632623ff..9e151bb05 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -28,6 +28,7 @@ Notation "% l" := (Loc l) (at level 8, format "% l") : expr_scope.
 
 Notation "' x" := (Var x) (at level 8, format "' x") : expr_scope.
 Notation "^ v" := (of_val' v%V) (at level 8, format "^ v") : expr_scope.
+Notation "^^ e" := (wexpr' e%E) (at level 8, format "^^ e") : expr_scope.
 
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)
-- 
GitLab