From 8062c1680ef2202f7e866965a0576e73e1692ba3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 26 May 2020 14:39:31 +0200
Subject: [PATCH] Typing rule for `Free`.

---
 opam                                |  2 +-
 theories/logrel/term_typing_rules.v | 11 +++++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/opam b/opam
index 48e7874..92354b9 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
 depends: [
-  "coq-iris" { (= "dev.2020-05-24.1.76bec8b7") | (= "dev") }
+  "coq-iris" { (= "dev.2020-05-26.1.d80e7abf") | (= "dev") }
 ]
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 1f15a0c..acf6978 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -271,6 +271,17 @@ Section properties.
     iExists l, v; iSplit=>//. iFrame "Hv Hl".
   Qed.
 
+  Lemma ltyped_free Γ1 Γ2 e A :
+    (Γ1 ⊨ e : ref_uniq A ⫤ Γ2) -∗
+    (Γ1 ⊨ Free e : () ⫤ Γ2).
+  Proof.
+    iIntros "#He" (vs) "!> HΓ1 /=".
+    wp_bind (subst_map vs e).
+    iApply (wp_wand with "(He HΓ1)"). iIntros (v) "[Hv HΓ2]".
+    iDestruct "Hv" as (l w ->) "[Hl Hw]".
+    wp_free. by iFrame "HΓ2".
+  Qed.
+
   Lemma ltyped_load Γ (x : string) A :
     Γ !! x = Some (ref_uniq A)%lty →
     ⊢ Γ ⊨ ! x : A ⫤ <[x := (ref_uniq (copy- A))%lty]> Γ.
-- 
GitLab