D.Dot.lr.sem_unstamped_typing
From D Require Export iris_prelude swap_later_impl.
From D.pure_program_logic Require Import weakestpre adequacy.
From D Require Import iris_extra.det_reduction.
From D.Dot Require Import skeleton path_repl typing_aux_defs.
From D.Dot Require Import unary_lr.
From D.Dot Require Import later_sub_sem binding_lr path_repl_lr defs_lr dsub_lr prims_lr.
From D.Dot Require Import binding_lr_syn path_repl_lr_syn prims_lr_syn later_sub_syn.
From stdpp Require Import relations.
(* Fix what is in scope. *)
Import stdpp.relations stdpp.tactics D.prelude dlang_adequacy.
Implicit Types (Σ : gFunctors)
(v w : vl) (e : tm) (d : dm) (ds : dms) (p : path)
(ρ : env) (l : label).
Section unstamped_judgs.
Context `{!dlangG Σ}.
(* Semantic, Unstamped, Expression TyPing *)
Definition suetp e_u Γ T : iProp Σ :=
<PB> ∃ e_s, ⌜ same_skel_tm e_u e_s⌝ ∧ Γ s⊨ e_s : T.
Definition sudstp ds_u Γ T : iProp Σ :=
<PB> ∃ ds_s, ⌜ same_skel_dms ds_u ds_s⌝ ∧ Γ s⊨ds ds_s : T.
Definition sudtp l d_u Γ T : iProp Σ :=
<PB> ∃ d_s, ⌜ same_skel_dm d_u d_s⌝ ∧ Γ s⊨ { l := d_s } : T.
Definition iuetp Γ T e := suetp e V⟦Γ⟧* V⟦T⟧.
Definition iudstp Γ T ds := sudstp ds V⟦Γ⟧* C⟦T⟧.
Definition iudtp Γ T l d := sudtp l d V⟦Γ⟧* C⟦T⟧.
Arguments suetp : simpl never.
Arguments sudstp : simpl never.
Arguments sudtp : simpl never.
Arguments iuetp : simpl never.
Arguments iudstp : simpl never.
Arguments iudtp : simpl never.
End unstamped_judgs.
#[global] Instance : Params (@suetp) 3 := {}.
#[global] Instance : Params (@sudstp) 3 := {}.
#[global] Instance : Params (@sudtp) 4 := {}.
Ltac rw ::= rewrite /iuetp /ietp /iudstp /idstp /iudtp /idtp /iptp /istpd ?lr.
Section unstamped_judgs_proper.
Context `{!dlangG Σ}.
#[global] Instance suetp_proper e : Proper2 (suetp e).
Proof. rewrite /suetp ⇒ ??????. by repeat f_equiv. Qed.
#[global] Instance sudstp_proper ds : Proper2 (sudstp ds).
Proof. rewrite /sudstp ⇒ ??????; by repeat f_equiv. Qed.
#[global] Instance sudtp_proper l d : Proper2 (sudtp l d).
Proof. rewrite /sudtp ⇒ ??????. by repeat f_equiv. Qed.
End unstamped_judgs_proper.
Notation "Γ su⊨ e : T" := (suetp e Γ T) (at level 74, e, T at next level).
Notation "Γ su⊨ { l := d } : T" := (sudtp l d Γ T) (at level 64, d, l, T at next level).
Notation "Γ su⊨ds ds : T" := (sudstp ds Γ T) (at level 74, ds, T at next level).
Notation "Γ u⊨ { l := d } : T" := (iudtp Γ T l d) (at level 74, d, l, T at next level).
Notation "Γ u⊨ds ds : T" := (iudstp Γ T ds) (at level 74, ds, T at next level).
Notation "Γ u⊨ e : T" := (iuetp Γ T e) (at level 74, e, T at next level).
Theorem unstamped_s_safety_dot_sem
Σ `{HdlangG : !dlangG Σ} `{HswapProp : !SwapPropI Σ}
{e_u}
(τ : ∀ `{!dlangG Σ}, olty Σ)
(Hwp : ∀ `{!dlangG Σ} `(!SwapPropI Σ), ⊢ [] su⊨ e_u : τ) :
safe e_u.
Proof.
intros e_u' [n Hsteps]%rtc_nsteps_1.
apply (soundness (M := iResUR Σ) _ n).
apply (bupd_plain_soundness _).
iDestruct (Hwp HdlangG HswapProp) as "#>#(%e_s & %Hsim & -#Hwp)".
iSpecialize ("Hwp" $! ids with "[//]"); rewrite hsubst_id /=.
iMod (wptp_safe_n n with "Hwp") as "Hwp".
iIntros "!>!>"; iRevert "Hwp"; iIntros "!% %Hsafe".
eapply same_skel_safe_n_impl, Hsteps; naive_solver.
Qed.
From D.pure_program_logic Require Import weakestpre adequacy.
From D Require Import iris_extra.det_reduction.
From D.Dot Require Import skeleton path_repl typing_aux_defs.
From D.Dot Require Import unary_lr.
From D.Dot Require Import later_sub_sem binding_lr path_repl_lr defs_lr dsub_lr prims_lr.
From D.Dot Require Import binding_lr_syn path_repl_lr_syn prims_lr_syn later_sub_syn.
From stdpp Require Import relations.
(* Fix what is in scope. *)
Import stdpp.relations stdpp.tactics D.prelude dlang_adequacy.
Implicit Types (Σ : gFunctors)
(v w : vl) (e : tm) (d : dm) (ds : dms) (p : path)
(ρ : env) (l : label).
Section unstamped_judgs.
Context `{!dlangG Σ}.
(* Semantic, Unstamped, Expression TyPing *)
Definition suetp e_u Γ T : iProp Σ :=
<PB> ∃ e_s, ⌜ same_skel_tm e_u e_s⌝ ∧ Γ s⊨ e_s : T.
Definition sudstp ds_u Γ T : iProp Σ :=
<PB> ∃ ds_s, ⌜ same_skel_dms ds_u ds_s⌝ ∧ Γ s⊨ds ds_s : T.
Definition sudtp l d_u Γ T : iProp Σ :=
<PB> ∃ d_s, ⌜ same_skel_dm d_u d_s⌝ ∧ Γ s⊨ { l := d_s } : T.
Definition iuetp Γ T e := suetp e V⟦Γ⟧* V⟦T⟧.
Definition iudstp Γ T ds := sudstp ds V⟦Γ⟧* C⟦T⟧.
Definition iudtp Γ T l d := sudtp l d V⟦Γ⟧* C⟦T⟧.
Arguments suetp : simpl never.
Arguments sudstp : simpl never.
Arguments sudtp : simpl never.
Arguments iuetp : simpl never.
Arguments iudstp : simpl never.
Arguments iudtp : simpl never.
End unstamped_judgs.
#[global] Instance : Params (@suetp) 3 := {}.
#[global] Instance : Params (@sudstp) 3 := {}.
#[global] Instance : Params (@sudtp) 4 := {}.
Ltac rw ::= rewrite /iuetp /ietp /iudstp /idstp /iudtp /idtp /iptp /istpd ?lr.
Section unstamped_judgs_proper.
Context `{!dlangG Σ}.
#[global] Instance suetp_proper e : Proper2 (suetp e).
Proof. rewrite /suetp ⇒ ??????. by repeat f_equiv. Qed.
#[global] Instance sudstp_proper ds : Proper2 (sudstp ds).
Proof. rewrite /sudstp ⇒ ??????; by repeat f_equiv. Qed.
#[global] Instance sudtp_proper l d : Proper2 (sudtp l d).
Proof. rewrite /sudtp ⇒ ??????. by repeat f_equiv. Qed.
End unstamped_judgs_proper.
Notation "Γ su⊨ e : T" := (suetp e Γ T) (at level 74, e, T at next level).
Notation "Γ su⊨ { l := d } : T" := (sudtp l d Γ T) (at level 64, d, l, T at next level).
Notation "Γ su⊨ds ds : T" := (sudstp ds Γ T) (at level 74, ds, T at next level).
Notation "Γ u⊨ { l := d } : T" := (iudtp Γ T l d) (at level 74, d, l, T at next level).
Notation "Γ u⊨ds ds : T" := (iudstp Γ T ds) (at level 74, ds, T at next level).
Notation "Γ u⊨ e : T" := (iuetp Γ T e) (at level 74, e, T at next level).
Theorem unstamped_s_safety_dot_sem
Σ `{HdlangG : !dlangG Σ} `{HswapProp : !SwapPropI Σ}
{e_u}
(τ : ∀ `{!dlangG Σ}, olty Σ)
(Hwp : ∀ `{!dlangG Σ} `(!SwapPropI Σ), ⊢ [] su⊨ e_u : τ) :
safe e_u.
Proof.
intros e_u' [n Hsteps]%rtc_nsteps_1.
apply (soundness (M := iResUR Σ) _ n).
apply (bupd_plain_soundness _).
iDestruct (Hwp HdlangG HswapProp) as "#>#(%e_s & %Hsim & -#Hwp)".
iSpecialize ("Hwp" $! ids with "[//]"); rewrite hsubst_id /=.
iMod (wptp_safe_n n with "Hwp") as "Hwp".
iIntros "!>!>"; iRevert "Hwp"; iIntros "!% %Hsafe".
eapply same_skel_safe_n_impl, Hsteps; naive_solver.
Qed.
Corollary unstamped_safety_dot_sem Σ `{HdlangG : !dlangG Σ} `{!SwapPropI Σ}
{e T}
(Hlog : ∀ `(!dlangG Σ) `(!SwapPropI Σ), ⊢ [] u⊨ e : T) :
safe e.
Proof. exact: (unstamped_s_safety_dot_sem Σ (λ _, V⟦T⟧)). Qed.
Lemma same_skel_dms_hasnt ds ds' l : dms_hasnt ds l → same_skel_dms ds ds' → dms_hasnt ds' l.
Proof.
rewrite /dms_hasnt; elim: ds ds' ⇒ [| [s d] ds IH] [|[s' d'] ds'] //= ? [<-{s'} ?].
case_match; naive_solver.
Qed.
#[local] Hint Resolve same_skel_dms_hasnt : core.
Definition coveringσ `{!dlangG Σ} σ (T : olty Σ) : Prop :=
∀ args ρ, T args ρ ≡ T args (∞ σ.|[ρ]).
Section coveringσ_intro_lemmas.
Context `{!dlangG Σ}.
Lemma nclosed_syn_coveringσ {n} {T : ty} (Hcl : nclosed T n) :
coveringσ (idsσ n) V⟦T⟧.
Proof.
move⇒ args ρ v /=.
by rewrite -interp_commute_finsubst_cl ?length_idsσ // closed_subst_idsρ.
Qed.
(* Maybe hard to use in general; nclosed requires equality on the nose? *)
Lemma nclosed_sem_coveringσ {n} {T : olty Σ} (Hcl : nclosed T n) :
coveringσ (idsσ n) T.
Proof.
move⇒ args ρ v.
by rewrite -olty_finsubst_commute_cl ?length_idsσ // closed_subst_idsρ.
Qed.
Lemma coveringσ_shift σ (T : olty Σ) :
coveringσ σ T → coveringσ (push_var σ) (shift T).
Proof.
move ⇒ + args ρ ⇒ /(_ args (stail ρ)) HclT.
rewrite /= !olty_weaken_one vls_subst_fold hsubst_comp stail_eq.
apply HclT.
Qed.
End coveringσ_intro_lemmas.
Section tmem_unstamped_lemmas.
Context `{!dlangG Σ}.
Lemma leadsto_envD_equiv_alloc {σ} {T : olty Σ}
(Hcl : coveringσ σ T) : ⊢ |==> ∃ s, s ↝[ σ ] T.
Proof.
iMod (saved_ho_sem_type_alloc T) as (s) "#Hs"; iIntros "!>".
iExists s, T; iFrame "Hs"; iIntros "!%". apply Hcl.
Qed.
Lemma leadsto_envD_equiv_alloc_shift {σ} {T : olty Σ} :
coveringσ σ T →
⊢ |==> ∃ s, s ↝[ push_var σ ] shift T.
Proof. intros Hcl; apply leadsto_envD_equiv_alloc, coveringσ_shift, Hcl. Qed.
Lemma suD_Typ_Gen {l Γ fakeT s σ} {T : olty Σ} :
s ↝[ σ ] T -∗ Γ su⊨ { l := dtysyn fakeT } : cTMem l (oLater T) (oLater T).
Proof.
pupd; iIntros "#Hs !>". iExists (dtysem σ s).
iSplit; first done; iApply (sD_Typ with "Hs").
Qed.
Lemma suD_Typ {l σ Γ fakeT} {T : olty Σ} (HclT : coveringσ σ T) :
⊢ Γ su⊨ { l := dtysyn fakeT } : cTMem l (oLater T) (oLater T).
Proof.
iModIntro.
iMod (leadsto_envD_equiv_alloc HclT) as (s) "#Hs".
iApply (suD_Typ_Gen with "Hs").
Qed.
{e T}
(Hlog : ∀ `(!dlangG Σ) `(!SwapPropI Σ), ⊢ [] u⊨ e : T) :
safe e.
Proof. exact: (unstamped_s_safety_dot_sem Σ (λ _, V⟦T⟧)). Qed.
Lemma same_skel_dms_hasnt ds ds' l : dms_hasnt ds l → same_skel_dms ds ds' → dms_hasnt ds' l.
Proof.
rewrite /dms_hasnt; elim: ds ds' ⇒ [| [s d] ds IH] [|[s' d'] ds'] //= ? [<-{s'} ?].
case_match; naive_solver.
Qed.
#[local] Hint Resolve same_skel_dms_hasnt : core.
Definition coveringσ `{!dlangG Σ} σ (T : olty Σ) : Prop :=
∀ args ρ, T args ρ ≡ T args (∞ σ.|[ρ]).
Section coveringσ_intro_lemmas.
Context `{!dlangG Σ}.
Lemma nclosed_syn_coveringσ {n} {T : ty} (Hcl : nclosed T n) :
coveringσ (idsσ n) V⟦T⟧.
Proof.
move⇒ args ρ v /=.
by rewrite -interp_commute_finsubst_cl ?length_idsσ // closed_subst_idsρ.
Qed.
(* Maybe hard to use in general; nclosed requires equality on the nose? *)
Lemma nclosed_sem_coveringσ {n} {T : olty Σ} (Hcl : nclosed T n) :
coveringσ (idsσ n) T.
Proof.
move⇒ args ρ v.
by rewrite -olty_finsubst_commute_cl ?length_idsσ // closed_subst_idsρ.
Qed.
Lemma coveringσ_shift σ (T : olty Σ) :
coveringσ σ T → coveringσ (push_var σ) (shift T).
Proof.
move ⇒ + args ρ ⇒ /(_ args (stail ρ)) HclT.
rewrite /= !olty_weaken_one vls_subst_fold hsubst_comp stail_eq.
apply HclT.
Qed.
End coveringσ_intro_lemmas.
Section tmem_unstamped_lemmas.
Context `{!dlangG Σ}.
Lemma leadsto_envD_equiv_alloc {σ} {T : olty Σ}
(Hcl : coveringσ σ T) : ⊢ |==> ∃ s, s ↝[ σ ] T.
Proof.
iMod (saved_ho_sem_type_alloc T) as (s) "#Hs"; iIntros "!>".
iExists s, T; iFrame "Hs"; iIntros "!%". apply Hcl.
Qed.
Lemma leadsto_envD_equiv_alloc_shift {σ} {T : olty Σ} :
coveringσ σ T →
⊢ |==> ∃ s, s ↝[ push_var σ ] shift T.
Proof. intros Hcl; apply leadsto_envD_equiv_alloc, coveringσ_shift, Hcl. Qed.
Lemma suD_Typ_Gen {l Γ fakeT s σ} {T : olty Σ} :
s ↝[ σ ] T -∗ Γ su⊨ { l := dtysyn fakeT } : cTMem l (oLater T) (oLater T).
Proof.
pupd; iIntros "#Hs !>". iExists (dtysem σ s).
iSplit; first done; iApply (sD_Typ with "Hs").
Qed.
Lemma suD_Typ {l σ Γ fakeT} {T : olty Σ} (HclT : coveringσ σ T) :
⊢ Γ su⊨ { l := dtysyn fakeT } : cTMem l (oLater T) (oLater T).
Proof.
iModIntro.
iMod (leadsto_envD_equiv_alloc HclT) as (s) "#Hs".
iApply (suD_Typ_Gen with "Hs").
Qed.
Unstamped typing only asserts that the subject bisimulates a
semantically typed stamped value, so type definitions in the subject are
ignored.
Lemma sudtp_respects_skel_sym {Γ l d1 d2 T}
(Hsk : same_skel_dm d1 d2) :
Γ su⊨ { l := d1 } : T -∗
Γ su⊨ { l := d2 } : T.
Proof.
pupd; iIntros "#(%d1s & %Hsk1 & H1) !>".
iExists d1s; iSplit; last done; iIntros "!%".
apply /same_skel_trans_dm /Hsk1 /same_skel_symm_dm /Hsk.
Qed.
Lemma suD_Typ_Stp {Γ} L1 L2 U1 U2 d l :
Γ s⊨ L2 <:[0] L1 -∗
Γ s⊨ U1 <:[0] U2 -∗
Γ su⊨ { l := d } : cTMem l L1 U1 -∗
Γ su⊨ { l := d } : cTMem l L2 U2.
Proof.
pupd; iIntros "#Hsub1 #Hsub2 #(%d1s & %Hsk1 & H1) !>".
by iExists d1s; iSplit; last iApply (sD_Typ_Stp with "Hsub1 Hsub2 H1").
Qed.
Lemma suD_Typ_Abs {l σ Γ L T U} fakeT (HclT : coveringσ σ T) :
Γ s⊨ L <:[0] oLater T -∗
Γ s⊨ oLater T <:[0] U -∗
Γ su⊨ { l := dtysyn fakeT } : cTMem l L U.
Proof.
by iIntros "H1 H2"; iApply (suD_Typ_Stp with "H1 H2"); iApply suD_Typ.
Qed.
Lemma uD_Typ_Abs {l n Γ L T U} fakeT (HclT : nclosed T n) :
Γ ⊨ L <:[0] TLater T -∗
Γ ⊨ TLater T <:[0] U -∗
Γ u⊨ { l := dtysyn fakeT } : TTMem l L U.
Proof. have := !!nclosed_syn_coveringσ HclT. rw. apply suD_Typ_Abs. Qed.
Lemma uD_Typ {l n Γ T} fakeT (HclT : nclosed T n) :
⊢ Γ u⊨ { l := dtysyn fakeT } : TTMem l (TLater T) (TLater T).
Proof. have := !!nclosed_syn_coveringσ HclT. rw. apply suD_Typ. Qed.
End tmem_unstamped_lemmas.
Section unstamped_lemmas.
Context `{!dlangG Σ}.
Lemma suT_All_E {Γ e1 e2 T1 T2} :
Γ su⊨ e1 : oAll T1 (shift T2) -∗
Γ su⊨ e2 : T1 -∗
(*────────────────────────────────────────────────────────────*)
Γ su⊨ tapp e1 e2 : T2.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) #(%e2s & %Hsk2 & H2) !>".
by iExists (tapp e1s e2s); iSplit; last iApply (sT_All_E with "H1 H2").
Qed.
Lemma uT_All_E {Γ e1 e2 T1 T2} :
Γ u⊨ e1 : TAll T1 (shift T2) -∗ Γ u⊨ e2 : T1 -∗ Γ u⊨ tapp e1 e2 : T2.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) #(%e2s & %Hsk2 & H2) !>".
by iExists (tapp e1s e2s); iSplit; last iApply (T_All_E with "H1 H2").
Qed.
Lemma suT_All_E_p {Γ e1 p2 T1 T2} :
Γ su⊨ e1 : oAll T1 T2 -∗
Γ s⊨p p2 : T1, 0 -∗
(*────────────────────────────────────────────────────────────*)
Γ su⊨ tapp e1 (path2tm p2) : T2 .sTp[ p2 /].
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) #H2 !>".
by iExists (tapp e1s (path2tm p2)); iSplit; last iApply (sT_All_E_p with "H1 H2").
Qed.
Lemma uT_All_E_p Γ e1 p2 T1 T2 T2' (Hrepl : T2 .Tp[ p2 /]~ T2') :
Γ u⊨ e1 : TAll T1 T2 -∗
Γ ⊨p p2 : T1, 0 -∗
(*────────────────────────────────────────────────────────────*)
Γ u⊨ tapp e1 (path2tm p2) : T2'.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) #H2 !>".
by iExists (tapp e1s (path2tm p2)); iSplit; last iApply (T_All_E_p with "H1 H2").
Qed.
Lemma suT_All_Ex {Γ e1 v2 T1 T2} :
Γ su⊨ e1 : oAll T1 T2 -∗
Γ s⊨p pv v2 : T1, 0 -∗
(*────────────────────────────────────────────────────────────*)
Γ su⊨ tapp e1 (tv v2) : T2.|[ v2 /].
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) #H2 !>".
iExists (tapp e1s (tv v2)); iSplit; last iApply (sT_All_Ex with "H1").
done.
by iApply (sT_Path (p := pv v2)).
Qed.
Lemma suT_Obj_E {Γ e T l} :
Γ su⊨ e : oVMem l T -∗
Γ su⊨ tproj e l : T.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) !>".
by iExists (tproj e1s l); iSplit; last iApply (sT_Obj_E with "H1").
Qed.
Lemma uT_Obj_E {Γ e T l} :
Γ u⊨ e : TVMem l T -∗
Γ u⊨ tproj e l : T.
Proof. rw. apply suT_Obj_E. Qed.
Lemma suT_All_I_Strong {Γ Γ'} T1 T2 e
(Hctx : s⊨G Γ <:* oLater <$> Γ') :
shift T1 :: Γ' su⊨ e : T2 -∗
(*─────────────────────────*)
Γ su⊨ tv (vabs e) : oAll T1 T2.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) !>".
by iExists (tv (vabs e1s)); iSplit; last iApply (sT_All_I_Strong with "H1").
Qed.
Lemma uT_All_I_Strong {Γ Γ'} T1 T2 e
(Hctx : ⊨G Γ <:* TLater <$> Γ') :
shift T1 :: Γ' u⊨ e : T2 -∗
Γ u⊨ tv (vabs e) : TAll T1 T2.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) !>".
by iExists (tv (vabs e1s)); iSplit; last iApply (T_All_I_Strong with "H1").
Qed.
Lemma suT_All_I {Γ} T1 T2 e :
shift T1 :: Γ su⊨ e : T2 -∗
(*─────────────────────────*)
Γ su⊨ tv (vabs e) : oAll T1 T2.
Proof.
apply suT_All_I_Strong ⇒ ρ. rewrite senv_TLater_commute. by iIntros "$".
Qed.
Lemma suT_Skip Γ e T :
Γ su⊨ e : oLater T -∗
Γ su⊨ tskip e : T.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) !>".
by iExists (tskip e1s); iSplit; last iApply (sT_Skip with "H1").
Qed.
Lemma uT_Skip Γ e T :
Γ u⊨ e : TLater T -∗
Γ u⊨ tskip e : T.
Proof. rw. apply suT_Skip. Qed.
Lemma suT_Sub {Γ e T1 T2} :
Γ su⊨ e : T1 -∗
Γ s⊨ T1 <:[0] T2 -∗
Γ su⊨ e : T2.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) #H2 !>".
by iExists e1s; iSplit; last iApply (sT_Sub with "H1 H2").
Qed.
Lemma uT_Sub {Γ e T1 T2} :
Γ u⊨ e : T1 -∗
Γ ⊨ T1 <:[0] T2 -∗
Γ u⊨ e : T2.
Proof. apply suT_Sub. Qed.
Lemma suT_Obj_I (Γ : sCtx Σ) (T : clty Σ) ds :
oLater T :: Γ su⊨ds ds : T -∗
Γ su⊨ tv (vobj ds) : oMu T.
Proof.
pupd; iIntros "#(%ds1s & %Hsk1 & H1) !>".
by iExists (tv (vobj ds1s)); iSplit; last iApply (sT_Obj_I with "H1").
Qed.
Lemma uT_Obj_I Γ T ds :
TLater T :: Γ u⊨ds ds : T -∗
Γ u⊨ tv (vobj ds) : TMu T.
Proof. rw. apply suT_Obj_I. Qed.
Lemma suT_Path Γ τ p :
Γ s⊨p p : τ, 0 -∗ Γ su⊨ path2tm p : τ.
Proof.
pupd; iIntros "#H1 !>".
by iExists (path2tm p); iSplit; last iApply (sT_Path with "H1").
Qed.
(* Primitives *)
Lemma suT_Un Γ u e1 B1 Br (Hu : un_op_semtype u B1 Br) :
Γ su⊨ e1 : oPrim B1 -∗
Γ su⊨ tun u e1 : oPrim Br.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) !>".
by iExists (tun u e1s); iSplit; last iApply (sT_Un with "H1").
Qed.
Lemma uT_Un Γ u e1 B1 Br (Hu : un_op_syntype u B1 Br) :
Γ u⊨ e1 : TPrim B1 -∗
Γ u⊨ tun u e1 : TPrim Br.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) !>".
by iExists (tun u e1s); iSplit; last iApply (T_Un with "H1").
Qed.
Lemma suT_Bin Γ b e1 e2 B1 B2 Br (Hu : bin_op_semtype b B1 B2 Br (const (const True))) :
Γ su⊨ e1 : oPrim B1 -∗
Γ su⊨ e2 : oPrim B2 -∗
Γ su⊨ tbin b e1 e2 : oPrim Br.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) #(%e2s & %Hsk2 & H2) !>".
by iExists (tbin b e1s e2s); iSplit; last iApply (sT_Bin with "H1 H2").
Qed.
Lemma uT_Bin Γ b e1 e2 B1 B2 Br (Hu : bin_op_syntype b B1 B2 Br) :
Γ u⊨ e1 : TPrim B1 -∗
Γ u⊨ e2 : TPrim B2 -∗
Γ u⊨ tbin b e1 e2 : TPrim Br.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) #(%e2s & %Hsk2 & H2) !>".
by iExists (tbin b e1s e2s); iSplit; last iApply (T_Bin with "H1 H2").
Qed.
Lemma suT_If Γ e1 e2 e3 T :
Γ su⊨ e1 : oBool -∗ Γ su⊨ e2 : T -∗ Γ su⊨ e3 : T -∗
Γ su⊨ tif e1 e2 e3 : T.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) #(%e2s & %Hsk2 & H2) #(%e3s & %Hsk3 & H3) !>".
by iExists (tif e1s e2s e3s); iSplit; last iApply (sT_If with "H1 H2 H3").
Qed.
Lemma uT_If Γ e1 e2 e3 T :
Γ u⊨ e1 : TBool -∗ Γ u⊨ e2 : T -∗ Γ u⊨ e3 : T -∗
Γ u⊨ tif e1 e2 e3 : T.
Proof. rw. apply suT_If. Qed.
Lemma suD_Nil Γ : ⊢ Γ su⊨ds [] : cTop.
Proof. iExists []. by rewrite -sD_Nil. Qed.
Lemma uD_Nil Γ : ⊢ Γ u⊨ds [] : TTop.
Proof. rw. apply suD_Nil. Qed.
Lemma suD_Cons Γ d1 ds2 l (T1 T2 : cltyO Σ)
(Hlds : dms_hasnt ds2 l) :
Γ su⊨ { l := d1 } : T1 -∗ Γ su⊨ds ds2 : T2 -∗
Γ su⊨ds (l, d1) :: ds2 : cAnd T1 T2.
Proof.
pupd; iIntros "#(%d1s & %Hsk1 & H1) #(%ds2s & %Hsk2 & H2) !>".
iExists ((l, d1s) :: ds2s); iSplit; last iApply (sD_Cons with "H1 H2");
naive_solver.
Qed.
Lemma uD_Cons Γ d1 ds2 l T1 T2
(Hlds : dms_hasnt ds2 l) :
Γ u⊨ { l := d1 } : T1 -∗ Γ u⊨ds ds2 : T2 -∗
Γ u⊨ds (l, d1) :: ds2 : TAnd T1 T2.
Proof. rw. exact: suD_Cons. Qed.
Lemma suD_Sing Γ d l (T : cltyO Σ) :
Γ su⊨ { l := d } : T -∗ Γ su⊨ds [(l, d)] : cAnd T cTop.
Proof.
pupd; iIntros "#(%d1s & %Hsk1 & H1) !>".
by iExists [(l, d1s)]; iSplit; last iApply (sD_Sing with "H1").
Qed.
Lemma uD_Sing Γ d l T :
Γ u⊨ { l := d } : T -∗ Γ u⊨ds [(l, d)] : TAnd T TTop.
Proof. rw. apply suD_Sing. Qed.
Lemma suD_Val {Γ} T v1 l :
Γ su⊨ tv v1 : T -∗
Γ su⊨ { l := dpt (pv v1) } : cVMem l T.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) !>".
destruct (same_skel_tv_tv Hsk1) as [v1s ->].
by iExists (dpt (pv v1s)); iSplit; last iApply (sD_Val with "H1").
Qed.
Lemma uD_Val {Γ} T v1 l :
Γ u⊨ tv v1 : T -∗
Γ u⊨ { l := dpt (pv v1) } : TVMem l T.
Proof. rw. apply suD_Val. Qed.
Lemma suD_Path {Γ} T p l :
Γ s⊨p p : T, 0 -∗
Γ su⊨ { l := dpt p } : cVMem l T.
Proof.
pupd; iIntros "#H1 !>".
by iExists (dpt p); iSplit; last iApply (sD_Path with "H1").
Qed.
Lemma uD_Path {Γ} T p l :
Γ ⊨p p : T, 0 -∗
Γ u⊨ { l := dpt p } : TVMem l T.
Proof. rw. apply suD_Path. Qed.
Lemma suD_Val_New {Γ l ds} {T : clty Σ} :
oAnd (oLater T) (oSing (pself (pv (ids 1)) l)) :: Γ su⊨ds ds : T -∗
Γ su⊨ { l := dpt (pv (vobj ds)) } : cVMem l (oMu T).
Proof.
pupd; iIntros "#(%ds1s & %Hsk1 & H1) !>".
by iExists (dpt (pv (vobj ds1s))); iSplit; last iApply (sD_Val_New with "H1").
Qed.
Lemma uD_Val_New {Γ l ds} T :
TAnd (TLater T) (TSing (pself (pv (ids 1)) l)) :: Γ u⊨ds ds : T -∗
Γ u⊨ { l := dpt (pv (vobj ds)) } : TVMem l (TMu T).
Proof. rw. apply suD_Val_New. Qed.
Lemma suD_Path_Stp {Γ T1 T2 p1 l} :
Γ s⊨ T1 <:[0] T2 -∗
Γ su⊨ { l := dpt p1 } : cVMem l T1 -∗
Γ su⊨ { l := dpt p1 } : cVMem l T2.
Proof.
pupd; iIntros "#Hsub #(%d1s & %Hsk1 & H1) !>".
destruct (same_skel_dpt_dpt Hsk1) as [p1s ->].
by iExists (dpt p1s); iSplit; last iApply (sD_Path_Stp with "Hsub H1").
Qed.
Lemma uD_Path_Stp {Γ T1 T2 p1 l}:
Γ ⊨ T1 <:[0] T2 -∗
Γ u⊨ { l := dpt p1 } : TVMem l T1 -∗
Γ u⊨ { l := dpt p1 } : TVMem l T2.
Proof. rw. apply suD_Path_Stp. Qed.
End unstamped_lemmas.
(Hsk : same_skel_dm d1 d2) :
Γ su⊨ { l := d1 } : T -∗
Γ su⊨ { l := d2 } : T.
Proof.
pupd; iIntros "#(%d1s & %Hsk1 & H1) !>".
iExists d1s; iSplit; last done; iIntros "!%".
apply /same_skel_trans_dm /Hsk1 /same_skel_symm_dm /Hsk.
Qed.
Lemma suD_Typ_Stp {Γ} L1 L2 U1 U2 d l :
Γ s⊨ L2 <:[0] L1 -∗
Γ s⊨ U1 <:[0] U2 -∗
Γ su⊨ { l := d } : cTMem l L1 U1 -∗
Γ su⊨ { l := d } : cTMem l L2 U2.
Proof.
pupd; iIntros "#Hsub1 #Hsub2 #(%d1s & %Hsk1 & H1) !>".
by iExists d1s; iSplit; last iApply (sD_Typ_Stp with "Hsub1 Hsub2 H1").
Qed.
Lemma suD_Typ_Abs {l σ Γ L T U} fakeT (HclT : coveringσ σ T) :
Γ s⊨ L <:[0] oLater T -∗
Γ s⊨ oLater T <:[0] U -∗
Γ su⊨ { l := dtysyn fakeT } : cTMem l L U.
Proof.
by iIntros "H1 H2"; iApply (suD_Typ_Stp with "H1 H2"); iApply suD_Typ.
Qed.
Lemma uD_Typ_Abs {l n Γ L T U} fakeT (HclT : nclosed T n) :
Γ ⊨ L <:[0] TLater T -∗
Γ ⊨ TLater T <:[0] U -∗
Γ u⊨ { l := dtysyn fakeT } : TTMem l L U.
Proof. have := !!nclosed_syn_coveringσ HclT. rw. apply suD_Typ_Abs. Qed.
Lemma uD_Typ {l n Γ T} fakeT (HclT : nclosed T n) :
⊢ Γ u⊨ { l := dtysyn fakeT } : TTMem l (TLater T) (TLater T).
Proof. have := !!nclosed_syn_coveringσ HclT. rw. apply suD_Typ. Qed.
End tmem_unstamped_lemmas.
Section unstamped_lemmas.
Context `{!dlangG Σ}.
Lemma suT_All_E {Γ e1 e2 T1 T2} :
Γ su⊨ e1 : oAll T1 (shift T2) -∗
Γ su⊨ e2 : T1 -∗
(*────────────────────────────────────────────────────────────*)
Γ su⊨ tapp e1 e2 : T2.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) #(%e2s & %Hsk2 & H2) !>".
by iExists (tapp e1s e2s); iSplit; last iApply (sT_All_E with "H1 H2").
Qed.
Lemma uT_All_E {Γ e1 e2 T1 T2} :
Γ u⊨ e1 : TAll T1 (shift T2) -∗ Γ u⊨ e2 : T1 -∗ Γ u⊨ tapp e1 e2 : T2.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) #(%e2s & %Hsk2 & H2) !>".
by iExists (tapp e1s e2s); iSplit; last iApply (T_All_E with "H1 H2").
Qed.
Lemma suT_All_E_p {Γ e1 p2 T1 T2} :
Γ su⊨ e1 : oAll T1 T2 -∗
Γ s⊨p p2 : T1, 0 -∗
(*────────────────────────────────────────────────────────────*)
Γ su⊨ tapp e1 (path2tm p2) : T2 .sTp[ p2 /].
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) #H2 !>".
by iExists (tapp e1s (path2tm p2)); iSplit; last iApply (sT_All_E_p with "H1 H2").
Qed.
Lemma uT_All_E_p Γ e1 p2 T1 T2 T2' (Hrepl : T2 .Tp[ p2 /]~ T2') :
Γ u⊨ e1 : TAll T1 T2 -∗
Γ ⊨p p2 : T1, 0 -∗
(*────────────────────────────────────────────────────────────*)
Γ u⊨ tapp e1 (path2tm p2) : T2'.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) #H2 !>".
by iExists (tapp e1s (path2tm p2)); iSplit; last iApply (T_All_E_p with "H1 H2").
Qed.
Lemma suT_All_Ex {Γ e1 v2 T1 T2} :
Γ su⊨ e1 : oAll T1 T2 -∗
Γ s⊨p pv v2 : T1, 0 -∗
(*────────────────────────────────────────────────────────────*)
Γ su⊨ tapp e1 (tv v2) : T2.|[ v2 /].
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) #H2 !>".
iExists (tapp e1s (tv v2)); iSplit; last iApply (sT_All_Ex with "H1").
done.
by iApply (sT_Path (p := pv v2)).
Qed.
Lemma suT_Obj_E {Γ e T l} :
Γ su⊨ e : oVMem l T -∗
Γ su⊨ tproj e l : T.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) !>".
by iExists (tproj e1s l); iSplit; last iApply (sT_Obj_E with "H1").
Qed.
Lemma uT_Obj_E {Γ e T l} :
Γ u⊨ e : TVMem l T -∗
Γ u⊨ tproj e l : T.
Proof. rw. apply suT_Obj_E. Qed.
Lemma suT_All_I_Strong {Γ Γ'} T1 T2 e
(Hctx : s⊨G Γ <:* oLater <$> Γ') :
shift T1 :: Γ' su⊨ e : T2 -∗
(*─────────────────────────*)
Γ su⊨ tv (vabs e) : oAll T1 T2.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) !>".
by iExists (tv (vabs e1s)); iSplit; last iApply (sT_All_I_Strong with "H1").
Qed.
Lemma uT_All_I_Strong {Γ Γ'} T1 T2 e
(Hctx : ⊨G Γ <:* TLater <$> Γ') :
shift T1 :: Γ' u⊨ e : T2 -∗
Γ u⊨ tv (vabs e) : TAll T1 T2.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) !>".
by iExists (tv (vabs e1s)); iSplit; last iApply (T_All_I_Strong with "H1").
Qed.
Lemma suT_All_I {Γ} T1 T2 e :
shift T1 :: Γ su⊨ e : T2 -∗
(*─────────────────────────*)
Γ su⊨ tv (vabs e) : oAll T1 T2.
Proof.
apply suT_All_I_Strong ⇒ ρ. rewrite senv_TLater_commute. by iIntros "$".
Qed.
Lemma suT_Skip Γ e T :
Γ su⊨ e : oLater T -∗
Γ su⊨ tskip e : T.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) !>".
by iExists (tskip e1s); iSplit; last iApply (sT_Skip with "H1").
Qed.
Lemma uT_Skip Γ e T :
Γ u⊨ e : TLater T -∗
Γ u⊨ tskip e : T.
Proof. rw. apply suT_Skip. Qed.
Lemma suT_Sub {Γ e T1 T2} :
Γ su⊨ e : T1 -∗
Γ s⊨ T1 <:[0] T2 -∗
Γ su⊨ e : T2.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) #H2 !>".
by iExists e1s; iSplit; last iApply (sT_Sub with "H1 H2").
Qed.
Lemma uT_Sub {Γ e T1 T2} :
Γ u⊨ e : T1 -∗
Γ ⊨ T1 <:[0] T2 -∗
Γ u⊨ e : T2.
Proof. apply suT_Sub. Qed.
Lemma suT_Obj_I (Γ : sCtx Σ) (T : clty Σ) ds :
oLater T :: Γ su⊨ds ds : T -∗
Γ su⊨ tv (vobj ds) : oMu T.
Proof.
pupd; iIntros "#(%ds1s & %Hsk1 & H1) !>".
by iExists (tv (vobj ds1s)); iSplit; last iApply (sT_Obj_I with "H1").
Qed.
Lemma uT_Obj_I Γ T ds :
TLater T :: Γ u⊨ds ds : T -∗
Γ u⊨ tv (vobj ds) : TMu T.
Proof. rw. apply suT_Obj_I. Qed.
Lemma suT_Path Γ τ p :
Γ s⊨p p : τ, 0 -∗ Γ su⊨ path2tm p : τ.
Proof.
pupd; iIntros "#H1 !>".
by iExists (path2tm p); iSplit; last iApply (sT_Path with "H1").
Qed.
(* Primitives *)
Lemma suT_Un Γ u e1 B1 Br (Hu : un_op_semtype u B1 Br) :
Γ su⊨ e1 : oPrim B1 -∗
Γ su⊨ tun u e1 : oPrim Br.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) !>".
by iExists (tun u e1s); iSplit; last iApply (sT_Un with "H1").
Qed.
Lemma uT_Un Γ u e1 B1 Br (Hu : un_op_syntype u B1 Br) :
Γ u⊨ e1 : TPrim B1 -∗
Γ u⊨ tun u e1 : TPrim Br.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) !>".
by iExists (tun u e1s); iSplit; last iApply (T_Un with "H1").
Qed.
Lemma suT_Bin Γ b e1 e2 B1 B2 Br (Hu : bin_op_semtype b B1 B2 Br (const (const True))) :
Γ su⊨ e1 : oPrim B1 -∗
Γ su⊨ e2 : oPrim B2 -∗
Γ su⊨ tbin b e1 e2 : oPrim Br.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) #(%e2s & %Hsk2 & H2) !>".
by iExists (tbin b e1s e2s); iSplit; last iApply (sT_Bin with "H1 H2").
Qed.
Lemma uT_Bin Γ b e1 e2 B1 B2 Br (Hu : bin_op_syntype b B1 B2 Br) :
Γ u⊨ e1 : TPrim B1 -∗
Γ u⊨ e2 : TPrim B2 -∗
Γ u⊨ tbin b e1 e2 : TPrim Br.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) #(%e2s & %Hsk2 & H2) !>".
by iExists (tbin b e1s e2s); iSplit; last iApply (T_Bin with "H1 H2").
Qed.
Lemma suT_If Γ e1 e2 e3 T :
Γ su⊨ e1 : oBool -∗ Γ su⊨ e2 : T -∗ Γ su⊨ e3 : T -∗
Γ su⊨ tif e1 e2 e3 : T.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) #(%e2s & %Hsk2 & H2) #(%e3s & %Hsk3 & H3) !>".
by iExists (tif e1s e2s e3s); iSplit; last iApply (sT_If with "H1 H2 H3").
Qed.
Lemma uT_If Γ e1 e2 e3 T :
Γ u⊨ e1 : TBool -∗ Γ u⊨ e2 : T -∗ Γ u⊨ e3 : T -∗
Γ u⊨ tif e1 e2 e3 : T.
Proof. rw. apply suT_If. Qed.
Lemma suD_Nil Γ : ⊢ Γ su⊨ds [] : cTop.
Proof. iExists []. by rewrite -sD_Nil. Qed.
Lemma uD_Nil Γ : ⊢ Γ u⊨ds [] : TTop.
Proof. rw. apply suD_Nil. Qed.
Lemma suD_Cons Γ d1 ds2 l (T1 T2 : cltyO Σ)
(Hlds : dms_hasnt ds2 l) :
Γ su⊨ { l := d1 } : T1 -∗ Γ su⊨ds ds2 : T2 -∗
Γ su⊨ds (l, d1) :: ds2 : cAnd T1 T2.
Proof.
pupd; iIntros "#(%d1s & %Hsk1 & H1) #(%ds2s & %Hsk2 & H2) !>".
iExists ((l, d1s) :: ds2s); iSplit; last iApply (sD_Cons with "H1 H2");
naive_solver.
Qed.
Lemma uD_Cons Γ d1 ds2 l T1 T2
(Hlds : dms_hasnt ds2 l) :
Γ u⊨ { l := d1 } : T1 -∗ Γ u⊨ds ds2 : T2 -∗
Γ u⊨ds (l, d1) :: ds2 : TAnd T1 T2.
Proof. rw. exact: suD_Cons. Qed.
Lemma suD_Sing Γ d l (T : cltyO Σ) :
Γ su⊨ { l := d } : T -∗ Γ su⊨ds [(l, d)] : cAnd T cTop.
Proof.
pupd; iIntros "#(%d1s & %Hsk1 & H1) !>".
by iExists [(l, d1s)]; iSplit; last iApply (sD_Sing with "H1").
Qed.
Lemma uD_Sing Γ d l T :
Γ u⊨ { l := d } : T -∗ Γ u⊨ds [(l, d)] : TAnd T TTop.
Proof. rw. apply suD_Sing. Qed.
Lemma suD_Val {Γ} T v1 l :
Γ su⊨ tv v1 : T -∗
Γ su⊨ { l := dpt (pv v1) } : cVMem l T.
Proof.
pupd; iIntros "#(%e1s & %Hsk1 & H1) !>".
destruct (same_skel_tv_tv Hsk1) as [v1s ->].
by iExists (dpt (pv v1s)); iSplit; last iApply (sD_Val with "H1").
Qed.
Lemma uD_Val {Γ} T v1 l :
Γ u⊨ tv v1 : T -∗
Γ u⊨ { l := dpt (pv v1) } : TVMem l T.
Proof. rw. apply suD_Val. Qed.
Lemma suD_Path {Γ} T p l :
Γ s⊨p p : T, 0 -∗
Γ su⊨ { l := dpt p } : cVMem l T.
Proof.
pupd; iIntros "#H1 !>".
by iExists (dpt p); iSplit; last iApply (sD_Path with "H1").
Qed.
Lemma uD_Path {Γ} T p l :
Γ ⊨p p : T, 0 -∗
Γ u⊨ { l := dpt p } : TVMem l T.
Proof. rw. apply suD_Path. Qed.
Lemma suD_Val_New {Γ l ds} {T : clty Σ} :
oAnd (oLater T) (oSing (pself (pv (ids 1)) l)) :: Γ su⊨ds ds : T -∗
Γ su⊨ { l := dpt (pv (vobj ds)) } : cVMem l (oMu T).
Proof.
pupd; iIntros "#(%ds1s & %Hsk1 & H1) !>".
by iExists (dpt (pv (vobj ds1s))); iSplit; last iApply (sD_Val_New with "H1").
Qed.
Lemma uD_Val_New {Γ l ds} T :
TAnd (TLater T) (TSing (pself (pv (ids 1)) l)) :: Γ u⊨ds ds : T -∗
Γ u⊨ { l := dpt (pv (vobj ds)) } : TVMem l (TMu T).
Proof. rw. apply suD_Val_New. Qed.
Lemma suD_Path_Stp {Γ T1 T2 p1 l} :
Γ s⊨ T1 <:[0] T2 -∗
Γ su⊨ { l := dpt p1 } : cVMem l T1 -∗
Γ su⊨ { l := dpt p1 } : cVMem l T2.
Proof.
pupd; iIntros "#Hsub #(%d1s & %Hsk1 & H1) !>".
destruct (same_skel_dpt_dpt Hsk1) as [p1s ->].
by iExists (dpt p1s); iSplit; last iApply (sD_Path_Stp with "Hsub H1").
Qed.
Lemma uD_Path_Stp {Γ T1 T2 p1 l}:
Γ ⊨ T1 <:[0] T2 -∗
Γ u⊨ { l := dpt p1 } : TVMem l T1 -∗
Γ u⊨ { l := dpt p1 } : TVMem l T2.
Proof. rw. apply suD_Path_Stp. Qed.
End unstamped_lemmas.