Commit a3479c77 authored by Amin Timany's avatar Amin Timany

Make lambda in Fμ,ref,par recursive

We used to have:

(λ x, b) a ->β b[a/x]

But now we have:

(λ f x, b) a ->β b[a/x, (λ f x, b)/f]
parent c7a553d3
...@@ -186,23 +186,27 @@ Section typed_interp. ...@@ -186,23 +186,27 @@ Section typed_interp.
Lemma typed_binary_interp_Lam Δ Γ e e' τ1 τ2 {HΔ : ✓✓ Δ} Lemma typed_binary_interp_Lam Δ Γ e e' τ1 τ2 {HΔ : ✓✓ Δ}
(Htyped : typed (τ1 :: Γ) e τ2) (Htyped : typed (TArrow τ1 τ2 :: τ1 :: Γ) e τ2)
(Htyped' : typed (τ1 :: Γ) e' τ2) (Htyped' : typed (TArrow τ1 τ2 :: τ1 :: Γ) e' τ2)
(IHHtyped : Δ τ1 :: Γ e log e' τ2) (IHHtyped : Δ TArrow τ1 τ2 :: τ1 :: Γ e log e' τ2)
: :
Δ Γ Lam e log Lam e' TArrow τ1 τ2. Δ Γ Lam e log Lam e' TArrow τ1 τ2.
Proof. Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn. intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
value_case. iExists (LamV _). iFrame "Htr". value_case. iExists (LamV _). iFrame "Htr".
iApply löb. rewrite -always_later. iIntros "#Hlat".
iAlways. iIntros {j' K' v} "[#Hiv Hv]". iAlways. iIntros {j' K' v} "[#Hiv Hv]".
iApply wp_lam; auto 1 using to_of_val. iNext. iApply wp_lam; auto 1 using to_of_val. iNext.
iPvs (step_lam _ _ _ j' K' _ (# (v.2)) (v.2) _ _ with "* -") as "Hz". iPvs (step_lam _ _ _ j' K' _ (# (v.2)) (v.2) _ _ with "* -") as "Hz".
iFrame "Hspec Hv"; trivial. iFrame "Hspec Hv"; trivial.
asimpl. erewrite ?typed_subst_head_simpl; eauto; asimpl.
simpl; try rewrite map_length; eauto with f_equal. specialize (IHHtyped ((LamV e.[upn 2 (env_subst (map fst vs))],
specialize (IHHtyped (v::vs)); simpl in IHHtyped. LamV e'.[upn 2 (env_subst (map snd vs))])
:: v :: vs)). simpl in IHHtyped.
erewrite <- ?typed_subst_head_simpl_2 in IHHtyped; eauto; simpl;
try rewrite map_length; auto.
iApply IHHtyped; auto. iApply IHHtyped; auto.
iFrame "Hheap Hspec Hiv HΓ"; trivial. repeat iSplitR; trivial. repeat iSplit; trivial.
(* unshelving *) (* unshelving *)
Unshelve. all: eauto using to_of_val. Unshelve. all: eauto using to_of_val.
Qed. Qed.
......
...@@ -106,10 +106,13 @@ Section typed_interp. ...@@ -106,10 +106,13 @@ Section typed_interp.
erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto); iNext; erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto); iNext;
[iApply IHHtyped2 | iApply IHHtyped3]; cbn; auto with itauto. [iApply IHHtyped2 | iApply IHHtyped3]; cbn; auto with itauto.
- (* lam *) - (* lam *)
value_case; apply (always_intro _ _); iIntros {w} "#Hw". value_case. iApply löb. rewrite -always_later.
iIntros "#Hlat". iAlways. iIntros {w} "#Hw".
iApply wp_lam; auto 1 using to_of_val. iApply wp_lam; auto 1 using to_of_val.
asimpl; erewrite typed_subst_head_simpl; [|eauto|cbn]; eauto. asimpl. change (Lam _) with (# (LamV e.[upn 2 (env_subst vs)])).
iNext; iApply (IHHtyped Δ HΔ (w :: vs)); cbn; auto with itauto. erewrite typed_subst_head_simpl_2; [|eauto|cbn]; eauto.
iNext; iApply (IHHtyped Δ HΔ (_ :: w :: vs)); cbn; auto.
repeat iSplit; trivial.
- (* app *) - (* app *)
smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHHtyped1. smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHHtyped1.
smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2. smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2.
......
...@@ -10,7 +10,7 @@ Module lang. ...@@ -10,7 +10,7 @@ Module lang.
Inductive expr := Inductive expr :=
| Var (x : var) | Var (x : var)
| Lam (e : {bind 1 of expr}) | Lam (e : {bind 2 of expr})
| App (e1 e2 : expr) | App (e1 e2 : expr)
(* Unit *) (* Unit *)
| Unit | Unit
...@@ -155,7 +155,7 @@ Module lang. ...@@ -155,7 +155,7 @@ Module lang.
(* β *) (* β *)
| BetaS e1 e2 v2 σ : | BetaS e1 e2 v2 σ :
to_val e2 = Some v2 to_val e2 = Some v2
head_step (App (Lam e1) e2) σ e1.[e2/] σ None head_step (App (Lam e1) e2) σ e1.[(Lam e1), e2/] σ None
(* Products *) (* Products *)
| FstS e1 v1 e2 v2 σ : | FstS e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2 to_val e1 = Some v1 to_val e2 = Some v2
......
...@@ -365,10 +365,12 @@ Section lang_rules. ...@@ -365,10 +365,12 @@ Section lang_rules.
(** Helper Lemmas for weakestpre. *) (** Helper Lemmas for weakestpre. *)
Lemma wp_lam E e1 e2 v Φ : Lemma wp_lam E e1 e2 v Φ :
to_val e2 = Some v WP e1.[e2 /] @ E {{Φ}} WP (App (Lam e1) e2) @ E {{Φ}}. to_val e2 = Some v
WP e1.[(Lam e1), e2 /] @ E {{Φ}} WP (App (Lam e1) e2) @ E {{Φ}}.
Proof. Proof.
intros <-%of_to_val. intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step (App _ _) e1.[of_val v /] None) //=. rewrite -(wp_lift_pure_det_step
(App _ _) e1.[(Lam e1), of_val v /] None) //=.
- by rewrite right_id. - by rewrite right_id.
- intros. inv_step; auto. - intros. inv_step; auto.
Qed. Qed.
......
...@@ -781,7 +781,7 @@ Section lang_rules. ...@@ -781,7 +781,7 @@ Section lang_rules.
Lemma step_lam N E ρ j K e1 e2 v : Lemma step_lam N E ρ j K e1 e2 v :
to_val e2 = Some v nclose N E to_val e2 = Some v nclose N E
(Spec_ctx N ρ j (fill K (App (Lam e1) e2))%I) (Spec_ctx N ρ j (fill K (App (Lam e1) e2))%I)
|={E}=>(j (fill K ((e1.[e2/]))))%I. |={E}=>(j (fill K ((e1.[Lam e1,e2/]))))%I.
Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed. Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed.
Lemma step_Tlam N E ρ j K e : Lemma step_Tlam N E ρ j K e :
......
...@@ -82,7 +82,7 @@ Local Open Scope bin_logrel_scope. ...@@ -82,7 +82,7 @@ Local Open Scope bin_logrel_scope.
Inductive typed_context_item : Inductive typed_context_item :
context_item (list type) type (list type) type Prop := context_item (list type) type (list type) type Prop :=
| TP_CTX_Lam : Γ τ τ', | TP_CTX_Lam : Γ τ τ',
typed_context_item CTX_Lam (τ :: Γ) τ' Γ (TArrow τ τ') typed_context_item CTX_Lam (TArrow τ τ' :: τ :: Γ) τ' Γ (TArrow τ τ')
| TP_CTX_AppL (e2 : expr) : Γ τ τ', | TP_CTX_AppL (e2 : expr) : Γ τ τ',
typed Γ e2 τ typed Γ e2 τ
typed_context_item (CTX_AppL e2) Γ (TArrow τ τ') Γ τ' typed_context_item (CTX_AppL e2) Γ (TArrow τ τ') Γ τ'
......
...@@ -39,7 +39,7 @@ Inductive typed (Γ : list type) : expr → type → Prop := ...@@ -39,7 +39,7 @@ Inductive typed (Γ : list type) : expr → type → Prop :=
typed (τ1 :: Γ) e1 τ3 typed (τ2 :: Γ) e2 τ3 typed (τ1 :: Γ) e1 τ3 typed (τ2 :: Γ) e2 τ3
typed Γ (Case e0 e1 e2) τ3 typed Γ (Case e0 e1 e2) τ3
| Lam_typed e τ1 τ2 : | Lam_typed e τ1 τ2 :
typed (τ1 :: Γ) e τ2 typed Γ (Lam e) (TArrow τ1 τ2) typed (TArrow τ1 τ2 :: τ1 :: Γ) e τ2 typed Γ (Lam e) (TArrow τ1 τ2)
| App_typed e1 e2 τ1 τ2 : | App_typed e1 e2 τ1 τ2 :
typed Γ e1 (TArrow τ1 τ2) typed Γ e2 τ1 typed Γ (App e1 e2) τ2 typed Γ e1 (TArrow τ1 τ2) typed Γ e2 τ1 typed Γ (App e1 e2) τ2
| TLam_typed e τ : | TLam_typed e τ :
...@@ -93,6 +93,16 @@ Proof. ...@@ -93,6 +93,16 @@ Proof.
by rewrite Hv. by rewrite Hv.
Qed. Qed.
Lemma typed_subst_head_simpl_2 Δ τ e w w' ws :
typed Δ e τ -> List.length Δ = 2 + (List.length ws)
e.[# w .: # w' .: env_subst ws] = e.[env_subst (w :: w' :: ws)]
.
Proof.
intros H1 H2.
rewrite /env_subst. eapply typed_subst_invariant; eauto => /= -[|[|x]] H3 //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first omega; simpl.
by rewrite Hv.
Qed.
Local Opaque eq_nat_dec. Local Opaque eq_nat_dec.
......
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