Commit e045456d authored by Amin Timany's avatar Amin Timany

Change the style of logical relation for μ types

parent 7947eab3
......@@ -107,24 +107,18 @@ Section typed_interp.
smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2.
iApply wp_mono; [|iApply "Hv"]; auto with itauto.
- (* TLam *)
value_case; iApply exist_intro; iSplit; trivial.
iIntros {τi}; destruct τi as [τi τiPr].
iPoseProof (always_intro with "HΓ") as "HP"; try typeclasses eauto;
try iExact "HP".
iIntros "#HΓ".
value_case.
iIntros {τi}; destruct τi as [τi τiPr]. iAlways.
iApply wp_TLam; iNext; simpl in *.
iApply IHHtyped; [rewrite map_length|]; trivial.
iRevert "HΓ".
rewrite zip_with_context_interp_subst.
iIntros "#HΓ"; trivial.
- (* TApp *)
smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
iDestruct "Hv" as {e'} "[% He']"; rewrite H.
iApply wp_TLam.
iSpecialize ("He'" $! ((interp τ' Δ) _)); cbn.
iSpecialize ("Hv" $! ((interp τ' Δ) _)); cbn.
iApply always_elim. iApply always_mono; [|trivial].
iIntros "He'"; iNext.
iApply wp_mono; [|trivial].
intros w; rewrite interp_subst; trivial.
apply wp_mono => w. by rewrite interp_subst.
- (* Fold *)
rewrite map_length in IHHtyped.
iApply (@wp_bind _ _ _ [FoldCtx]).
......
......@@ -156,19 +156,17 @@ Section logrel.
{|
cofe_mor_car :=
λ w,
( e, w = TLamV e
(τ'i : {f : (leibniz_val -n> iProp lang Σ) |
Val_to_IProp_Persistent f}),
(WP e @ {{λ v, (τi (`τ'i) v)}}))%I
( (τ'i : {f : (leibniz_val -n> iProp lang Σ) |
Val_to_IProp_Persistent f}),
(WP TApp (# w) @ {{λ v, (τi (`τ'i) v)}}))%I
|}
|}.
Next Obligation.
Proof.
intros τ τ' x y Hxy; cbn. apply exist_ne => e; apply and_ne; auto.
rewrite Hxy; trivial.
intros τ τ' x y Hxy; cbn; rewrite Hxy; trivial.
Qed.
Next Obligation.
intros n f g Hfg x; cbn. apply exist_ne => e; apply and_ne; auto.
intros n f g Hfg x; cbn.
apply forall_ne=> P.
apply always_ne, wp_ne => w.
rewrite Hfg; trivial.
......
......@@ -119,25 +119,22 @@ Section typed_interp.
smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2.
iApply wp_mono; [|iApply "Hv"]; auto with itauto.
- (* TLam *)
value_case; iApply exist_intro; iSplit; trivial.
value_case.
iIntros {τi}; destruct τi as [τi τiPr].
iRevert "Hheap".
iPoseProof (always_intro with "HΓ") as "HP"; try typeclasses eauto;
try (iApply always_impl; iExact "HP").
iIntros "#HΓ #Hheap".
iApply wp_TLam; iNext.
iApply IHHtyped; [rewrite map_length|]; trivial.
iSplit; trivial.
iRevert "Hheap HΓ". rewrite zip_with_context_interp_subst.
iIntros "#Hheap #HΓ"; trivial.
- (* TApp *)
smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
iDestruct "Hv" as {e'} "[% He']"; rewrite H.
iApply wp_TLam.
iSpecialize ("He'" $! ((interp τ' Δ) _)); cbn.
iSpecialize ("Hv" $! ((interp τ' Δ) _)); cbn.
iApply always_elim. iApply always_mono; [|trivial].
iIntros "He'"; iNext.
iApply wp_mono; [|trivial].
iIntros {w} "#H". rewrite -interp_subst; trivial.
apply wp_mono => w. by rewrite -interp_subst; simpl.
- (* Fold *)
rewrite map_length in IHHtyped.
iApply (@wp_bind _ _ _ [FoldCtx]).
......
......@@ -161,19 +161,17 @@ Section logrel.
{|
cofe_mor_car :=
λ w,
( e, w = TLamV e
(τ'i : {f : (leibniz_val -n> iPropG lang Σ) |
Val_to_IProp_Persistent f}),
(WP e @ {{λ v, (τi (`τ'i) v)}}))%I
( (τ'i : {f : (leibniz_val -n> iPropG lang Σ) |
Val_to_IProp_Persistent f}),
(WP TApp (# w) @ {{λ v, (τi (`τ'i) v)}}))%I
|}
|}.
Next Obligation.
Proof.
intros τ τ' x y Hxy; cbn. apply exist_ne => e; apply and_ne; auto.
rewrite Hxy; trivial.
intros τ τ' x y Hxy; cbn; rewrite Hxy; trivial.
Qed.
Next Obligation.
intros n f g Hfg x; cbn. apply exist_ne => e; apply and_ne; auto.
intros n f g Hfg x; cbn.
apply forall_ne=> P.
apply always_ne, wp_ne => w.
rewrite Hfg; trivial.
......
......@@ -36,9 +36,12 @@ Section Stack_refinement.
unfold CG_stack, FG_stack.
iApply wp_value; eauto.
iExists (TLamV _); iFrame "Hj".
iExists (_, _); iSplit; eauto.
iIntros {τi}. destruct τi as [τi Hτ]; simpl.
iAlways. clear j K. iIntros {j K} "Hj".
iPvs (step_Tlam _ _ _ j K with "[Hj]")
as "Hj"; eauto.
iFrame "Hspec Hj"; trivial.
iApply wp_TLam; iNext.
iPvs (steps_newlock _ _ _ j (K ++ [AppRCtx (LamV _)]) _ with "[Hj]")
as {l} "[Hj Hl]"; eauto.
rewrite fill_app; simpl.
......
......@@ -281,14 +281,18 @@ Section typed_interp.
Δ Γ TLam e log TLam e' TForall τ.
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
value_case. iExists (TLamV _). iFrame "Htr"; simpl.
iExists (e.[env_subst (map fst vs)], e'.[env_subst (map snd vs)]).
iSplit; trivial.
value_case.
iExists (TLamV _). iFrame "Htr".
iIntros {τi}; destruct τi as [τi τiPr].
iAlways. iIntros {j' K'} "Hv". simpl.
iApply wp_TLam; iNext.
iPvs (step_Tlam _ _ _ j' K' (e'.[env_subst (map snd vs)]) _ with "* -")
as "Hz".
iFrame "Hspec Hv"; trivial.
iApply IHHtyped; [rewrite map_length; trivial|].
iFrame "Hheap Hspec Hv".
rewrite zip_with_context_interp_subst; trivial.
iFrame "Hheap Hspec".
rewrite zip_with_context_interp_subst; by iFrame "HΓ".
Unshelve. all: trivial.
Qed.
Lemma typed_binary_interp_TApp Δ Γ e e' τ τ' {HΔ : ✓✓ Δ}
......@@ -297,17 +301,12 @@ Section typed_interp.
Δ Γ TApp e log TApp e' τ.[τ'/].
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
smart_wp_bind (TAppCtx) v v' "[Hv #Hiv]"
smart_wp_bind (TAppCtx) v v' "[Hj #Hv]"
(IHHtyped _ _ _ j (K ++ [TAppCtx])); cbn.
iDestruct "Hiv" as {e''} "[% He'']".
inversion H; subst.
iSpecialize ("He''" $! ((interp τ' Δ) _)); cbn.
iPvs (step_Tlam _ _ _ j K (e''.2) _ with "* -") as "Hz".
iFrame "Hspec Hv"; trivial.
iApply wp_TLam.
iRevert "He''"; iIntros "#He''". (*To get rid of . Is this the best way?!*)
iNext.
iApply wp_wand_l; iSplitR; [|iApply "He''"; auto].
iSpecialize ("Hv" $! ((interp τ' Δ) _)); cbn.
iRevert "Hv"; iIntros "#Hv". (*To get rid of . Is this the best way?!*)
iSpecialize ("Hv" $! j K); cbn.
iApply wp_wand_l; iSplitR; [|iApply "Hv"; auto].
iIntros {w} "Hw". iDestruct "Hw" as {w'} "[Hw #Hiw]".
iExists _; iFrame "Hw".
rewrite -interp_subst; trivial.
......
......@@ -132,25 +132,22 @@ Section typed_interp.
smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2.
iApply wp_mono; [|iApply "Hv"]; auto with itauto.
- (* TLam *)
value_case; iApply exist_intro; iSplit; trivial.
value_case.
iIntros {τi}; destruct τi as [τi τiPr].
iRevert "Hheap".
iPoseProof (always_intro with "HΓ") as "HP"; try typeclasses eauto;
try (iApply always_impl; iExact "HP").
iIntros "#HΓ #Hheap".
iApply wp_TLam; iNext.
iApply IHHtyped; [rewrite map_length|]; trivial.
iSplit; trivial.
iRevert "Hheap HΓ". rewrite zip_with_context_interp_subst.
iIntros "#Hheap #HΓ"; trivial.
- (* TApp *)
smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
iDestruct "Hv" as {e'} "[% He']"; rewrite H.
iApply wp_TLam.
iSpecialize ("He'" $! ((interp τ' Δ) _)); cbn.
iSpecialize ("Hv" $! ((interp τ' Δ) _)); cbn.
iApply always_elim. iApply always_mono; [|trivial].
iIntros "He'"; iNext.
iApply wp_mono; [|trivial].
iIntros {w} "#H". rewrite -interp_subst; trivial.
apply wp_mono => w. by rewrite -interp_subst; simpl.
- (* Fold *)
specialize (IHHtyped Δ HΔ vs Hlen).
setoid_rewrite <- interp_subst in IHHtyped.
......
......@@ -224,24 +224,22 @@ Section logrel.
{|
cofe_mor_car :=
λ w,
( e, w = (TLamV (e.1), TLamV (e.2))
(τ'i : {f : (bivalC -n> iPropG lang Σ) |
BiVal_to_IProp_Persistent f}),
( j K,
j (fill K (e.2))
WP e.1 @
{{v, v', j (fill K (# v'))
(τi (`τ'i) (v, v'))}}))%I
( (τ'i : {f : (bivalC -n> iPropG lang Σ) |
BiVal_to_IProp_Persistent f}),
( j K,
j (fill K (TApp (# w.2)))
WP TApp (# w.1) @
{{v, v', j (fill K (# v'))
(τi (`τ'i) (v, v'))}}))%I
|}
|}.
Next Obligation.
Proof.
intros τi n [x1 x2] [y1 y2 ] [H1 H2].
apply exist_ne => e; apply and_ne; simpl in *; auto.
intros τi n [x1 x2] [y1 y2 ] [H1 H2]. simpl in *; auto.
inversion H1; subst; inversion H2; subst; trivial.
Qed.
Next Obligation.
intros n f g Hfg x; cbn. apply exist_ne => e; apply and_ne; auto.
intros n f g Hfg x; cbn.
apply forall_ne=> P.
apply always_ne.
apply forall_ne => j; apply forall_ne => K.
......
......@@ -170,19 +170,17 @@ Section logrel.
{|
cofe_mor_car :=
λ w,
( e, w = TLamV e
(τ'i : {f : (valC -n> iPropG lang Σ) |
Val_to_IProp_Persistent f}),
(WP e @ {{λ v, (τi (`τ'i) v)}}))%I
( (τ'i : {f : (valC -n> iPropG lang Σ) |
Val_to_IProp_Persistent f}),
(WP TApp (# w) @ {{λ v, (τi (`τ'i) v)}}))%I
|}
|}.
Next Obligation.
Proof.
intros τ τ' x y Hxy; cbn. apply exist_ne => e; apply and_ne; auto.
rewrite Hxy; trivial.
intros τ τ' x y Hxy; cbn; rewrite Hxy; trivial.
Qed.
Next Obligation.
intros n f g Hfg x; cbn. apply exist_ne => e; apply and_ne; auto.
intros n f g Hfg x; cbn.
apply forall_ne=> P.
apply always_ne, wp_ne => w.
rewrite Hfg; trivial.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment