make type inclusion a relation in Iris

theories/typing/function.v

@@ -48,8 +48,9 @@ Section fn.
       iDestruct "Hzip" as %(? & ? & ([? ?] & (? & Hty'1 &
         (? & Hty'2 & [=->->])%bind_Some)%bind_Some & [=->->->])%bind_Some)%bind_Some.
       specialize (Htys x). eapply Forall2_lookup_lr in Htys; try done.
-      iApply (Htys.(subtype_own _ _ _ _) with "LFT [] HL0 Hown").
-      rewrite /elctx_interp_0 big_sepL_app. by iSplit.
+      iDestruct (Htys with "* [] [] []") as "(_ & #Ho & _)"; [done| |done|].
+      + rewrite /elctx_interp_0 big_sepL_app. by iSplit.
+      + by iApply "Ho".
   Qed.
 
   Lemma fn_subtype_specialize {A B n} (σ : A → B) E0 L0 E tys ty :

theories/typing/own.v

@@ -102,19 +102,20 @@ Section own.
   Global Instance own_mono E L n :
     Proper (subtype E L ==> subtype E L) (own n).
   Proof.
-    intros ty1 ty2 Hincl. split.
-    - done.
-    - iIntros (??) "#LFT #HE #HL H". iDestruct "H" as (l) "(%&Hmt&H†)". subst.
+    intros ty1 ty2 Hincl. iIntros. iSplit; first done.
+    iDestruct (Hincl with "* [] [] []") as "(_ & #Ho & #Hs)"; [done..|clear Hincl].
+    iSplit; iAlways.
+    - iIntros (??) "H". iDestruct "H" as (l) "(%&Hmt&H†)". subst.
       iExists _. iSplit. done. iDestruct "Hmt" as (vl') "[Hmt Hown]". iNext.
       iDestruct (ty_size_eq with "Hown") as %<-.
-      iDestruct (Hincl.(subtype_own _ _ _ _) with "LFT HE HL Hown") as "Hown".
+      iDestruct ("Ho" with "* Hown") as "Hown".
       iDestruct (ty_size_eq with "Hown") as %<-. iFrame.
       iExists _. by iFrame.
-    - iIntros (????) "#LFT #HE #HL H". iDestruct "H" as (l') "[Hfb #Hvs]".
+    - iIntros (????) "H". iDestruct "H" as (l') "[Hfb #Hvs]".
       iExists l'. iFrame. iIntros "!#". iIntros (F') "%".
       iMod ("Hvs" with "* [%]") as "Hvs'". done. iModIntro. iNext.
       iMod "Hvs'" as "[Hshr|H†]"; last by auto.
-      iLeft. iApply (Hincl.(subtype_shr _ _ _ _) with "LFT HE HL Hshr").
+      iLeft. iApply ("Hs" with "Hshr").
   Qed.
 
   Global Instance own_proper E L n :

theories/typing/product.v

@@ -57,17 +57,18 @@ Section product.
   Global Instance product2_mono E L:
     Proper (subtype E L ==> subtype E L ==> subtype E L) product2.
   Proof.
-    iIntros (ty11 ty12 H1 ty21 ty22 H2). split.
-    - by rewrite /= (subtype_sz _ _ _ _ H1) (subtype_sz _ _ _ _ H2).
-    - iIntros (??) "#LFT #HE #HL H". iDestruct "H" as (vl1 vl2) "(% & Hown1 & Hown2)".
+    iIntros (ty11 ty12 H1 ty21 ty22 H2). iIntros.
+    iDestruct (H1 with "* [] [] []") as "(% & #Ho1 & #Hs1)"; [done..|]. clear H1.
+    iDestruct (H2 with "* [] [] []") as "(% & #Ho2 & #Hs2)"; [done..|]. clear H2.
+    iSplit; first by (iPureIntro; simpl; f_equal). iSplit; iAlways.
+    - iIntros (??) "H". iDestruct "H" as (vl1 vl2) "(% & Hown1 & Hown2)".
       iExists _, _. iSplit. done. iSplitL "Hown1".
-      by iApply (H1.(subtype_own _ _ _ _) with "LFT HE HL").
-      by iApply (H2.(subtype_own _ _ _ _) with "LFT HE HL").
-    - iIntros (????) "#LFT #HE #HL H".
-      iDestruct "H" as (vl1 vl2) "(% & #Hshr1 & #Hshr2)".
-      iExists _, _. iSplit. done. erewrite subtype_sz; last done. iSplit.
-      by iApply (H1.(subtype_shr _ _ _ _) with "LFT HE HL").
-      by iApply (H2.(subtype_shr _ _ _ _) with "LFT HE HL").
+      + by iApply "Ho1".
+      + by iApply "Ho2".
+    - iIntros (????) "H". iDestruct "H" as (vl1 vl2) "(% & #Hshr1 & #Hshr2)".
+      iExists _, _. iSplit; first done. iSplit.
+      + by iApply "Hs1".
+      + rewrite -(_ : ty_size ty11 = ty_size ty12) //. by iApply "Hs2".
   Qed.
   Global Instance product2_proper E L:
     Proper (eqtype E L ==> eqtype E L ==> eqtype E L) product2.
@@ -151,11 +152,11 @@ Section typing.
       iExists E2, E3. iSplit. by iPureIntro; set_solver. by iFrame.
   Qed.
 
+(*
   Lemma ty_incl_prod_flatten ρ tyl1 tyl2 tyl3 :
     ty_incl ρ (Π(tyl1 ++ Π tyl2 :: tyl3))
               (Π(tyl1 ++ tyl2 ++ tyl3)).
   Proof.
-  Admitted.
   (*   apply (ty_incl_weaken _ ⊤). apply perm_incl_top. *)
   (*   induction tyl1; last by apply (ty_incl_prod2 _ _ _ _ _ _). *)
   (*   induction tyl2 as [|ty tyl2 IH]; simpl. *)
@@ -172,7 +173,6 @@ Section typing.
     ty_incl ρ (Π(tyl1 ++ tyl2 ++ tyl3))
               (Π(tyl1 ++ Π tyl2 :: tyl3)).
   Proof.
-  Admitted.
   (*   apply (ty_incl_weaken _ ⊤). apply perm_incl_top. *)
   (*   induction tyl1; last by apply (ty_incl_prod2 _ _ _ _ _ _). *)
   (*   induction tyl2 as [|ty tyl2 IH]; simpl. *)
@@ -188,4 +188,5 @@ Section typing.
   (*   - etransitivity; last apply ty_incl_prod2_assoc1. *)
   (*     eapply (ty_incl_prod2 _ _ _ _ _ _). done. apply IH. *)
   (* Qed. *)
+*)
 End typing.

theories/typing/shr_bor.v

@@ -22,7 +22,8 @@ Section shr_bor.
     iIntros (??) "#LFT #HE #HL H". iDestruct (Hκ with "HE HL") as "#Hκ".
     iDestruct "H" as (l) "(% & H)". subst. iExists _. iSplit. done.
     iApply (ty2.(ty_shr_mono) with "LFT Hκ"). reflexivity.
-    by iApply (Hty.(subtype_shr _ _ _ _ ) with "LFT HE HL").
+    iDestruct (Hty with "* [] [] []") as "(_ & _ & #Hs1)"; [done..|clear Hty].
+    by iApply "Hs1".
   Qed.
   Global Instance subtype_shr_bor_mono' E L :
     Proper (lctx_lft_incl E L ==> subtype E L --> flip (subtype E L)) shr_bor.
@@ -125,4 +126,4 @@ Section typing.
       + iMod ("Hclose'" with "[H↦]"). by auto.
         by iDestruct (lft_tok_dead with "[-] H†") as "[]".
   Qed.
-End typing.
\ No newline at end of file
+End typing.

theories/typing/sum.v

@@ -110,11 +110,6 @@ Notation "Σ[ ty1 ; .. ; tyn ]" :=
 Section incl.
   Context `{typeG Σ}.
 
-   (* FIXME : do we need that anywhere?. *)
-  Lemma ty_incl_emp ρ ty : ty_incl ρ ∅ ty.
-  Proof.
-  Admitted.
-
   (* TODO *)
   (* Lemma ty_incl_sum ρ n tyl1 tyl2 (_ : LstTySize n tyl1) (_ : LstTySize n tyl2) : *)
   (*   Duplicable ρ → Forall2 (ty_incl ρ) tyl1 tyl2 → *)

theories/typing/type.v

@@ -117,30 +117,44 @@ Delimit Scope lrust_type_scope with T.
 Bind Scope lrust_type_scope with type.
 
 Section subtyping.
-  Context `{typeG Σ} (E : elctx) (L : llctx).
+  Context `{typeG Σ}.
+  Definition type_incl (ty1 ty2 : type) : iProp Σ :=
+    (⌜ty1.(ty_size) = ty2.(ty_size)⌝ ∗
+     (□ ∀ tid vl, ty1.(ty_own) tid vl -∗ ty2.(ty_own) tid vl) ∗
+     (□ ∀ κ tid F l, ty1.(ty_shr) κ tid F l -∗ ty2.(ty_shr) κ tid F l))%I.
+
+  Global Instance type_incl_persistent ty1 ty2 : PersistentP (type_incl ty1 ty2) := _.
+(*  Typeclasses Opaque type_incl. *)
+
+  Lemma type_incl_refl ty : type_incl ty ty.
+  Proof. iSplit; first done. iSplit; iAlways; iIntros; done. Qed.
+
+  Lemma type_incl_trans ty1 ty2 ty3 :
+    type_incl ty1 ty2 -∗ type_incl ty2 ty3 -∗ type_incl ty1 ty3.
+  Proof.
+    (* TODO: this iIntros takes suspiciously long. *)
+    iIntros "(% & #Ho12 & #Hs12) (% & #Ho23 & #Hs23)".
+    iSplit; first (iPureIntro; etrans; done).
+    iSplit; iAlways; iIntros.
+    - iApply "Ho23". iApply "Ho12". done.
+    - iApply "Hs23". iApply "Hs12". done.
+  Qed.
 
-  Record subtype (ty1 ty2 : type) : Prop :=
-    { subtype_sz : ty1.(ty_size) = ty2.(ty_size);
-      subtype_own tid vl:
-        lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
-           ty1.(ty_own) tid vl -∗ ty2.(ty_own) tid vl;
-      subtype_shr κ tid F l:
-        lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
-           ty1.(ty_shr) κ tid F l -∗ ty2.(ty_shr) κ tid F l }.
+  Context (E : elctx) (L : llctx).
+
+  Definition subtype (ty1 ty2 : type) : Prop :=
+    lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
+            type_incl ty1 ty2.
 
   Global Instance subtype_preorder : PreOrder subtype.
   Proof.
     split.
-    - intros ty. split; [done|intros|intros]; iIntros "_ _ _ $".
-    - intros ty1 ty2 ty3 H1 H2. split.
-      + etrans. eapply H1. eapply H2.
-      + iIntros (??) "#LFT #HE #HL * H".
-        iApply (H2.(subtype_own _ _) with "LFT HE HL *").
-        by iApply (H1.(subtype_own _ _) with "LFT HE HL *").
-      + iIntros (????) "#LFT #HE #HL * H".
-        iApply (H2.(subtype_shr _ _) with "LFT HE HL *").
-        by iApply (H1.(subtype_shr _ _) with "LFT HE HL *").
-  Qed.
+    - intros ty. iIntros. iApply type_incl_refl.
+    - intros ty1 ty2 ty3 H12 H23. iIntros.
+      iApply (type_incl_trans with "[] []").
+      + iApply (H12 with "[] []"); done.
+      + iApply (H23 with "[] []"); done.
+Qed.
 
   Definition eqtype (ty1 ty2 : type) : Prop :=
     subtype ty1 ty2 ∧ subtype ty2 ty1.
@@ -159,9 +173,10 @@ Section subtyping.
                  st1.(st_own) tid vl -∗ st2.(st_own) tid vl) →
     subtype st1 st2.
   Proof.
-    intros Hsz Hst. split; [done|by apply Hst|].
-    iIntros (????) "#LFT #HE #HL H /=".
-    iDestruct "H" as (vl) "[Hf [Hown|H†]]"; iExists vl; iFrame "Hf"; last by auto.
-    iLeft. by iApply (Hst with "LFT HE HL *").
+    intros Hsz Hst. iIntros. iSplit; first done. iSplit; iAlways.
+    - iIntros. iApply (Hst with "* [] [] []"); done.
+    - iIntros (????) "H".
+      iDestruct "H" as (vl) "[Hf [Hown|H†]]"; iExists vl; iFrame "Hf"; last by auto.
+      iLeft. by iApply (Hst with "* [] [] []").
   Qed.
 End subtyping.

theories/typing/type_context.v

@@ -73,7 +73,8 @@ Section type_context.
   Proof.
     iIntros (Hst ?) "#LFT #HE #HL H". rewrite /tctx_interp !big_sepL_singleton /=.
     iDestruct "H" as (v) "[% H]". iExists _. iFrame "%".
-    by iApply (Hst.(subtype_own _ _ _ _) with "LFT HE HL").
+    iDestruct (Hst with "* [] [] []") as "(_ & #Ho & _)"; [done..|].
+    iApply ("Ho" with "*"). done.
   Qed.
 
   Definition deguard_tctx_elt κ x :=

theories/typing/uniq_bor.v

@@ -67,18 +67,19 @@ Section uniq_bor.
   Global Instance subtype_uniq_mono E L :
     Proper (lctx_lft_incl E L --> eqtype E L ==> subtype E L) uniq_bor.
   Proof.
-    intros κ1 κ2 Hκ ty1 ty2 [Hty1 Hty2]. split.
-    - done.
-    - iIntros (??) "#LFT #HE #HL H". iDestruct (Hκ with "HE HL") as "#Hκ".
-      iDestruct "H" as (l P) "[[% #HPiff] Hown]". subst.
+    intros κ1 κ2 Hκ ty1 ty2 [Hty1 Hty2]. iIntros. iSplit; first done.
+    iDestruct (Hty1 with "* [] [] []") as "(_ & #Ho1 & #Hs1)"; [done..|clear Hty1].
+    iDestruct (Hty2 with "* [] [] []") as "(_ & #Ho2 & #Hs2)"; [done..|clear Hty2].
+    iDestruct (Hκ with "[] []") as "#Hκ"; [done..|].
+    iSplit; iAlways.
+    - iIntros (??) "H". iDestruct "H" as (l P) "[[% #HPiff] Hown]". subst.
       iExists _, _. iSplitR; last by iApply (bor_shorten with "Hκ"). iSplit. done.
       iIntros "!#". iSplit; iIntros "H".
       + iDestruct ("HPiff" with "H") as (vl) "[??]". iExists vl. iFrame.
-        by iApply (Hty1.(subtype_own _ _ _ _) with "LFT HE HL").
+        by iApply "Ho1".
       + iDestruct "H" as (vl) "[??]". iApply "HPiff". iExists vl. iFrame.
-        by iApply (Hty2.(subtype_own _ _ _ _) with "LFT HE HL").
-    - iIntros (????) "#LFT #HE #HL H". iDestruct (Hκ with "HE HL") as "#Hκ".
-      iAssert (κ2 ∪ κ ⊑ κ1 ∪ κ)%I as "#Hincl'".
+        by iApply "Ho2".
+    - iIntros (κ ???) "H". iAssert (κ2 ∪ κ ⊑ κ1 ∪ κ)%I as "#Hincl'".
       { iApply (lft_incl_glb with "[] []").
         - iApply (lft_incl_trans with "[] Hκ"). iApply lft_le_incl.
           apply gmultiset_union_subseteq_l.
@@ -86,8 +87,7 @@ Section uniq_bor.
       iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'. iIntros "{$Hbor}!#%%".
       iMod ("Hupd" with "* [%]") as "Hupd'"; try done. iModIntro. iNext.
       iMod "Hupd'" as "[H|H†]"; last by auto.
-      iLeft. iApply (ty_shr_mono with "LFT Hincl'"). reflexivity.
-      by iApply (Hty1.(subtype_shr _ _ _ _) with "LFT HE HL").
+      iLeft. iApply (ty_shr_mono with "[] Hincl'"); [done..|]. by iApply "Hs1".
   Qed.
   Global Instance subtype_uniq_mono' E L :
     Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L)) uniq_bor.