From 5bb3af05c16a64ffdb9e109031d42a5ee70f87d2 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 3 Jan 2017 17:46:22 +0100
Subject: [PATCH] Adding more automation: extracting from a type context. Also,
 reformulated some of the proof rules, so that they can be applied without the
 consequence rule.

---
 theories/typing/bool.v         |   8 ++-
 theories/typing/borrow.v       |  29 +++++++--
 theories/typing/case.v         |  33 +++++++++-
 theories/typing/cont.v         |   2 +-
 theories/typing/function.v     |  40 ++++++++----
 theories/typing/programs.v     |  32 +++++++---
 theories/typing/type.v         |  13 ++--
 theories/typing/type_context.v | 110 +++++++++++++++++++++++++++++++--
 theories/typing/uniq_bor.v     |  39 ++++++++++--
 9 files changed, 260 insertions(+), 46 deletions(-)

diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 580cd631..a51c6ba3 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -1,3 +1,4 @@
+From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs.
@@ -24,11 +25,12 @@ Section typing.
   Qed.
 
   Lemma type_if E L C T e1 e2 p:
+    (p ◁ bool)%TC ∈ T →
     typed_body E L C T e1 → typed_body E L C T e2 →
-    typed_body E L C ((p ◁ bool) :: T) (if: p then e1 else e2).
+    typed_body E L C T (if: p then e1 else e2).
   Proof.
-    iIntros (He1 He2 tid qE) "#HEAP #LFT Htl HE HL HC".
-    rewrite tctx_interp_cons. iIntros "[Hp HT]".
+    iIntros (Hp He1 He2 tid qE) "#HEAP #LFT Htl HE HL HC HT".
+    iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "#Hp".
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
     iDestruct "Hown" as (b) "Hv". iDestruct "Hv" as %[=->].
     destruct b; wp_if.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index edec4c76..f96250b8 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -25,7 +25,25 @@ Section borrow.
         by iMod ("Hext" with "H†") as "$".
   Qed.
 
-  Lemma type_deref_uniq_own E L κ p n ty :
+  Lemma tctx_extract_hasty_borrow E L p n ty κ T :
+    tctx_extract_hasty E L p (&uniq{κ}ty) ((p ◁ own n ty)::T)
+                       ((p ◁{κ} own n ty)::T).
+  Proof. apply (tctx_incl_frame_r E L _ [_] [_;_]), tctx_borrow. Qed.
+
+  (* See the comment above [tctx_extract_hasty_share] in [uniq_bor.v]. *)
+  Lemma tctx_extract_hasty_borrow_share E L p ty ty' κ n T :
+    lctx_lft_alive E L κ → subtype E L ty' ty →
+    tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ own n ty')::T)
+                       ((p ◁ &shr{κ}ty')::(p ◁{κ} own n ty')::T).
+  Proof.
+    intros. apply (tctx_incl_frame_r E L _ [_] [_;_;_]). etrans.
+    { by apply tctx_borrow. }
+    apply (tctx_incl_frame_r E L _ [_] [_;_]). etrans.
+    by apply tctx_share. etrans. by apply copy_tctx_incl, _.
+    by apply (tctx_incl_frame_r E L _ [_] [_]), subtype_tctx_incl, shr_mono'.
+  Qed.
+
+  Lemma type_deref_uniq_own {E L} κ p n ty :
     lctx_lft_alive E L κ →
     typed_instruction_ty E L [p ◁ &uniq{κ} own n ty] (!p) (&uniq{κ} ty).
   Proof.
@@ -48,7 +66,7 @@ Section borrow.
       rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
   Qed.
 
-  Lemma type_deref_shr_own E L κ p n ty :
+  Lemma type_deref_shr_own {E L} κ p n ty :
     lctx_lft_alive E L κ →
     typed_instruction_ty E L [p ◁ &shr{κ} own n ty] (!p) (&shr{κ} ty).
   Proof.
@@ -65,7 +83,7 @@ Section borrow.
       rewrite tctx_interp_singleton tctx_hasty_val' //. iExists _. auto.
   Qed.
 
