From 083062017a23ae2b7ed083f0aac39fdf4563962d Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 14 Dec 2016 11:46:50 +0100
Subject: [PATCH] make type inclusion a relation in Iris
---
theories/typing/function.v | 5 +--
theories/typing/own.v | 13 ++++----
theories/typing/product.v | 25 +++++++-------
theories/typing/shr_bor.v | 5 +--
theories/typing/sum.v | 5 ---
theories/typing/type.v | 61 +++++++++++++++++++++-------------
theories/typing/type_context.v | 3 +-
theories/typing/uniq_bor.v | 20 +++++------
8 files changed, 76 insertions(+), 61 deletions(-)
diff --git a/theories/typing/function.v b/theories/typing/function.v
index ed55d80b..d749e2ad 100644
--- a/theories/typing/function.v
+++ b/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 :
diff --git a/theories/typing/own.v b/theories/typing/own.v
index aaf7b21d..c5d754e5 100644
--- a/theories/typing/own.v
+++ b/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 :
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 0933c519..6271f46a 100644
--- a/theories/typing/product.v
+++ b/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.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 310440f0..197290bd 100644
--- a/theories/typing/shr_bor.v
+++ b/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.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index c707306a..32140825 100644
--- a/theories/typing/sum.v
+++ b/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 → *)
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 6ad88ebc..fb8e4382 100644
--- a/theories/typing/type.v
+++ b/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.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 299b976b..54c2a32b 100644
--- a/theories/typing/type_context.v
+++ b/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 :=
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index dde9e736..3743290b 100644
--- a/theories/typing/uniq_bor.v
+++ b/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.
--
GitLab