diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index a601779a9da3592de6188fe88c28e56bf3907d6a..117e65c7c4be8d57dad2dae91d1ba801bd7725bf 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -1,5 +1,5 @@
From lrust.lifetime Require Import definitions.
-From lrust.typing Require Export type bool.
+From lrust.typing Require Export lft_contexts type bool.
Section fixpoint.
Context `{typeG Σ}.
@@ -64,41 +64,97 @@ Section fixpoint.
Qed.
End fixpoint.
-(* TODO : is there a way to declare this as a [Proper] instance ? *)
-Lemma fixpoint_mono `{typeG Σ} T1 `{Contractive T1} T2 `{Contractive T2} E L :
- (∀ ty1 ty2, subtype E L ty1 ty2 → subtype E L (T1 ty1) (T2 ty2)) →
- subtype E L (fixpoint T1) (fixpoint T2).
-Proof.
- intros H12. apply fixpoint_ind.
- - intros ?? [[EQsz EQown] EQshr] ?. etrans; last done. iIntros "_ _ _".
- unfold type_incl. simpl in *. iSplit; [|iSplit].
- + by iPureIntro; eapply symmetry, EQsz.
- + iIntros "!# *". specialize (EQown tid vl). simpl in EQown. rewrite EQown. auto.
- + iIntros "!# *". rewrite (EQshr κ tid l). auto.
- - by eexists _.
- - intros. rewrite (fixpoint_unfold_eqtype T2). by apply H12.
- - intros c Hc.
- assert (Hsz : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
- ⌜lft_contexts.llctx_interp_0 L⌠-∗
- ⌜(compl c).(ty_size) = (fixpoint T2).(ty_size)âŒ).
- { iIntros "LFT HE HL". iDestruct (Hc 0%nat with "LFT HE HL") as "[$ _]". }
- assert (Hown : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
- ⌜lft_contexts.llctx_interp_0 L⌠-∗
- □ (∀ tid vl, (compl c).(ty_own) tid vl -∗ (fixpoint T2).(ty_own) tid vl)).
- { apply uPred.entails_equiv_and, equiv_dist=>n.
- destruct (conv_compl (S n) c) as [[_ Heq] _]. setoid_rewrite (λ tid vl, Heq tid vl).
- apply equiv_dist, uPred.entails_equiv_and. iIntros "LFT HE HL".
- iDestruct (Hc (S n) with "LFT HE HL") as "[_ [$ _]]". }
- assert (Hshr : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
- ⌜lft_contexts.llctx_interp_0 L⌠-∗
- □ (∀ κ tid l,
- (compl c).(ty_shr) κ tid l -∗ (fixpoint T2).(ty_shr) κ tid l)).
- { apply uPred.entails_equiv_and, equiv_dist=>n.
- destruct (conv_compl n c) as [_ Heq]. setoid_rewrite (λ κ tid l, Heq κ tid l).
- apply equiv_dist, uPred.entails_equiv_and. iIntros "LFT HE HL".
- iDestruct (Hc n with "LFT HE HL") as "[_ [_ $]]". }
- iIntros "LFT HE HL". iSplit; [|iSplit].
- + iApply (Hsz with "LFT HE HL").
- + iApply (Hown with "LFT HE HL").
- + iApply (Hshr with "LFT HE HL").
-Qed.
+Section subtyping.
+ Context `{typeG Σ} (E : elctx) (L : llctx).
+
+ (* TODO : is there a way to declare these as a [Proper] instances ? *)
+ Lemma fixpoint_mono T1 `{Contractive T1} T2 `{Contractive T2} :
+ (∀ ty1 ty2, subtype E L ty1 ty2 → subtype E L (T1 ty1) (T2 ty2)) →
+ subtype E L (fixpoint T1) (fixpoint T2).
+ Proof.
+ intros H12. apply fixpoint_ind.
+ - intros ?? EQ ?. etrans; last done. by apply equiv_subtype.
+ - by eexists _.
+ - intros. rewrite (fixpoint_unfold_eqtype T2). by apply H12.
+ - intros c Hc.
+ assert (Hsz : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
+ ⌜lft_contexts.llctx_interp_0 L⌠-∗
+ ⌜(compl c).(ty_size) = (fixpoint T2).(ty_size)âŒ).
+ { iIntros "LFT HE HL". iDestruct (Hc 0%nat with "LFT HE HL") as "[$ _]". }
+ assert (Hown : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
+ ⌜lft_contexts.llctx_interp_0 L⌠-∗
+ □ (∀ tid vl, (compl c).(ty_own) tid vl -∗ (fixpoint T2).(ty_own) tid vl)).
+ { apply uPred.entails_equiv_and, equiv_dist=>n.
+ destruct (conv_compl (S n) c) as [[_ Heq] _]. setoid_rewrite (λ tid vl, Heq tid vl).
+ apply equiv_dist, uPred.entails_equiv_and. iIntros "LFT HE HL".
+ iDestruct (Hc (S n) with "LFT HE HL") as "[_ [$ _]]". }
+ assert (Hshr : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
+ ⌜lft_contexts.llctx_interp_0 L⌠-∗
+ □ (∀ κ tid l,
+ (compl c).(ty_shr) κ tid l -∗ (fixpoint T2).(ty_shr) κ tid l)).
+ { apply uPred.entails_equiv_and, equiv_dist=>n.
+ destruct (conv_compl n c) as [_ Heq]. setoid_rewrite (λ κ tid l, Heq κ tid l).
+ apply equiv_dist, uPred.entails_equiv_and. iIntros "LFT HE HL".
+ iDestruct (Hc n with "LFT HE HL") as "[_ [_ $]]". }
+ iIntros "LFT HE HL". iSplit; [|iSplit].
+ + iApply (Hsz with "LFT HE HL").
+ + iApply (Hown with "LFT HE HL").
+ + iApply (Hshr with "LFT HE HL").
+ Qed.
+
+ Lemma fixpoint_proper T1 `{Contractive T1} T2 `{Contractive T2} :
+ (∀ ty1 ty2, eqtype E L ty1 ty2 → eqtype E L (T1 ty1) (T2 ty2)) →
+ eqtype E L (fixpoint T1) (fixpoint T2).
+ Proof.
+ intros H12. apply fixpoint_ind.
+ - intros ?? EQ ?. etrans; last done. by apply equiv_eqtype.
+ - by eexists _.
+ - intros. rewrite (fixpoint_unfold_eqtype T2). by apply H12.
+ - intros c Hc. setoid_rewrite eqtype_unfold in Hc. rewrite eqtype_unfold.
+ assert (Hsz : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
+ ⌜lft_contexts.llctx_interp_0 L⌠-∗
+ ⌜(compl c).(ty_size) = (fixpoint T2).(ty_size)âŒ).
+ { iIntros "LFT HE HL". iDestruct (Hc 0%nat with "LFT HE HL") as "[$ _]". }
+ assert (Hown : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
+ ⌜lft_contexts.llctx_interp_0 L⌠-∗
+ □ (∀ tid vl, (compl c).(ty_own) tid vl ↔ (fixpoint T2).(ty_own) tid vl)).
+ { apply uPred.entails_equiv_and, equiv_dist=>n.
+ destruct (conv_compl (S n) c) as [[_ Heq] _]. setoid_rewrite (λ tid vl, Heq tid vl).
+ apply equiv_dist, uPred.entails_equiv_and. iIntros "LFT HE HL".
+ iDestruct (Hc (S n) with "LFT HE HL") as "[_ [$ _]]". }
+ assert (Hshr : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
+ ⌜lft_contexts.llctx_interp_0 L⌠-∗
+ □ (∀ κ tid l,
+ (compl c).(ty_shr) κ tid l ↔ (fixpoint T2).(ty_shr) κ tid l)).
+ { apply uPred.entails_equiv_and, equiv_dist=>n.
+ destruct (conv_compl n c) as [_ Heq]. setoid_rewrite (λ κ tid l, Heq κ tid l).
+ apply equiv_dist, uPred.entails_equiv_and. iIntros "LFT HE HL".
+ iDestruct (Hc n with "LFT HE HL") as "[_ [_ $]]". }
+ iIntros "LFT HE HL". iSplit; [|iSplit].
+ + iApply (Hsz with "LFT HE HL").
+ + iApply (Hown with "LFT HE HL").
+ + iApply (Hshr with "LFT HE HL").
+ Qed.
+
+ Lemma fixpoint_unfold_subtype_l ty T `{Contractive T} :
+ subtype E L ty (T (fixpoint T)) → subtype E L ty (fixpoint T).
+ Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
+ Lemma fixpoint_unfold_subtype_r ty T `{Contractive T} :
+ subtype E L (T (fixpoint T)) ty → subtype E L (fixpoint T) ty.
+ Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
+ Lemma fixpoint_unfold_eqtype_l ty T `{Contractive T} :
+ eqtype E L ty (T (fixpoint T)) → eqtype E L ty (fixpoint T).
+ Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
+ Lemma fixpoint_unfold_eqtype_r ty T `{Contractive T} :
+ eqtype E L (T (fixpoint T)) ty → eqtype E L (fixpoint T) ty.
+ Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
+End subtyping.
+
+Hint Resolve fixpoint_mono fixpoint_proper : lrust_typing.
+
+(* These hints can loop if [fixpoint_mono] and [fixpoint_proper] have
+ not been tried before, so we give them a high cost *)
+Hint Resolve fixpoint_unfold_subtype_l|100 : lrust_typing.
+Hint Resolve fixpoint_unfold_subtype_r|100 : lrust_typing.
+Hint Resolve fixpoint_unfold_eqtype_l|100 : lrust_typing.
+Hint Resolve fixpoint_unfold_eqtype_r|100 : lrust_typing.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 23a767f8322ba5b96afde162ed38746ba02aae6a..61a9b237987c1e0bb4cf729d8ba91bb24a96b543 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -64,30 +64,33 @@ End fn.
Section typing.
Context `{typeG Σ}.
- Lemma fn_subtype_ty {A n} E0 L0 E (tys1 : A → vec type n) tys2 ty1 ty2 :
- (∀ x, Forall2 (subtype (E0 ++ E x) L0) (tys2 x : vec _ n) (tys1 x)) →
- (∀ x, subtype (E0 ++ E x) L0 (ty1 x) (ty2 x)) →
- subtype E0 L0 (fn E tys1 ty1) (fn E tys2 ty2).
+ Lemma fn_subtype_full {A n} E0 L0 E E' (tys tys' : A → vec type n) ty ty' :
+ (∀ x, elctx_incl E0 L0 (E x) (E' x)) →
+ (∀ x, Forall2 (subtype (E0 ++ E x) L0) (tys' x) (tys x)) →
+ (∀ x, subtype (E0 ++ E x) L0 (ty x) (ty' x)) →
+ subtype E0 L0 (fn E' tys ty) (fn E tys' ty').
Proof.
- intros Htys Hty. apply subtype_simple_type=>//= _ vl.
+ intros HE Htys Hty. apply subtype_simple_type=>//= _ vl.
iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. iAlways. iNext.
rewrite /typed_body. iIntros "* #HEAP _ Htl HE HL HC HT".
- iDestruct (elctx_interp_persist with "HE") as "#HE'".
- iApply ("Hf" with "* HEAP LFT Htl HE HL [HC] [HT]").
- - iIntros "HE". unfold cctx_interp. iIntros (elt) "Helt".
+ iDestruct (elctx_interp_persist with "HE") as "#HEp".
+ iMod (HE with "HE0 HL0 * HE") as (qE') "[HE' Hclose]". done.
+ iApply ("Hf" with "* HEAP LFT Htl HE' HL [HC Hclose] [HT]").
+ - iIntros "HE'". unfold cctx_interp. iIntros (elt) "Helt".
iDestruct "Helt" as %->%elem_of_list_singleton. iIntros (ret) "Htl HL HT".
+ iMod ("Hclose" with "HE'") as "HE".
iSpecialize ("HC" with "HE"). unfold cctx_elt_interp.
iApply ("HC" $! (_ â—cont(_, _)%CC) with "[%] * Htl HL >").
- { by apply elem_of_list_singleton. }
+ { by apply elem_of_list_singleton. }
rewrite /tctx_interp !big_sepL_singleton /=.
iDestruct "HT" as (v) "[HP Hown]". iExists v. iFrame "HP".
- iDestruct (Hty x with "LFT [HE0 HE'] HL0") as "(_ & #Hty & _)".
+ iDestruct (Hty x with "LFT [HE0 HEp] HL0") as "(_ & #Hty & _)".
{ rewrite /elctx_interp_0 big_sepL_app. by iSplit. }
by iApply "Hty".
- rewrite /tctx_interp
- -(fst_zip (tys1 x) (tys2 x)) ?vec_to_list_length //
- -{1}(snd_zip (tys1 x) (tys2 x)) ?vec_to_list_length //
+ -(fst_zip (tys x) (tys' x)) ?vec_to_list_length //
+ -{1}(snd_zip (tys x) (tys' x)) ?vec_to_list_length //
!zip_with_fmap_r !(zip_with_zip (λ _ _, (_ ∘ _) _ _)) !big_sepL_fmap.
iApply big_sepL_impl. iSplit; last done. iIntros "{HT}!#".
iIntros (i [p [ty1' ty2']]) "#Hzip H /=".
@@ -101,40 +104,38 @@ Section typing.
+ by iApply "Ho".
Qed.
- Lemma fn_subtype_specialize {A B n} (σ : A → B) E0 L0 E tys ty :
- subtype E0 L0 (fn (n:=n) E tys ty) (fn (E ∘ σ) (tys ∘ σ) (ty ∘ σ)).
+ Lemma fn_subtype_ty {A n} E0 L0 E (tys1 tys2 : A → vec type n) ty1 ty2 :
+ (∀ x, Forall2 (subtype (E0 ++ E x) L0) (tys2 x) (tys1 x)) →
+ (∀ x, subtype (E0 ++ E x) L0 (ty1 x) (ty2 x)) →
+ subtype E0 L0 (fn E tys1 ty1) (fn E tys2 ty2).
Proof.
- apply subtype_simple_type=>//= _ vl.
- iIntros "#LFT _ _ Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
- iExists fb, kb, xb, e, _. iSplit. done. iSplit. done.
- rewrite /typed_body. iAlways. iNext. iIntros "*". iApply "Hf".
+ intros. apply fn_subtype_full; try done. intros. apply elctx_incl_refl.
Qed.
Lemma fn_subtype_elctx_sat {A n} E0 L0 E E' (tys : A → vec type n) ty :
(∀ x, elctx_sat (E x) [] (E' x)) →
subtype E0 L0 (fn E' tys ty) (fn E tys ty).
Proof.
- intros HEE'. apply subtype_simple_type=>//= _ vl.
- iIntros "#LFT _ _ Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
- iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. rewrite /typed_body.
- iAlways. iNext. iIntros "* #HEAP _ Htl HE #HL HC HT".
- iMod (HEE' x with "[%] HE HL") as (qE') "[HE Hclose]". done.
- iApply ("Hf" with "* HEAP LFT Htl HE HL [Hclose HC] HT"). iIntros "HE".
- iApply fupd_cctx_interp. iApply ("HC" with ">").
- by iMod ("Hclose" with "HE") as "[$ _]".
+ intros. apply fn_subtype_full; try done. by intros; apply elctx_sat_incl.
Qed.
Lemma fn_subtype_lft_incl {A n} E0 L0 E κ κ' (tys : A → vec type n) ty :
lctx_lft_incl E0 L0 κ κ' →
subtype E0 L0 (fn (λ x, (κ ⊑ κ') :: E x)%EL tys ty) (fn E tys ty).
Proof.
- intros Hκκ'. apply subtype_simple_type=>//= _ vl.
- iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
- iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. rewrite /typed_body.
- iAlways. iNext. iIntros "* #HEAP _ Htl HE #HL HC HT".
- iApply ("Hf" with "* HEAP LFT Htl [HE] HL [HC] HT").
- { rewrite /elctx_interp big_sepL_cons. iFrame. iApply (Hκκ' with "HE0 HL0"). }
- rewrite /elctx_interp big_sepL_cons. iIntros "[_ HE]". by iApply "HC".
+ intros Hκκ'. apply fn_subtype_full; try done. intros.
+ apply elctx_incl_lft_incl; last by apply elctx_incl_refl.
+ iIntros "#HE #HL". iApply (Hκκ' with "[HE] HL").
+ rewrite /elctx_interp_0 big_sepL_app. iDestruct "HE" as "[_ $]".
+ Qed.
+
+ Lemma fn_subtype_specialize {A B n} (σ : A → B) E0 L0 E tys ty :
+ subtype E0 L0 (fn (n:=n) E tys ty) (fn (E ∘ σ) (tys ∘ σ) (ty ∘ σ)).
+ Proof.
+ apply subtype_simple_type=>//= _ vl.
+ iIntros "#LFT _ _ Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
+ iExists fb, kb, xb, e, _. iSplit. done. iSplit. done.
+ rewrite /typed_body. iAlways. iNext. iIntros "*". iApply "Hf".
Qed.
(* TODO: Define some syntactic sugar for calling and letrec like we do on paper. *)
@@ -166,7 +167,7 @@ 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.
+ iMod (HEsat 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]".
@@ -202,3 +203,6 @@ Section typing.
by iApply sendc_change_tid.
Qed.
End typing.
+
+Hint Resolve fn_subtype_full : lrust_typing.
+Hint Constructors Forall2 : lrust_typing.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 9ac50908059ce36eb8153c5b8ba82326c2b19fa3..7ca89fbde839dfe4c1e3d2383fa9bdc8b66a83fd 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -154,18 +154,21 @@ Section lft_contexts.
Definition lctx_lft_incl κ κ' : Prop :=
elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗ κ ⊑ κ'.
+ Lemma lctx_lft_incl_relf κ : lctx_lft_incl κ κ.
+ Proof. iIntros "_ _". iApply lft_incl_refl. Qed.
+
Global Instance lctx_lft_incl_preorder : PreOrder lctx_lft_incl.
Proof.
- split.
- - iIntros (?) "_ _". iApply lft_incl_refl.
- - iIntros (??? H1 H2) "#HE #HL". iApply (lft_incl_trans with "[#] [#]").
- iApply (H1 with "HE HL"). iApply (H2 with "HE HL").
+ 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").
Qed.
Lemma lctx_lft_incl_static κ : lctx_lft_incl κ static.
Proof. iIntros "_ _". iApply lft_incl_static. Qed.
- Lemma lctx_lft_incl_local κ κ' κs : (κ ⊑ κs)%LL ∈ L → κ' ∈ κs → lctx_lft_incl κ κ'.
+ 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.
@@ -175,12 +178,20 @@ Section lft_contexts.
- etrans. done. apply gmultiset_union_subseteq_r.
Qed.
+ Lemma lctx_lft_incl_local' κ κ' κ'' κs :
+ (κ ⊑ κs)%LL ∈ L → κ' ∈ κs → lctx_lft_incl κ' κ'' → lctx_lft_incl κ κ''.
+ Proof. intros. etrans; last done. by eapply lctx_lft_incl_local. Qed.
+
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.
Qed.
+ Lemma lctx_lft_incl_external' κ κ' κ'' :
+ (κ ⊑ κ')%EL ∈ E → lctx_lft_incl κ' κ'' → lctx_lft_incl κ κ''.
+ Proof. intros. etrans; last done. by eapply lctx_lft_incl_external. Qed.
+
(* Lifetime aliveness *)
Definition lctx_lft_alive (κ : lft) : Prop :=
@@ -240,24 +251,31 @@ Section lft_contexts.
by iApply "Hclose'".
Qed.
+ Lemma lctx_lft_alive_external' κ κ':
+ (☀κ)%EL ∈ 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 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).
Lemma elctx_sat_nil : elctx_sat [].
Proof.
- iIntros (qE qL F) "%$$". iExists 1%Qp. rewrite /elctx_interp big_sepL_nil. auto.
+ 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').
Proof.
- iIntros (Hκ HE' qE qL F) "% [HE1 HE2] [HL1 HL2]".
+ 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.
+ 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']".
@@ -266,14 +284,84 @@ Section lft_contexts.
iApply "Hclose'". iFrame. by rewrite /elctx_interp.
Qed.
- Lemma elctx_sat_incl E' κ κ' :
+ Lemma elctx_sat_lft_incl E' κ κ' :
lctx_lft_incl κ κ' → elctx_sat E' → elctx_sat ((κ ⊑ κ') :: E').
Proof.
- iIntros (Hκκ' HE' qE qL F) "% HE HL".
+ 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.
+ iMod (HE' with "HE HL") as (q) "[HE' Hclose']". done.
iExists q. rewrite {1 2 4 5}/elctx_interp big_sepL_cons /=.
iIntros "{$Hincl $HE'}!>[_ ?]". by iApply "Hclose'".
Qed.
End lft_contexts.
+
+
+Section elctx_incl.
+ (* External lifetime context inclusion, in a persistent context.
+ (Used for function types subtyping). *)
+
+ 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).
+
+ Lemma elctx_incl_refl E' : elctx_incl E' E'.
+ Proof. iIntros (??) "_ _ * ?". iExists _. iFrame. eauto. Qed.
+
+ Lemma elctx_incl_nil E' : elctx_incl E' [].
+ Proof.
+ iIntros (??) "_ _ * $". iExists 1%Qp.
+ rewrite /elctx_interp big_sepL_nil. auto.
+ Qed.
+
+ Lemma elctx_incl_lft_alive E1 E2 κ :
+ lctx_lft_alive E1 [] κ → elctx_incl E1 E2 → elctx_incl E1 ((☀κ) :: E2).
+ Proof.
+ iIntros (Hκ HE2 ??) "#HE #HL * [HE11 HE12]".
+ iMod (Hκ _ _ 1%Qp with "HE11 []") as (qE21) "[Hκ Hclose]". done.
+ { by rewrite /llctx_interp big_sepL_nil. }
+ iMod (HE2 with "HE HL * HE12") as (qE22) "[HE2 Hclose']". done.
+ destruct (Qp_lower_bound qE21 qE22) as (qE2 & ? & ? & -> & ->).
+ iExists qE2. rewrite /elctx_interp big_sepL_cons /=.
+ iDestruct "HE2" as "[$ HE2]". iDestruct "Hκ" as "[$ Hκ]". iIntros "!> [Hκ' HE2']".
+ iMod ("Hclose" with "[$Hκ $Hκ']") as "[$ _]".
+ iApply "Hclose'". by iFrame.
+ Qed.
+
+ Lemma elctx_incl_lft_incl E1 E2 κ κ' :
+ lctx_lft_incl (E1 ++ E) 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. rewrite /elctx_interp big_sepL_cons /=. iFrame "∗#".
+ iIntros "!> [_ HE2']". by iApply "Hclose'".
+ 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.
+End elctx_incl.
+
+Hint Constructors Forall elem_of_list : 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_incl_refl elctx_incl_nil elctx_incl_lft_alive elctx_incl_lft_incl
+ : lrust_typing.
+
+Hint Resolve lctx_lft_alive_external' | 100 : lrust_typing.
\ No newline at end of file
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 1de12dcd04118092344fdc0f396b38052e9be855..8c5d5da06b675ce3e526433e06605aa5bbd7896e 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -111,10 +111,15 @@ Section own.
iMod ("Hvs" with "* [%] Htok") as "Hvs'". done. iModIntro. iNext.
iMod "Hvs'" as "[Hshr $]". iApply ("Hs" with "Hshr").
Qed.
-
+ Lemma own_mono' E L n ty1 ty2 :
+ subtype E L ty1 ty2 → subtype E L (own n ty1) (own n ty2).
+ Proof. apply own_mono. Qed.
Global Instance own_proper E L n :
Proper (eqtype E L ==> eqtype E L) (own n).
Proof. intros ?? Heq. split; f_equiv; apply Heq. Qed.
+ Lemma own_proper' E L n ty1 ty2 :
+ eqtype E L ty1 ty2 → eqtype E L (own n ty1) (own n ty2).
+ Proof. apply own_proper. Qed.
Global Instance own_contractive n : Contractive (own n).
Proof.
@@ -123,7 +128,6 @@ Section own.
- destruct m=>// tid vl /=. repeat (apply EQ || f_contractive || f_equiv).
- intros κ tid l. repeat (apply EQ || f_contractive || f_equiv).
Qed.
-
Global Instance own_ne n m : Proper (dist m ==> dist m) (own n).
Proof. apply contractive_ne, _. Qed.
@@ -210,3 +214,5 @@ Section typing.
rewrite freeable_sz_full. by iFrame.
Qed.
End typing.
+
+Hint Resolve own_mono' own_proper' : lrust_typing.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index c57ba87f990a6fee4ddf04654755d25203ca5da8..b83e10de9ee8453f7f919646a719f51982ba0d30 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -91,9 +91,17 @@ Section product.
+ by iApply "Hs1".
+ rewrite -(_ : ty_size ty11 = ty_size ty12) //. by iApply "Hs2".
Qed.
+ Lemma product2_mono' E L ty11 ty12 ty21 ty22 :
+ subtype E L ty11 ty12 → subtype E L ty21 ty22 →
+ subtype E L (product2 ty11 ty21) (product2 ty12 ty22).
+ Proof. by intros; apply product2_mono. Qed.
Global Instance product2_proper E L:
Proper (eqtype E L ==> eqtype E L ==> eqtype E L) product2.
Proof. by intros ??[]??[]; split; apply product2_mono. Qed.
+ Lemma product2_proper' E L ty11 ty12 ty21 ty22 :
+ eqtype E L ty11 ty12 → eqtype E L ty21 ty22 →
+ eqtype E L (product2 ty11 ty21) (product2 ty12 ty22).
+ Proof. by intros; apply product2_proper. Qed.
Global Instance product2_copy `{!Copy ty1} `{!Copy ty2} :
Copy (product2 ty1 ty2).
@@ -152,9 +160,15 @@ Section product.
Global Instance product_mono E L:
Proper (Forall2 (subtype E L) ==> subtype E L) product.
Proof. intros ??. induction 1=>//=. by f_equiv. Qed.
+ Lemma product_mono' E L tyl1 tyl2 :
+ Forall2 (subtype E L) tyl1 tyl2 → subtype E L (product tyl1) (product tyl2).
+ Proof. apply product_mono. Qed.
Global Instance product_proper E L:
Proper (Forall2 (eqtype E L) ==> eqtype E L) product.
Proof. intros ??. induction 1=>//=. by f_equiv. Qed.
+ Lemma product_proper' E L tyl1 tyl2 :
+ Forall2 (eqtype E L) tyl1 tyl2 → eqtype E L (product tyl1) (product tyl2).
+ Proof. apply product_proper. Qed.
Global Instance product_copy tys : LstCopy tys → Copy (product tys).
Proof. induction 1; apply _. Qed.
Global Instance product_send tys : LstSend tys → Send (product tys).
@@ -229,3 +243,8 @@ Section typing.
eqtype E L (Î [Î tyl1; Î tyl2]) (Î (tyl1 ++ tyl2)).
Proof. by rewrite -prod_flatten_r -prod_flatten_l. Qed.
End typing.
+
+
+Hint Resolve product_mono' product_proper' : lrust_type_scope.
+Hint Constructors Forall2 : lrust_type_scope.
+Hint Resolve product2_mono' product2_proper' | 100 : lrust_type_scope.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index ac6617e070389103e918b40b6372d71cfa37e8fb..85e63252dee30a9c0c928b450c14a31607ab02c9 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -13,7 +13,7 @@ Section shr_bor.
iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
Qed.
- Global Instance subtype_shr_bor_mono E L :
+ Global Instance shr_mono E L :
Proper (flip (lctx_lft_incl E L) ==> subtype E L ==> subtype E L) shr_bor.
Proof.
intros κ1 κ2 Hκ ty1 ty2 Hty. apply subtype_simple_type.
@@ -23,12 +23,12 @@ Section shr_bor.
iDestruct (Hty with "* [] [] []") as "(_ & _ & #Hs1)"; [done..|clear Hty].
by iApply "Hs1".
Qed.
- Global Instance subtype_shr_bor_mono' E L :
+ Global Instance shr_mono_flip E L :
Proper (lctx_lft_incl E L ==> flip (subtype E L) ==> flip (subtype E L)) shr_bor.
- Proof. intros ??????. by apply subtype_shr_bor_mono. Qed.
- Global Instance subtype_shr_bor_proper E L κ :
+ Proof. intros ??????. by apply shr_mono. Qed.
+ Global Instance shr_proper E L κ :
Proper (eqtype E L ==> eqtype E L) (shr_bor κ).
- Proof. intros ??[]. by split; apply subtype_shr_bor_mono. Qed.
+ Proof. intros ??[]. by split; apply shr_mono. Qed.
Global Instance shr_contractive κ : Contractive (shr_bor κ).
Proof.
@@ -52,6 +52,14 @@ Notation "&shr{ κ } ty" := (shr_bor κ ty)
Section typing.
Context `{typeG Σ}.
+ Lemma shr_mono' E L κ1 κ2 ty1 ty2 :
+ lctx_lft_incl E L κ2 κ1 → subtype E L ty1 ty2 →
+ subtype E L (&shr{κ1} ty1) (&shr{κ2} ty2).
+ Proof. by intros; apply shr_mono. Qed.
+ Lemma shr_proper' E L κ ty1 ty2 :
+ eqtype E L ty1 ty2 → eqtype E L (&shr{κ} ty1) (&shr{κ} ty2).
+ Proof. by intros; apply shr_proper. Qed.
+
Lemma tctx_reborrow_shr E L p ty κ κ' :
lctx_lft_incl E L κ' κ →
tctx_incl E L [p â— &shr{κ}ty] [p â— &shr{κ'}ty; p â—{κ} &shr{κ}ty].
@@ -85,3 +93,5 @@ Section typing.
iMod ("Hclose" with "Hκ") as "[$ $]". iExists _. auto.
Qed.
End typing.
+
+Hint Resolve shr_mono' shr_proper' : lrust_typing.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 1944f785c8df44dd2bfdcd25db962f11a333904c..a60c01d19e2ae802583ed31c5c6639df60ee04bc 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -145,13 +145,18 @@ Section sum.
iDestruct "Hlen" as %<-. done.
+ iDestruct ("Hty" $! i) as "(_ & _ & #Htyi)". by iApply "Htyi".
Qed.
-
+ Lemma sum_mono' E L tyl1 tyl2 :
+ Forall2 (subtype E L) tyl1 tyl2 → subtype E L (sum tyl1) (sum tyl2).
+ Proof. apply sum_mono. Qed.
Global Instance sum_proper E L :
Proper (Forall2 (eqtype E L) ==> eqtype E L) sum.
Proof.
intros tyl1 tyl2 Heq; split; eapply sum_mono; [|rewrite -Forall2_flip];
(eapply Forall2_impl; [done|by intros ?? []]).
Qed.
+ Lemma sum_proper' E L tyl1 tyl2 :
+ Forall2 (eqtype E L) tyl1 tyl2 → eqtype E L (sum tyl1) (sum tyl2).
+ Proof. apply sum_proper. Qed.
Lemma nth_empty {A : Type} i (d : A) :
nth i [] d = d.
@@ -231,3 +236,6 @@ End sum.
as Î for products. We stick to the following form. *)
Notation "Σ[ ty1 ; .. ; tyn ]" :=
(sum (cons ty1 (..(cons tyn nil)..))) : lrust_type_scope.
+
+Hint Resolve sum_mono' sum_proper' : lrust_type_scope.
+Hint Constructors Forall2 : lrust_type_scope.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 823bed72138f39f859c5f35e9fbe275d6bcbf106..f1170b38cb0f0ee80d906427b23b28a79753e331 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -332,7 +332,7 @@ Section subtyping.
(□ ∀ κ tid l, ty1.(ty_shr) κ tid l -∗ ty2.(ty_shr) κ tid l))%I.
Global Instance type_incl_persistent ty1 ty2 : PersistentP (type_incl ty1 ty2) := _.
-(* Typeclasses Opaque type_incl. *)
+ (* Typeclasses Opaque type_incl. *)
Lemma type_incl_refl ty : type_incl ty ty.
Proof. iSplit; first done. iSplit; iAlways; iIntros; done. Qed.
@@ -354,28 +354,64 @@ Section subtyping.
lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗
type_incl ty1 ty2.
+ Lemma subtype_refl ty : subtype ty ty.
+ Proof. iIntros. iApply type_incl_refl. Qed.
+
+ Lemma equiv_subtype ty1 ty2 : ty1 ≡ ty2 → subtype ty1 ty2.
+ Proof. unfold subtype, type_incl=>EQ. setoid_rewrite EQ. apply subtype_refl. Qed.
+
Global Instance subtype_preorder : PreOrder subtype.
Proof.
- split.
- - 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.
+ split; first by intros ?; apply subtype_refl.
+ intros ty1 ty2 ty3 H12 H23. iIntros.
+ iApply (type_incl_trans with "[] []").
+ - iApply (H12 with "[] []"); done.
+ - iApply (H23 with "[] []"); done.
Qed.
(* TODO: The prelude should have a symmetric closure. *)
Definition eqtype (ty1 ty2 : type) : Prop :=
subtype ty1 ty2 ∧ subtype ty2 ty1.
+ Lemma eqtype_unfold ty1 ty2 :
+ eqtype ty1 ty2 ↔
+ (lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗
+ (⌜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).
+ Proof.
+ split.
+ - iIntros ([EQ1 EQ2]) "#LFT #HE #HL".
+ iDestruct (EQ1 with "LFT HE HL") as "[#Hsz [#H1own #H1shr]]".
+ iDestruct (EQ2 with "LFT HE HL") 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 "#LFT #HE #HL"; (iSplit; last iSplit);
+ iDestruct (EQ with "LFT HE HL") as "[% [#Hown #Hshr]]".
+ + done.
+ + iIntros "!#* H". by iApply "Hown".
+ + iIntros "!#* H". by iApply "Hshr".
+ + done.
+ + iIntros "!#* H". by iApply "Hown".
+ + iIntros "!#* H". by iApply "Hshr".
+ Qed.
+
+ Lemma eqtype_refl ty : eqtype ty ty.
+ Proof. by split. Qed.
+
+ Lemma equiv_eqtype ty1 ty2 : ty1 ≡ ty2 → eqtype ty1 ty2.
+ Proof. by split; apply equiv_subtype. Qed.
+
Global Instance subtype_proper :
Proper (eqtype ==> eqtype ==> iff) subtype.
Proof. intros ??[] ??[]. split; intros; by etrans; [|etrans]. Qed.
- Global Instance subtype_equivalence : Equivalence eqtype.
+ Global Instance eqtype_equivalence : Equivalence eqtype.
Proof.
split.
- - split; done.
+ - by split.
- intros ?? Heq; split; apply Heq.
- intros ??? H1 H2. split; etrans; (apply H1 || apply H2).
Qed.
@@ -392,3 +428,7 @@ Section subtyping.
by iApply (Hst with "* [] [] []").
Qed.
End subtyping.
+
+Hint Resolve subtype_refl eqtype_refl : lrust_typing.
+
+Ltac solve_typing := by eauto 100 with lrust_typing.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index 6153466d31c78feb7a2f2101a1d2d5124b5091a8..45f009475689ebbaee8d55ba03db7834e76c5f82 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -27,12 +27,21 @@ Section uninit.
Lemma uninit_sz n : ty_size (uninit n) = n.
Proof. induction n. done. simpl. by f_equal. Qed.
- Lemma uninit_product E L ns :
+ Lemma uninit_product_eqtype E L ns :
eqtype E L (uninit (foldr plus 0%nat ns)) (Î (uninit <$> ns)).
Proof.
induction ns as [|n ns IH]. done. revert IH.
by rewrite /= /uninit replicate_plus prod_flatten_l -!prod_app=>->.
Qed.
+ Lemma uninit_product_eqtype' E L ns :
+ eqtype E L (Î (uninit <$> ns)) (uninit (foldr plus 0%nat ns)).
+ Proof. symmetry; apply uninit_product_eqtype. Qed.
+ Lemma uninit_product_subtype E L ns :
+ subtype E L (uninit (foldr plus 0%nat ns)) (Î (uninit <$> ns)).
+ Proof. apply uninit_product_eqtype'. Qed.
+ Lemma uninit_product_subtype' E L ns :
+ subtype E L (Î (uninit <$> ns)) (uninit (foldr plus 0%nat ns)).
+ Proof. apply uninit_product_eqtype. Qed.
Lemma uninit_own n tid vl :
(uninit n).(ty_own) tid vl ⊣⊢ ⌜length vl = nâŒ.
@@ -46,3 +55,6 @@ Section uninit.
iApply "IH". by inversion Heq.
Qed.
End uninit.
+
+Hint Resolve uninit_product_eqtype uninit_product_eqtype'
+ uninit_product_subtype uninit_product_subtype' : lrust_typing.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index dc509a109b5a553b24f8aee1d34ecfc4794714b5..df6e966aa0a83a90ae379a69cf391ed719610b42 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -71,7 +71,7 @@ Section uniq_bor.
by iApply (ty_shr_mono with "LFT Hκ0").
Qed.
- Global Instance subtype_uniq_mono E L :
+ Global Instance uniq_mono E L :
Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) uniq_bor.
Proof.
intros κ1 κ2 Hκ ty1 ty2 [Hty1 Hty2]. iIntros. iSplit; first done.
@@ -97,12 +97,12 @@ Section uniq_bor.
iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
iApply (ty_shr_mono with "[] Hincl'"); [done..|]. by iApply "Hs1".
Qed.
- Global Instance subtype_uniq_mono' E L :
+ Global Instance uniq_mono_flip E L :
Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L)) uniq_bor.
- Proof. intros ??????. apply subtype_uniq_mono. done. by symmetry. Qed.
- Global Instance subtype_uniq_proper E L κ :
+ Proof. intros ??????. apply uniq_mono. done. by symmetry. Qed.
+ Global Instance uniq_proper E L κ :
Proper (eqtype E L ==> eqtype E L) (uniq_bor κ).
- Proof. split; by apply subtype_uniq_mono. Qed.
+ Proof. split; by apply uniq_mono. Qed.
Global Instance uniq_contractive κ : Contractive (uniq_bor κ).
Proof.
@@ -142,6 +142,14 @@ Notation "&uniq{ κ } ty" := (uniq_bor κ ty)
Section typing.
Context `{typeG Σ}.
+ Lemma uniq_mono' E L κ1 κ2 ty1 ty2 :
+ lctx_lft_incl E L κ2 κ1 → eqtype E L ty1 ty2 →
+ subtype E L (&uniq{κ1} ty1) (&uniq{κ2} ty2).
+ Proof. by intros; apply uniq_mono. Qed.
+ Lemma uniq_proper' E L κ ty1 ty2 :
+ eqtype E L ty1 ty2 → eqtype E L (&uniq{κ} ty1) (&uniq{κ} ty2).
+ Proof. by intros; apply uniq_proper. Qed.
+
Lemma tctx_share E L p κ ty :
lctx_lft_alive E L κ → tctx_incl E L [p ◠&uniq{κ}ty] [p ◠&shr{κ}ty].
Proof.
@@ -207,3 +215,5 @@ Section typing.
iExists _, _. erewrite <-uPred.iff_refl. auto.
Qed.
End typing.
+
+Hint Resolve uniq_mono' uniq_proper' : lrust_typing.