From e6a4bef441f94f5888dc5ccb4710bced79aa7178 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 8 Aug 2018 17:17:51 +0200
Subject: [PATCH] also prove faking a shared uniq ref

---
 _CoqProject                           |  2 +-
 theories/typing/lib/fake_shared.v     | 66 +++++++++++++++++++++++++++
 theories/typing/lib/fake_shared_box.v | 36 ---------------
 3 files changed, 67 insertions(+), 37 deletions(-)
 create mode 100644 theories/typing/lib/fake_shared.v
 delete mode 100644 theories/typing/lib/fake_shared_box.v

diff --git a/_CoqProject b/_CoqProject
index 34b5eeb8..7ebac333 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -53,7 +53,7 @@ theories/typing/typing.v
 theories/typing/soundness.v
 theories/typing/lib/panic.v
 theories/typing/lib/option.v
-theories/typing/lib/fake_shared_box.v
+theories/typing/lib/fake_shared.v
 theories/typing/lib/cell.v
 theories/typing/lib/spawn.v
 theories/typing/lib/join.v
diff --git a/theories/typing/lib/fake_shared.v b/theories/typing/lib/fake_shared.v
new file mode 100644
index 00000000..7d50663f
--- /dev/null
+++ b/theories/typing/lib/fake_shared.v
@@ -0,0 +1,66 @@
+From iris.proofmode Require Import tactics.
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section fake_shared.
+  Context `{typeG Σ}.
+
+  Definition fake_shared_box : val :=
+    funrec: <> ["x"] := Skip ;; return: ["x"].
+
+  Lemma fake_shared_box_type ty `{!TyWf ty} :
+    typed_val fake_shared_box
+      (fn(∀ '(α, β), ∅; &shr{α}(&shr{β} ty)) → &shr{α}(box ty)).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk HT".
+    rewrite tctx_interp_singleton tctx_hasty_val.
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    iAssert (▷ ty_own (own_ptr 1 (&shr{α}(box ty))) tid [x])%I with "[HT]" as "HT".
+    { destruct x as [[|l|]|]=>//=. iDestruct "HT" as "[H $]".
+      iNext. iDestruct "H" as ([|[[]|][]]) "[H↦ H]"; try done.
+      iExists _. iFrame. iDestruct "H" as (vl) "[#Hf H]".
+      iNext. destruct vl as [|[[|l'|]|][]]; try done. iExists l'. iSplit.
+      { iApply frac_bor_iff; last done. iIntros "!>!# *".
+        rewrite heap_mapsto_vec_singleton. iSplit; auto. }
+      iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
+      simpl. by iApply ty_shr_mono. }
+    do 2 wp_seq.
+    iApply (type_type [] _ _ [ x ◁ box (&shr{α}(box ty)) ]
+            with "[] LFT [] Hna HL Hk [HT]"); last first.
+    { by rewrite tctx_interp_singleton tctx_hasty_val. }
+    { by rewrite /elctx_interp. }
+    iApply type_jump; simpl; solve_typing.
+  Qed.
+
+  Definition fake_shared_uniq : val :=
+    funrec: <> ["x"] := Skip ;; return: ["x"].
+
+  Lemma fake_shared_uniq_type ty `{!TyWf ty} :
+    typed_val fake_shared_box
+      (fn(∀ '(α, β), ∅; &shr{α}(&shr{β} ty)) → &shr{α}(&uniq{β} ty)).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk HT".
+    rewrite tctx_interp_singleton tctx_hasty_val.
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    (* FIXME: WTF, using &uniq{β} here does not work. *)
+    iAssert (▷ ty_own (own_ptr 1 (&shr{α} (uniq_bor β ty))) tid [x])%I with "[HT]" as "HT".
+    { destruct x as [[|l|]|]=>//=. iDestruct "HT" as "[H $]".
+      iNext. iDestruct "H" as ([|[[]|][]]) "[H↦ H]"; try done.
+      iExists _. iFrame. iDestruct "H" as (vl) "[#Hf H]".
+      iNext. destruct vl as [|[[|l'|]|][]]; try done. iExists l'. iSplit.
+      { iApply frac_bor_iff; last done. iIntros "!>!# *".
+        rewrite heap_mapsto_vec_singleton. iSplit; auto. }
+      iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
+      simpl. iApply ty_shr_mono; last done. iApply lft_intersect_incl_l. }
+    do 2 wp_seq.
+    iApply (type_type [] _ _ [ x ◁ box (&shr{α}(&uniq{β} ty)) ]
+            with "[] LFT [] Hna HL Hk [HT]"); last first.
+    { by rewrite tctx_interp_singleton tctx_hasty_val. }
+    { by rewrite /elctx_interp. }
+    iApply type_jump; simpl; solve_typing.
+  Qed.
+End fake_shared.
diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
deleted file mode 100644
index d6cb31f4..00000000
--- a/theories/typing/lib/fake_shared_box.v
+++ /dev/null
@@ -1,36 +0,0 @@
-From iris.proofmode Require Import tactics.
-From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
-
-Section fake_shared_box.
-  Context `{typeG Σ}.
-
-  Definition fake_shared_box : val :=
-    funrec: <> ["x"] := Skip ;; return: ["x"].
-
-  Lemma fake_shared_box_type ty `{!TyWf ty} :
-    typed_val fake_shared_box
-      (fn(∀ '(α, β), ∅; &shr{α}(&shr{β} ty)) → &shr{α}(box ty)).
-  Proof.
-    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk HT".
-    rewrite tctx_interp_singleton tctx_hasty_val.
-    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
-    iAssert (▷ ty_own (own_ptr 1 (&shr{α}(box ty))) tid [x])%I with "[HT]" as "HT".
-    { destruct x as [[|l|]|]=>//=. iDestruct "HT" as "[H $]".
-      iNext. iDestruct "H" as ([|[[]|][]]) "[H↦ H]"; try done.
-      iExists _. iFrame. iDestruct "H" as (vl) "[#Hf H]".
-      iNext. destruct vl as [|[[|l'|]|][]]; try done. iExists l'. iSplit.
-      { iApply frac_bor_iff; last done. iIntros "!>!# *".
-        rewrite heap_mapsto_vec_singleton. iSplit; auto. }
-      iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
-      by iApply ty_shr_mono. }
-    do 2 wp_seq.
-    iApply (type_type [] _ _ [ x ◁ box (&shr{α}(box ty)) ]
-            with "[] LFT [] Hna HL Hk [HT]"); last first.
-    { by rewrite tctx_interp_singleton tctx_hasty_val. }
-    { by rewrite /elctx_interp. }
-    iApply type_jump; simpl; solve_typing.
-  Qed.
-End fake_shared_box.
-- 
GitLab