Commit 75cfa329 authored by Amin Timany's avatar Amin Timany

Simplify env_subst

parent 76c60e8f
......@@ -23,7 +23,7 @@ Section fundamental.
induction 1; iIntros (Δ vs HΔ) "#HΓ"; cbn.
- (* var *)
iDestruct (interp_env_Some_l with "HΓ") as (v) "[% ?]"; first done.
rewrite /env_subst. simplify_option_eq. by iApply wp_value.
erewrite env_subst_lookup; eauto. by iApply wp_value.
- (* unit *) by iApply wp_value.
- (* pair *)
smart_wp_bind (PairLCtx e2.[env_subst vs]) v "# Hv" IHtyped1.
......@@ -48,16 +48,14 @@ Section fundamental.
iDestruct (interp_env_length with "HΓ") as %?.
iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as (w) "[% Hw]"; simplify_eq/=.
+ iApply wp_pure_step_later; auto; asimpl. iNext.
erewrite typed_subst_head_simpl by naive_solver.
iApply (IHtyped2 Δ (w :: vs)). iApply interp_env_cons; auto.
+ iApply wp_pure_step_later; auto 1 using to_of_val; asimpl. iNext.
erewrite typed_subst_head_simpl by naive_solver.
iApply (IHtyped3 Δ (w :: vs)). iApply interp_env_cons; auto.
- (* lam *)
iApply wp_value; simpl; iAlways; iIntros (w) "#Hw".
iDestruct (interp_env_length with "HΓ") as %?.
iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
asimpl. erewrite typed_subst_head_simpl by naive_solver.
asimpl.
iApply (IHtyped Δ (w :: vs)). iApply interp_env_cons; auto.
- (* app *)
smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHtyped1.
......
......@@ -10,7 +10,7 @@ Proof.
intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
eapply (wp_adequacy Σ); eauto.
iIntros (Hinv ?). iModIntro. iExists (λ _ _, True%I). iSplit=> //.
rewrite -(empty_env_subst e).
replace e with e.[env_subst[]] by by asimpl.
set (HΣ := IrisG _ _ Hinv (λ _ _ _, True)%I (λ _, True)%I).
iApply (wp_wand with "[]"). iApply Hlog; eauto. by iApply interp_env_nil. auto.
Qed.
......
......@@ -48,18 +48,18 @@ Proof.
induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with lia.
Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
from_option id (Var x) (of_val <$> vs !! x).
Fixpoint env_subst (vs : list val) : var expr :=
match vs with
| [] => ids
| v :: vs' => #v .: env_subst vs'
end.
Lemma typed_subst_head_simpl Δ τ e w ws :
Δ ⊢ₜ e : τ length Δ = S (length ws)
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)].
Lemma env_subst_lookup vs x v :
vs !! x = Some v env_subst vs x = of_val v.
Proof.
intros H1 H2. rewrite /env_subst.
eapply typed_subst_invariant; eauto=> /= -[|x] ? //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' ?]; first lia.
by simplify_option_eq.
Qed.
Lemma empty_env_subst e : e.[env_subst []] = e.
Proof. change (env_subst []) with (@ids expr _). by asimpl. Qed.
revert vs; induction x => vs.
- by destruct vs; inversion 1.
- destruct vs as [|w vs]; first by inversion 1.
rewrite -lookup_tail /=.
apply IHx.
Qed.
\ No newline at end of file
......@@ -22,7 +22,7 @@ Section fundamental.
induction 1; iIntros (Δ vs HΔ) "#HΓ /=".
- (* var *)
iDestruct (interp_env_Some_l with "HΓ") as (v) "[% ?]"; first done.
rewrite /env_subst. simplify_option_eq. by iApply wp_value.
erewrite env_subst_lookup; eauto. by iApply wp_value.
- (* unit *) by iApply wp_value.
- (* pair *)
smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHtyped1.
......@@ -47,16 +47,14 @@ Section fundamental.
iDestruct (interp_env_length with "HΓ") as %?.
iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as (w) "[% Hw]"; simplify_eq/=.
+ iApply wp_pure_step_later; auto 1 using to_of_val; asimpl. iNext.
erewrite typed_subst_head_simpl by naive_solver.
iApply (IHtyped2 Δ (w :: vs)). iApply interp_env_cons; auto.
+ iApply wp_pure_step_later; auto 1 using to_of_val; asimpl. iNext.
erewrite typed_subst_head_simpl by naive_solver.
iApply (IHtyped3 Δ (w :: vs)). iApply interp_env_cons; auto.
- (* lam *)
iApply wp_value. simpl. iAlways. iIntros (w) "#Hw".
iDestruct (interp_env_length with "HΓ") as %?.
iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
asimpl. erewrite typed_subst_head_simpl by naive_solver.
asimpl.
iApply (IHtyped Δ (w :: vs)). iApply interp_env_cons; auto.
- (* app *)
smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHtyped1.
......
......@@ -48,8 +48,9 @@ Section fundamental.
Γ !! x = Some τ Γ Var x log Var x : τ.
Proof.
iIntros (? Δ vvs ρ ?) "[#Hρ #HΓ]". iIntros (K) "Hj /=".
iDestruct (interp_env_Some_l with "HΓ") as ([v v']) "[% Hv]"; first done.
rewrite /env_subst !list_lookup_fmap; simplify_option_eq.
iDestruct (interp_env_Some_l with "HΓ") as ([v v']) "[Heq Hv]"; first done.
iDestruct "Heq" as %Heq.
erewrite !env_subst_lookup; rewrite ?list_lookup_fmap ?Heq; eauto.
iApply wp_value; auto.
Qed.
......@@ -137,15 +138,15 @@ Section fundamental.
iDestruct "Hiv" as "[Hiv|Hiv]".
- iDestruct "Hiv" as ([w w']) "[% Hw]"; simplify_eq.
iMod (step_case_inl _ _ K (of_val w') with "* [-]") as "Hz"; eauto.
simpl.
iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
asimpl. erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto).
iApply ('`IHHtyped2 _ ((w,w') :: vvs)); repeat iSplit; eauto.
asimpl. iApply ('`IHHtyped2 _ ((w,w') :: vvs)); repeat iSplit; eauto.
iApply interp_env_cons; auto.
- iDestruct "Hiv" as ([w w']) "[% Hw]"; simplify_eq.
iMod (step_case_inr _ _ K (of_val w') with "* [-]") as "Hz"; eauto.
simpl.
iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
asimpl. erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto).
iApply ('`IHHtyped3 _ ((w,w') :: vvs)); repeat iSplit; eauto.
asimpl. iApply ('`IHHtyped3 _ ((w,w') :: vvs)); repeat iSplit; eauto.
iApply interp_env_cons; auto.
Qed.
......@@ -161,8 +162,7 @@ Section fundamental.
iDestruct (interp_env_length with "HΓ") as %?.
iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
iMod (step_lam _ _ K' _ (of_val v') with "* [-]") as "Hz"; eauto.
asimpl. erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto).
iApply ('`IHHtyped _ ((v,v') :: vvs)); repeat iSplit; eauto.
asimpl. iApply ('`IHHtyped _ ((v,v') :: vvs)); repeat iSplit; eauto.
iApply interp_env_cons; iSplit; auto.
Qed.
......
......@@ -21,7 +21,7 @@ Proof.
iModIntro. iExists (λ σ _, own γ ( to_gen_heap σ)); iFrame.
set (HeapΣ := (HeapG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
iApply (wp_wand with "[]").
- rewrite -(empty_env_subst e).
- replace e with e.[env_subst[]] by by asimpl.
iApply (Hlog HeapΣ [] []). iApply (@interp_env_nil _ HeapΣ).
- auto.
Qed.
......@@ -32,8 +32,8 @@ Corollary type_soundness e τ e' thp σ σ' :
is_Some (to_val e') reducible e' σ'.
Proof.
intros ??. set (Σ := #[invΣ ; gen_heapΣ loc val]).
set (HG := HeapPreG Σ _ _).
set (HG := HeapPreG Σ _ _).
eapply (soundness Σ).
- intros ?. by apply fundamental.
- intros ?. by apply fundamental.
- eauto.
Qed.
......@@ -30,8 +30,9 @@ Proof.
iApply wp_fupd. iApply (wp_wand with "[-]").
- iPoseProof (Hlog _ _ with "[$Hcfg]") as "Hrel".
{ iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
rewrite (empty_env_subst e). iApply ("Hrel" $! []).
rewrite /tpool_mapsto (empty_env_subst e'). asimpl. iFrame.
replace e with e.[env_subst[]] at 2 by by asimpl.
iApply ("Hrel" $! []).
rewrite /tpool_mapsto. asimpl. iFrame.
- iModIntro. iIntros (v'). iDestruct 1 as (v2) "[Hj #Hinterp]".
iInv specN as ">Hinv" "Hclose".
iDestruct "Hinv" as (e'' σ) "[Hown %]".
......
......@@ -87,9 +87,21 @@ Proof.
asimpl; rewrite H1; auto with lia.
Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
from_option id (Var x) (of_val <$> vs !! x).
Fixpoint env_subst (vs : list val) : var expr :=
match vs with
| [] => ids
| v :: vs' => #v .: env_subst vs'
end.
Lemma env_subst_lookup vs x v :
vs !! x = Some v env_subst vs x = of_val v.
Proof.
revert vs; induction x => vs.
- by destruct vs; inversion 1.
- destruct vs as [|w vs]; first by inversion 1.
rewrite -lookup_tail /=.
apply IHx.
Qed.
Lemma typed_n_closed Γ τ e : Γ ⊢ₜ e : τ ( f, e.[upn (length Γ) f] = e).
Proof.
intros H. induction H => f; asimpl; simpl in *; auto with f_equal.
......@@ -97,40 +109,6 @@ Proof.
- by f_equal; rewrite map_length in IHtyped.
Qed.
Lemma n_closed_subst_head_simpl n e w ws :
( f, e.[upn n f] = e)
S (length ws) = n
e.[of_val w .: env_subst ws] = e.[env_subst (w :: ws)].
Proof.
intros H1 H2.
rewrite /env_subst. eapply n_closed_invariant; eauto=> /= -[|x] ? //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first lia; simpl.
by rewrite Hv.
Qed.
Lemma typed_subst_head_simpl Δ τ e w ws :
Δ ⊢ₜ e : τ length Δ = S (length ws)
e.[of_val w .: env_subst ws] = e.[env_subst (w :: ws)].
Proof. eauto using n_closed_subst_head_simpl, typed_n_closed. Qed.
Lemma n_closed_subst_head_simpl_2 n e w w' ws :
( f, e.[upn n f] = e) (S (S (length ws))) = n
e.[of_val w .: of_val w' .: env_subst ws] = e.[env_subst (w :: w' :: ws)].
Proof.
intros H1 H2.
rewrite /env_subst. eapply n_closed_invariant; eauto => /= -[|[|x]] H3 //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first lia; simpl.
by rewrite Hv.
Qed.
Lemma typed_subst_head_simpl_2 Δ τ e w w' ws :
Δ ⊢ₜ e : τ length Δ = 2 + length ws
e.[of_val w .: of_val w' .: env_subst ws] = e.[env_subst (w :: w' :: ws)].
Proof. eauto using n_closed_subst_head_simpl_2, typed_n_closed. Qed.
Lemma empty_env_subst e : e.[env_subst []] = e.
Proof. change (env_subst []) with (@ids expr _). by asimpl. Qed.
(** Weakening *)
Lemma context_gen_weakening ξ Γ' Γ e τ :
Γ' ++ Γ ⊢ₜ e : τ
......
......@@ -76,7 +76,6 @@ Section fact_equiv.
Proof.
iIntros (? vs ρ _) "[#HE HΔ]".
iDestruct (interp_env_length with "HΔ") as %?; destruct vs; simplify_eq.
rewrite !empty_env_subst.
iClear "HΔ". simpl.
iIntros (j K) "Hj"; simpl.
iApply wp_value; iExists (LamV _); iFrame.
......@@ -155,7 +154,6 @@ Section fact_equiv.
Proof.
iIntros (? vs ρ _) "[#HE HΔ]".
iDestruct (interp_env_length with "HΔ") as %?; destruct vs; simplify_eq.
rewrite !empty_env_subst.
iClear "HΔ". simpl.
iIntros (j K) "Hj"; simpl.
iApply wp_value; iExists (RecV _); iFrame.
......
......@@ -48,8 +48,10 @@ Section fundamental.
Γ !! x = Some τ Γ Var x log Var x : τ.
Proof.
iIntros (? Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
iDestruct (interp_env_Some_l with "HΓ") as ([v v']) "[% ?]"; first done.
rewrite /env_subst !list_lookup_fmap; simplify_option_eq. iApply wp_value; eauto.
iDestruct (interp_env_Some_l with "HΓ") as ([v v']) "[Heq ?]"; first done.
iDestruct "Heq" as %Heq.
erewrite !env_subst_lookup; rewrite ?list_lookup_fmap ?Heq; eauto.
iApply wp_value; eauto.
Qed.
Lemma bin_log_related_unit Γ : Γ Unit log Unit : TUnit.
......@@ -150,14 +152,12 @@ Section fundamental.
iMod (step_case_inl with "[Hs Hv]") as "Hz"; eauto.
iApply wp_pure_step_later; auto. fold of_val. iModIntro. iNext.
asimpl.
erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto).
iApply ('`IHHtyped2 _ ((w,w') :: vvs)). repeat iSplit; eauto.
iApply interp_env_cons; auto.
- iApply fupd_wp.
iMod (step_case_inr with "[Hs Hv]") as "Hz"; eauto.
iApply wp_pure_step_later; auto. fold of_val. iModIntro. iNext.
asimpl.
erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto).
iApply ('`IHHtyped3 _ ((w,w') :: vvs)); repeat iSplit; eauto.
iApply interp_env_cons; auto.
Qed.
......@@ -214,7 +214,6 @@ Section fundamental.
iApply fupd_wp.
iMod (step_rec _ _ j' K' _ (of_val v') v' with "* [-]") as "Hz"; eauto.
asimpl. change (Rec ?e) with (of_val (RecV e)).
erewrite !n_closed_subst_head_simpl_2 by (rewrite ?fmap_length; eauto).
iApply ('`IHHtyped _ ((_,_) :: (v,v') :: vvs)); repeat iSplit; eauto.
iModIntro.
rewrite !interp_env_cons; iSplit; try iApply interp_env_cons; auto.
......@@ -234,7 +233,6 @@ Section fundamental.
iApply fupd_wp.
iMod (step_lam _ _ j' K' _ (of_val v') v' with "* [-]") as "Hz"; eauto.
asimpl. iFrame "#". change (Lam ?e) with (of_val (LamV e)).
erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto).
iApply ('`IHHtyped _ ((v,v') :: vvs)); repeat iSplit; eauto.
iModIntro.
rewrite !interp_env_cons; iSplit; try iApply interp_env_cons; auto.
......@@ -254,7 +252,6 @@ Section fundamental.
iMod (step_letin _ _ j K with "[-]") as "Hz"; eauto.
iApply wp_pure_step_later; auto. iModIntro.
asimpl.
erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto).
iApply ('`IHHtyped2 _ ((v, v') :: vvs)); repeat iSplit; eauto.
rewrite !interp_env_cons; iSplit; try iApply interp_env_cons; auto.
Qed.
......
......@@ -23,7 +23,8 @@ Section typed_interp.
induction 1; iIntros (Δ vs HΔ) "#HΓ /=".
- (* var *)
iDestruct (interp_env_Some_l with "HΓ") as (v) "[% ?]"; first done.
rewrite /env_subst. simplify_option_eq. by iApply wp_value.
erewrite env_subst_lookup; eauto.
by iApply wp_value.
- (* unit *) iApply wp_value; trivial.
- (* nat *) iApply wp_value; simpl; eauto.
- (* bool *) iApply wp_value; simpl; eauto.
......@@ -57,10 +58,8 @@ Section typed_interp.
iDestruct (interp_env_length with "HΓ") as %?.
iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as (w) "[% Hw]"; simplify_eq/=.
+ iApply wp_pure_step_later; auto 1 using to_of_val; asimpl. iNext.
erewrite typed_subst_head_simpl by naive_solver.
iApply (IHtyped2 Δ (w :: vs)). iApply interp_env_cons; auto.
+ iApply wp_pure_step_later; auto 1 using to_of_val; asimpl. iNext.
erewrite typed_subst_head_simpl by naive_solver.
iApply (IHtyped3 Δ (w :: vs)). iApply interp_env_cons; auto.
- (* If *)
smart_wp_bind (IfCtx _ _) v "#Hv" IHtyped1; cbn.
......@@ -72,7 +71,6 @@ Section typed_interp.
iDestruct (interp_env_length with "HΓ") as %?.
iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
asimpl. change (Rec _) with (of_val (RecV e.[upn 2 (env_subst vs)])) at 2.
erewrite typed_subst_head_simpl_2 by naive_solver.
iApply (IHtyped Δ (_ :: w :: vs)).
iApply interp_env_cons; iSplit; [|iApply interp_env_cons]; auto.
- (* Lam *)
......@@ -80,15 +78,13 @@ Section typed_interp.
iDestruct (interp_env_length with "HΓ") as %?.
iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
asimpl.
erewrite typed_subst_head_simpl by naive_solver.
iApply (IHtyped Δ (w :: vs)); auto.
iApply interp_env_cons; iSplit; auto.
- (* LetIn *)
smart_wp_bind (LetInCtx _) v "#Hv" IHtyped1; cbn.
iDestruct (interp_env_length with "HΓ") as %?.
iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
asimpl. erewrite typed_subst_head_simpl by naive_solver.
iApply (IHtyped2 Δ (v :: vs)).
asimpl. iApply (IHtyped2 Δ (v :: vs)).
iApply interp_env_cons; iSplit; eauto.
- (* Seq *)
smart_wp_bind (SeqCtx _) v "#Hv" IHtyped1; cbn.
......
......@@ -29,8 +29,9 @@ Proof.
iPoseProof ((Hlog _ _ [] [] ([e'], )) with "[$Hcfg]") as "Hrel".
{ iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
simpl.
rewrite empty_env_subst empty_env_subst. iApply ("Hrel" $! 0 []).
{ rewrite /tpool_mapsto. iAsimpl. by iFrame. }
replace e with e.[env_subst[]] at 2 by by asimpl.
iApply ("Hrel" $! 0 []).
{ rewrite /tpool_mapsto. asimpl. by iFrame. }
iModIntro. iIntros (v1); iDestruct 1 as (v2) "[Hj #Hinterp]".
iInv specN as (tp σ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
rewrite /tpool_mapsto /=.
......
......@@ -20,7 +20,7 @@ Proof.
iModIntro. iExists (λ σ _, own γ ( to_gen_heap σ)); iFrame.
set (HeapΣ := (HeapIG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
iApply (wp_wand with "[]").
- rewrite -(empty_env_subst e).
- replace e with e.[env_subst[]] by by asimpl.
iApply (Hlog HeapΣ [] []). iApply (@interp_env_nil _ HeapΣ).
- eauto.
Qed.
......
......@@ -123,8 +123,21 @@ Proof.
asimpl; rewrite H1; auto with lia.
Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
from_option id (Var x) (of_val <$> vs !! x).
Fixpoint env_subst (vs : list val) : var expr :=
match vs with
| [] => ids
| v :: vs' => (of_val v) .: env_subst vs'
end.
Lemma env_subst_lookup vs x v :
vs !! x = Some v env_subst vs x = of_val v.
Proof.
revert vs; induction x => vs.
- by destruct vs; inversion 1.
- destruct vs as [|w vs]; first by inversion 1.
rewrite -lookup_tail /=.
apply IHx.
Qed.
Lemma typed_n_closed Γ τ e : Γ ⊢ₜ e : τ ( f, e.[upn (length Γ) f] = e).
Proof.
......@@ -134,40 +147,6 @@ Proof.
- by f_equal; rewrite map_length in IHtyped.
Qed.
Lemma n_closed_subst_head_simpl n e w ws :
( f, e.[upn n f] = e)
S (length ws) = n
e.[of_val w .: env_subst ws] = e.[env_subst (w :: ws)].
Proof.
intros H1 H2.
rewrite /env_subst. eapply n_closed_invariant; eauto=> /= -[|x] ? //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first lia; simpl.
by rewrite Hv.
Qed.
Lemma typed_subst_head_simpl Δ τ e w ws :
Δ ⊢ₜ e : τ length Δ = S (length ws)
e.[of_val w .: env_subst ws] = e.[env_subst (w :: ws)].
Proof. eauto using n_closed_subst_head_simpl, typed_n_closed. Qed.
Lemma n_closed_subst_head_simpl_2 n e w w' ws :
( f, e.[upn n f] = e) (S (S (length ws))) = n
e.[of_val w .: of_val w' .: env_subst ws] = e.[env_subst (w :: w' :: ws)].
Proof.
intros H1 H2.
rewrite /env_subst. eapply n_closed_invariant; eauto => /= -[|[|x]] H3 //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first lia; simpl.
by rewrite Hv.
Qed.
Lemma typed_subst_head_simpl_2 Δ τ e w w' ws :
Δ ⊢ₜ e : τ length Δ = 2 + length ws
e.[of_val w .: of_val w' .: env_subst ws] = e.[env_subst (w :: w' :: ws)].
Proof. eauto using n_closed_subst_head_simpl_2, typed_n_closed. Qed.
Lemma empty_env_subst e : e.[env_subst []] = e.
Proof. change (env_subst []) with (@ids expr _). by asimpl. Qed.
(** Weakening *)
Lemma context_gen_weakening ξ Γ' Γ e τ :
Γ' ++ Γ ⊢ₜ e : τ
......
......@@ -18,7 +18,7 @@ Section typed_interp.
induction Htyped; iIntros (vs) "#Hctx /=".
- (* var *)
iDestruct (interp_env_Some_l with "[]") as (v) "[#H1 #H2]"; eauto;
iDestruct "H1" as %Heq; rewrite /env_subst Heq /=.
iDestruct "H1" as %Heq. erewrite env_subst_lookup; eauto.
by iApply wp_value.
- (* unit *) by iApply wp_value.
- (* pair *)
......@@ -43,17 +43,15 @@ Section typed_interp.
iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as (w) "[% Hw]"; subst.
+ simpl. iApply wp_pure_step_later; auto. asimpl.
specialize (IHHtyped2 (w::vs)).
erewrite <- ?typed_subst_head_simpl in *; eauto; simpl in *; auto.
iNext. iApply (IHHtyped2). iApply interp_env_cons; by iSplit.
+ simpl. iApply wp_pure_step_later; auto. asimpl.
specialize (IHHtyped3 (w::vs)).
erewrite <- ?typed_subst_head_simpl in *; eauto; simpl in *; auto.
iNext. iApply (IHHtyped3). iApply interp_env_cons; by iSplit.
- (* lam *)
iDestruct (interp_env_length with "[]") as %Hlen; auto.
iApply wp_value. simpl. iAlways; iIntros (w) "#Hw".
iApply wp_pure_step_later; auto.
asimpl; erewrite typed_subst_head_simpl; [|eauto|cbn]; eauto.
asimpl.
iNext; iApply (IHHtyped (w :: vs)). iApply interp_env_cons; by iSplit.
- (* app *)
smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHHtyped1.
......
......@@ -4,7 +4,8 @@ From iris.program_logic Require Import adequacy.
Lemma wp_soundness `{irisG stlc_lang Σ} e τ : [] ⊢ₜ e : τ (WP e {{ τ }})%I.
Proof.
iIntros (?). rewrite -(empty_env_subst e).
iIntros (?).
replace e with e.[env_subst[]] by by asimpl.
iApply fundamental; eauto. iApply interp_env_nil.
Qed.
......
......@@ -34,18 +34,18 @@ Proof.
induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with lia.
Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
from_option id (Var x) (of_val <$> vs !! x).
Fixpoint env_subst (vs : list val) : var expr :=
match vs with
| [] => ids
| v :: vs' => #v .: env_subst vs'
end.
Lemma typed_subst_head_simpl Δ τ e w ws :
Δ ⊢ₜ e : τ length Δ = S (length ws)
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)].
Lemma env_subst_lookup vs x v :
vs !! x = Some v env_subst vs x = of_val v.
Proof.
intros H1 H2.
rewrite /env_subst. eapply typed_subst_invariant; eauto=> /= -[|x] ? //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first lia; simpl.
by rewrite Hv.
Qed.
Lemma empty_env_subst e : e.[env_subst []] = e.
Proof. change (env_subst []) with ids. by asimpl. Qed.
revert vs; induction x => vs.
- by destruct vs; inversion 1.
- destruct vs as [|w vs]; first by inversion 1.
rewrite -lookup_tail /=.
apply IHx.
Qed.
\ No newline at end of file
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