From de9fc5a629a9945a9bf221a3ebb127444a3eec56 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 22 Mar 2017 13:12:15 +0100
Subject: [PATCH] WIP: "Lifetime of a function" instead of liveness assumptions
in external lifetime context
---
opam.pins | 2 +-
theories/lang/notation.v | 2 +-
theories/lifetime/lifetime.v | 12 ++
theories/typing/bool.v | 8 +-
theories/typing/cont.v | 26 +--
theories/typing/cont_context.v | 27 ++-
theories/typing/int.v | 8 +-
theories/typing/lft_contexts.v | 337 +++++++--------------------------
theories/typing/own.v | 21 +-
theories/typing/product.v | 28 +--
theories/typing/programs.v | 89 +++++----
theories/typing/type.v | 51 +++--
theories/typing/type_context.v | 31 ++-
13 files changed, 233 insertions(+), 409 deletions(-)
diff --git a/opam.pins b/opam.pins
index 4e9b917a..426ea20f 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 3d6525a57844edcc8868ec9271a0966bcc2a5e89
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq e0ed90f7719571785cafde1e9e9b6b8ca380a284
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index bb7cadf6..855e5c26 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -86,7 +86,7 @@ Notation "'withcont:' k1 ':' e1 'cont:' k2 xl := e2" :=
((Lam (@cons binder k1%RustB nil) e1%E) [Rec k2%RustB ((fun _ : eq k1%RustB k2%RustB => xl%RustB) eq_refl) e2%E])
(only parsing, at level 151, k1, k2, xl at level 1, e2 at level 150) : expr_scope.
-Notation "'call:' f args → k" := (f (@cons expr k args))%E
+Notation "'call:' f args → k" := (f (@cons expr (λ: ["_r"], Endlft ;; k ["_r"])%V args))%E
(only parsing, at level 102, f, args, k at level 1) : expr_scope.
Notation "'letcall:' x := f args 'in' e" :=
(letcont: "_k" [ x ] := e in call: f args → "_k")%E
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 8feb89a6..f1e0c77e 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -15,6 +15,8 @@ Module Export lifetime : lifetime_sig.
Include creation.
End lifetime.
+Notation lft_intersect_list l := (foldr lft_intersect static l).
+
Instance lft_inhabited : Inhabited lft := populate static.
Canonical lftC := leibnizC lft.
@@ -111,4 +113,14 @@ Proof.
- iIntros (q) "?". iExists 1%Qp. iSplitR. by iApply lft_tok_static. auto.
- iIntros "Hst". by iDestruct (lft_dead_static with "Hst") as "[]".
Qed.
+
+Lemma lft_intersect_list_elem_of_incl κs κ :
+ κ ∈ κs → (lft_intersect_list κs ⊑ κ)%I.
+Proof.
+ induction 1 as [|???? IH].
+ - iApply lft_intersect_incl_l.
+ - iApply lft_incl_trans; last iApply IH. (* FIXME: Why does "done" not do this? Looks like "assumption" to me. *)
+ iApply lft_intersect_incl_r.
+Qed.
+
End derived.
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index cb2c8def..0f6eee22 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -25,7 +25,7 @@ Section typing.
Lemma type_bool_instr (b : Datatypes.bool) : typed_val #b bool.
Proof.
- iIntros (E L tid qE) "_ $ $ $ _". wp_value.
+ iIntros (E L tid) "_ _ $ $ _". wp_value.
rewrite tctx_interp_singleton tctx_hasty_val. by destruct b.
Qed.
@@ -40,11 +40,11 @@ Section typing.
typed_body E L C T e1 -∗ typed_body E L C T e2 -∗
typed_body E L C T (if: p then e1 else e2).
Proof.
- iIntros (Hp) "He1 He2". iIntros (tid qE) "#LFT Htl HE HL HC HT".
+ iIntros (Hp) "He1 He2". iIntros (tid) "#LFT #HE Htl HL HC HT".
iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "#Hp".
wp_bind p. iApply (wp_hasty with "Hp").
iIntros ([[| |[|[]|]]|]) "_ H1"; try done; (iApply wp_case; [done..|iNext]).
- - iApply ("He2" with "LFT Htl HE HL HC HT").
- - iApply ("He1" with "LFT Htl HE HL HC HT").
+ - iApply ("He2" with "LFT HE Htl HL HC HT").
+ - iApply ("He1" with "LFT HE Htl HL HC HT").
Qed.
End typing.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 020f883e..91665210 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -17,9 +17,9 @@ Section typing.
tctx_incl E L T (T' (list_to_vec argsv)) →
typed_body E L C T (k args).
Proof.
- iIntros (Hargs HC Hincl tid qE) "#LFT Hna HE HL HC HT".
- iMod (Hincl with "LFT HE HL HT") as "(HE & HL & HT)".
- iSpecialize ("HC" with "HE []"); first done.
+ iIntros (Hargs HC Hincl tid) "#LFT #HE Hna HL HC HT".
+ iMod (Hincl with "LFT HE HL HT") as "(HL & HT)".
+ iSpecialize ("HC" with "[]"); first done.
assert (args = of_val <$> argsv) as ->.
{ clear -Hargs. induction Hargs as [|a av ?? [<-%of_to_val| ->] _ ->]=>//=. }
rewrite -{3}(vec_to_list_of_list argsv). iApply ("HC" with "Hna HL HT").
@@ -33,15 +33,15 @@ Section typing.
(subst_v (kb::argsb) (k:::args) econt)) -∗
typed_body E L2 C T (letcont: kb argsb := econt in e2).
Proof.
- iIntros (Hc1 Hc2) "He2 #Hecont". iIntros (tid qE) "#LFT Htl HE HL HC HT".
+ iIntros (Hc1 Hc2) "He2 #Hecont". iIntros (tid) "#LFT #HE Htl HL HC HT".
iApply wp_let'; first by rewrite /= decide_left.
- iModIntro. iApply ("He2" with "LFT Htl HE HL [HC] HT").
- iIntros "HE". iLöb as "IH". iIntros (x) "H".
- iDestruct "H" as %[->|?]%elem_of_cons; last by iApply ("HC" with "HE").
+ iModIntro. iApply ("He2" with "LFT HE Htl HL [HC] HT").
+ iLöb as "IH". iIntros (x) "H".
+ iDestruct "H" as %[->|?]%elem_of_cons; last by iApply "HC".
iIntros (args) "Htl HL HT". iApply wp_rec; try done.
{ rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
{ by rewrite -(subst_v_eq (_ :: _) (RecV _ _ _ ::: _)). }
- iNext. iApply ("Hecont" with "LFT Htl HE HL [HC] HT"). by iApply "IH".
+ iNext. iApply ("Hecont" with "LFT HE Htl HL [HC] HT"). by iApply "IH".
Qed.
Lemma type_cont_norec argsb L1 (T' : vec val (length argsb) → _) E L2 C T econt e2 kb :
@@ -51,14 +51,14 @@ Section typing.
typed_body E L1 C (T' args) (subst_v (kb :: argsb) (k:::args) econt)) -∗
typed_body E L2 C T (letcont: kb argsb := econt in e2).
Proof.
- iIntros (Hc1 Hc2) "He2 Hecont". iIntros (tid qE) "#LFT Htl HE HL HC HT".
+ iIntros (Hc1 Hc2) "He2 Hecont". iIntros (tid) "#LFT #HE Htl HL HC HT".
iApply wp_let'; first by rewrite /= decide_left.
- iModIntro. iApply ("He2" with "LFT Htl HE HL [HC Hecont] HT").
- iIntros "HE". iIntros (x) "H".
- iDestruct "H" as %[->|?]%elem_of_cons; last by iApply ("HC" with "HE").
+ iModIntro. iApply ("He2" with "LFT HE Htl HL [HC Hecont] HT").
+ iIntros (x) "H".
+ iDestruct "H" as %[->|?]%elem_of_cons; last by iApply "HC".
iIntros (args) "Htl HL HT". iApply wp_rec; try done.
{ rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
{ by rewrite -(subst_v_eq (_ :: _) (RecV _ _ _ ::: _)). }
- iNext. iApply ("Hecont" with "LFT Htl HE HL HC HT").
+ iNext. iApply ("Hecont" with "LFT HE Htl HL HC HT").
Qed.
End typing.
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index e09992b7..5d90ab31 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -20,7 +20,7 @@ Notation cctx := (list cctx_elt).
Delimit Scope lrust_cctx_scope with CC.
Bind Scope lrust_cctx_scope with cctx_elt.
-Notation "k â—cont( L , T )" := (CCtx_iscont k L _ T%TC)
+Notation "k â—cont( L , T )" := (CCtx_iscont k L%LL _ T%TC)
(at level 70, format "k â—cont( L , T )") : lrust_cctx_scope.
Notation "a :: b" := (@cons cctx_elt a%CC b%CC)
(at level 60, right associativity) : lrust_cctx_scope.
@@ -77,38 +77,35 @@ Section cont_context.
Qed.
Definition cctx_incl (E : elctx) (C1 C2 : cctx): Prop :=
- ∀ tid q, lft_ctx -∗ (elctx_interp E q -∗ cctx_interp tid C1) -∗
- (elctx_interp E q -∗ cctx_interp tid C2).
+ ∀ tid, lft_ctx -∗ elctx_interp E -∗ cctx_interp tid C1 -∗ cctx_interp tid C2.
Global Arguments cctx_incl _%EL _%CC _%CC.
Global Instance cctx_incl_preorder E : PreOrder (cctx_incl E).
Proof.
split.
- - iIntros (???) "_ $".
- - iIntros (??? H1 H2 ??) "#LFT HE".
- iApply (H2 with "LFT"). by iApply (H1 with "LFT").
+ - iIntros (??) "_ _ $".
+ - iIntros (??? H1 H2 ?) "#LFT #HE HC".
+ iApply (H2 with "LFT HE"). by iApply (H1 with "LFT HE").
Qed.
Lemma incl_cctx_incl E C1 C2 : C1 ⊆ C2 → cctx_incl E C2 C1.
Proof.
- rewrite /cctx_incl /cctx_interp. iIntros (HC1C2 tid ?) "_ H HE * %".
- iApply ("H" with "HE [%]"). by apply HC1C2.
+ rewrite /cctx_incl /cctx_interp. iIntros (HC1C2 tid) "_ #HE H * %".
+ iApply ("H" with "[%]"). by apply HC1C2.
Qed.
Lemma cctx_incl_cons_match E k L n (T1 T2 : vec val n → tctx) C1 C2 :
cctx_incl E C1 C2 → (∀ args, tctx_incl E L (T2 args) (T1 args)) →
cctx_incl E (k â—cont(L, T1) :: C1) (k â—cont(L, T2) :: C2).
Proof.
- iIntros (HC1C2 HT1T2 ??) "#LFT H HE". rewrite /cctx_interp.
+ iIntros (HC1C2 HT1T2 ?) "#LFT #HE H". rewrite /cctx_interp.
iIntros (x) "Hin". iDestruct "Hin" as %[->|Hin]%elem_of_cons.
- iIntros (args) "Htl HL HT".
- iMod (HT1T2 with "LFT HE HL HT") as "(HE & HL & HT)".
- iSpecialize ("H" with "HE").
+ iMod (HT1T2 with "LFT HE HL HT") as "(HL & HT)".
iApply ("H" $! (_ â—cont(_, _))%CC with "[%] Htl HL HT").
constructor.
- - iApply (HC1C2 with "LFT [H] HE [%]"); last done.
- iIntros "HE". iIntros (x') "%".
- iApply ("H" with "HE [%]"). by apply elem_of_cons; auto.
+ - iApply (HC1C2 with "LFT HE [H] [%]"); last done.
+ iIntros (x') "%". iApply ("H" with "[%]"). by apply elem_of_cons; auto.
Qed.
Lemma cctx_incl_nil E C : cctx_incl E C [].
@@ -121,7 +118,7 @@ Section cont_context.
cctx_incl E C1 (k â—cont(L, T2) :: C2).
Proof.
intros Hin ??. rewrite <-cctx_incl_cons_match; try done.
- iIntros (??) "_ HC HE". iSpecialize ("HC" with "HE").
+ iIntros (?) "_ #HE HC".
rewrite cctx_interp_cons. iSplit; last done. clear -Hin.
iInduction Hin as [] "IH"; rewrite cctx_interp_cons;
[iDestruct "HC" as "[$ _]" | iApply "IH"; iDestruct "HC" as "[_ $]"].
diff --git a/theories/typing/int.v b/theories/typing/int.v
index f87c9ac0..520901b9 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -24,7 +24,7 @@ Section typing.
Lemma type_int_instr (z : Z) : typed_val #z int.
Proof.
- iIntros (E L tid qE) "_ $ $ $ _". wp_value.
+ iIntros (E L tid) "_ _ $ $ _". wp_value.
by rewrite tctx_interp_singleton tctx_hasty_val.
Qed.
@@ -37,7 +37,7 @@ Section typing.
Lemma type_plus_instr E L p1 p2 :
typed_instruction_ty E L [p1 â— int; p2 â— int] (p1 + p2) int.
Proof.
- iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+ iIntros (tid) "_ _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
iIntros "[Hp1 Hp2]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
@@ -54,7 +54,7 @@ Section typing.
Lemma type_minus_instr E L p1 p2 :
typed_instruction_ty E L [p1 â— int; p2 â— int] (p1 - p2) int.
Proof.
- iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+ iIntros (tid) "_ _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
iIntros "[Hp1 Hp2]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
@@ -71,7 +71,7 @@ Section typing.
Lemma type_le_instr E L p1 p2 :
typed_instruction_ty E L [p1 ◠int; p2 ◠int] (p1 ≤ p2) bool.
Proof.
- iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+ iIntros (tid) "_ _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
iIntros "[Hp1 Hp2]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 43042ef7..f0c218ea 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -6,9 +6,7 @@ From lrust.typing Require Export base.
From lrust.lifetime Require Import frac_borrow.
Set Default Proof Using "Type".
-Inductive elctx_elt : Type :=
-| ELCtx_Alive (κ : lft)
-| ELCtx_Incl (κ κ' : lft).
+Definition elctx_elt : Type := lft * lft.
Notation elctx := (list elctx_elt).
Delimit Scope lrust_elctx_scope with EL.
@@ -17,8 +15,7 @@ Delimit Scope lrust_elctx_scope with EL.
notations, so we have to use [Arguments] everywhere. *)
Bind Scope lrust_elctx_scope with elctx_elt.
-Coercion ELCtx_Alive : lft >-> elctx_elt.
-Infix "⊑" := ELCtx_Incl (at level 70) : lrust_elctx_scope.
+Notation "κ1 ⊑ κ2" := (@pair lft lft κ1 κ2) (at level 70) : lrust_elctx_scope.
Notation "a :: b" := (@cons elctx_elt a%EL b%EL)
(at level 60, right associativity) : lrust_elctx_scope.
@@ -47,61 +44,22 @@ Section lft_contexts.
Implicit Type (κ : lft).
(* External lifetime contexts. *)
- Definition elctx_elt_interp (x : elctx_elt) (q : Qp) : iProp Σ :=
- match x with
- | ELCtx_Alive κ => q.[κ]%I
- | κ ⊑ κ' => (κ ⊑ κ')%I
- end%EL.
- Global Instance elctx_elt_interp_fractional x:
- Fractional (elctx_elt_interp x).
- Proof. destruct x; unfold elctx_elt_interp; apply _. Qed.
- Definition elctx_elt_interp_0 (x : elctx_elt) : iProp Σ :=
- match x with
- | ELCtx_Alive κ => True%I
- | κ ⊑ κ' => (κ ⊑ κ')%I
- end%EL.
- Global Instance elctx_elt_interp_0_persistent x:
- PersistentP (elctx_elt_interp_0 x).
- Proof. destruct x; apply _. Qed.
-
- Lemma elctx_elt_interp_persist x q :
- elctx_elt_interp x q -∗ elctx_elt_interp_0 x.
- Proof. destruct x; by iIntros "?/=". Qed.
-
- Definition elctx_interp (E : elctx) (q : Qp) : iProp Σ :=
- ([∗ list] x ∈ E, elctx_elt_interp x q)%I.
- Global Arguments elctx_interp _%EL _%Qp.
- Global Instance elctx_interp_fractional E:
- Fractional (elctx_interp E).
- Proof. intros ??. rewrite -big_sepL_sepL. by setoid_rewrite <-fractional. Qed.
- Global Instance elctx_interp_as_fractional E q:
- AsFractional (elctx_interp E q) (elctx_interp E) q.
- Proof. split. done. apply _. Qed.
- Global Instance elctx_interp_permut:
- Proper ((≡ₚ) ==> eq ==> (⊣⊢)) elctx_interp.
- Proof. intros ????? ->. by apply big_opL_permutation. Qed.
-
- Definition elctx_interp_0 (E : elctx) : iProp Σ :=
- ([∗ list] x ∈ E, elctx_elt_interp_0 x)%I.
- Global Arguments elctx_interp_0 _%EL.
- Global Instance elctx_interp_0_persistent E:
- PersistentP (elctx_interp_0 E).
- Proof. apply _. Qed.
- Global Instance elctx_interp_0_permut:
- Proper ((≡ₚ) ==> (⊣⊢)) elctx_interp_0.
+ Definition elctx_elt_interp (x : elctx_elt) : iProp Σ :=
+ (x.1 ⊑ x.2)%I.
+
+ Definition elctx_interp (E : elctx) : iProp Σ :=
+ ([∗ list] x ∈ E, elctx_elt_interp x)%I.
+ Global Arguments elctx_interp _%EL.
+ Global Instance elctx_interp_permut :
+ Proper ((≡ₚ) ==> (⊣⊢)) elctx_interp.
Proof. intros ???. by apply big_opL_permutation. Qed.
-
- Lemma elctx_interp_persist x q :
- elctx_interp x q -∗ elctx_interp_0 x.
- Proof.
- unfold elctx_interp, elctx_interp_0. f_equiv. intros _ ?.
- apply elctx_elt_interp_persist.
- Qed.
+ Global Instance elctx_interp_persistent E :
+ PersistentP (elctx_interp E).
+ Proof. apply _. Qed.
(* Local lifetime contexts. *)
-
Definition llctx_elt_interp (x : llctx_elt) (q : Qp) : iProp Σ :=
- let κ' := foldr lft_intersect static (x.2) in
+ let κ' := lft_intersect_list (x.2) in
(∃ κ0, ⌜x.1 = κ' ⊓ κ0⌠∗ q.[κ0] ∗ □ (1.[κ0] ={↑lftN,∅}▷=∗ [†κ0]))%I.
Global Instance llctx_elt_interp_fractional x :
Fractional (llctx_elt_interp x).
@@ -116,41 +74,22 @@ Section lft_contexts.
iExists κ0. by iFrame "∗%".
Qed.
- Definition llctx_elt_interp_0 (x : llctx_elt) : Prop :=
- let κ' := foldr lft_intersect static (x.2) in (∃ κ0, x.1 = κ' ⊓ κ0).
- Lemma llctx_elt_interp_persist x q :
- llctx_elt_interp x q -∗ ⌜llctx_elt_interp_0 xâŒ.
- Proof.
- iIntros "H". unfold llctx_elt_interp.
- iDestruct "H" as (κ0) "[% _]". by iExists κ0.
- Qed.
-
Definition llctx_interp (L : llctx) (q : Qp) : iProp Σ :=
([∗ list] x ∈ L, llctx_elt_interp x q)%I.
Global Arguments llctx_interp _%LL _%Qp.
- Global Instance llctx_interp_fractional L:
+ Global Instance llctx_interp_fractional L :
Fractional (llctx_interp L).
Proof. intros ??. rewrite -big_sepL_sepL. by setoid_rewrite <-fractional. Qed.
- Global Instance llctx_interp_as_fractional L q:
+ Global Instance llctx_interp_as_fractional L q :
AsFractional (llctx_interp L q) (llctx_interp L) q.
Proof. split. done. apply _. Qed.
- Global Instance llctx_interp_permut:
+ Global Instance llctx_interp_permut :
Proper ((≡ₚ) ==> eq ==> (⊣⊢)) llctx_interp.
Proof. intros ????? ->. by apply big_opL_permutation. Qed.
- Definition llctx_interp_0 (L : llctx) : Prop :=
- ∀ x, x ∈ L → llctx_elt_interp_0 x.
- Global Arguments llctx_interp_0 _%LL.
- Lemma llctx_interp_persist L q :
- llctx_interp L q -∗ ⌜llctx_interp_0 LâŒ.
- Proof.
- iIntros "H". iIntros (x ?). iApply llctx_elt_interp_persist.
- unfold llctx_interp. by iApply (big_sepL_elem_of with "H").
- Qed.
-
- Lemma lctx_equalize_lft qE qL κ1 κ2 `{!frac_borG Σ} :
+ Lemma lctx_equalize_lft qL κ1 κ2 `{!frac_borG Σ} :
lft_ctx -∗ llctx_elt_interp (κ1 ⊑ [κ2]%list) qL ={⊤}=∗
- elctx_elt_interp (κ1 ⊑ κ2) qE ∗ elctx_elt_interp (κ2 ⊑ κ1) qE.
+ elctx_elt_interp (κ1 ⊑ κ2) ∗ elctx_elt_interp (κ2 ⊑ κ1).
Proof.
iIntros "#LFT Hκ". rewrite /llctx_elt_interp /=. (* TODO: Why is this unfold necessary? *)
iDestruct "Hκ" as (κ) "(% & Hκ & _)".
@@ -169,21 +108,23 @@ Section lft_contexts.
Context (E : elctx) (L : llctx).
(* Lifetime inclusion *)
-
Definition lctx_lft_incl κ κ' : Prop :=
- elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗ κ ⊑ κ'.
+ ∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗ κ ⊑ κ').
Definition lctx_lft_eq κ κ' : Prop :=
lctx_lft_incl κ κ' ∧ lctx_lft_incl κ' κ.
Lemma lctx_lft_incl_relf κ : lctx_lft_incl κ κ.
- Proof. iIntros "_ _". iApply lft_incl_refl. Qed.
+ Proof. iIntros (qL) "_ !# _". iApply lft_incl_refl. Qed.
Global Instance lctx_lft_incl_preorder : PreOrder lctx_lft_incl.
Proof.
split; first by intros ?; apply lctx_lft_incl_relf.
- iIntros (??? H1 H2) "#HE #HL". iApply (lft_incl_trans with "[#] [#]").
- iApply (H1 with "HE HL"). iApply (H2 with "HE HL").
+ iIntros (??? H1 H2 ?) "HL".
+ iDestruct (H1 with "HL") as "#H1".
+ iDestruct (H2 with "HL") as "#H2".
+ iClear "∗". iIntros "!# #HE". iApply lft_incl_trans.
+ by iApply "H1". by iApply "H2".
Qed.
Global Instance lctx_lft_incl_proper :
@@ -199,17 +140,17 @@ Section lft_contexts.
Qed.
Lemma lctx_lft_incl_static κ : lctx_lft_incl κ static.
- Proof. iIntros "_ _". iApply lft_incl_static. Qed.
+ Proof. iIntros (qL) "_ !# _". iApply lft_incl_static. Qed.
Lemma lctx_lft_incl_local κ κ' κs :
(κ ⊑ κs)%LL ∈ L → κ' ∈ κs → lctx_lft_incl κ κ'.
Proof.
- iIntros (? Hκ'κs) "_ H". iDestruct "H" as %HL.
- edestruct HL as [κ0 EQ]. done. simpl in EQ; subst.
+ iIntros (? Hκ'κs qL) "H".
+ iDestruct (big_sepL_elem_of with "H") as "H"; first done.
+ iDestruct "H" as (κ'') "[EQ _]". iDestruct "EQ" as %EQ.
+ simpl in EQ; subst. iIntros "!# #HE".
iApply lft_incl_trans; first iApply lft_intersect_incl_l.
- clear -Hκ'κs. induction Hκ'κs.
- - iApply lft_intersect_incl_l.
- - iApply lft_incl_trans; last done. iApply lft_intersect_incl_r.
+ by iApply lft_intersect_list_elem_of_incl.
Qed.
Lemma lctx_lft_incl_local' κ κ' κ'' κs :
@@ -218,8 +159,8 @@ Section lft_contexts.
Lemma lctx_lft_incl_external κ κ' : (κ ⊑ κ')%EL ∈ E → lctx_lft_incl κ κ'.
Proof.
- iIntros (?) "H _".
- rewrite /elctx_interp_0 /elctx_elt_interp_0 big_sepL_elem_of //. done.
+ iIntros (??) "_ !# #HE".
+ rewrite /elctx_interp /elctx_elt_interp big_sepL_elem_of //. done.
Qed.
Lemma lctx_lft_incl_external' κ κ' κ'' :
@@ -229,118 +170,89 @@ Section lft_contexts.
(* Lifetime aliveness *)
Definition lctx_lft_alive (κ : lft) : Prop :=
- ∀ F qE qL, ↑lftN ⊆ F → elctx_interp E qE -∗ llctx_interp L qL ={F}=∗
- ∃ q', q'.[κ] ∗ (q'.[κ] ={F}=∗ elctx_interp E qE ∗ llctx_interp L qL).
+ ∀ F qL, ↑lftN ⊆ F → elctx_interp E -∗ llctx_interp L qL ={F}=∗
+ ∃ q', q'.[κ] ∗ (q'.[κ] ={F}=∗ llctx_interp L qL).
Lemma lctx_lft_alive_static : lctx_lft_alive static.
Proof.
- iIntros (F qE qL ?) "$$". iExists 1%Qp. iSplitL. by iApply lft_tok_static. auto.
+ iIntros (F qL ?) "_ $". iExists 1%Qp. iSplitL. by iApply lft_tok_static. auto.
Qed.
Lemma lctx_lft_alive_local κ κs:
(κ ⊑ κs)%LL ∈ L → Forall lctx_lft_alive κs → lctx_lft_alive κ.
Proof.
- iIntros ([i HL]%elem_of_list_lookup_1 Hκs F qE qL ?) "HE HL".
+ iIntros ([i HL]%elem_of_list_lookup_1 Hκs F qL ?) "#HE HL".
iDestruct "HL" as "[HL1 HL2]". rewrite {2}/llctx_interp /llctx_elt_interp.
iDestruct (big_sepL_lookup_acc with "HL2") as "[Hκ Hclose]". done.
iDestruct "Hκ" as (κ0) "(EQ & Htok & #Hend)". simpl. iDestruct "EQ" as %->.
iAssert (∃ q', q'.[foldr lft_intersect static κs] ∗
- (q'.[foldr lft_intersect static κs] ={F}=∗ elctx_interp E qE ∗ llctx_interp L (qL / 2)))%I
+ (q'.[foldr lft_intersect static κs] ={F}=∗ llctx_interp L (qL / 2)))%I
with "[> HE HL1]" as "H".
{ move:(qL/2)%Qp=>qL'. clear HL. iClear "Hend".
- iInduction Hκs as [|κ κs Hκ ?] "IH" forall (qE qL').
+ iInduction Hκs as [|κ κs Hκ ?] "IH" forall (qL').
- iExists 1%Qp. iFrame. iSplitR; last by auto. iApply lft_tok_static.
- - iDestruct "HL1" as "[HL1 HL2]". iDestruct "HE" as "[HE1 HE2]".
- iMod (Hκ with "HE1 HL1") as (q') "[Htok' Hclose]". done.
- iMod ("IH" with "HE2 HL2") as (q'') "[Htok'' Hclose']".
+ - iDestruct "HL1" as "[HL1 HL2]".
+ iMod (Hκ with "HE HL1") as (q') "[Htok' Hclose]". done.
+ iMod ("IH" with "HL2") as (q'') "[Htok'' Hclose']".
destruct (Qp_lower_bound q' q'') as (q0 & q'2 & q''2 & -> & ->).
iExists q0. rewrite -lft_tok_sep. iDestruct "Htok'" as "[$ Hr']".
iDestruct "Htok''" as "[$ Hr'']". iIntros "!>[Hκ Hfold]".
- iMod ("Hclose" with "[$Hκ $Hr']") as "[$$]". iApply "Hclose'". iFrame. }
+ iMod ("Hclose" with "[$Hκ $Hr']") as "$". iApply "Hclose'". iFrame. }
iDestruct "H" as (q') "[Htok' Hclose']". rewrite -{5}(Qp_div_2 qL).
destruct (Qp_lower_bound q' (qL/2)) as (q0 & q'2 & q''2 & -> & ->).
iExists q0. rewrite -(lft_tok_sep q0). iDestruct "Htok" as "[$ Htok]".
iDestruct "Htok'" as "[$ Htok']". iIntros "!>[Hfold Hκ0]".
- iMod ("Hclose'" with "[$Hfold $Htok']") as "[$$]".
+ iMod ("Hclose'" with "[$Hfold $Htok']") as "$".
rewrite /llctx_interp /llctx_elt_interp. iApply "Hclose". iExists κ0. iFrame. auto.
Qed.
- Lemma lctx_lft_alive_external κ: (ELCtx_Alive κ) ∈ E → lctx_lft_alive κ.
- Proof.
- iIntros ([i HE]%elem_of_list_lookup_1 F qE qL ?) "HE $ !>".
- iDestruct (big_sepL_lookup_acc with "HE") as "[Hκ Hclose]". done.
- iExists qE. iFrame. iIntros "?!>". by iApply "Hclose".
- Qed.
-
Lemma lctx_lft_alive_incl κ κ':
lctx_lft_alive κ → lctx_lft_incl κ κ' → lctx_lft_alive κ'.
Proof.
- iIntros (Hal Hinc F qE qL ?) "HE HL".
- iAssert (κ ⊑ κ')%I with "[#]" as "#Hincl". iApply (Hinc with "[HE] [HL]").
- by iApply elctx_interp_persist. by iApply llctx_interp_persist.
+ iIntros (Hal Hinc F qL ?) "#HE HL".
+ iAssert (κ ⊑ κ')%I with "[#]" as "#Hincl". iApply (Hinc with "HL HE").
iMod (Hal with "HE HL") as (q') "[Htok Hclose]". done.
iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose']". done.
iExists q''. iIntros "{$Htok}!>Htok". iApply ("Hclose" with "[> -]").
by iApply "Hclose'".
Qed.
- Lemma lctx_lft_alive_external' κ κ':
- (ELCtx_Alive κ) ∈ E → (κ ⊑ κ')%EL ∈ E → lctx_lft_alive κ'.
- Proof.
- intros. eapply lctx_lft_alive_incl, lctx_lft_incl_external; last done.
- by apply lctx_lft_alive_external.
- Qed.
-
(* External lifetime context satisfiability *)
Definition elctx_sat E' : Prop :=
- ∀ qE qL F, ↑lftN ⊆ F → elctx_interp E qE -∗ llctx_interp L qL ={F}=∗
- ∃ qE', elctx_interp E' qE' ∗
- (elctx_interp E' qE' ={F}=∗ elctx_interp E qE ∗ llctx_interp L qL).
+ ∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗ elctx_interp E').
Lemma elctx_sat_nil : elctx_sat [].
Proof.
- iIntros (qE qL F ?) "$$". iExists 1%Qp. rewrite /elctx_interp big_sepL_nil. auto.
- Qed.
-
- Lemma elctx_sat_alive E' κ :
- lctx_lft_alive κ → elctx_sat E' → elctx_sat (κ :: E')%EL.
- Proof.
- iIntros (Hκ HE' qE qL F ?) "[HE1 HE2] [HL1 HL2]".
- iMod (Hκ with "HE1 HL1") as (q) "[Htok Hclose]". done.
- iMod (HE' with "HE2 HL2") as (q') "[HE' Hclose']". done.
- destruct (Qp_lower_bound q q') as (q0 & q2 & q'2 & -> & ->). iExists q0.
- rewrite {5 6}/elctx_interp big_sepL_cons /=.
- iDestruct "Htok" as "[$ Htok]". iDestruct "HE'" as "[Hf HE']".
- iSplitL "Hf". by rewrite /elctx_interp.
- iIntros "!>[Htok' ?]". iMod ("Hclose" with "[$Htok $Htok']") as "[$$]".
- iApply "Hclose'". iFrame.
+ iIntros (?) "_ !# _". rewrite /elctx_interp big_sepL_nil. auto.
Qed.
Lemma elctx_sat_lft_incl E' κ κ' :
lctx_lft_incl κ κ' → elctx_sat E' → elctx_sat ((κ ⊑ κ') :: E')%EL.
Proof.
- iIntros (Hκκ' HE' qE qL F ?) "HE HL".
- iAssert (κ ⊑ κ')%I with "[#]" as "#Hincl". iApply (Hκκ' with "[HE] [HL]").
- by iApply elctx_interp_persist. by iApply llctx_interp_persist.
- iMod (HE' with "HE HL") as (q) "[HE' Hclose']". done.
- iExists q. iFrame "HE'". iIntros "{$Hincl}!>[_ ?]". by iApply "Hclose'".
+ iIntros (Hκκ' HE' qL) "HL".
+ iDestruct (Hκκ' with "HL") as "#Hincl".
+ iDestruct (HE' with "HL") as "#HE'".
+ iClear "∗". iIntros "!# #HE".
+ (* FIXME: Why does iSplit fail here? The goal is persistent. *)
+ iSplitL.
+ - by iApply "Hincl".
+ - by iApply "HE'".
Qed.
Lemma elctx_sat_app E1 E2 :
elctx_sat E1 → elctx_sat E2 → elctx_sat (E1 ++ E2).
Proof.
- iIntros (HE1 HE2 ????) "[HE1 HE2] [HL1 HL2]".
- iMod (HE1 with "HE1 HL1") as (qE1) "[HE1 Hclose1]". done.
- iMod (HE2 with "HE2 HL2") as (qE2) "[HE2 Hclose2]". done.
- destruct (Qp_lower_bound qE1 qE2) as (q & qE1' & qE2' & -> & ->). iExists q.
- rewrite !fractional [elctx_interp E qE]fractional_half /elctx_interp big_sepL_app.
- iDestruct "HE1" as "[$ HE1]". iDestruct "HE2" as "[$ HE2]". iIntros "!> [Hq1 Hq2]".
- iMod ("Hclose1" with "[$HE1 $Hq1]") as "[$ $]". iApply "Hclose2". iFrame.
+ iIntros (HE1 HE2 ?) "HL".
+ iDestruct (HE1 with "HL") as "#HE1".
+ iDestruct (HE2 with "HL") as "#HE2".
+ iClear "∗". iIntros "!# #HE".
+ iDestruct ("HE1" with "HE") as "#$".
+ iApply ("HE2" with "HE").
Qed.
Lemma elctx_sat_refl : elctx_sat E.
- Proof. iIntros (????) "??". iExists _. eauto with iFrame. Qed.
+ Proof. iIntros (?) "_ !# ?". done. Qed.
End lft_contexts.
Arguments lctx_lft_incl {_ _ _} _%EL _%LL _ _.
@@ -351,9 +263,8 @@ Arguments elctx_sat {_ _ _} _%EL _%LL _%EL.
Lemma elctx_sat_cons_weaken `{invG Σ, lftG Σ} e0 E E' L :
elctx_sat E L E' → elctx_sat (e0 :: E) L E'.
Proof.
- iIntros (HE' ????). rewrite /elctx_interp. setoid_rewrite big_sepL_cons.
- iIntros "[? HE] HL". iMod (HE' with "HE HL") as (?) "[H Hclose]". done.
- auto 10 with iFrame.
+ iIntros (HE' ?) "HL". iDestruct (HE' with "HL") as "#HE'".
+ iClear "∗". iIntros "!# #[_ HE]". iApply "HE'". done.
Qed.
Lemma elctx_sat_app_weaken_l `{invG Σ, lftG Σ} E0 E E' L :
@@ -363,126 +274,20 @@ Proof. induction E0=>//= ?. auto using elctx_sat_cons_weaken. Qed.
Lemma elctx_sat_app_weaken_r `{invG Σ, lftG Σ} E0 E E' L :
elctx_sat E L E' → elctx_sat (E ++ E0) L E'.
Proof.
- intros ?????. rewrite /elctx_sat /elctx_interp.
+ intros ?. rewrite /elctx_sat /elctx_interp.
setoid_rewrite (big_opL_permutation _ (E++E0)); try apply Permutation_app_comm.
by apply elctx_sat_app_weaken_l.
Qed.
-Section elctx_incl.
- (* External lifetime context inclusion, in a persistent context.
- (Used for function types subtyping).
- On paper, this corresponds to using only the inclusions from E, L
- to show E1; [] |- E2.
- *)
-
- Context `{invG Σ, lftG Σ} (E : elctx) (L : llctx).
-
- Definition elctx_incl E1 E2 : Prop :=
- ∀ F, ↑lftN ⊆ F → elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗
- ∀ qE1, elctx_interp E1 qE1 ={F}=∗ ∃ qE2, elctx_interp E2 qE2 ∗
- (elctx_interp E2 qE2 ={F}=∗ elctx_interp E1 qE1).
- Global Instance : RewriteRelation elctx_incl.
- Arguments elctx_incl _%EL _%EL.
-
- Global Instance elctx_incl_preorder : PreOrder elctx_incl.
- Proof.
- split.
- - iIntros (???) "_ _ * ?". iExists _. iFrame. eauto.
- - iIntros (x y z Hxy Hyz ??) "#HE #HL * HE1".
- iMod (Hxy with "HE HL HE1") as (qy) "[HE1 Hclose1]"; first done.
- iMod (Hyz with "HE HL HE1") as (qz) "[HE1 Hclose2]"; first done.
- iModIntro. iExists qz. iFrame "HE1". iIntros "HE1".
- iApply ("Hclose1" with "[> -]"). by iApply "Hclose2".
- Qed.
-
- Lemma elctx_incl_refl E' : elctx_incl E' E'.
- Proof. reflexivity. Qed.
-
- Lemma elctx_incl_nil E' : elctx_incl E' [].
- Proof.
- iIntros (??) "_ _ * $". iExists 1%Qp.
- rewrite /elctx_interp big_sepL_nil. auto.
- Qed.
-
- Global Instance elctx_incl_app_proper :
- Proper (elctx_incl ==> elctx_incl ==> elctx_incl) app.
- Proof.
- iIntros (?? HE1 ?? HE2 ??) "#HE #HL *". rewrite {1}/elctx_interp big_sepL_app.
- iIntros "[HE1 HE2]".
- iMod (HE1 with "HE HL HE1") as (q1) "[HE1 Hclose1]"; first done.
- iMod (HE2 with "HE HL HE2") as (q2) "[HE2 Hclose2]"; first done.
- destruct (Qp_lower_bound q1 q2) as (q & ? & ? & -> & ->).
- iModIntro. iExists q. rewrite /elctx_interp !big_sepL_app.
- iDestruct "HE1" as "[$ HE1]". iDestruct "HE2" as "[$ HE2]".
- iIntros "[HE1' HE2']".
- iMod ("Hclose1" with "[$HE1 $HE1']") as "$".
- iMod ("Hclose2" with "[$HE2 $HE2']") as "$".
- done.
- Qed.
- Global Instance elctx_incl_cons_proper x :
- Proper (elctx_incl ==> elctx_incl) (cons x).
- Proof. by apply (elctx_incl_app_proper [_] [_]). Qed.
-
- Lemma elctx_incl_dup E1 :
- elctx_incl E1 (E1 ++ E1).
- Proof.
- iIntros (??) "#HE #HL * [HE1 HE1']".
- iModIntro. iExists (qE1 / 2)%Qp.
- rewrite /elctx_interp !big_sepL_app. iFrame.
- iIntros "[HE1 HE1']". by iFrame.
- Qed.
-
- Lemma elctx_sat_incl E1 E2 :
- elctx_sat E1 [] E2 → elctx_incl E1 E2.
- Proof.
- iIntros (H12 ??) "#HE #HL * HE1".
- iMod (H12 _ 1%Qp with "HE1 []") as (qE2) "[HE2 Hclose]". done.
- { by rewrite /llctx_interp big_sepL_nil. }
- iExists qE2. iFrame. iIntros "!> HE2".
- by iMod ("Hclose" with "HE2") as "[$ _]".
- Qed.
-
- Lemma elctx_incl_lft_alive E1 E2 κ :
- lctx_lft_alive E1 [] κ → elctx_incl E1 E2 → elctx_incl E1 (κ :: E2).
- Proof.
- intros Hκ HE2. rewrite (elctx_incl_dup E1).
- apply (elctx_incl_app_proper _ [_]); last done.
- apply elctx_sat_incl. apply elctx_sat_alive, elctx_sat_nil; first done.
- Qed.
-
- Lemma elctx_incl_lft_incl E1 E2 κ κ' :
- lctx_lft_incl (E ++ E1) L κ κ' → elctx_incl E1 E2 →
- elctx_incl E1 ((κ ⊑ κ') :: E2).
- Proof.
- iIntros (Hκκ' HE2 ??) "#HE #HL * HE1".
- iDestruct (elctx_interp_persist with "HE1") as "#HE1'".
- iDestruct (Hκκ' with "[HE HE1'] HL") as "#Hκκ'".
- { rewrite /elctx_interp_0 big_sepL_app. auto. }
- iMod (HE2 with "HE HL HE1") as (qE2) "[HE2 Hclose']". done.
- iExists qE2. iFrame "∗#". iIntros "!> [_ HE2']". by iApply "Hclose'".
- Qed.
-End elctx_incl.
-
-Arguments elctx_incl {_ _ _} _%EL _%LL _%EL _%EL.
-
Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
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_external
- elctx_sat_nil elctx_sat_alive elctx_sat_lft_incl elctx_sat_app elctx_sat_refl
- elctx_incl_refl elctx_incl_nil elctx_incl_lft_alive elctx_incl_lft_incl
+ lctx_lft_alive_static lctx_lft_alive_local
+ 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
- lctx_lft_alive_external' | 100 : lrust_typing.
+ | 100 : lrust_typing.
-Hint Opaque elctx_incl elctx_sat lctx_lft_alive lctx_lft_incl : lrust_typing.
-
-Lemma elctx_incl_lft_incl_alive `{invG Σ, lftG Σ} E L E1 E2 κ κ' :
- lctx_lft_incl (E ++ E1) L κ κ' → elctx_incl E L E1 E2 →
- elctx_incl E L (κ :: E1) (κ' :: E2).
-Proof.
- move=> ? /elctx_incl_lft_incl -> //.
- apply (elctx_incl_app_proper _ _ [_; _] [_]); solve_typing.
-Qed.
+Hint Opaque elctx_sat lctx_lft_alive lctx_lft_incl : lrust_typing.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index f5458177..52ef89cf 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -105,8 +105,10 @@ Section own.
Global Instance own_mono E L n :
Proper (subtype E L ==> subtype E L) (own_ptr n).
Proof.
- intros ty1 ty2 Hincl. iIntros.
- iApply own_type_incl; first by auto. iApply Hincl; auto.
+ intros ty1 ty2 Hincl. iIntros (qL) "HL".
+ iDestruct (Hincl with "HL") as "#Hincl".
+ iClear "∗". iIntros "!# #HE".
+ iApply own_type_incl; first by auto. iApply "Hincl"; auto.
Qed.
Lemma own_mono' E L n1 n2 ty1 ty2 :
n1 = n2 → subtype E L ty1 ty2 → subtype E L (own_ptr n1 ty1) (own_ptr n2 ty2).
@@ -157,7 +159,10 @@ Section box.
Global Instance box_mono E L :
Proper (subtype E L ==> subtype E L) box.
Proof.
- intros ty1 ty2 Hincl. iIntros. iApply box_type_incl. iApply Hincl; auto.
+ intros ty1 ty2 Hincl. iIntros (qL) "HL".
+ iDestruct (Hincl with "HL") as "#Hincl".
+ iClear "∗". iIntros "!# #HE".
+ iApply box_type_incl. iApply "Hincl"; auto.
Qed.
Lemma box_mono' E L ty1 ty2 :
subtype E L ty1 ty2 → subtype E L (box ty1) (box ty2).
@@ -213,7 +218,7 @@ Section typing.
Lemma write_own {E L} ty ty' n :
ty.(ty_size) = ty'.(ty_size) → typed_write E L (own_ptr n ty') ty (own_ptr n ty).
Proof.
- iIntros (Hsz) "!#". iIntros ([[]|] tid F qE qL ?) "_ $ $ Hown"; try done.
+ iIntros (Hsz) "!#". iIntros ([[]|] tid F qL ?) "_ _ $ Hown"; try done.
rewrite /= Hsz. iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as "#>%". iExists _, _. iFrame "H↦". auto.
Qed.
@@ -221,7 +226,7 @@ Section typing.
Lemma read_own_copy E L ty n :
Copy ty → typed_read E L (own_ptr n ty) ty (own_ptr n ty).
Proof.
- iIntros (Hsz) "!#". iIntros ([[]|] tid F qE qL ?) "_ $ $ $ Hown"; try done.
+ iIntros (Hsz) "!#". iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
iExists l, _, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !>".
iExists _. auto.
@@ -230,7 +235,7 @@ Section typing.
Lemma read_own_move E L ty n :
typed_read E L (own_ptr n ty) ty (own_ptr n $ uninit ty.(ty_size)).
Proof.
- iAlways. iIntros ([[]|] tid F qE qL ?) "_ $ $ $ Hown"; try done.
+ iAlways. iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as "#>%".
iExists l, vl, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !> !>".
@@ -242,7 +247,7 @@ Section typing.
let n' := Z.to_nat n in
typed_instruction_ty E L [] (new [ #n ]%E) (own_ptr n' (uninit n')).
Proof.
- iIntros (? tid q) "#LFT $ $ $ _".
+ iIntros (? tid) "#LFT #HE $ $ _".
iApply wp_new; first done. iModIntro.
iIntros (l vl) "(% & H†& Hlft)". subst. rewrite tctx_interp_singleton tctx_hasty_val.
iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame.
@@ -274,7 +279,7 @@ Section typing.
Z.of_nat (ty.(ty_size)) = n →
typed_instruction E L [p ◠own_ptr ty.(ty_size) ty] (delete [ #n; p])%E (λ _, []).
Proof.
- iIntros (<- tid eq) "#LFT $ $ $ Hp". rewrite tctx_interp_singleton.
+ iIntros (<- tid) "#LFT #HE $ $ Hp". rewrite tctx_interp_singleton.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
iDestruct "Hown" as "[H↦: >H†]". iDestruct "H↦:" as (vl) "[>H↦ Hown]".
rewrite tctx_interp_nil. iDestruct (ty_size_eq with "Hown") as "#>EQ".
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 5a27d299..50c7427b 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -81,9 +81,11 @@ 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). iIntros.
- iDestruct (H1 with "[] []") as "(% & #Ho1 & #Hs1)"; [done..|]. clear H1.
- iDestruct (H2 with "[] []") as "(% & #Ho2 & #Hs2)"; [done..|]. clear H2.
+ iIntros (ty11 ty12 H1 ty21 ty22 H2). iIntros (qL) "HL".
+ iDestruct (H1 with "HL") as "#H1". iDestruct (H2 with "HL") as "#H2".
+ iClear "∗". iIntros "!# #HE".
+ iDestruct ("H1" with "HE") as "#(% & #Ho1 & #Hs1)". clear H1.
+ iDestruct ("H2" with "HE") as "#(% & #Ho2 & #Hs2)". 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".
@@ -182,39 +184,39 @@ Section typing.
Global Instance prod2_assoc E L : Assoc (eqtype E L) product2.
Proof.
- split; (iIntros; (iSplit; first by rewrite /= assoc); iSplit; iAlways;
- last iIntros (?); iIntros (??) "H").
+ intros ???. apply eqtype_unfold. iIntros (?) "_ !# _".
+ iSplit; first by rewrite /= assoc. iSplit; iIntros "!# *"; iSplit; iIntros "H".
- iDestruct "H" as (vl1 vl') "(% & Ho1 & H)".
iDestruct "H" as (vl2 vl3) "(% & Ho2 & Ho3)". subst.
iExists _, _. iSplit. by rewrite assoc. iFrame. iExists _, _. by iFrame.
- - iDestruct "H" as "(Hs1 & Hs2 & Hs3)". rewrite shift_loc_assoc_nat.
- by iFrame.
- iDestruct "H" as (vl1 vl') "(% & H & Ho3)".
iDestruct "H" as (vl2 vl3) "(% & Ho1 & Ho2)". subst.
iExists _, _. iSplit. by rewrite -assoc. iFrame. iExists _, _. by iFrame.
+ - iDestruct "H" as "(Hs1 & Hs2 & Hs3)". rewrite shift_loc_assoc_nat.
+ by iFrame.
- iDestruct "H" as "[[Hs1 Hs2] Hs3]". rewrite /= shift_loc_assoc_nat.
by iFrame.
Qed.
Global Instance prod2_unit_leftid E L : LeftId (eqtype E L) unit product2.
Proof.
- intros ty. split; (iIntros; (iSplit; first done); iSplit; iAlways;
- last iIntros (?); iIntros (??) "H").
+ intros ty. apply eqtype_unfold. iIntros (?) "_ !# _". iSplit; first done.
+ iSplit; iIntros "!# *"; iSplit; iIntros "H".
- iDestruct "H" as (? ?) "(% & % & ?)". by subst.
+ - iExists [], _. eauto.
- iDestruct "H" as "(? & ?)". rewrite shift_loc_0.
iApply ty_shr_mono; last done.
iApply lft_incl_refl.
- - iExists [], _. eauto.
- simpl. rewrite shift_loc_0. by iFrame.
Qed.
Global Instance prod2_unit_rightid E L : RightId (eqtype E L) unit product2.
Proof.
- intros ty. split; (iIntros; (iSplit; first by rewrite /= -plus_n_O); iSplit;
- iAlways; last iIntros (?); iIntros (??) "H").
+ intros ty. apply eqtype_unfold. iIntros (?) "_ !# _".
+ iSplit; first by rewrite /= -plus_n_O. iSplit; iIntros "!# *"; iSplit; iIntros "H".
- iDestruct "H" as (? ?) "(% & ? & %)". subst. by rewrite app_nil_r.
- - iDestruct "H" as "(? & _)". done.
- iExists _, []. rewrite app_nil_r. eauto.
+ - iDestruct "H" as "(? & _)". done.
- simpl. iFrame.
Qed.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 72f5e56b..7f545608 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -10,9 +10,8 @@ Section typing.
(* This is an iProp because it is also used by the function type. *)
Definition typed_body (E : elctx) (L : llctx) (C : cctx) (T : tctx)
(e : expr) : iProp Σ :=
- (∀ tid qE, lft_ctx -∗ na_own tid ⊤ -∗
- elctx_interp E qE -∗ llctx_interp L 1 -∗
- (elctx_interp E qE -∗ cctx_interp tid C) -∗ tctx_interp tid T -∗
+ (∀ tid, lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗ llctx_interp L 1 -∗
+ cctx_interp tid C -∗ tctx_interp tid T -∗
WP e {{ _, cont_postcondition }})%I.
Global Arguments typed_body _%EL _%LL _%CC _%TC _%E.
@@ -35,10 +34,10 @@ Section typing.
(typed_body E L).
Proof.
intros C1 C2 HC T1 T2 HT e ? <-. iIntros "H".
- iIntros (tid qE) "#LFT Htl HE HL HC HT".
- iMod (HT with "LFT HE HL HT") as "(HE & HL & HT)".
- iApply ("H" with "LFT Htl HE HL [HC] HT").
- iIntros "HE". by iApply (HC with "LFT HC").
+ iIntros (tid) "#LFT #HE Htl HL HC HT".
+ iMod (HT with "LFT HE HL HT") as "(HL & HT)".
+ iApply ("H" with "LFT HE Htl HL [HC] HT").
+ by iApply (HC with "LFT HE HC").
Qed.
Global Instance typed_body_mono_flip E L:
@@ -49,19 +48,19 @@ Section typing.
(** Instruction *)
Definition typed_instruction (E : elctx) (L : llctx)
(T1 : tctx) (e : expr) (T2 : val → tctx) : iProp Σ :=
- (∀ tid qE, lft_ctx -∗ na_own tid ⊤ -∗
- elctx_interp E qE -∗ llctx_interp L 1 -∗ tctx_interp tid T1 -∗
- WP e {{ v, na_own tid ⊤ ∗ elctx_interp E qE ∗
+ (∀ tid, lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗
+ llctx_interp L 1 -∗ tctx_interp tid T1 -∗
+ WP e {{ v, na_own tid ⊤ ∗
llctx_interp L 1 ∗ tctx_interp tid (T2 v) }})%I.
Global Arguments typed_instruction _%EL _%LL _%TC _%E _%TC.
(** Writing and Reading **)
Definition typed_write (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
- (□ ∀ v tid F qE qL, ⌜lftE ∪ (↑lrustN) ⊆ F⌠→
- lft_ctx -∗ elctx_interp E qE -∗ llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
+ (□ ∀ v tid F qL, ⌜lftE ∪ (↑lrustN) ⊆ F⌠→
+ lft_ctx -∗ elctx_interp E -∗ llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = #l⌠∗ l ↦∗ vl ∗
(▷ l ↦∗: ty.(ty_own) tid ={F}=∗
- elctx_interp E qE ∗ llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
+ llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
Global Arguments typed_write _%EL _%LL _%T _%T _%T.
(* Technically speaking, we could remvoe the vl quantifiaction here and use
@@ -70,11 +69,11 @@ Section typing.
that nobody could possibly have changed the vl (because only half the
fraction was given). So we go with the definition that is easier to prove. *)
Definition typed_read (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
- (□ ∀ v tid F qE qL, ⌜lftE ∪ (↑lrustN) ⊆ F⌠→
- lft_ctx -∗ na_own tid F -∗
- elctx_interp E qE -∗ llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
+ (□ ∀ v tid F qL, ⌜lftE ∪ (↑lrustN) ⊆ F⌠→
+ lft_ctx -∗ elctx_interp E -∗ na_own tid F -∗
+ llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
∃ (l : loc) vl q, ⌜v = #l⌠∗ l ↦∗{q} vl ∗ ▷ ty.(ty_own) tid vl ∗
- (l ↦∗{q} vl ={F}=∗ na_own tid F ∗ elctx_interp E qE ∗
+ (l ↦∗{q} vl ={F}=∗ na_own tid F ∗
llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
Global Arguments typed_read _%EL _%LL _%T _%T _%T.
End typing.
@@ -100,13 +99,11 @@ Section typing_rules.
typed_body ((κ1 ⊑ κ2) :: (κ2 ⊑ κ1) :: E) L C T e →
typed_body E ((κ1 ⊑ [κ2]%list) :: L) C T e.
Proof.
- iIntros (He tid qE) "#LFT Htl HE HL HC HT".
+ iIntros (He tid) "#LFT #HE Htl HL HC HT".
rewrite /llctx_interp big_sepL_cons. iDestruct "HL" as "[Hκ HL]".
iMod (lctx_equalize_lft with "LFT Hκ") as "[Hκ1 Hκ2]".
- iApply (He with "LFT Htl [Hκ1 Hκ2 HE] HL [HC] HT").
- - rewrite /elctx_interp !big_sepL_cons. by iFrame.
- - rewrite /elctx_interp !big_sepL_cons. iIntros "(_ & _ & HE)".
- iApply "HC". done.
+ iApply (He with "LFT [Hκ1 Hκ2 HE] Htl HL HC HT").
+ rewrite /elctx_interp !big_sepL_cons. by iFrame.
Qed.
Lemma type_let' E L T1 T2 (T : tctx) C xb e e' :
@@ -115,11 +112,11 @@ Section typing_rules.
(∀ v : val, typed_body E L C (T2 v ++ T) (subst' xb v e')) -∗
typed_body E L C (T1 ++ T) (let: xb := e in e').
Proof.
- iIntros (Hc) "He He'". iIntros (tid qE) "#LFT Htl HE HL HC HT". rewrite tctx_interp_app.
- iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[He HE HL HT1 Htl]").
- { iApply ("He" with "LFT Htl HE HL HT1"). }
- iIntros (v) "/= (Htl & HE & HL & HT2)". iApply wp_let; first wp_done.
- iModIntro. iApply ("He'" with "LFT Htl HE HL HC [HT2 HT]").
+ iIntros (Hc) "He He'". iIntros (tid) "#LFT #HE Htl HL HC HT". rewrite tctx_interp_app.
+ iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[He HL HT1 Htl]").
+ { iApply ("He" with "LFT HE Htl HL HT1"). }
+ iIntros (v) "/= (Htl & HL & HT2)". iApply wp_let; first wp_done.
+ iModIntro. iApply ("He'" with "LFT HE Htl HL HC [HT2 HT]").
rewrite tctx_interp_app. by iFrame.
Qed.
@@ -152,10 +149,10 @@ Section typing_rules.
(∀ κ, typed_body E ((κ ⊑ κs) :: L) C T e) -∗
typed_body E L C T (Newlft ;; e).
Proof.
- iIntros (Hc) "He". iIntros (tid qE) "#LFT Htl HE HL HC HT".
+ iIntros (Hc) "He". iIntros (tid) "#LFT #HE Htl HL HC HT".
iMod (lft_create with "LFT") as (Λ) "[Htk #Hinh]"; first done.
- set (κ' := foldr lft_intersect static κs). wp_seq.
- iApply ("He" $! (κ' ⊓ Λ) with "LFT Htl HE [HL Htk] HC HT").
+ set (κ' := lft_intersect_list κs). wp_seq.
+ iApply ("He" $! (κ' ⊓ Λ) with "LFT HE Htl [HL Htk] HC HT").
rewrite /llctx_interp big_sepL_cons. iFrame "HL".
iExists Λ. iSplit; first done. iFrame. done.
Qed.
@@ -166,20 +163,20 @@ Section typing_rules.
Closed [] e → UnblockTctx κ T1 T2 →
typed_body E L C T2 e -∗ typed_body E ((κ ⊑ κs) :: L) C T1 (Endlft ;; e).
Proof.
- iIntros (Hc Hub) "He". iIntros (tid qE) "#LFT Htl HE".
+ iIntros (Hc Hub) "He". iIntros (tid) "#LFT #HE Htl".
rewrite /llctx_interp big_sepL_cons. iIntros "[Hκ HL] HC HT".
iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
iApply (wp_mask_mono (↑lftN)); first done.
iApply (wp_step_fupd with "Hend"). done. set_solver. wp_seq.
- iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT Htl HE HL HC [> -]").
+ iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT HE Htl HL HC [> -]").
iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
Qed.
Lemma type_path_instr {E L} p ty :
typed_instruction_ty E L [p â— ty] p ty.
Proof.
- iIntros (??) "_ $$$ ?". rewrite tctx_interp_singleton.
+ iIntros (?) "_ _ $$ ?". rewrite tctx_interp_singleton.
iApply (wp_hasty with "[-]"). done. iIntros (v) "_ Hv".
rewrite tctx_interp_singleton. iExists v. iFrame. by rewrite eval_path_of_val.
Qed.
@@ -195,7 +192,7 @@ Section typing_rules.
typed_write E L ty1 ty ty1' →
typed_instruction E L [p1 ◠ty1; p2 ◠ty] (p1 <- p2) (λ _, [p1 ◠ty1']%TC).
Proof.
- iIntros (Hwrt tid qE) "#LFT $ HE HL".
+ iIntros (Hwrt tid) "#LFT #HE $ HL".
rewrite tctx_interp_cons tctx_interp_singleton. iIntros "[Hp1 Hp2]".
wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "_ Hown2".
@@ -204,7 +201,7 @@ Section typing_rules.
rewrite <-Hsz in *. destruct vl as [|v[|]]; try done.
rewrite heap_mapsto_vec_singleton. iApply wp_fupd. wp_write.
rewrite -heap_mapsto_vec_singleton.
- iMod ("Hclose" with "[Hl Hown2]") as "($ & $ & Hown)".
+ iMod ("Hclose" with "[Hl Hown2]") as "($ & Hown)".
{ iExists _. iFrame. }
rewrite tctx_interp_singleton tctx_hasty_val' //.
Qed.
@@ -221,10 +218,10 @@ Section typing_rules.
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.
- iIntros (Hsz Hread tid qE) "#LFT Htl HE HL Hp".
+ iIntros (Hsz Hread tid) "#LFT #HE Htl HL Hp".
rewrite tctx_interp_singleton. wp_bind p. iApply (wp_hasty with "Hp").
iIntros (v) "% Hown".
- iMod (Hread with "[] LFT Htl HE HL Hown") as
+ iMod (Hread with "[] LFT HE Htl HL Hown") as
(l vl q) "(% & Hl & Hown & Hclose)"; first done.
subst v. iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
destruct vl as [|v [|]]; try done.
@@ -243,29 +240,29 @@ Section typing_rules.
typed_body E L C T (let: x := !p in e).
Proof. iIntros. by iApply type_let; [apply type_deref_instr|solve_typing|]. Qed.
- Lemma type_memcpy_iris E qE L qL tid ty ty1 ty1' ty2 ty2' (n : Z) p1 p2 :
+ Lemma type_memcpy_iris E L qL tid ty ty1 ty1' ty2 ty2' (n : Z) p1 p2 :
Z.of_nat (ty.(ty_size)) = n →
typed_write E L ty1 ty ty1' -∗ typed_read E L ty2 ty ty2' -∗
- {{{ lft_ctx ∗ na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
+ {{{ lft_ctx ∗ elctx_interp E ∗ na_own tid ⊤ ∗ llctx_interp L qL ∗
tctx_elt_interp tid (p1 ◠ty1) ∗ tctx_elt_interp tid (p2 ◠ty2) }}}
(p1 <-{n} !p2)
- {{{ RET #(); na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
+ {{{ RET #(); na_own tid ⊤ ∗ llctx_interp L qL ∗
tctx_elt_interp tid (p1 ◠ty1') ∗ tctx_elt_interp tid (p2 ◠ty2') }}}.
Proof.
iIntros (<-) "#Hwrt #Hread !#".
- iIntros (Φ) "(#LFT & Htl & [HE1 HE2] & [HL1 HL2] & [Hp1 Hp2]) HΦ".
+ iIntros (Φ) "(#LFT & #HE & Htl & [HL1 HL2] & [Hp1 Hp2]) HΦ".
wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "% Hown2".
- iMod ("Hwrt" with "[] LFT HE1 HL1 Hown1")
+ iMod ("Hwrt" with "[] LFT HE HL1 Hown1")
as (l1 vl1) "([% %] & Hl1 & Hcl1)"; first done.
- iMod ("Hread" with "[] LFT Htl HE2 HL2 Hown2")
+ iMod ("Hread" with "[] LFT HE Htl HL2 Hown2")
as (l2 vl2 q2) "(% & Hl2 & Hown2 & Hcl2)"; first done.
iDestruct (ty_size_eq with "Hown2") as "#>%". subst v1 v2. iApply wp_fupd.
iApply (wp_memcpy with "[$Hl1 $Hl2]"); try congruence; [].
iNext. iIntros "[Hl1 Hl2]". iApply ("HΦ" with "[> -]"). rewrite !tctx_hasty_val' //.
- iMod ("Hcl1" with "[Hl1 Hown2]") as "($ & $ & $)".
+ iMod ("Hcl1" with "[Hl1 Hown2]") as "($ & $)".
{ iExists _. iFrame. }
- iMod ("Hcl2" with "Hl2") as "($ & $ & $ & $)". done.
+ iMod ("Hcl2" with "Hl2") as "($ & $ & $)". done.
Qed.
Lemma type_memcpy_instr {E L} ty ty1 ty1' ty2 ty2' (n : Z) p1 p2 :
@@ -274,7 +271,7 @@ Section typing_rules.
typed_instruction E L [p1 â— ty1; p2 â— ty2] (p1 <-{n} !p2)
(λ _, [p1 ◠ty1'; p2 ◠ty2']%TC).
Proof.
- iIntros (Hsz Hwrt Hread tid qE) "#LFT Htl HE HL HT".
+ iIntros (Hsz Hwrt Hread tid) "#LFT #HE Htl HL HT".
iApply (type_memcpy_iris with "[] [] [$LFT $Htl $HE $HL HT]"); try done.
{ iApply Hwrt. }
{ iApply Hread. }
diff --git a/theories/typing/type.v b/theories/typing/type.v
index bb4e3563..02c80040 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -472,7 +472,7 @@ Instance: Params (@type_incl) 2.
(* Typeclasses Opaque type_incl. *)
Definition subtype `{typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
- elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗ type_incl ty1 ty2.
+ ∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗ type_incl ty1 ty2).
Instance: Params (@subtype) 4.
(* TODO: The prelude should have a symmetric closure. *)
@@ -505,12 +505,15 @@ Section subtyping.
Qed.
Lemma subtype_refl E L ty : subtype E L ty ty.
- Proof. iIntros. iApply type_incl_refl. Qed.
+ Proof. iIntros (?) "_ !# _". iApply type_incl_refl. Qed.
Global Instance subtype_preorder E L : PreOrder (subtype E L).
Proof.
split; first by intros ?; apply subtype_refl.
- intros ty1 ty2 ty3 H12 H23. iIntros.
- iApply type_incl_trans. by iApply H12. by iApply H23.
+ intros ty1 ty2 ty3 H12 H23. iIntros (?) "HL".
+ iDestruct (H12 with "HL") as "#H12".
+ iDestruct (H23 with "HL") as "#H23".
+ iClear "∗". iIntros "!# #HE".
+ iApply (type_incl_trans with "[#]"). by iApply "H12". by iApply "H23".
Qed.
Lemma equiv_subtype E L ty1 ty2 : ty1 ≡ ty2 → subtype E L ty1 ty2.
@@ -518,21 +521,27 @@ Section subtyping.
Lemma eqtype_unfold E L ty1 ty2 :
eqtype E L ty1 ty2 ↔
- (elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗
+ (∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗
(⌜ty1.(ty_size) = ty2.(ty_size)⌠∗
(□ ∀ tid vl, ty1.(ty_own) tid vl ↔ ty2.(ty_own) tid vl) ∗
- (□ ∀ κ tid l, ty1.(ty_shr) κ tid l ↔ ty2.(ty_shr) κ tid l))%I).
+ (□ ∀ κ tid l, ty1.(ty_shr) κ tid l ↔ ty2.(ty_shr) κ tid l)))%I).
Proof.
split.
- - iIntros ([EQ1 EQ2]) "#HE #HL".
- iDestruct (EQ1 with "HE HL") as "[#Hsz [#H1own #H1shr]]".
- iDestruct (EQ2 with "HE HL") as "[_ [#H2own #H2shr]]".
+ - iIntros ([EQ1 EQ2] qL) "HL".
+ iDestruct (EQ1 with "HL") as "#EQ1".
+ iDestruct (EQ2 with "HL") as "#EQ2".
+ iClear "∗". iIntros "!# #HE".
+ iDestruct ("EQ1" with "HE") as "[#Hsz [#H1own #H1shr]]".
+ iDestruct ("EQ2" with "HE") as "[_ [#H2own #H2shr]]".
iSplit; last iSplit.
+ done.
+ by iIntros "!#*"; iSplit; iIntros "H"; [iApply "H1own"|iApply "H2own"].
+ by iIntros "!#*"; iSplit; iIntros "H"; [iApply "H1shr"|iApply "H2shr"].
- - intros EQ. split; iIntros "#HE #HL"; (iSplit; last iSplit);
- iDestruct (EQ with "HE HL") as "[% [#Hown #Hshr]]".
+ - intros EQ. split; (iIntros (qL) "HL";
+ iDestruct (EQ with "HL") as "#EQ";
+ iClear "∗"; iIntros "!# #HE";
+ iDestruct ("EQ" with "HE") as "[% [#Hown #Hshr]]";
+ (iSplit; last iSplit)).
+ done.
+ iIntros "!#* H". by iApply "Hown".
+ iIntros "!#* H". by iApply "Hshr".
@@ -560,25 +569,25 @@ Section subtyping.
Qed.
Lemma subtype_simple_type E L (st1 st2 : simple_type) :
- (∀ tid vl, elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗
- st1.(st_own) tid vl -∗ st2.(st_own) tid vl) →
+ (∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗
+ ∀ tid vl, st1.(st_own) tid vl -∗ st2.(st_own) tid vl)) →
subtype E L st1 st2.
Proof.
- intros Hst. iIntros. iSplit; first done. iSplit; iAlways.
- - iIntros. iApply Hst; done.
+ intros Hst. iIntros (qL) "HL". iDestruct (Hst with "HL") as "#Hst".
+ iClear "∗". iIntros "!# #HE". iSplit; first done. iSplit; iAlways.
+ - iIntros. iApply "Hst"; done.
- iIntros (???). iDestruct 1 as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
- by iApply Hst.
+ by iApply "Hst".
Qed.
Lemma subtype_weaken E1 E2 L1 L2 ty1 ty2 :
E1 ⊆+ E2 → L1 ⊆+ L2 →
subtype E1 L1 ty1 ty2 → subtype E2 L2 ty1 ty2.
Proof.
- iIntros (HE12 ? Hsub) "HE HL".
- iApply (Hsub with "[HE] [HL]").
- - rewrite /elctx_interp_0. by iApply big_sepL_submseteq.
- - iDestruct "HL" as %HL. iPureIntro. intros ??. apply HL.
- eauto using elem_of_submseteq.
+ iIntros (HE12 ? Hsub qL) "HL". iDestruct (Hsub with "[HL]") as "#Hsub".
+ { rewrite /llctx_interp. by iApply big_sepL_submseteq. }
+ iClear "∗". iIntros "!# #HE". iApply "Hsub".
+ rewrite /elctx_interp. by iApply big_sepL_submseteq.
Qed.
End subtyping.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 92ef13e3..077f13ce 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -176,32 +176,31 @@ Section type_context.
(** Type context inclusion *)
Definition tctx_incl (E : elctx) (L : llctx) (T1 T2 : tctx): Prop :=
- ∀ tid q1 q2, lft_ctx -∗ elctx_interp E q1 -∗ llctx_interp L q2 -∗
- tctx_interp tid T1 ={⊤}=∗ elctx_interp E q1 ∗ llctx_interp L q2 ∗
- tctx_interp tid T2.
+ ∀ tid q2, lft_ctx -∗ elctx_interp E -∗ llctx_interp L q2 -∗
+ tctx_interp tid T1 ={⊤}=∗ llctx_interp L q2 ∗ tctx_interp tid T2.
Global Arguments tctx_incl _%EL _%LL _%TC _%TC.
Global Instance : ∀ E L, RewriteRelation (tctx_incl E L).
Global Instance tctx_incl_preorder E L : PreOrder (tctx_incl E L).
Proof.
split.
- - by iIntros (????) "_ $ $ $".
- - iIntros (??? H1 H2 ???) "#LFT HE HL H".
- iMod (H1 with "LFT HE HL H") as "(HE & HL & H)".
- by iMod (H2 with "LFT HE HL H") as "($ & $ & $)".
+ - by iIntros (???) "_ _ $ $".
+ - iIntros (??? H1 H2 ??) "#LFT #HE HL H".
+ iMod (H1 with "LFT HE HL H") as "(HL & H)".
+ by iMod (H2 with "LFT HE HL H") as "($ & $)".
Qed.
Lemma contains_tctx_incl E L T1 T2 : T1 ⊆+ T2 → tctx_incl E L T2 T1.
Proof.
- rewrite /tctx_incl. iIntros (Hc ???) "_ $ $ H". by iApply big_sepL_submseteq.
+ rewrite /tctx_incl. iIntros (Hc ??) "_ _ $ H". by iApply big_sepL_submseteq.
Qed.
Global Instance tctx_incl_app E L :
Proper (tctx_incl E L ==> tctx_incl E L ==> tctx_incl E L) app.
Proof.
- 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 & $)".
+ intros ?? Hincl1 ?? Hincl2 ??. rewrite /tctx_interp !big_sepL_app.
+ iIntros "#LFT #HE HL [H1 H2]".
+ iMod (Hincl1 with "LFT HE HL H1") as "(HL & $)".
iApply (Hincl2 with "LFT HE HL H2").
Qed.
Global Instance tctx_incl_cons E L x :
@@ -218,7 +217,7 @@ Section type_context.
Lemma copy_tctx_incl E L p `{!Copy ty} :
tctx_incl E L [p â— ty] [p â— ty; p â— ty].
Proof.
- iIntros (???) "_ $ $ *". rewrite /tctx_interp !big_sepL_cons big_sepL_nil.
+ iIntros (??) "_ _ $ *". rewrite /tctx_interp !big_sepL_cons big_sepL_nil.
by iIntros "[#$ $]".
Qed.
@@ -234,11 +233,9 @@ Section type_context.
Lemma subtype_tctx_incl E L p ty1 ty2 :
subtype E L ty1 ty2 → tctx_incl E L [p ◠ty1] [p ◠ty2].
Proof.
- iIntros (Hst ???) "#LFT HE HL H". rewrite /tctx_interp !big_sepL_singleton /=.
- iDestruct (elctx_interp_persist with "HE") as "#HE'".
- iDestruct (llctx_interp_persist with "HL") as "#HL'".
- iFrame "HE HL". iDestruct "H" as (v) "[% H]". iExists _. iFrame "%".
- iDestruct (Hst with "[] []") as "(_ & #Ho & _)"; [done..|by iApply "Ho"].
+ iIntros (Hst ??) "#LFT #HE HL H". rewrite /tctx_interp !big_sepL_singleton /=.
+ iDestruct "H" as (v) "[% H]". iDestruct (Hst with "HL HE") as "#(_ & Ho & _)".
+ iFrame "HL". iExists _. iFrame "%". by iApply "Ho".
Qed.
(* Extracting from a type context. *)
--
GitLab