-  Lemma type_deref_uniq_uniq E L κ κ' p ty :
+  Lemma type_deref_uniq_uniq {E L} κ κ' p ty :
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
     typed_instruction_ty E L [p ◁ &uniq{κ} &uniq{κ'} ty] (!p) (&uniq{κ} ty).
   Proof.
@@ -95,7 +113,7 @@ Section borrow.
     iApply (lft_incl_glb with "Hincl"). iApply lft_incl_refl.
   Qed.
 
-  Lemma type_deref_shr_uniq E L κ κ' p ty :
+  Lemma type_deref_shr_uniq {E L} κ κ' p ty :
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
     typed_instruction_ty E L [p ◁ &shr{κ} &uniq{κ'} ty] (!p) (&shr{κ} ty).
   Proof.
@@ -119,3 +137,6 @@ Section borrow.
       iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT Hincl' Hshr").
   Qed.
 End borrow.
+
+Hint Resolve tctx_extract_hasty_borrow
+     tctx_extract_hasty_borrow_share : lrust_typing.
diff --git a/theories/typing/case.v b/theories/typing/case.v
index 138b4080..99bb0d84 100644
--- a/theories/typing/case.v
+++ b/theories/typing/case.v
@@ -8,7 +8,7 @@ Section case.
   Context `{typeG Σ}.
 
   (* FIXME : the doc does not give [p +ₗ #(S (ty.(ty_size))) ◁ ...]. *)
-  Lemma type_case_own E L C T p n tyl el:
+  Lemma type_case_own E L C T p n tyl el :
     Forall2 (λ ty e,
       typed_body E L C ((p +ₗ #0 ◁ own n (uninit 1)) :: (p +ₗ #1 ◁ own n ty) ::
          (p +ₗ #(S (ty.(ty_size))) ◁
@@ -49,7 +49,17 @@ Section case.
       iFrame. iExists i, vl', vl''. rewrite /= app_length nth_lookup EQty. auto.
   Qed.
 
-  Lemma type_case_uniq E L C T p κ tyl el:
+  Lemma type_case_own' E L C T T' p n tyl el :
+    tctx_extract_hasty E L p (own n (sum tyl)) T T' →
+    Forall2 (λ ty e,
+      typed_body E L C ((p +ₗ #0 ◁ own n (uninit 1)) :: (p +ₗ #1 ◁ own n ty) ::
+         (p +ₗ #(S (ty.(ty_size))) ◁
+            own n (uninit (list_max (map ty_size tyl) - ty_size ty))) :: T') e ∨
+      typed_body E L C ((p ◁ own n (sum tyl)) :: T') e) tyl el →
+    typed_body E L C T (case: !p of el).
+  Proof. unfold tctx_extract_hasty. intros ->. apply type_case_own. Qed.
+
+  Lemma type_case_uniq E L C T p κ tyl el :
     lctx_lft_alive E L κ →
     Forall2 (λ ty e,
       typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T) e ∨
@@ -97,6 +107,15 @@ Section case.
       iExists _, _. iFrame. iSplit. done. iSplit; iIntros "!>!#$".
   Qed.
 
+  Lemma type_case_uniq' E L C T T' p κ tyl el :
+    tctx_extract_hasty E L p (&uniq{κ}sum tyl) T T' →
+    lctx_lft_alive E L κ →
+    Forall2 (λ ty e,
+      typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T') e ∨
+      typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T') e) tyl el →
+    typed_body E L C T (case: !p of el).
+  Proof. unfold tctx_extract_hasty. intros ->. apply type_case_uniq. Qed.
+
   Lemma type_case_shr E L C T p κ tyl el:
     lctx_lft_alive E L κ →
     Forall2 (λ ty e,
@@ -122,4 +141,14 @@ Section case.
     - iExists _. auto.
     - iExists _. iSplit. done. iExists i. rewrite nth_lookup EQty /=. auto.
   Qed.
+
+  Lemma type_case_shr' E L C T p κ tyl el :
+    (p ◁ &shr{κ}sum tyl)%TC ∈ T →
+    lctx_lft_alive E L κ →
+    Forall2 (λ ty e, typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e) tyl el →
+    typed_body E L C T (case: !p of el).
+  Proof.
+    intros. rewrite ->copy_elem_of_tctx_incl; last done; last apply _.
+    apply type_case_shr; first done. eapply Forall2_impl; first done. auto.
+  Qed.
 End case.
\ No newline at end of file
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 3fc7d459..d708479f 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -19,7 +19,7 @@ Section typing.
     rewrite -{3}(vec_to_list_of_list args). iApply ("HC" with "* Htl HL HT").
   Qed.
 
-  Lemma type_cont E L1 L2 C T argsb econt e2 T' kb :
+  Lemma type_cont L1 {argsb} T' E L2 C T  econt e2 kb :
     Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
     (∀ k args, typed_body E L1 (k ◁cont(L1, T') :: C) (T' args)
                           (subst_v (kb::argsb) (k:::args) econt)) →
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 61a9b237..b3e5e533 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -139,17 +139,16 @@ Section typing.
   Qed.
 
   (* TODO: Define some syntactic sugar for calling and letrec like we do on paper. *)
-  Lemma type_call {A} E L E' T T' p (ps : list path)
+  Lemma type_call {A} E L E' T p (ps : list path)
                         (tys : A → vec type (length ps)) ty k x :
-    tctx_incl E L T (zip_with TCtx_hasty ps (tys x) ++ T') → elctx_sat E L (E' x) →
-    typed_body E L [k ◁cont(L, λ v : vec _ 1, (v!!!0 ◁ ty x) :: T')]
-               ((p ◁ fn E' tys ty) :: T) (p (of_val k :: ps)).
+    elctx_sat E L (E' x) →
+    typed_body E L [k ◁cont(L, λ v : vec _ 1, (v!!!0 ◁ ty x) :: T)]
+               ((p ◁ fn E' tys ty) :: zip_with TCtx_hasty ps (tys x) ++ T)
+               (p (of_val k :: ps)).
   Proof.
-    iIntros (HTsat HEsat tid qE) "#HEAP #LFT Htl HE HL HC".
-    rewrite tctx_interp_cons. iIntros "[Hf HT]".
+    iIntros (HE tid qE) "#HEAP #LFT Htl HE HL HC".
+    rewrite tctx_interp_cons tctx_interp_app. iIntros "(Hf & Hargs & HT)".
     wp_bind p. iApply (wp_hasty with "Hf"). iIntros (v) "% Hf".
-    iMod (HTsat with "LFT HE HL HT") as "(HE & HL & HT)". rewrite tctx_interp_app.
-    iDestruct "HT" as "[Hargs HT']". clear HTsat.
     iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = k⌝):::
                vmap (λ ty (v : val), tctx_elt_interp tid (v ◁ ty)) (tys x))%I
             with "* [Hargs]"); first wp_done.
@@ -167,12 +166,12 @@ Section typing.
       { rewrite -fmap_cons Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
       { rewrite -fmap_cons -(subst_v_eq (fb::kb::xb) (_:::k:::vl)) //. }
       iNext. iSpecialize ("Hf" $! x k vl).
-      iMod (HEsat with "HE HL") as (q') "[HE' Hclose]"; first done.
-      iApply ("Hf" with "HEAP LFT Htl HE' [] [HC Hclose HT']").
+      iMod (HE with "HE HL") as (q') "[HE' Hclose]"; first done.
+      iApply ("Hf" with "HEAP LFT Htl HE' [] [HC Hclose HT]").
       + by rewrite /llctx_interp big_sepL_nil.
       + iIntros "HE'". iApply fupd_cctx_interp. iMod ("Hclose" with "HE'") as "[HE HL]".
         iSpecialize ("HC" with "HE"). iModIntro. iIntros (y) "IN".
-        iDestruct "IN" as %->%elem_of_list_singleton. iIntros (args) "Htl _ HT".
+        iDestruct "IN" as %->%elem_of_list_singleton. iIntros (args) "Htl _ Hret".
         iSpecialize ("HC" with "* []"); first by (iPureIntro; apply elem_of_list_singleton).
         iApply ("HC" $! args with "Htl HL").
         rewrite tctx_interp_singleton tctx_interp_cons. iFrame.
@@ -181,6 +180,23 @@ Section typing.
         iApply (big_sepL_mono' with "Hvl"). by iIntros (i [v ty']).
   Qed.
 
+  Lemma type_call' {A} x E L E' C T T' T'' p (ps : list path)
+                        (tys : A → vec type (length ps)) ty k :
+    (p ◁ fn E' tys ty)%TC ∈ T →
+    elctx_sat E L (E' x) →
+    tctx_extract_ctx E L (zip_with TCtx_hasty ps (tys x)) T T' →
+    (k ◁cont(L, T''))%CC ∈ C →
+    (∀ ret : val, tctx_incl E L ((ret ◁ ty x)::T') (T'' [# ret])) →
+    typed_body E L C T (p (of_val k :: ps)).
+  Proof.
+    intros Hfn HE HTT' HC HT'T''.
+    rewrite -typed_body_mono /flip; last done; first by eapply type_call.
+    - etrans. eapply (incl_cctx_incl _ [_]); first by intros ? ->%elem_of_list_singleton.
+      apply cctx_incl_cons; first done. intros args. inv_vec args=>ret q. inv_vec q. done.
+    - etrans; last by apply (tctx_incl_frame_l _ _ [_]).
+      apply copy_elem_of_tctx_incl; last done. apply _.
+  Qed.
+
   Lemma type_fn {A} E L E' fb kb (argsb : list binder) e
         (tys : A → vec type (length argsb)) ty
         T `{!CopyC T, !SendC T} :
@@ -205,4 +221,4 @@ Section typing.
 End typing.
 
 Hint Resolve fn_subtype_full : lrust_typing.
-Hint Constructors Forall2 : lrust_typing.
+Hint Constructors Forall2 elem_of_list: lrust_typing.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index a4d52d7d..5ce9ce92 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -17,21 +17,21 @@ Section typing.
                WP e {{ _, cont_postcondition }})%I.
   Global Arguments typed_body _%EL _%LL _%CC _%TC _%E.
 
-  Instance typed_body_llctx_permut E :
+  Global Instance typed_body_llctx_permut E :
     Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> (⊢)) (typed_body E).
   Proof.
     intros L1 L2 HL C ? <- T ? <- e ? <-. rewrite /typed_body.
     by setoid_rewrite HL.
   Qed.
 
-  Instance typed_body_elctx_permut :
+  Global Instance typed_body_elctx_permut :
     Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> eq ==> (⊢)) typed_body.
   Proof.
     intros E1 E2 HE L ? <- C ? <- T ? <- e ? <-. rewrite /typed_body.
     by setoid_rewrite HE.
   Qed.
 
-  Instance typed_body_mono E L:
+  Global Instance typed_body_mono E L:
     Proper (flip (cctx_incl E) ==> flip (tctx_incl E L) ==> eq ==> (⊢))
            (typed_body E L).
   Proof.
@@ -42,6 +42,11 @@ Section typing.
     iIntros "HE". by iApply (HC with "LFT HC").
   Qed.
 
+  Global Instance typed_body_mono_flip E L:
+    Proper (cctx_incl E ==> tctx_incl E L ==> eq ==> flip (⊢))
+           (typed_body E L).
+  Proof. intros ?????????. by eapply typed_body_mono. Qed.
+
   (** Instruction *)
   Definition typed_instruction (E : elctx) (L : llctx)
              (T1 : tctx) (e : expr) (T2 : val → tctx) : Prop :=
@@ -79,7 +84,7 @@ Notation typed_instruction_ty E L T1 e ty :=
 Section typing_rules.
   Context `{typeG Σ}.
 
-  Lemma type_let E L T1 T2 T C xb e e' :
+  Lemma type_let E L T1 T2 (T : tctx) C xb e e' :
     Closed (xb :b: []) e' →
     typed_instruction E L T1 e T2 →
     (∀ v : val, typed_body E L C (T2 v ++ T) (subst' xb v e')) →
@@ -93,6 +98,17 @@ Section typing_rules.
     rewrite tctx_interp_app. by iFrame.
   Qed.
 
+  Lemma type_let' E L T T' T1 T2 C xb e e' :
+    Closed (xb :b: []) e' →
+    typed_instruction E L T1 e T2 →
+    tctx_extract_ctx E L T1 T T' →
+    (∀ v : val, typed_body E L C (T2 v ++ T') (subst' xb v e')) →
+    typed_body E L C T (let: xb := e in e').
+  Proof.
+    intros ?? HT ?. unfold tctx_extract_ctx in HT. rewrite ->HT.
+    by eapply type_let.
+  Qed.
+
   Lemma typed_newlft E L C T κs e :
     Closed [] e →
     (∀ κ, typed_body E ((κ ⊑ κs) :: L) C T e) →
@@ -120,7 +136,7 @@ Section typing_rules.
     iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
   Qed.
 
-  Lemma type_assign E L ty1 ty ty1' p1 p2 :
+  Lemma type_assign {E L} ty ty1 ty1' p1 p2 :
     typed_write E L ty1 ty ty1' →
     typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <- p2) (λ _, [p1 ◁ ty1']%TC).
   Proof.
@@ -139,7 +155,7 @@ Section typing_rules.
     rewrite tctx_interp_singleton tctx_hasty_val' //.
   Qed.
 
-  Lemma type_deref E L ty1 ty ty1' p :
+  Lemma type_deref {E L} ty ty1 ty1' p :
     ty.(ty_size) = 1%nat → typed_read E L ty1 ty ty1' →
     typed_instruction E L [p ◁ ty1] (!p) (λ v, [p ◁ ty1'; v ◁ ty]%TC).
   Proof.
@@ -157,7 +173,7 @@ Section typing_rules.
     by iFrame.
   Qed.
 
-  Lemma type_memcpy_iris E qE L qL tid ty1 ty1' ty2 ty2' ty n p1 p2 :
+  Lemma type_memcpy_iris E qE L qL tid ty ty1 ty1' ty2 ty2' n p1 p2 :
     ty.(ty_size) = n → typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
     {{{ heap_ctx ∗ lft_ctx ∗ na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
         tctx_elt_interp tid (p1 ◁ ty1) ∗ tctx_elt_interp tid (p2 ◁ ty2) }}}
@@ -181,7 +197,7 @@ Section typing_rules.
     iMod ("Hcl2" with "Hl2") as "($ & $ & $ & $)". done.
   Qed.
 
-  Lemma type_memcpy E L ty1 ty1' ty2 ty2' ty n p1 p2 :
+  Lemma type_memcpy {E L} ty ty1 ty1' ty2 ty2' n p1 p2 :
     ty.(ty_size) = n → typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
     typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2] (p1 <-{n} !p2)
                       (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
diff --git a/theories/typing/type.v b/theories/typing/type.v
index f1170b38..ce6cdd10 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -79,21 +79,20 @@ Section type.
   Lemma shr_locsE_shrN l n :
     shr_locsE l n ⊆ ↑shrN.
   Proof.
-    revert l; induction n; intros l.
-    - simpl. set_solver+.
-    - simpl. apply union_least; last by auto. solve_ndisj.
+    revert l; induction n=>l /=; first by set_solver+.
+    apply union_least; last by auto. solve_ndisj.
   Qed.
 
   Lemma shr_locsE_subseteq l n m :
     (n ≤ m)%nat → shr_locsE l n ⊆ shr_locsE l m.
   Proof.
-    induction 1; first done.
-    rewrite ->IHle. rewrite -Nat.add_1_l [(_ + _)%nat]comm_L.
-    rewrite shr_locsE_shift. set_solver+.
+    induction 1; first done. etrans; first done.
+    rewrite -Nat.add_1_l [(_ + _)%nat]comm_L shr_locsE_shift. set_solver+.
   Qed.
 
   Lemma shr_locsE_split_tok l n m tid :
-    na_own tid (shr_locsE l (n + m)) ⊣⊢ na_own tid (shr_locsE l n) ∗ na_own tid (shr_locsE (shift_loc l n) m).
+    na_own tid (shr_locsE l (n + m)) ⊣⊢
+      na_own tid (shr_locsE l n) ∗ na_own tid (shr_locsE (shift_loc l n) m).
   Proof.
     rewrite shr_locsE_shift na_own_union //. apply shr_locsE_disj.
   Qed.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 82706f49..f7d7159e 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -30,6 +30,7 @@ Notation "[ x ]" := (@cons tctx_elt x%TC (@nil tctx_elt)) : lrust_tctx_scope.
 
 Section type_context.
   Context `{typeG Σ}.
+  Implicit Types T : tctx.
 
   Fixpoint eval_path (p : path) : option val :=
     match p with
@@ -181,20 +182,38 @@ Section type_context.
     rewrite /tctx_incl. iIntros (Hc ???) "_ $ $ H". by iApply big_sepL_contains.
   Qed.
 
-  Lemma tctx_incl_frame E L T T1 T2 :
-    tctx_incl E L T2 T1 → tctx_incl E L (T++T2) (T++T1).
+  Lemma tctx_incl_frame E L T11 T12 T21 T22 :
+    tctx_incl E L T11 T12 → tctx_incl E L T21 T22 →
+    tctx_incl E L (T11++T21) (T12++T22).
   Proof.
-    intros Hincl ???. rewrite /tctx_interp !big_sepL_app. iIntros "#LFT HE HL [$ ?]".
-    by iApply (Hincl with "LFT HE HL").
+    intros Hincl1 Hincl2 ???. rewrite /tctx_interp !big_sepL_app.
+    iIntros "#LFT HE HL [H1 H2]".
+    iMod (Hincl1 with "LFT HE HL H1") as "(HE & HL & $)".
+    iApply (Hincl2 with "LFT HE HL H2").
   Qed.
+  Lemma tctx_incl_frame_l E L T T1 T2 :
+    tctx_incl E L T1 T2 → tctx_incl E L (T++T1) (T++T2).
+  Proof. by apply tctx_incl_frame. Qed.
+  Lemma tctx_incl_frame_r E L T T1 T2 :
+    tctx_incl E L T1 T2 → tctx_incl E L (T1++T) (T2++T).
+  Proof. by intros; apply tctx_incl_frame. Qed.
 
   Lemma copy_tctx_incl E L p `{!Copy ty} :
     tctx_incl E L [p ◁ ty] [p ◁ ty; p ◁ ty].
-   Proof.
+  Proof.
     iIntros (???) "_ $ $ *". rewrite /tctx_interp !big_sepL_cons big_sepL_nil.
     by iIntros "[#$ $]".
   Qed.
 
+  Lemma copy_elem_of_tctx_incl E L T p `{!Copy ty} :
+    (p ◁ ty)%TC ∈ T → tctx_incl E L T ((p ◁ ty) :: T).
+  Proof.
+    remember (p ◁ ty)%TC. induction 1 as [|???? IH]; subst.
+    - apply (tctx_incl_frame_r E L _ [_] [_;_]), copy_tctx_incl, _.
+    - etrans. by apply (tctx_incl_frame_l E L [_]), IH, reflexivity.
+      apply contains_tctx_incl, contains_swap.
+  Qed.
+
   Lemma subtype_tctx_incl E L p ty1 ty2 :
     subtype E L ty1 ty2 → tctx_incl E L [p ◁ ty1] [p ◁ ty2].
   Proof.
@@ -206,6 +225,79 @@ Section type_context.
     iApply ("Ho" with "*"). done.
   Qed.
 
+  (* Extracting from a type context. *)
+
+  Definition tctx_extract_hasty E L p ty T T' : Prop :=
+    tctx_incl E L T ((p ◁ ty)::T').
+  Lemma tctx_extract_hasty_cons E L p ty T T' x :
+    tctx_extract_hasty E L p ty T T' →
+    tctx_extract_hasty E L p ty (x::T) (x::T').
+  Proof.
+    move=> /(tctx_incl_frame_l E L [x]) /= Hincl. rewrite /tctx_extract_hasty.
+    etrans; first done. apply contains_tctx_incl, contains_swap.
+  Qed.
+  Lemma tctx_extract_hasty_here_copy E L p ty ty' T `{!Copy ty} :
+    subtype E L ty ty' →
+    tctx_extract_hasty E L p ty' ((p ◁ ty)::T) ((p ◁ ty)::T).
+  Proof.
+    intros. apply (tctx_incl_frame_r E L _ [_] [_;_]).
+    etrans; first by apply copy_tctx_incl, _.
+    by apply (tctx_incl_frame_r E L _ [_] [_]), subtype_tctx_incl.
+  Qed.
+  Lemma tctx_extract_hasty_here E L p ty ty' T :
+    subtype E L ty ty' → tctx_extract_hasty E L p ty' ((p ◁ ty)::T) T.
+  Proof.
+    intros. apply (tctx_incl_frame_r E L _ [_] [_]).
+    by apply subtype_tctx_incl.
+  Qed.
+
+  Definition tctx_extract_blocked E L p κ ty T T' : Prop :=
+    tctx_incl E L T ((p ◁{κ} ty)::T').
+  Lemma tctx_extract_blocked_cons E L p κ ty T T' x :
+    tctx_extract_blocked E L p κ ty T T' →
+    tctx_extract_blocked E L p κ ty (x::T) (x::T').
+  Proof.
+    move=> /(tctx_incl_frame_l E L [x]) /= Hincl. rewrite /tctx_extract_blocked.
+    etrans; first done. apply contains_tctx_incl, contains_swap.
+  Qed.
+  Lemma tctx_extract_blocked_here E L p κ ty T :
+    tctx_extract_blocked E L p κ ty ((p ◁{κ} ty)::T) T.
+  Proof. intros. by apply (tctx_incl_frame_r E L _ [_] [_]). Qed.
+
+  Definition tctx_extract_ctx E L T T1 T2 : Prop :=
+    tctx_incl E L T1 (T++T2).
+  Lemma tctx_extract_ctx_nil E L T:
+    tctx_extract_ctx E L [] T T.
+  Proof. by unfold tctx_extract_ctx. Qed.
+  Lemma tctx_extract_ctx_hasty E L T T1 T2 T3 p ty:
+    tctx_extract_hasty E L p ty T1 T2 → tctx_extract_ctx E L T T2 T3 →
+    tctx_extract_ctx E L ((p ◁ ty)::T) T1 T3.
+  Proof.
+    intros. rewrite /tctx_extract_ctx. etrans; first done.
+    by apply (tctx_incl_frame_l _ _ [_]).
+  Qed.
+  Lemma tctx_extract_ctx_blocked E L T T1 T2 T3 p κ ty:
+    tctx_extract_blocked E L p κ ty T1 T2 → tctx_extract_ctx E L T T2 T3 →
+    tctx_extract_ctx E L ((p ◁{κ} ty)::T) T1 T3.
+  Proof.
+    intros. rewrite /tctx_extract_ctx. etrans; first done.
+    by apply (tctx_incl_frame_l _ _ [_]).
+  Qed.
+
+  Lemma tctx_extract_ctx_incl E L T T' T0:
+    tctx_extract_ctx E L T' T T0 →
+    tctx_incl E L T T'.
+  Proof.
+    intros. etrans; first done. rewrite {2}(app_nil_end T').
+    apply tctx_incl_frame_l, contains_tctx_incl, contains_nil_l.
+  Qed.
+
+  (* Unblocking a type context. *)
+  (* TODO : That would be great if this could also remove all the
+     instances mentionning the lifetime in question.
+     E.g., if [p ◁ &uniq{κ} ty] should be removed, because this is now
+     useless. *)
+
   Class UnblockTctx (κ : lft) (T1 T2 : tctx) : Prop :=
     unblock_tctx : ∀ tid, [†κ] -∗ tctx_interp tid T1 ={⊤}=∗ tctx_interp tid T2.
 
@@ -228,3 +320,11 @@ Section type_context.
     by iMod (H12 with "H† HT1") as "$".
   Qed.
 End type_context.
+
+Hint Resolve tctx_extract_hasty_here_copy : lrust_tctx_scope.
+Hint Resolve tctx_extract_hasty_here | 50 : lrust_tctx_scope.
+Hint Resolve tctx_extract_hasty_cons | 100 : lrust_tctx_scope.
+Hint Extern 1 (Copy _) => typeclasses eauto : lrust_tctx_scope.
+Hint Resolve tctx_extract_blocked_here tctx_extract_blocked_cons
+             tctx_extract_ctx_nil tctx_extract_ctx_hasty
+             tctx_extract_ctx_blocked tctx_extract_ctx_incl : lrust_tctx_scope.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index eaa3d752..6795ade5 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -166,7 +166,7 @@ Section typing.
 
   Lemma tctx_reborrow_uniq E L p ty κ κ' :
     lctx_lft_incl E L κ' κ →
-    tctx_incl E L [p ◁ &uniq{κ}ty] [p ◁ &uniq{κ'}ty; p ◁{κ} &uniq{κ}ty].
+    tctx_incl E L [p ◁ &uniq{κ}ty] [p ◁ &uniq{κ'}ty; p ◁{κ'} &uniq{κ}ty].
   Proof.
     iIntros (Hκκ' tid ??) "#LFT HE HL H".
     iDestruct (elctx_interp_persist with "HE") as "#HE'".
@@ -177,11 +177,41 @@ Section typing.
     iDestruct "EQ" as %[=->]. iMod (bor_iff with "LFT [] Hb") as "Hb". done. by eauto.
     iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]". done. iModIntro. iSplitL "Hb".
     - iExists _. iSplit. done. iExists _, _. erewrite <-uPred.iff_refl. eauto.
-    - iExists _. iSplit. done. iIntros "#H†".
-      iMod ("Hext" with ">[]") as "Hb". by iApply (lft_incl_dead with "Hκκ' H†").
+    - iExists _. iSplit. done. iIntros "#H†". iMod ("Hext" with "H†") as "Hb".
       iExists _, _. erewrite <-uPred.iff_refl. eauto.
   Qed.
 
+  (* When sharing during extraction, we do the (arbitrary) choice of
+     sharing at the lifetime requested (κ). In some cases, we could
+     actually desire a longer lifetime and then use subtyping, because
+     then we get, in the environment, a shared borrow at this longer
+     lifetime.
+
+     In the case the user wants to do the sharing at a longer
+     lifetime, she has to manually perform the extraction herself at
+     the desired lifetime. *)
+  Lemma tctx_extract_hasty_share E L p ty ty' κ κ' T :
+    lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' → subtype E L ty' ty →
+    tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ &uniq{κ'}ty')::T)
+                       ((p ◁ &shr{κ}ty')::(p ◁{κ} &uniq{κ'}ty')::T).
+  Proof.
+    intros. apply (tctx_incl_frame_r E L _ [_] [_;_;_]). etrans.
+    { by apply tctx_reborrow_uniq. }
+    apply (tctx_incl_frame_r E L _ [_] [_;_]). etrans.
+    by apply tctx_share. etrans. by apply copy_tctx_incl, _.
+    by apply (tctx_incl_frame_r E L _ [_] [_]), subtype_tctx_incl, shr_mono'.
+  Qed.
+
+  Lemma tctx_extract_hasty_reborrow E L p ty ty' κ κ' T :
+    lctx_lft_incl E L κ' κ → eqtype E L ty ty' →
+    tctx_extract_hasty E L p (&uniq{κ'}ty) ((p ◁ &uniq{κ}ty')::T)
+                       ((p ◁{κ'} &uniq{κ}ty')::T).
+  Proof.
+    intros. apply (tctx_incl_frame_r E L _ [_] [_;_]). etrans.
+    by apply tctx_reborrow_uniq.
+    by apply (tctx_incl_frame_r E L _ [_] [_]), subtype_tctx_incl, uniq_mono'.
+  Qed.
+
   Lemma read_uniq E L κ ty :
     Copy ty → lctx_lft_alive E L κ → typed_read E L (&uniq{κ}ty) ty (&uniq{κ}ty).
   Proof.
@@ -216,4 +246,5 @@ Section typing.
   Qed.
 End typing.
 
-Hint Resolve uniq_mono' uniq_proper' : lrust_typing.
+Hint Resolve uniq_mono' uniq_proper' tctx_extract_hasty_share
+             tctx_extract_hasty_reborrow : lrust_typing.
-- 
GitLab