Commit 8b20b70e authored by Jonas Kastberg's avatar Jonas Kastberg

Added kinded polymorphism

parent 12aa1f34
......@@ -17,8 +17,8 @@ theories/examples/sort_br_del.v
theories/examples/sort_fg.v
theories/examples/map.v
theories/examples/map_reduce.v
theories/logrel/model.v
theories/logrel/ltyping.v
theories/logrel/lsty.v
theories/logrel/session_types.v
theories/logrel/types.v
theories/logrel/subtyping.v
......
......@@ -196,7 +196,7 @@ Section copying.
Lemma ltyped_rec Γ Γ' f x e A1 A2 :
env_copy Γ Γ' -
(binder_insert f (A1 A2)%lty (binder_insert x A1 Γ') e : A2) -
(binder_insert f (A1 A2)%kind (binder_insert x A1 Γ') e : A2) -
Γ (rec: f x := e) : A1 A2 .
Proof.
iIntros "#Hcopy #He". iIntros (vs) "!> HΓ /=". iApply wp_fupd. wp_pures.
......
......@@ -98,7 +98,7 @@ Section double.
iSplitL; last by iApply env_ltyped_empty.
iIntros (c) "Hc".
iApply (wp_prog with "[Hc]").
{ iApply (iProto_mapsto_le _ (<??> lty_int; <??> lty_int; END)%lsty with "Hc").
{ iApply (iProto_mapsto_le _ (<??> lty_int; <??> lty_int; END)%kind with "Hc").
iApply iProto_le_recv.
iIntros "!> !> !>" (? [x ->]).
iExists _. do 2 (iSplit; [done|]).
......
From actris.logrel Require Import model.
From iris.heap_lang Require Export lifting metatheory.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import adequacy notation proofmode.
(* The domain of semantic types: Iris predicates over values *)
Record lty Σ := Lty {
lty_car :> val iProp Σ;
}.
Arguments Lty {_} _%I.
Arguments lty_car {_} _ _ : simpl never.
Bind Scope lty_scope with lty.
Delimit Scope lty_scope with lty.
(* The COFE structure on semantic types *)
Section lty_ofe.
Context `{Σ : gFunctors}.
(* Equality of semantic types is extensional equality *)
Instance lty_equiv : Equiv (lty Σ) := λ A B, w, A w B w.
Instance lty_dist : Dist (lty Σ) := λ n A B, w, A w {n} B w.
(* OFE and COFE structure is taken from isomorphism with val -d> iProp Σ *)
Lemma lty_ofe_mixin : OfeMixin (lty Σ).
Proof. by apply (iso_ofe_mixin (lty_car : _ val -d> _)). Qed.
Canonical Structure ltyO := OfeT (lty Σ) lty_ofe_mixin.
Global Instance lty_cofe : Cofe ltyO.
Proof. by apply (iso_cofe (@Lty _ : (val -d> _) ltyO) lty_car). Qed.
Global Instance lty_inhabited : Inhabited (lty Σ) := populate (Lty inhabitant).
Global Instance lty_car_ne n : Proper (dist n ==> (=) ==> dist n) lty_car.
Proof. by intros A A' ? w ? <-. Qed.
Global Instance lty_car_proper : Proper (() ==> (=) ==> ()) lty_car.
Proof. by intros A A' ? w ? <-. Qed.
Global Instance lty_ne n : Proper (pointwise_relation _ (dist n) ==> dist n) Lty.
Proof. by intros ???. Qed.
Global Instance lty_proper : Proper (pointwise_relation _ () ==> ()) Lty.
Proof. by intros ???. Qed.
End lty_ofe.
Arguments ltyO : clear implicits.
(* Typing for operators *)
Class LTyUnboxed {Σ} (A : lty Σ) :=
lty_unboxed v : A v - val_is_unboxed v .
Class LTyUnOp {Σ} (op : un_op) (A B : lty Σ) :=
lty_un_op v : A v - w, un_op_eval op v = Some w B w.
Class LTyBinOp {Σ} (op : bin_op) (A1 A2 B : lty Σ) :=
lty_bin_op v1 v2 : A1 v1 - A2 v2 - w, bin_op_eval op v1 v2 = Some w B w.
Section Environment.
Context `{invG Σ}.
Implicit Types A : lty Σ.
......
From iris.heap_lang Require Export lifting metatheory.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import notation proofmode.
From actris.channel Require Import proto proofmode.
Record lty_raw Σ := Lty {
lty_car :> val iProp Σ;
}.
Arguments Lty {_} _%I.
Arguments lty_car {_} _ _ : simpl never.
(* The COFE structure on semantic types *)
Section lty_ofe.
Context `{Σ : gFunctors}.
(* Equality of semantic types is extensional equality *)
Instance lty_equiv : Equiv (lty_raw Σ) := λ A B, w, A w B w.
Instance lty_dist : Dist (lty_raw Σ) := λ n A B, w, A w {n} B w.
(* OFE and COFE structure is taken from isomorphism with val -d> iProp Σ *)
Lemma lty_ofe_mixin : OfeMixin (lty_raw Σ).
Proof. by apply (iso_ofe_mixin (lty_car : _ val -d> _)). Qed.
Canonical Structure lty_rawO := OfeT (lty_raw Σ) lty_ofe_mixin.
Global Instance lty_cofe : Cofe lty_rawO.
Proof. by apply (iso_cofe (@Lty _ : (val -d> _) lty_rawO) lty_car). Qed.
Global Instance lty_inhabited : Inhabited (lty_raw Σ) := populate (Lty inhabitant).
Global Instance lty_car_ne n : Proper (dist n ==> (=) ==> dist n) lty_car.
Proof. by intros A A' ? w ? <-. Qed.
Global Instance lty_car_proper : Proper (() ==> (=) ==> ()) lty_car.
Proof. by intros A A' ? w ? <-. Qed.
Global Instance lty_ne n : Proper (pointwise_relation _ (dist n) ==> dist n) Lty.
Proof. by intros ???. Qed.
Global Instance lty_proper : Proper (pointwise_relation _ () ==> ()) Lty.
Proof. by intros ???. Qed.
End lty_ofe.
Arguments lty_rawO : clear implicits.
Record lsty_raw Σ := Lsty {
lsty_car :> iProto Σ;
}.
Arguments Lsty {_} _%proto.
Arguments lsty_car {_} _ : simpl never.
Section lsty_ofe.
Context `{Σ : gFunctors}.
Instance lsty_equiv : Equiv (lsty_raw Σ) :=
λ P Q, lsty_car P lsty_car Q.
Instance lsty_dist : Dist (lsty_raw Σ) :=
λ n P Q, lsty_car P {n} lsty_car Q.
Lemma lsty_ofe_mixin : OfeMixin (lsty_raw Σ).
Proof. by apply (iso_ofe_mixin (lsty_car : _ iProto _)). Qed.
Canonical Structure lsty_rawO := OfeT (lsty_raw Σ) lsty_ofe_mixin.
Global Instance lsty_cofe : Cofe lsty_rawO.
Proof. by apply (iso_cofe (@Lsty _ : _ lsty_rawO) lsty_car). Qed.
Global Instance lsty_inhabited : Inhabited (lsty_raw Σ) :=
populate (Lsty inhabitant).
Global Instance lsty_car_ne : NonExpansive lsty_car.
Proof. intros n A A' H. exact H. Qed.
Global Instance lsty_car_proper : Proper (() ==> ()) lsty_car.
Proof. intros A A' H. exact H. Qed.
Global Instance Lsty_ne : NonExpansive Lsty.
Proof. solve_proper. Qed.
Global Instance Lsty_proper : Proper (() ==> ()) Lsty.
Proof. solve_proper. Qed.
End lsty_ofe.
Arguments lsty_rawO : clear implicits.
Inductive kind :=
| ty_kind | sty_kind.
Definition kind_interp (k : kind) Σ : Type :=
match k with
| ty_kind => lty_raw Σ
| sty_kind => lsty_raw Σ
end.
Notation lty Σ := (kind_interp ty_kind Σ).
Notation lsty Σ := (kind_interp sty_kind Σ).
Bind Scope kind_scope with kind_interp.
Delimit Scope kind_scope with kind.
(* The COFE structure on semantic types *)
Section lty_ofe.
Context `{Σ : gFunctors}.
Instance kind_interp_equiv k : Equiv (kind_interp k Σ) :=
match k with
| ty_kind => λ A B, w, A w B w
| lty_kind => λ S T, lsty_car S lsty_car T
end.
Instance kind_interp_dist k : Dist (kind_interp k Σ) :=
match k with
| ty_kind => λ n A B, w, A w {n} B w
| lty_kind => λ n S T, lsty_car S {n} lsty_car T
end.
Lemma kind_interp_mixin k : OfeMixin (kind_interp k Σ).
Proof.
destruct k.
- by apply (iso_ofe_mixin (lty_car : _ val -d> _)).
- by apply (iso_ofe_mixin (lsty_car : _ iProto _)).
Qed.
Canonical Structure kind_interpO k :=
OfeT (kind_interp k Σ) (kind_interp_mixin k).
Global Instance kind_interp_cofe k : Cofe (kind_interpO k).
Proof.
destruct k.
- by apply (iso_cofe (@Lty _ : (val -d> _) (kind_interpO ty_kind)) lty_car).
- by apply (iso_cofe (@Lsty _ : _ (kind_interpO sty_kind)) lsty_car).
Qed.
Global Instance kind_interp_inhabited k : Inhabited (kind_interp k Σ).
Proof.
destruct k.
- apply (populate (Lty inhabitant)).
- apply (populate (Lsty inhabitant)).
Qed.
End lty_ofe.
Arguments kind_interpO : clear implicits.
Notation ltyO Σ := (kind_interpO Σ ty_kind).
Notation lstyO Σ := (kind_interpO Σ sty_kind).
(* Typing for operators *)
Class LTyUnboxed {Σ} (A : lty Σ) :=
lty_unboxed v : A v - val_is_unboxed v .
Class LTyUnOp {Σ} (op : un_op) (A B : lty Σ) :=
lty_un_op v : A v - w, un_op_eval op v = Some w B w.
Class LTyBinOp {Σ} (op : bin_op) (A1 A2 B : lty Σ) :=
lty_bin_op v1 v2 : A1 v1 - A2 v2 - w, bin_op_eval op v1 v2 = Some w B w.
From actris.logrel Require Export ltyping lsty.
From actris.logrel Require Export model.
From iris.algebra Require Import gmap.
From iris.heap_lang Require Export lifting metatheory.
From iris.base_logic.lib Require Import invariants.
......@@ -113,9 +113,9 @@ Section Propers.
Proof. intros [S]. rewrite /lsty_app. by rewrite right_id. Qed.
End Propers.
Notation "'END'" := lsty_end : lsty_scope.
Notation "'END'" := lsty_end : kind_scope.
Notation "<!!> A ; S" :=
(lsty_send A S) (at level 20, A, S at level 200) : lsty_scope.
(lsty_send A S) (at level 20, A, S at level 200) : kind_scope.
Notation "<??> A ; S" :=
(lsty_recv A S) (at level 20, A, S at level 200) : lsty_scope.
Infix "<++>" := lsty_app (at level 60) : lsty_scope.
(lsty_recv A S) (at level 20, A, S at level 200) : kind_scope.
Infix "<++>" := lsty_app (at level 60) : kind_scope.
......@@ -6,7 +6,7 @@ From iris.heap_lang Require Import proofmode.
Definition lty_le {Σ} (A1 A2 : lty Σ) : iProp Σ :=
( v, A1 v - A2 v)%I.
Arguments lty_le {_} _%lty _%lty.
Arguments lty_le {_} _%kind _%kind.
Infix "<:" := lty_le (at level 70).
Instance: Params (@lty_le) 1 := {}.
Instance lty_le_ne {Σ} : NonExpansive2 (@lty_le Σ).
......@@ -16,7 +16,7 @@ Proof. solve_proper. Qed.
Definition lty_bi_le {Σ} (A1 A2 : lty Σ) : iProp Σ :=
A1 <: A2 A2 <: A1.
Arguments lty_bi_le {_} _%lty _%lty.
Arguments lty_bi_le {_} _%kind _%kind.
Infix "<:>" := lty_bi_le (at level 70).
Instance: Params (@lty_bi_le) 1 := {}.
Instance lty_bi_le_ne {Σ} : NonExpansive2 (@lty_bi_le Σ).
......@@ -26,7 +26,7 @@ Proof. solve_proper. Qed.
Definition lsty_le {Σ} (P1 P2 : lsty Σ) : iProp Σ :=
( iProto_le P1 P2)%I.
Arguments lsty_le {_} _%lsty _%lsty.
Arguments lsty_le {_} _%kind _%kind.
Infix "<s:" := lsty_le (at level 70).
Instance: Params (@lsty_le) 1 := {}.
Instance lsty_le_ne {Σ} : NonExpansive2 (@lsty_le Σ).
......@@ -36,7 +36,7 @@ Proof. solve_proper. Qed.
Definition lsty_bi_le {Σ} (S1 S2 : lsty Σ) : iProp Σ :=
S1 <s: S2 S2 <s: S1.
Arguments lty_bi_le {_} _%lsty _%lsty.
Arguments lty_bi_le {_} _%kind _%kind.
Infix "<s:>" := lsty_bi_le (at level 70).
Instance: Params (@lsty_bi_le) 1 := {}.
Instance lsty_bi_le_ne {Σ} : NonExpansive2 (@lsty_bi_le Σ).
......@@ -318,7 +318,7 @@ Section subtype.
Lemma lsty_le_app_choice a (Ss : gmap Z (lsty Σ)) S2 :
lsty_choice a Ss <++> S2 <s:>
lsty_choice a ((λ S1, S1 <++> S2)%lsty <$> Ss).
lsty_choice a ((λ S1, S1 <++> S2)%kind <$> Ss).
Proof.
destruct a.
- rewrite /lsty_app iProto_app_message_tele.
......@@ -331,7 +331,7 @@ Section subtype.
* destruct HSs as [S HSs]=> /=.
rewrite !lookup_total_alt HSs /=.
rewrite lookup_fmap in HSs.
apply fmap_Some_1 in HSs as [S' [-> ->]].
apply fmap_Some_1 in HSs as [S' [Heq1 ->]]. rewrite Heq1.
iApply iProto_le_refl.
+ rewrite /lsty_select /lsty_choice.
iApply iProto_le_send.
......@@ -359,16 +359,16 @@ Section subtype.
* destruct HSs as [S HSs]=> /=.
rewrite !lookup_total_alt HSs /=.
rewrite lookup_fmap in HSs.
apply fmap_Some_1 in HSs as [S' [-> ->]].
apply fmap_Some_1 in HSs as [S' [Heq ->]]. rewrite Heq.
iApply iProto_le_refl.
Qed.
Lemma lsty_le_app_select A Ss S2 :
(lsty_select Ss) <++> S2 <s:> (lsty_select ((λ S1, S1 <++> S2)%lsty <$> Ss)).
(lsty_select Ss) <++> S2 <s:> (lsty_select ((λ S1, S1 <++> S2)%kind <$> Ss)).
Proof. apply lsty_le_app_choice. Qed.
Lemma lsty_le_app_branch A Ss S2 :
(lsty_branch Ss) <++> S2 <s:> (lsty_branch ((λ S1, S1 <++> S2)%lsty <$> Ss)).
(lsty_branch Ss) <++> S2 <s:> (lsty_branch ((λ S1, S1 <++> S2)%kind <$> Ss)).
Proof. apply lsty_le_app_choice. Qed.
Lemma lsty_le_app_id_l S : (END <++> S) <s:> S.
......@@ -418,7 +418,7 @@ Section subtype.
* destruct HSs as [S HSs]=> /=.
rewrite !lookup_total_alt HSs /=.
rewrite lookup_fmap in HSs.
apply fmap_Some_1 in HSs as [S' [-> ->]].
apply fmap_Some_1 in HSs as [S' [Heq ->]]. rewrite Heq.
iApply iProto_le_refl.
- rewrite /lsty_dual iProto_dual_message_tele.
iSplit; iIntros "!>".
......@@ -430,7 +430,7 @@ Section subtype.
* destruct HSs as [S HSs]=> /=.
rewrite !lookup_total_alt HSs /=.
rewrite lookup_fmap in HSs.
apply fmap_Some_1 in HSs as [S' [-> ->]].
apply fmap_Some_1 in HSs as [S' [Heq ->]]. rewrite Heq.
iApply iProto_le_refl.
+ rewrite /lsty_select /lsty_choice.
iApply iProto_le_send.
......
From stdpp Require Import pretty.
From actris.utils Require Import switch.
From actris.logrel Require Export ltyping session_types.
From actris.logrel Require Export model ltyping session_types.
From actris.channel Require Import proto proofmode.
From iris.bi.lib Require Export core.
From iris.heap_lang Require Export lifting metatheory.
......@@ -30,14 +30,10 @@ Section types.
Proof. solve_contractive. Qed.
Definition lty_rec (C : lty Σ lty Σ) `{!Contractive C} : lty Σ :=
fixpoint (lty_rec_aux C).
Definition lty_forall (C : lty Σ lty Σ) : lty Σ := Lty (λ w,
A : lty Σ, WP w #() {{ C A }})%I.
Definition lty_forall_lsty (C : lsty Σ lty Σ) : lty Σ := Lty (λ w,
A : lsty Σ, WP w #() {{ C A }})%I.
Definition lty_exist (C : lty Σ lty Σ) : lty Σ := Lty (λ w,
A : lty Σ, C A w)%I.
Definition lty_exist_lsty (C : lsty Σ lty Σ) : lty Σ := Lty (λ w,
A : lsty Σ, C A w)%I.
Definition lty_forall {k} (C : kind_interp k Σ lty Σ) : lty Σ := Lty (λ w,
A : kind_interp k Σ, WP w #() {{ C A }})%I.
Definition lty_exist {k} (C : kind_interp k Σ lty Σ) : lty Σ := Lty (λ w,
A : kind_interp k Σ, C A w)%I.
Definition lty_ref_mut (A : lty Σ) : lty Σ := Lty (λ w,
(l : loc) (v : val), w = #l l v A v)%I.
Definition ref_shrN := nroot .@ "shr_ref".
......@@ -55,32 +51,24 @@ Section types.
Definition lty_chan `{chanG Σ} (P : lsty Σ) : lty Σ := Lty (λ w, w P)%I.
End types.
Notation "()" := lty_unit : lty_scope.
Notation "'copy' A" := (lty_copy A) (at level 10) : lty_scope.
Notation "'copy-' A" := (lty_copyminus A) (at level 10) : lty_scope.
Notation "A → B" := (lty_copy (lty_arr A B)) : lty_scope.
Notation "A ⊸ B" := (lty_arr A B) (at level 99, B at level 200, right associativity) : lty_scope.
Infix "*" := lty_prod : lty_scope.
Infix "+" := lty_sum : lty_scope.
Notation "()" := lty_unit : kind_scope.
Notation "'copy' A" := (lty_copy A) (at level 10) : kind_scope.
Notation "'copy-' A" := (lty_copyminus A) (at level 10) : kind_scope.
Notation "A → B" := (lty_copy (lty_arr A B)) : kind_scope.
Notation "A ⊸ B" := (lty_arr A B) (at level 99, B at level 200, right associativity) : kind_scope.
Infix "*" := lty_prod : kind_scope.
Infix "+" := lty_sum : kind_scope.
Notation any := lty_any.
Notation "∀ A1 .. An , C" :=
(lty_forall (λ A1, .. (lty_forall (λ An, C%lty)) ..)) : lty_scope.
(lty_forall (λ A1, .. (lty_forall (λ An, C%kind)) ..)) : kind_scope.
Notation "∃ A1 .. An , C" :=
(lty_exist (λ A1, .. (lty_exist (λ An, C%lty)) ..)) : lty_scope.
Notation "∀p A1 .. An , C" :=
(lty_forall_lsty (λ A1, .. (lty_forall_lsty (λ An, C%lty)) ..))
(at level 200, A1 binder, An binder, right associativity,
format "'[ ' '[ ' ∀p A1 .. An ']' , '/' C ']'") : lty_scope.
Notation "∃p A1 .. An , C" :=
(lty_exist_lsty (λ A1, .. (lty_exist_lsty (λ An, C%lty)) ..))
(at level 200, A1 binder, An binder, right associativity,
format "'[ ' '[ ' ∃p A1 .. An ']' , '/' C ']'") : type_scope.
Notation "'ref_mut' A" := (lty_ref_mut A) (at level 10) : lty_scope.
Notation "'ref_shr' A" := (lty_ref_shr A) (at level 10) : lty_scope.
Notation "'mutex' A" := (lty_mutex A) (at level 10) : lty_scope.
Notation "'mutexguard' A" := (lty_mutexguard A) (at level 10) : lty_scope.
Notation "'chan' A" := (lty_chan A) (at level 10) : lty_scope.
(lty_exist (λ A1, .. (lty_exist (λ An, C%kind)) ..)) : kind_scope.
Notation "'ref_mut' A" := (lty_ref_mut A) (at level 10) : kind_scope.
Notation "'ref_shr' A" := (lty_ref_shr A) (at level 10) : kind_scope.
Notation "'mutex' A" := (lty_mutex A) (at level 10) : kind_scope.
Notation "'mutexguard' A" := (lty_mutexguard A) (at level 10) : kind_scope.
Notation "'chan' A" := (lty_chan A) (at level 10) : kind_scope.
Section properties.
Context `{heapG Σ}.
......@@ -321,29 +309,18 @@ Section properties.
Qed.
(** Universal Properties *)
Global Instance lty_forall_ne n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall Σ _).
Proof. solve_proper. Qed.
Global Instance lty_forall_contractive n :
Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_forall Σ _).
Proof.
intros F F' A. apply lty_ne=> w. f_equiv=> B.
apply (wp_contractive _ _ _ _ _)=> u. specialize (A B).
by destruct n as [|n]; simpl.
Qed.
Global Instance lty_forall_lsty_ne n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall_lsty Σ _).
Global Instance lty_forall_ne k n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall Σ _ k).
Proof. solve_proper. Qed.
Global Instance lty_forall_lsty_contractive n :
Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_forall_lsty Σ _).
Global Instance lty_forall_contractive k n :
Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_forall Σ _ k).
Proof.
intros F F' A. apply lty_ne=> w. f_equiv=> B.
apply (wp_contractive _ _ _ _ _)=> u. specialize (A B).
by destruct n as [|n]; simpl.
Qed.
Lemma ltyped_tlam Γ e C :
Lemma ltyped_tlam Γ e k (C : kind_interp k Σ lty Σ) :
( A, Γ e : C A ) - Γ (λ: <>, e) : A, C A .
Proof.
iIntros "#He" (vs) "!> HΓ /=". wp_pures.
......@@ -351,60 +328,33 @@ Section properties.
iIntros (A) "/=". wp_pures.
iApply (wp_wand with "(He HΓ)"). iIntros (v) "[$ _]".
Qed.
Lemma ltyped_tlam_lsty Γ e C :
( A, Γ e : C A ) - Γ (λ: <>, e) : p A, C A .
Proof.
iIntros "#He" (vs) "!> HΓ /=". wp_pures.
iSplitL; last by iApply env_ltyped_empty.
iIntros (A) "/=". wp_pures.
iApply (wp_wand with "(He HΓ)"). iIntros (v) "[$ _]".
Qed.
Lemma ltyped_tapp Γ Γ2 e C A :
Lemma ltyped_tapp Γ Γ2 e k (C : kind_interp k Σ lty Σ) A :
(Γ e : A, C A Γ2) - Γ e #() : C A Γ2.
Proof.
iIntros "#He" (vs) "!> HΓ /=".
wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB HΓ]".
by iApply (wp_wand with "HB [HΓ]"); iIntros (v) "$ //".
Qed.
Lemma ltyped_tapp_lsty Γ Γ2 e C A :
(Γ e : p A, C A Γ2) - Γ e #() : C A Γ2.
iIntros "#He" (vs) "!> HΓ /=".
wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB HΓ]".
by iApply (wp_wand with "HB [HΓ]"); iIntros (v) "$ //".
Qed.
(** Existential properties *)
Global Instance lty_exist_ne n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist Σ).
Global Instance lty_exist_ne k n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist Σ k).
Proof. solve_proper. Qed.
Global Instance lty_exist_contractive n :
Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_exist Σ).
Global Instance lty_exist_contractive k n :
Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_exist Σ k).
Proof. solve_contractive. Qed.
Global Instance lty_exist_lsty_ne n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist_lsty Σ).
Proof. solve_proper. Qed.
Global Instance lty_exist_lsty_contractive n :
Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_exist_lsty Σ).
Proof. solve_contractive. Qed.
Lemma ltyped_pack Γ e C A :
Lemma ltyped_pack Γ e k (C : kind_interp k Σ lty Σ) A :
(Γ e : C A) - Γ e : A, C A.
Proof.
iIntros "#He" (vs) "!> HΓ /=".
wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists A.
Qed.
Lemma ltyped_pack_lsty Γ e C A :
(Γ e : C A) - Γ e : p A, C A.
Proof.
iIntros "#He" (vs) "!> HΓ /=".
wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists A.
Qed.
Definition unpack : val := λ: "exist" "f", "f" #() "exist".
Lemma ltyped_unpack C B :
Lemma ltyped_unpack k (C : kind_interp k Σ lty Σ) B :
unpack : ( A, C A) ( A, C A B) B.
Proof.
iIntros (vs) "!> HΓ /=". iApply wp_value.
......@@ -418,20 +368,6 @@ Section properties.
wp_apply (wp_wand with "(Hf [Hv //])").
iIntros (w) "HB". iApply "HB".
Qed.
Lemma ltyped_unpack_lsty C B :
unpack : (p A, C A) (p A, C A B) B.
Proof.
iIntros (vs) "!> HΓ /=". iApply wp_value.
iSplitL; last by iApply env_ltyped_empty.
iIntros "!>" (v). iDestruct 1 as (A) "Hv".
rewrite /unpack. wp_pures.
iIntros (fty) "Hfty". wp_pures.
iSpecialize ("Hfty" $! A).