remove unused file type_incl

_CoqProject

@@ -24,7 +24,6 @@ theories/lang/races.v
 theories/lang/tactics.v
 theories/lang/wp_tactics.v
 theories/typing/type.v
-theories/typing/type_incl.v
 theories/typing/perm.v
 theories/typing/typing.v
 theories/typing/lft_contexts.v

theories/typing/function.v

@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Import hoare.
 From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
-From lrust.typing Require Import type_incl typing lft_contexts type_context cont_context.
+From lrust.typing Require Import typing lft_contexts type_context cont_context.
 
 Section fn.
   Context `{typeG Σ}.

theories/typing/product.v

 From iris.proofmode Require Import tactics.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
-From lrust.typing Require Import perm type_incl.
+From lrust.typing Require Import perm.
 
 Section product.
   Context `{typeG Σ}.

theories/typing/sum.v

 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import fractional.
 From lrust.lifetime Require Import borrow frac_borrow.
-From lrust.typing Require Export type.
-From lrust.typing Require Import type_incl.
+From lrust.typing Require Export type perm.
 
 Section sum.
   Context `{typeG Σ}.

theories/typing/type_incl.v

-From iris.base_logic Require Import big_op.
-From iris.program_logic Require Import hoare.
-From lrust.typing Require Export type perm.
-From lrust.lifetime Require Import frac_borrow borrow.
-
-Section ty_incl.
-  Context `{typeG Σ}.
-
-  Definition ty_incl (ρ : perm) (ty1 ty2 : type) :=
-    ∀ tid, lft_ctx -∗ ρ tid ={⊤}=∗
-      (□ ∀ vl, ty1.(ty_own) tid vl → ty2.(ty_own) tid vl) ∗
-      (□ ∀ κ E l, ty1.(ty_shr) κ tid E l →
-       (* [ty_incl] needs to prove something about the length of the
-          object when it is shared. We place this property under the
-          hypothesis that [ty2.(ty_shr)] holds, so that the [!] type
-          is still included in any other. *)
-                  ty2.(ty_shr) κ tid E l ∗ ⌜ty1.(ty_size) = ty2.(ty_size)⌝).
-
-  Lemma ty_incl_trans ρ θ ty1 ty2 ty3 :
-    ty_incl ρ ty1 ty2 → ty_incl θ ty2 ty3 → ty_incl (ρ ∗ θ) ty1 ty3.
-  Proof.
-    iIntros (H12 H23 tid) "#LFT [H1 H2]".
-    iMod (H12 with "LFT H1") as "[#H12 #H12']".
-    iMod (H23 with "LFT H2") as "[#H23 #H23']".
-    iModIntro; iSplit; iIntros "!#*H1".
-    - by iApply "H23"; iApply "H12".
-    - iDestruct ("H12'" $! _ _ _ with "H1") as "[H2 %]".
-      iDestruct ("H23'" $! _ _ _ with "H2") as "[$ %]".
-      iPureIntro. congruence.
-  Qed.
-
-  Lemma ty_incl_weaken ρ θ ty1 ty2 :
-    ρ ⇒ θ → ty_incl θ ty1 ty2 → ty_incl ρ ty1 ty2.
-  Proof.
-    iIntros (Hρθ Hρ' tid) "#LFT H". iApply (Hρ' with "LFT>"). iApply (Hρθ with "LFT H").
-  Qed.
-
-  Lemma ty_incl_perm_incl ρ ty1 ty2 ν :
-    ty_incl ρ ty1 ty2 → ρ ∗ ν ◁ ty1 ⇒ ν ◁ ty2.
-  Proof.
-    iIntros (Hincl tid) "#LFT [Hρ Hty1]". iMod (Hincl with "LFT Hρ") as "[#Hownincl _]".
-    unfold has_type. destruct (eval_expr ν); last done. by iApply "Hownincl".
-  Qed.
-End ty_incl.
\ No newline at end of file