From 8ba197a127a15f659463b879fff5a09945454876 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 11 Feb 2017 12:30:50 +0100
Subject: [PATCH] show join_handle_subtype inside the logic

---
 theories/typing/type.v         |  1 +
 theories/typing/unsafe/spawn.v | 19 ++++++++++++-------
 2 files changed, 13 insertions(+), 7 deletions(-)

diff --git a/theories/typing/type.v b/theories/typing/type.v
index 5a8ba446..86459792 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -353,6 +353,7 @@ Section subtyping.
 
   Definition subtype (ty1 ty2 : type) : Prop :=
     lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗ type_incl ty1 ty2.
+  (* TODO RJ: I'd really like to get rid of this definition. *)
   Definition ctx_eq {A} (x1 x2 : A) : Prop :=
     lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗ ⌜x1 = x2⌝.
 
diff --git a/theories/typing/unsafe/spawn.v b/theories/typing/unsafe/spawn.v
index b140d744..aa79c626 100644
--- a/theories/typing/unsafe/spawn.v
+++ b/theories/typing/unsafe/spawn.v
@@ -32,17 +32,22 @@ Section join_handle.
     iIntros (?) "* _ _ _". auto.
   Qed.
 
+  Lemma join_handle_subtype ty1 ty2 :
+    type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).
+  Proof.
+    iIntros "#Hincl". iSplit; first done. iSplit; iAlways.
+    - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try by iDestruct "Hvl" as "[]".
+      iDestruct "Hvl" as (ty) "[Hincl' ?]". iExists ty. iFrame.
+      iApply (type_incl_trans with "Hincl'"). done.
+    - iIntros "* _". auto.
+  Qed.
+
   Global Instance join_handle_mono E L :
     Proper (subtype E L ==> subtype E L) join_handle.
   Proof.
-    iIntros (ty1 ty2 Hsub) "#? #? #?". iSplit; last iSplit; first done.
-    - iIntros "!# * Hvl". destruct vl as [|[[|vl|]|] [|]]; try by iDestruct "Hvl" as "[]".
-      iDestruct "Hvl" as (ty) "[Hincl ?]". iExists ty. iFrame.
-      iApply (type_incl_trans with "Hincl").
-      iDestruct (Hsub with "[] [] []") as "$"; done.
-    - iIntros "!# * _". auto.
+    iIntros (ty1 ty2 Hsub) "#? #? #?". iApply join_handle_subtype.
+    iApply Hsub; done.
   Qed.
-
   Global Instance join_handle_proper E L :
     Proper (eqtype E L ==> eqtype E L) join_handle.
   Proof. intros ??[]. by split; apply join_handle_mono. Qed.
-- 
GitLab