From mininix Require Export dynlang.interp.
From stdpp Require Import options.
Module Import dynlang.
Export dynlang.
Lemma interp_S n : interp (S n) = interp1 (interp n).
Proof. done. Qed.
Fixpoint thunk_size (t : thunk) : nat :=
S (map_sum_with thunk_size (thunk_env t)).
Definition env_size (E : env) : nat :=
map_sum_with thunk_size E.
Lemma env_ind (P : env → Prop) :
(∀ E, map_Forall (λ i, P ∘ thunk_env) E → P E) →
∀ E : env, P E.
Proof.
intros Pbs E.
induction (Nat.lt_wf_0_projected env_size E) as [E _ IH].
apply Pbs, map_Forall_lookup=> y [E' e'] Hy.
apply (map_sum_with_lookup_le thunk_size) in Hy.
apply IH. by rewrite -Nat.le_succ_l.
Qed.
(** Correspondence to operational semantics *)
Definition subst_env' (thunk_to_expr : thunk → expr) (E : env) : expr → expr :=
subst (thunk_to_expr <$> E).
Fixpoint thunk_to_expr (t : thunk) : expr :=
subst_env' thunk_to_expr (thunk_env t) (thunk_expr t).
Notation subst_env := (subst_env' thunk_to_expr).
Lemma subst_env_eq e E :
subst_env E e =
match e with
| EString s => EString s
| EId ds e => EId ((thunk_to_expr <$> E) ∪ ds) (subst_env E e)
| EAbs ex e => EAbs (subst_env E ex) (subst_env E e)
| EApp e1 e2 => EApp (subst_env E e1) (subst_env E e2)
end.
Proof. by destruct e. Qed.
Lemma subst_env_alt E e : subst_env E e = subst (thunk_to_expr <$> E) e.
Proof. done. Qed.
(* Use the unfolding lemmas, don't rely on conversion *)
Opaque subst_env'.
Definition val_to_expr (v : val) : expr :=
match v with
| VString s => EString s
| VClo x E e => EAbs (EString x) (subst_env E e)
end.
Lemma val_final v : final (val_to_expr v).
Proof. by destruct v. Qed.
Lemma subst_empty e : subst ∅ e = e.
Proof. induction e; f_equal/=; auto. by rewrite left_id_L. Qed.
Lemma subst_env_empty e : subst_env ∅ e = e.
Proof. rewrite subst_env_alt. apply subst_empty. Qed.
Lemma interp_le {n1 n2 E e mv} :
interp n1 E e = Res mv → n1 ≤ n2 → interp n2 E e = Res mv.
Proof.
revert n2 E e mv.
induction n1 as [|n1 IH]; intros [|n2] E e mv He ?; [by (done || lia)..|].
rewrite interp_S in He; rewrite interp_S; destruct e;
repeat match goal with
| _ => case_match
| H : context [(_ <$> ?mx)] |- _ => destruct mx eqn:?; simplify_res
| H : ?r ≫= _ = _ |- _ => destruct r as [[]|] eqn:?; simplify_res
| H : _ <$> ?r = _ |- _ => destruct r as [[]|] eqn:?; simplify_res
| |- interp ?n ?E ?e ≫= _ = _ => erewrite (IH n E e) by (done || lia)
| _ => progress simplify_res
| _ => progress simplify_option_eq
end; eauto with lia.
Qed.
Lemma interp_agree {n1 n2 E e mv1 mv2} :
interp n1 E e = Res mv1 → interp n2 E e = Res mv2 → mv1 = mv2.
Proof.
intros He1 He2. apply (inj Res). destruct (total (≤) n1 n2).
- rewrite -He2. symmetry. eauto using interp_le.
- rewrite -He1. eauto using interp_le.
Qed.
Lemma subst_env_union E1 E2 e :
subst_env (E1 ∪ E2) e = subst_env E1 (subst_env E2 e).
Proof.
revert E1 E2. induction e; intros E1 E2; rewrite subst_env_eq /=.
- done.
- rewrite !(subst_env_eq (EId _ _)) IHe. f_equal.
by rewrite assoc_L map_fmap_union.
- rewrite !(subst_env_eq (EAbs _ _)) /=. f_equal; auto.
- rewrite !(subst_env_eq (EApp _ _)) /=. f_equal; auto.
Qed.
Lemma subst_env_insert E x e t :
subst_env (<[x:=t]> E) e = subst {[x:=thunk_to_expr t]} (subst_env E e).
Proof.
rewrite insert_union_singleton_l subst_env_union subst_env_alt.
by rewrite map_fmap_singleton.
Qed.
Lemma subst_env_insert_eq e1 e2 E1 E2 x E1' E2' e1' e2' :
subst_env E1 e1 = subst_env E2 e2 →
subst_env E1' e1' = subst_env E2' e2' →
subst_env (<[x:=Thunk E1' e1']> E1) e1 = subst_env (<[x:=Thunk E2' e2']> E2) e2.
Proof. intros He He'. by rewrite !subst_env_insert //= He' He. Qed.
Lemma interp_proper n E1 E2 e1 e2 mv :
subst_env E1 e1 = subst_env E2 e2 →
interp n E1 e1 = Res mv →
∃ mw m, interp m E2 e2 = Res mw ∧
val_to_expr <$> mv = val_to_expr <$> mw.
Proof.
revert n E1 E2 e1 e2 mv. induction n as [|n IHn]; [done|].
intros E1 E2 e1 e2 mv Hsubst Hinterp.
rewrite 2!subst_env_eq in Hsubst.
rewrite interp_S in Hinterp. destruct e1, e2; simplify_res; try done.
- eexists (Some (VString _)), 1. by rewrite interp_S.
- destruct (interp n _ e1) as [mv1|] eqn:Hinterp'; simplify_eq/=.
eapply IHn in Hinterp' as (mw1 & m1 & Hinterp1 & ?); last done.
destruct mv1 as [v1|], mw1 as [w1|]; simplify_res; last first.
{ exists None, (S m1). by rewrite interp_S /= Hinterp1. }
destruct (maybe VString v1) as [x|] eqn:Hv1;
simplify_res; last first.
{ exists None, (S m1). split; [|done]. rewrite interp_S /= Hinterp1 /=.
destruct v1, w1; repeat destruct select base_lit; by simplify_eq/=. }
destruct v1, w1; repeat destruct select base_lit; simplify_eq/=.
assert (∀ (ds : stringmap expr) (E : env) x,
thunk_to_expr <$> (E !! x) ∪ (Thunk ∅ <$> ds !! x)
= ((thunk_to_expr <$> E) ∪ ds) !! x) as HE.
{ intros ds' E x. rewrite lookup_union lookup_fmap.
repeat destruct (_ !! _); f_equal/=; by rewrite subst_env_empty. }
pose proof (f_equal (.!! s0) Hsubst) as Hs. rewrite -!HE {HE} in Hs.
destruct (E1 !! s0 ∪ _) as [[E1' e1']|],
(E2 !! s0 ∪ _) as [[E2' e2']|] eqn:HE2; simplify_res; last first.
{ exists None, (S m1). rewrite interp_S /= Hinterp1 /=. by rewrite HE2. }
eapply IHn in Hinterp as (mw & m2 & Hinterp2 & ?); [|by eauto..].
exists mw, (S (m1 `max` m2)). split; [|done]. rewrite interp_S /=.
rewrite (interp_le Hinterp1) /=; last lia. rewrite HE2 /=.
eauto using interp_le with lia.
- destruct (interp n _ _) as [mv1|] eqn:Hinterp'; simplify_eq/=.
eapply IHn in Hinterp' as (mw1 & m1 & Hinterp1 & ?); last done.
destruct mv1 as [v1|], mw1 as [w1|]; simplify_res; last first.
{ exists None, (S m1). by rewrite interp_S /= Hinterp1. }
destruct (maybe VString _) eqn:Hstring; simplify_res; last first.
{ exists None, (S m1). rewrite interp_S /= Hinterp1 /=.
by assert (maybe VString w1 = None) as -> by (by destruct v1, w1). }
destruct v1, w1; simplify_eq/=.
eexists (Some (VClo _ _ _)), (S m1).
rewrite interp_S /= Hinterp1 /=. split; [done|]. by do 2 f_equal/=.
- destruct (interp n _ _) as [mv'|] eqn:Hinterp'; simplify_res.
eapply IHn in Hinterp' as (mw' & m1 & Hinterp1 & ?); last done.
destruct mv' as [v'|], mw' as [w'|]; simplify_res; last first.
{ exists None, (S m1). by rewrite interp_S /= Hinterp1. }
destruct (maybe3 VClo _) eqn:Hclo; simplify_res; last first.
{ exists None, (S m1). rewrite interp_S /= Hinterp1 /=.
by assert (maybe3 VClo w' = None) as -> by (by destruct v', w'). }
destruct v', w'; simplify_eq/=.
eapply IHn with (E2 := <[x0:=Thunk E2 e2_2]> E0) in Hinterp
as (w & m2 & Hinterp2 & ?); last by apply subst_env_insert_eq.
exists w, (S (m1 `max` m2)). rewrite interp_S /=.
rewrite (interp_le Hinterp1) /=; last lia.
rewrite (interp_le Hinterp2) /=; last lia. done.
Qed.
Lemma subst_as_subst_env x e1 e2 :
subst {[x:=e2]} e1 = subst_env (<[x:=Thunk ∅ e2]> ∅) e1.
Proof. rewrite subst_env_insert //= !subst_env_empty //. Qed.
Lemma interp_subst n x e1 e2 mv :
interp n ∅ (subst {[x:=e2]} e1) = Res mv →
∃ mw m, interp m (<[x:=Thunk ∅ e2]> ∅) e1 = Res mw ∧
val_to_expr <$> mv = val_to_expr <$> mw.
Proof.
apply interp_proper.
by rewrite subst_env_empty subst_as_subst_env.
Qed.
Lemma interp_step e1 e2 n mv :
e1 --> e2 →
interp n ∅ e2 = Res mv →
∃ mw m, interp m ∅ e1 = Res mw ∧ val_to_expr <$> mv = val_to_expr <$> mw.
Proof.
intros Hstep. revert mv n.
induction Hstep; intros mv n Hinterp.
- apply interp_subst in Hinterp as (w & [|m] & Hinterp & Hv);
simplify_eq/=; [|done..].
exists w, (S (S (S m))). rewrite !interp_S /= -!interp_S.
eauto using interp_le with lia.
- exists mv, (S (S n)). rewrite !interp_S /= -interp_S.
rewrite lookup_empty left_id_L H /=. eauto using interp_le with lia.
- destruct n as [|n]; [done|rewrite interp_S /= in Hinterp].
destruct (interp n _ _) as [mv'|] eqn:Hinterp'; simplify_res.
apply IHHstep in Hinterp' as (mw' & m1 & Hinterp1 & ?); simplify_res.
destruct mv' as [v'|], mw' as [w'|]; simplify_res; last first.
{ exists None, (S m1). by rewrite interp_S /= Hinterp1. }
destruct (maybe VString _) eqn:Hstring; simplify_res; last first.
{ exists None, (S m1). rewrite interp_S /= Hinterp1 /=.
by assert (maybe VString w' = None) as -> by (by destruct v', w'). }
destruct v', w'; simplify_eq/=.
eexists (Some (VClo _ _ _)), (S m1). rewrite !interp_S /=.
rewrite (interp_le Hinterp1) /=; last lia. done.
- destruct n as [|n]; [done|rewrite interp_S /= in Hinterp].
destruct (interp n _ _) as [mv'|] eqn:Hinterp'; simplify_res.
apply IHHstep in Hinterp' as (mw' & m1 & Hinterp1 & ?); simplify_res.
destruct mv' as [v'|], mw' as [w'|]; simplify_res; last first.
{ exists None, (S m1). by rewrite interp_S /= Hinterp1. }
destruct (maybe3 VClo _) eqn:Hclo; simplify_res; last first.
{ exists None, (S m1). rewrite interp_S /= Hinterp1 /=.
by assert (maybe3 VClo w' = None) as -> by (by destruct v', w'). }
destruct v', w'; simplify_eq/=.
eapply interp_proper in Hinterp as (mw & m2 & Hinterp2 & Hv);
last apply subst_env_insert_eq; try done.
exists mw, (S (m1 `max` m2)). rewrite !interp_S /=.
rewrite (interp_le Hinterp1) /=; last lia.
by rewrite (interp_le Hinterp2) /=; last lia.
- destruct n as [|n]; [done|rewrite interp_S /= in Hinterp].
destruct (interp n _ e1') as [mv1|] eqn:Hinterp1; simplify_eq/=.
apply IHHstep in Hinterp1 as (mw1 & m & Hinterp1 & Hw1).
destruct mv1 as [v1|], mw1 as [w1|]; simplify_res; last first.
{ exists None, (S m). by rewrite interp_S /= Hinterp1. }
exists mv, (S (n `max` m)). split; [|done].
rewrite interp_S /= (interp_le Hinterp1) /=; last lia.
assert (maybe VString w1 = maybe VString v1) as ->.
{ destruct v1, w1; naive_solver. }
destruct (maybe VString v1); simplify_res; [|done].
destruct (_ ∪ _); simplify_res; eauto using interp_le with lia.
Qed.
Lemma final_interp e :
final e →
∃ w m, interp m ∅ e = mret w ∧ e = val_to_expr w.
Proof.
induction e as [| |[]|]; inv 1.
- eexists (VString _), 1. by rewrite interp_S /=.
- eexists (VClo _ _ _), 2. rewrite interp_S /=. split; [done|].
by rewrite subst_env_empty.
Qed.
Lemma red_final_interp e :
red step e ∨ final e ∨ ∃ m, interp m ∅ e = mfail.
Proof.
induction e.
- (* ENat *) right; left. constructor.
- (* EId *) destruct IHe as [[??]|[Hfinal|[m Hinterp]]].
+ left. by repeat econstructor.
+ apply final_interp in Hfinal as (w & m & Hinterp & ->).
destruct (maybe VString w) as [x|] eqn:Hw; last first.
{ do 2 right. eexists (S m). rewrite interp_S /= Hinterp /=.
by rewrite Hw. }
destruct w; simplify_eq/=.
destruct (ds !! x) as [e|] eqn:Hx; last first.
{ do 2 right. eexists (S m). rewrite interp_S /= Hinterp /=.
by rewrite Hx. }
left. by repeat econstructor.
+ do 2 right. exists (S m). rewrite interp_S /= Hinterp. done.
- (* EAbs *) destruct IHe1 as [[??]|[Hfinal|[m Hinterp]]].
+ left. by repeat econstructor.
+ apply final_interp in Hfinal as (w & m & Hinterp & ->).
destruct (maybe VString w) as [x|] eqn:Hw; last first.
{ do 2 right. eexists (S m). rewrite interp_S /= Hinterp /=.
by rewrite Hw. }
destruct w; naive_solver.
+ do 2 right. exists (S m). rewrite interp_S /= Hinterp. done.
- (* EApp *) destruct IHe1 as [[??]|[Hfinal|[m Hinterp]]].
+ left. by repeat econstructor.
+ apply final_interp in Hfinal as (w & m & Hinterp & ->).
destruct (maybe3 VClo w) eqn:Hw.
{ destruct w; simplify_eq/=. left. by repeat econstructor. }
do 2 right. exists (S m). by rewrite interp_S /= Hinterp /= Hw.
+ do 2 right. exists (S m). by rewrite interp_S /= Hinterp.
Qed.
Lemma interp_complete e1 e2 :
e1 -->* e2 →
nf step e2 →
∃ mw m, interp m ∅ e1 = Res mw ∧
if mw is Some w then e2 = val_to_expr w else ¬final e2.
Proof.
intros Hsteps Hnf. induction Hsteps as [e|e1 e2 e3 Hstep _ IH].
{ destruct (red_final_interp e) as [?|[Hfinal|[m Hinterp]]]; [done|..].
- apply final_interp in Hfinal as (w & m & ? & ?).
by exists (Some w), m.
- exists None, m. split; [done|]. intros Hfinal.
apply final_interp in Hfinal as (w & m' & ? & _).
by assert (mfail = mret w) by eauto using interp_agree. }
destruct IH as (mw & m & Hinterp & ?); try done.
eapply interp_step in Hinterp as (mw' & m' & ? & ?); last done.
destruct mw, mw'; naive_solver.
Qed.
Lemma interp_complete_ret e1 e2 :
e1 -->* e2 → final e2 →
∃ w m, interp m ∅ e1 = mret w ∧ e2 = val_to_expr w.
Proof.
intros Hsteps Hfinal. apply interp_complete in Hsteps
as ([w|] & m & ? & ?); naive_solver eauto using final_nf.
Qed.
Lemma interp_complete_fail e1 e2 :
e1 -->* e2 → nf step e2 → ¬final e2 →
∃ m, interp m ∅ e1 = mfail.
Proof.
intros Hsteps Hnf Hforce.
apply interp_complete in Hsteps as ([w|] & m & ? & ?); simplify_eq/=; try by eauto.
destruct Hforce. apply val_final.
Qed.
Lemma interp_sound_open E e n mv :
interp n E e = Res mv →
∃ e', subst_env E e -->* e' ∧
if mv is Some v then e' = val_to_expr v else stuck e'.
Proof.
revert E e mv.
induction n as [|n IH]; intros E e mv Hinterp; first done.
rewrite subst_env_eq. rewrite interp_S in Hinterp.
destruct e; simplify_res.
- (* EString *) by eexists.
- (* EId *)
destruct (interp _ _ _) as [mv1|] eqn:Hinterp1; simplify_res.
apply IH in Hinterp1 as (e1' & Hsteps1 & He1').
destruct mv1 as [v1|]; simplify_res; last first.
{ eexists; split; [by eapply SId_rtc|]. split; [|inv 1].
intros [??]. destruct He1' as [Hnf []].
inv_step; simpl; eauto. destruct Hnf; eauto. }
destruct (maybe VString _) as [x|] eqn:Hv1; simplify_res; last first.
{ eexists; split; [by eapply SId_rtc|]. split; [|inv 1].
intros [??]. destruct v1; inv_step. }
destruct v1; simplify_eq/=.
assert (thunk_to_expr <$> (E !! x) ∪ (Thunk ∅ <$> ds !! x)
= ((thunk_to_expr <$> E) ∪ ds) !! x).
{ rewrite lookup_union lookup_fmap.
repeat destruct (_ !! _); f_equal/=; by rewrite subst_env_empty. }
destruct (_ ∪ _) as [[E' e']|] eqn:Hx; simplify_res.
* apply IH in Hinterp as (e'' & Hsteps & He'').
exists e''; split; [|done]. etrans; [by eapply SId_rtc|].
eapply rtc_l; [|done]. by econstructor.
* eexists; split; [by eapply SId_rtc|]. split; [|inv 1].
intros [? Hstep]. inv_step; simplify_eq/=; congruence.
- (* EAbs *)
destruct (interp _ _ _) as [mv1|] eqn:Hinterp1; simplify_res.
apply IH in Hinterp1 as (e1' & Hsteps1 & He1').
destruct mv1 as [v1|]; simplify_res; last first.
{ eexists; split; [by eapply SAbsL_rtc|]. split.
+ intros [??]. destruct He1' as [Hnf []].
inv_step; simpl; eauto. destruct Hnf; eauto.
+ intros ?. destruct He1' as [_ []]. by destruct e1'. }
eexists; split; [by eapply SAbsL_rtc|].
destruct (maybe VString _) as [x|] eqn:Hv1; simplify_res; last first.
{ split; [|destruct v1; inv 1]. intros [??]. destruct v1; inv_step. }
by destruct v1; simplify_eq/=.
- (* EApp *) destruct (interp _ _ _) as [mv'|] eqn:Hinterp'; simplify_res.
apply IH in Hinterp' as (e' & Hsteps & He'); try done.
destruct mv' as [v'|]; simplify_res; last first.
{ eexists; repeat split; [by apply SAppL_rtc| |inv 1].
intros [e'' Hstep]. destruct He' as [Hnf Hfinal].
inv Hstep; [by destruct Hfinal; constructor|]. destruct Hnf. eauto. }
destruct (maybe3 VClo v') eqn:?; simplify_res; last first.
{ eexists; repeat split; [by apply SAppL_rtc| |inv 1].
intros [e'' Hstep]. inv Hstep; destruct v'; by repeat inv_step. }
destruct v'; simplify_res.
apply IH in Hinterp as (e'' & Hsteps' & He'').
eexists; split; [|done]. etrans; [by apply SAppL_rtc|].
eapply rtc_l; first by constructor.
rewrite subst_env_insert // in Hsteps'.
Qed.
Lemma interp_sound n e mv :
interp n ∅ e = Res mv →
∃ e', e -->* e' ∧ if mv is Some v then e' = val_to_expr v else stuck e'.
Proof.
intros Hsteps%interp_sound_open; try done.
by rewrite subst_env_empty in Hsteps.
Qed.
(** Final theorems *)
Theorem interp_sound_complete_ret e v :
(∃ w n, interp n ∅ e = mret w ∧ val_to_expr v = val_to_expr w)
↔ e -->* val_to_expr v.
Proof.
split.
- by intros (n & w & (e' & ? & ->)%interp_sound & ->).
- intros Hsteps. apply interp_complete_ret in Hsteps as ([] & ? & ? & ?);
eauto using val_final.
Qed.
Theorem interp_sound_complete_ret_string e s :
(∃ n, interp n ∅ e = mret (VString s)) ↔ e -->* EString s.
Proof.
split.
- by intros [n (e' & ? & ->)%interp_sound].
- intros Hsteps. apply interp_complete_ret in Hsteps as ([] & ? & ? & ?);
simplify_eq/=; eauto.
Qed.
Theorem interp_sound_complete_fail e :
(∃ n, interp n ∅ e = mfail) ↔ ∃ e', e -->* e' ∧ stuck e'.
Proof.
split.
- by intros [n ?%interp_sound].
- intros (e' & Hsteps & Hnf & Hforced). by eapply interp_complete_fail.
Qed.
Theorem interp_sound_complete_no_fuel e :
(∀ n, interp n ∅ e = NoFuel) ↔ all_loop step e.
Proof.
rewrite all_loop_alt. split.
- intros Hnofuel e' Hsteps.
destruct (red_final_interp e') as [|[|He']]; [done|..].
+ apply interp_complete_ret in Hsteps as (w & m & Hinterp & _); last done.
by rewrite Hnofuel in Hinterp.
+ apply interp_sound_complete_fail in He' as (e'' & ? & [Hnf _]).
destruct (interp_complete e e'') as (mv & n & Hinterp & _); [by etrans|done|].
by rewrite Hnofuel in Hinterp.
- intros Hred n. destruct (interp n ∅ e) as [mv|] eqn:Hinterp; [|done].
apply interp_sound in Hinterp as (e' & Hsteps%Hred & Hstuck).
destruct mv as [v|]; simplify_eq/=.
+ apply final_nf in Hsteps as []. apply val_final.
+ by destruct Hstuck as [[] ?].
Qed.
End dynlang.
