From dffd84ad1a7d624220442d309d3e80ba52cb9cde Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 22 Mar 2017 15:59:08 +0100
Subject: [PATCH] Add lemma [lctx_lft_alive_external], which is useful for
 automation.

---
 theories/typing/lft_contexts.v | 10 ++++++++--
 theories/typing/lib/option.v   |  6 +++---
 2 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 37c358ac..1e5514c0 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -216,7 +216,13 @@ Section lft_contexts.
     iExists q''. iIntros "{$Htok}!>Htok". iApply ("Hclose" with "[> -]").
     by iApply "Hclose'".
   Qed.
-  
+
+  Lemma lctx_lft_alive_external κ κ':
+    (κ ⊑ κ')%EL ∈ E → lctx_lft_alive κ → lctx_lft_alive κ'.
+  Proof.
+    intros. by eapply lctx_lft_alive_incl, lctx_lft_incl_external.
+  Qed.
+
   Lemma lctx_lft_alive_list κs ϝ `{!frac_borG Σ} :
     Forall lctx_lft_alive κs →
     ∀ (F : coPset) (qL : Qp),
@@ -305,7 +311,7 @@ Hint Resolve of_val_unlock : lrust_typing.
 Hint Resolve
      lctx_lft_incl_relf lctx_lft_incl_static lctx_lft_incl_local'
      lctx_lft_incl_external'
-     lctx_lft_alive_static lctx_lft_alive_local
+     lctx_lft_alive_static lctx_lft_alive_local lctx_lft_alive_external
      elctx_sat_nil elctx_sat_lft_incl elctx_sat_app elctx_sat_refl
   : lrust_typing.
 Hint Resolve elctx_sat_cons_weaken elctx_sat_app_weaken_l elctx_sat_app_weaken_r
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index e95e0aa0..68ab6ea0 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -54,10 +54,10 @@ Section option.
         return: ["r"]].
 
   Lemma option_unwrap_or_type Ï„ :
-    typed_val (option_unwrap_or τ) (fn([]; option τ, τ) → τ).
+    typed_val (option_unwrap_or τ) (fn((λ ϝ, []); option τ, τ) → τ).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
-      inv_vec p=>o def. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([] ϝ ret p). inv_vec p=>o def. simpl_subst.
     iApply type_case_own; [solve_typing|]. constructor; last constructor; last constructor.
     + right. iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing.
-- 
GitLab