4 files changed, 725 insertions, 0 deletions

diff --git a/theories/lambda/interp.v b/theories/lambda/interp.v
new file mode 100644
index 0000000..5bc60d1
--- /dev/null
+++ b/theories/lambda/interp.v
@@ -0,0 +1,44 @@
+From mininix Require Export res lambda.operational_props.
+From stdpp Require Import options.
+
+Module Import lambda.
+Export lambda.
+
+Inductive thunk :=
+  Thunk { thunk_env : gmap string thunk; thunk_expr : expr }.
+Add Printing Constructor thunk.
+Notation env := (gmap string thunk).
+
+Inductive val :=
+  | VString (s : string)
+  | VClo (x : string) (E : env) (e : expr).
+
+Global Instance maybe_VClo : Maybe3 VClo := λ v,
+  if v is VClo x E e then Some (x, E, e) else None.
+
+Definition interp1 (interp : env → expr → res val) (E : env) (e : expr) : res val :=
+  match e with
+  | EString s =>
+      mret (VString s)
+  | EId x =>
+      t ← Res (E !! x);
+      interp (thunk_env t) (thunk_expr t)
+  | EAbs x e =>
+      mret (VClo x E e)
+  | EApp e1 e2 =>
+      v1 ← interp E e1;
+      '(x, E', e') ← Res (maybe3 VClo v1);
+      interp (<[x:=Thunk E e2]> E') e'
+  end.
+
+Fixpoint interp (n : nat) (E : env) (e : expr) : res val :=
+  match n with
+  | O => NoFuel
+  | S n => interp1 (interp n) E e
+  end.
+
+Global Opaque interp.
+
+End lambda.
+
+Add Printing Constructor lambda.thunk.
diff --git a/theories/lambda/interp_proofs.v b/theories/lambda/interp_proofs.v
new file mode 100644
index 0000000..efd0982
--- /dev/null
+++ b/theories/lambda/interp_proofs.v
@@ -0,0 +1,614 @@
+From mininix Require Export lambda.interp.
+From stdpp Require Import options.
+
+Module Import lambda.
+Export lambda.
+
+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 x => if E !! x is Some t then thunk_to_expr t else EId x
+    | EAbs x e => EAbs x (subst_env (delete x E) e)
+    | EApp e1 e2 => EApp (subst_env E e1) (subst_env E e2)
+    end.
+Proof.
+  rewrite /subst_env. destruct e; simpl; try done.
+  - rewrite lookup_fmap. by destruct (E !! x) as [[]|].
+  - by rewrite fmap_delete.
+Qed.
+Lemma subst_env_id x E :
+  subst_env E (EId x) = if E !! x is Some t then thunk_to_expr t else EId x.
+Proof. by rewrite subst_env_eq. 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 x (subst_env (delete x E) e)
+  end.
+
+Lemma final_val_to_expr v : final (val_to_expr v).
+Proof. by destruct v. Qed.
+Lemma step_not_val_to_expr v e : val_to_expr v --> e → False.
+Proof. intros []%step_not_final. apply final_val_to_expr. Qed.
+
+Lemma subst_empty e : subst ∅ e = e.
+Proof. induction e; f_equal/=; auto. 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.
+
+Definition is_not_id (e : expr) : Prop :=
+  match e with EId _ => False | _ => True end.
+
+Lemma id_or_not e : (∃ x, e = EId x) ∨ is_not_id e.
+Proof. destruct e; naive_solver. Qed.
+
+Lemma interp_not_id n E e v :
+  interp n E e = mret v → is_not_id (subst_env E e).
+Proof.
+  revert E e v. induction n as [|n IH]; intros E e v; [done|].
+  rewrite interp_S. destruct e; simpl; try done.
+  rewrite subst_env_id. destruct (_ !! _) as [[[]]|]; naive_solver.
+Qed.
+
+Fixpoint closed (X : stringset) (e : expr) : Prop :=
+  match e with
+  | EString _ => True
+  | EId x => x ∈ X
+  | EAbs x e => closed ({[ x ]} ∪ X) e
+  | EApp e1 e2 => closed X e1 ∧ closed X e2
+  end.
+
+Inductive closed_thunk (t : thunk) : Prop := {
+  closed_thunk_env : map_Forall (λ _, closed_thunk) (thunk_env t);
+  closed_thunk_expr : closed (dom (thunk_env t)) (thunk_expr t);
+}.
+Notation closed_env := (map_Forall (M:=env) (λ _, closed_thunk)).
+
+Definition closed_val (v : val) : Prop :=
+  match v with
+  | VString _ => True
+  | VClo x E e => closed_env E ∧ closed ({[x]} ∪ dom E) e
+  end.
+
+Lemma closed_thunk_eq E e :
+  closed_thunk (Thunk E e) ↔ closed_env E ∧ closed (dom E) e.
+Proof. split; inv 1; constructor; done. Qed.
+
+Lemma closed_env_delete x E : closed_env E → closed_env (delete x E).
+Proof. apply map_Forall_delete. Qed.
+
+Lemma closed_env_insert x t E :
+  closed_thunk t → closed_env E → closed_env (<[x:=t]> E).
+Proof. apply: map_Forall_insert_2. Qed.
+
+Lemma closed_env_lookup E x t :
+  closed_env E → E !! x = Some t → closed_thunk t.
+Proof. apply map_Forall_lookup_1. Qed.
+
+Lemma closed_subst E ds e :
+  dom ds ## E → closed E e → subst ds e = e.
+Proof.
+  revert E ds.
+  induction e; intros E ds Hdisj Heclosed; simplify_eq/=; first done.
+  - assert (Hxds : x ∉ dom ds) by set_solver.
+    by rewrite (not_elem_of_dom_1 _ _ Hxds).
+  - f_equal. by apply IHe with (E := {[x]} ∪ E); first set_solver.
+  - f_equal; naive_solver.
+Qed.
+
+Lemma closed_weaken X Y e : closed X e → X ⊆ Y → closed Y e.
+Proof. revert X Y; induction e; naive_solver eauto with set_solver. Qed.
+
+Lemma subst_closed ds X e :
+  map_Forall (λ _, closed ∅) ds →
+  closed (dom ds ∪ X) e →
+  closed X (subst ds e).
+Proof.
+  revert X ds. induction e; intros X ds; repeat (case_decide || simplify_eq/=).
+  - done.
+  - intros. case_match.
+    + apply H in H1. by eapply closed_weaken.
+    + apply not_elem_of_dom in H1. set_solver.
+  - intros. apply IHe.
+    + by apply map_Forall_delete.
+    + by rewrite dom_delete_L assoc_L difference_union_L
+                 [dom _ ∪ _]comm_L -assoc_L.
+  - naive_solver.
+Qed.
+
+Lemma subst_env_delete_closed E X e x :
+  closed_env E →
+  closed ({[x]} ∪ X) (subst_env E e) →
+  closed ({[x]} ∪ X) (subst_env (delete x E) e).
+Proof.
+  revert E X x.
+  induction e as [s | z | z e IHe | e1 IHe1 e2 IHe2]; intros E X x.
+  - rewrite !subst_env_eq //.
+  - rewrite !subst_env_eq /=. case_match.
+    + destruct (decide (x = z)) as [->|?].
+      * rewrite lookup_delete. set_solver.
+      * rewrite lookup_delete_ne // H //.
+    + destruct (decide (x = z)) as [->|?].
+      * rewrite delete_notin // H //.
+      * rewrite lookup_delete_ne // H //.
+  - intros HE.
+    rewrite [subst_env (delete _ _) _]subst_env_eq subst_env_eq /=
+            delete_commute comm_L -assoc_L.
+    by apply IHe, map_Forall_delete.
+  - rewrite [subst_env (delete _ _) _]subst_env_eq subst_env_eq /=.
+    naive_solver.
+Qed.
+
+Lemma subst_env_closed E X e :
+  closed_env E → closed (dom E ∪ X) e → closed X (subst_env E e).
+Proof.
+  revert e X. induction E using env_ind.
+  induction e; intros X Hcenv Hclosed; simplify_eq/=.
+  - done.
+  - rewrite subst_env_eq. case_match.
+    + destruct t as [Et et]; simpl.
+      apply closed_env_lookup in H0 as Htclosed; last done.
+      apply closed_thunk_eq in Htclosed as [HEtclosed Hetclosed].
+      apply (H _ _ H0); simpl.
+      * exact HEtclosed.
+      * eapply closed_weaken; set_solver.
+    + simpl in *. apply not_elem_of_dom in H0. set_solver.
+  - rewrite subst_env_eq. simpl in *.
+    rewrite comm_L -assoc_L in Hclosed.
+    apply IHe in Hclosed; last exact Hcenv.
+    apply subst_env_delete_closed; first done.
+    by rewrite comm_L.
+  - rewrite subst_env_eq. naive_solver.
+Qed.
+
+Lemma thunk_to_expr_closed t : closed_thunk t → closed ∅ (thunk_to_expr t).
+Proof.
+  destruct t as [E e]. intros [HEclosed Heclosed]%closed_thunk_eq.
+  by apply subst_env_closed; last rewrite union_empty_r_L.
+Qed.
+
+Lemma subst_env_insert E x e t :
+  closed_env E → 
+  subst_env (<[x:=t]> E) e
+  = subst {[x:=thunk_to_expr t]} (subst_env (delete x E) e).
+Proof.
+  revert E. induction e; intros E HEclosed; simpl.
+  - done.
+  - destruct (decide (x = x0)) as [->|?].
+    + rewrite subst_env_eq lookup_insert subst_env_id
+        lookup_delete /= lookup_singleton. done.
+    + rewrite subst_env_eq lookup_insert_ne // subst_env_id.
+      destruct (E !! x0) eqn:Elookup.
+      * apply closed_env_lookup in Elookup as Hc0closed; last done.
+        apply thunk_to_expr_closed in Hc0closed.
+        rewrite lookup_delete_ne // Elookup.
+        by erewrite closed_subst with (E := ∅).
+      * by rewrite lookup_delete_ne // Elookup /= lookup_singleton_ne.
+  - rewrite (subst_env_eq (EAbs x0 e)) (subst_env_eq (EAbs _ _)) /=. f_equal.
+    destruct (decide (x0 = x)) as [->|?].
+    + by rewrite delete_insert_delete delete_idemp
+                 delete_singleton subst_empty.
+    + rewrite delete_insert_ne // delete_singleton_ne // delete_commute.
+      apply IHe. by apply closed_env_delete.
+  - rewrite (subst_env_eq (EApp _ _)) [subst_env (delete x E) _]subst_env_eq /=.
+    f_equal; auto.
+Qed.
+
+Lemma subst_env_insert_eq e1 e2 E1 E2 x E1' E2' e1' e2' :
+  closed_env E1 → closed_env E2 →
+  subst_env (delete x E1) e1 = subst_env (delete x 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 HE1closed HE2closed He' He.
+  rewrite !subst_env_insert //=. by rewrite He' He.
+Qed.
+
+Lemma interp_closed n E e mv :
+  closed_env E → closed (dom E) e → interp n E e = Res mv →
+  if mv is Some v then closed_val v else True.
+Proof.
+  revert E e mv.
+  induction n; first done; intros E e mv HEclosed Heclosed Hinterp.
+  destruct e.
+  - rewrite interp_S /= in Hinterp. by destruct mv; simplify_res.
+  - rewrite interp_S /= in Hinterp. simplify_option_eq.
+    destruct (E !! x) eqn:Hlookup; simplify_res; try done.
+    apply closed_env_lookup in Hlookup; last assumption.
+    destruct t as [E' e']. apply closed_thunk_eq in Hlookup as [Henv Hexpr].
+    by apply IHn with (E := E') (e := e').
+  - rewrite interp_S /= in Hinterp. simplify_option_eq.
+    destruct mv as [v|]; simplify_res. split_and!.
+    + set_solver.
+    + done.
+  - rewrite interp_S /= in Hinterp. simplify_option_eq.
+    destruct Heclosed as [He1closed He2closed].
+    destruct (interp n E e1) as [[[]|]|] eqn:Einterp; simplify_res; try done.
+    apply IHn in Einterp; try done.
+    simpl in Einterp. destruct Einterp as [Hinterp1 Hinterp2].
+    apply IHn in Hinterp; first done.
+    + rewrite <-insert_delete_insert.
+      apply map_Forall_insert; first apply lookup_delete. split.
+      * by split.
+      * by apply closed_env_delete.
+    + by rewrite dom_insert_L.
+Qed.
+
+Lemma interp_proper n E1 E2 e1 e2 mv :
+  closed_env E1 → closed_env E2 →
+  closed (dom E1) e1 → closed (dom E2) e2 →
+  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 E2 E1 e1 e2 mv. induction n as [|n IHn]; [done|].
+  intros E2. induction E2 as [E2 IH] using env_ind.
+  intros E1 e1 e2 mv HE1closed HE2closed He1closed He2closed Hsubst Hinterp.
+  destruct (id_or_not e1) as [[x ->]|?].
+  { rewrite interp_S /= in Hinterp.
+    destruct (E1 !! x) as [[E' e']|] eqn:Hx; simplify_eq/=;
+      last by apply not_elem_of_dom in Hx.
+    rewrite subst_env_id Hx in Hsubst.
+    apply closed_env_lookup in Hx; last done.
+    rewrite closed_thunk_eq in Hx.
+    destruct Hx as [HE'close He'closed].
+    eauto. }
+  destruct (id_or_not e2) as [[x ->]|?].
+  { rewrite subst_env_id in Hsubst.
+    destruct (E2 !! x) as [[E' e']|] eqn:Hx; simplify_eq/=.
+    - apply closed_env_lookup in Hx as Hclosed; last done.
+      rewrite closed_thunk_eq in Hclosed.
+      destruct Hclosed as [HE'closed He'closed].
+      rewrite map_Forall_lookup in IH.
+      odestruct (IH _ _ Hx) as (w & m & Hinterp' & Hw);
+        first apply HE1closed; try done.
+      exists w, (S m). by rewrite interp_S /= Hx /=.
+    - destruct mv as [v|].
+      + apply interp_not_id in Hinterp. by rewrite Hsubst in Hinterp.
+      + exists None, 1. by rewrite interp_S /= Hx. }
+  rewrite (subst_env_eq e1) (subst_env_eq e2) in Hsubst.
+  rewrite interp_S in Hinterp. destruct e1, e2; simplify_res; try done.
+  - eexists (Some (VString _)), 1. by rewrite interp_S.
+  - eexists (Some (VClo _ _ _)), 1. split; first by rewrite interp_S.
+    by do 2 f_equal/=.
+  - destruct (interp n _ _) as [mv'|] eqn:Hinterp'; simplify_res.
+    destruct He1closed as [He1_1closed He1_2closed],
+             He2closed as [He2_1closed He2_2closed].
+    apply interp_closed in Hinterp' as Hclosed; [|done..].
+    eapply IHn with (e2 := e2_1) in Hinterp' as (mw' & m1 & Hinterp1 & ?);
+      try 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 & ?).
+    + exists w, (S (m1 `max` m2)). rewrite interp_S /=.
+      rewrite (interp_le Hinterp1) /=; last lia.
+      rewrite (interp_le Hinterp2) /=; last lia. done.
+    + rewrite -insert_delete_insert.
+      apply map_Forall_insert; first apply lookup_delete.
+      split; first done. apply closed_env_delete. naive_solver.
+    + apply interp_closed in Hinterp1; [|done..].
+      rewrite /closed_val in Hinterp1. destruct Hinterp1 as [??].
+      by apply map_Forall_insert_2.
+    + rewrite dom_insert_L. naive_solver.
+    + rewrite dom_insert_L.
+      apply interp_closed in Hinterp1; [|done..].
+      rewrite /closed_val in Hinterp1. by destruct Hinterp1 as [_ ?].
+    + apply interp_closed in Hinterp1; [|done..].
+      rewrite /closed_val in Hinterp1. destruct Hinterp1 as [? _].
+      apply subst_env_insert_eq; try naive_solver.
+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 :
+  closed {[x]} e1 → closed ∅ e2 →
+  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.
+  intros He1 He2.
+  apply interp_proper.
+  - done.
+  - by apply closed_env_insert.
+  - apply subst_closed.
+    + by apply map_Forall_singleton.
+    + by rewrite dom_singleton_L dom_empty_L union_empty_r_L.
+  - by rewrite insert_empty dom_singleton_L.
+  - by rewrite subst_env_empty subst_as_subst_env.
+Qed.
+
+Lemma closed_step e1 e2 : closed ∅ e1 → e1 --> e2 → closed ∅ e2.
+Proof.
+  intros Hclosed Hstep. revert Hclosed.
+  induction Hstep; intros He1closed.
+  - simplify_eq/=. destruct He1closed.
+    apply subst_closed.
+    + by eapply map_Forall_singleton.
+    + by rewrite dom_singleton_L.
+  - simplify_eq/=. destruct He1closed. auto.
+Qed.
+
+Lemma closed_steps e1 e2 : closed ∅ e1 → e1 -->* e2 → closed ∅ e2.
+Proof. induction 2; eauto using closed_step. Qed.
+
+Lemma interp_step e1 e2 n v :
+  closed ∅ e1 →
+  e1 --> e2 →
+  interp n ∅ e2 = Res v →
+  ∃ w m, interp m ∅ e1 = Res w ∧ val_to_expr <$> v = val_to_expr <$> w.
+Proof.
+  intros He1closed Hstep. revert v n He1closed.
+  induction Hstep as [|???? IH]; intros v n He1closed Hinterp.
+  { rewrite /= union_empty_r_L in He1closed.
+    destruct He1closed as [He1closed He2closed].
+    apply interp_subst in Hinterp as (w & [|m] & Hinterp & Hv);
+      simplify_eq/=; [|done..].
+    exists w, (S (S m)). by rewrite !interp_S /= -interp_S. }
+  simpl in He1closed. destruct He1closed as [He1closed He2closed].
+  destruct n as [|n]; [done|rewrite interp_S /= in Hinterp].
+  destruct (interp n _ _) eqn:Hinterp'; simplify_res.
+  destruct x; simplify_res; last first.
+  { apply IH in Hinterp' as (mw' & m1 & Hinterp1 & ?); simplify_res; last done.
+    destruct mw'; try done. exists None, (S m1).
+    by rewrite interp_S /= Hinterp1. }
+  apply closed_step in Hstep as He1'closed; last done.
+  apply interp_closed in Hinterp' as Hcloclosed;
+    [|done|by rewrite dom_empty_L].
+  apply IH in Hinterp' as ([] & m1 & Hinterp1 & ?); simplify_eq/=; last done.
+  destruct (maybe3 VClo _) eqn:Hclo; simplify_res; last first.
+  { exists None, (S m1). rewrite interp_S /= Hinterp1 /=.
+    by assert (maybe3 VClo v1 = None) as -> by (by destruct v1, v0). }
+  simplify_option_eq.
+  simpl in Hcloclosed. destruct Hcloclosed as [HEclosed Heclosed].
+  apply interp_closed in Hinterp1 as Hcloclosed;
+    [|done|by rewrite dom_empty_L]. simpl in Hcloclosed.
+  destruct v1; simplify_option_eq.
+  destruct Hcloclosed as [HE0closed He0closed].
+  eapply interp_proper with (E2 := <[x0:=Thunk ∅ e2]> E0) (e2 := e0)
+    in Hinterp as (w & m2 & Hinterp2 & Hv); last apply subst_env_insert_eq.
+  { exists w, (S (m1 `max` m2)). rewrite !interp_S /=.
+    rewrite (interp_le Hinterp1) /=; last lia.
+    by rewrite (interp_le Hinterp2) /=; last lia. }
+  - by apply closed_env_insert.
+  - by apply closed_env_insert.
+  - by rewrite dom_insert_L.
+  - by rewrite dom_insert_L.
+  - done.
+  - done.
+  - done.
+  - done.
+Qed.
+
+Lemma final_interp e :
+  final e →
+  ∃ w m, interp m ∅ e = mret w ∧ e = val_to_expr w.
+Proof.
+  induction e; inv 1.
+  - eexists (VString _), 1. by rewrite interp_S /=.
+  - eexists (VClo _ _ _), 1. rewrite interp_S /=. split; [done|].
+    by rewrite delete_empty 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 *) do 2 right. by exists 1.
+  - (* EAbs *) right; left. constructor.
+  - (* 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 :
+  closed ∅ e1 →
+  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 He1 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. }
+  apply closed_step in Hstep as He2; last assumption.
+  destruct IH as (mw & m & Hinterp & ?); try done.
+  eapply interp_step in Hinterp as (mw' & m' & ? & ?).
+  - destruct mw, mw'; naive_solver.
+  - done.
+  - done.
+Qed.
+
+Lemma interp_complete_ret e1 e2 :
+  closed ∅ e1 →
+  e1 -->* e2 → final e2 →
+  ∃ w m, interp m ∅ e1 = mret w ∧ e2 = val_to_expr w.
+Proof.
+  intros Hclosed Hsteps Hfinal. apply interp_complete in Hsteps
+    as ([w|] & m & ? & ?); naive_solver eauto using final_nf.
+Qed.
+Lemma interp_complete_fail e1 e2 :
+  closed ∅ e1 →
+  e1 -->* e2 → nf step e2 → ¬final e2 →
+  ∃ m, interp m ∅ e1 = mfail.
+Proof.
+  intros Hclosed Hsteps Hnf Hforce.
+  apply interp_complete in Hsteps as ([w|] & m & ? & ?); simplify_eq/=; try by eauto.
+  destruct Hforce. apply final_val_to_expr.
+Qed.
+
+Lemma interp_sound_open E e n mv :
+  closed_env E → closed (dom E) e →
+  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 HEclosed Heclosed Hinterp; first done.
+  rewrite subst_env_eq. rewrite interp_S in Hinterp.
+  destruct e; simplify_res.
+  - (* ENat *) by eexists.
+  - (* EId *) destruct (_ !! _) as [[E' e]|] eqn:Hx; simplify_res.
+    + apply closed_env_lookup in Hx as Hxclosed; last done.
+      rewrite closed_thunk_eq in Hxclosed. destruct_and!.
+      apply IH in Hinterp as (e' & Hsteps & He'); naive_solver.
+    + eexists; repeat split; [done| |inv 1]. intros [? Hstep]. inv Hstep.
+  - (* EAbs *) by eexists.
+  - (* EApp *) destruct_and!.
+    destruct (interp _ _ _) as [mv'|] eqn:Hinterp'; simplify_res.
+    apply interp_closed in Hinterp' as Hvclosed; [|done..].
+    apply IH in Hinterp' as (e' & Hsteps & He'); [|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. destruct_and!.
+    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'.
+    + by apply closed_env_insert.
+    + by rewrite dom_insert_L.
+Qed.
+
+Lemma interp_sound n e mv :
+  closed ∅ e →
+  interp n ∅ e = Res mv →
+  ∃ e', e -->* e' ∧ if mv is Some v then e' = val_to_expr v else stuck e'.
+Proof.
+  intros He Hsteps%interp_sound_open; try done.
+  by rewrite subst_env_empty in Hsteps.
+Qed.
+
+(** Final theorems *)
+Theorem interp_sound_complete_ret e v :
+  closed ∅ e →
+  (∃ 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 in Hsteps as ([] & ? & ? & ?);
+      unfold nf, red;
+      naive_solver eauto using final_val_to_expr, step_not_val_to_expr.
+Qed.
+
+Theorem interp_sound_complete_ret_string e s :
+  closed ∅ e →
+  (∃ 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 :
+  closed ∅ 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 :
+  closed ∅ 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 & _); [|done..].
+      by rewrite Hnofuel in Hinterp.
+    + apply interp_sound_complete_fail in He' as (e'' & ? & [Hnf _]);
+        last by eauto using closed_steps.
+      destruct (interp_complete e e'') as (mv & n & Hinterp & _); [done|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); [|done].
+    destruct mv as [v|]; simplify_eq/=.
+    + apply final_nf in Hsteps as []. apply final_val_to_expr.
+    + by destruct Hstuck as [[] ?].
+Qed.
+
+End lambda.
diff --git a/theories/lambda/operational.v b/theories/lambda/operational.v
new file mode 100644
index 0000000..b0fa366
--- /dev/null
+++ b/theories/lambda/operational.v
@@ -0,0 +1,38 @@
+From mininix Require Export utils.
+From stdpp Require Import options.
+
+Module Import lambda.
+
+Inductive expr :=
+  | EString (s : string)
+  | EId (x : string)
+  | EAbs (x : string) (e : expr)
+  | EApp (e1 e2 : expr).
+
+Fixpoint subst (ds : gmap string expr) (e : expr) : expr :=
+  match e with
+  | EString s => EString s
+  | EId x => if ds !! x is Some d then d else EId x
+  | EAbs x e => EAbs x (subst (delete x ds) e)
+  | EApp e1 e2 => EApp (subst ds e1) (subst ds e2)
+  end.
+
+Reserved Infix "-->" (right associativity, at level 55).
+Inductive step : expr → expr → Prop :=
+  | Sβ x e1 e2 : EApp (EAbs x e1) e2 --> subst {[x:=e2]} e1
+  | SAppL e1 e1' e2 : e1 --> e1' → EApp e1 e2 --> EApp e1' e2
+where "e1 --> e2" := (step e1 e2).
+
+Infix "-->*" := (rtc step) (right associativity, at level 55).
+
+Definition final (e : expr) : Prop :=
+  match e with
+  | EString _ => True
+  | EAbs _ _ => True
+  | _ => False
+  end.
+
+Definition stuck (e : expr) : Prop :=
+  nf step e ∧ ¬final e.
+
+End lambda.
diff --git a/theories/lambda/operational_props.v b/theories/lambda/operational_props.v
new file mode 100644
index 0000000..c331924
--- /dev/null
+++ b/theories/lambda/operational_props.v
@@ -0,0 +1,29 @@
+From mininix Require Export lambda.operational.
+From stdpp Require Import options.
+
+Module Import lambda.
+Export lambda.
+
+(** Properties of operational semantics *)
+Lemma step_not_final e1 e2 : e1 --> e2 → ¬final e1.
+Proof. induction 1; inv 1; naive_solver. Qed.
+Lemma final_nf e : final e → nf step e.
+Proof. by intros ? [??%step_not_final]. Qed.
+
+Lemma SAppL_rtc e1 e1' e2 : e1 -->* e1' → EApp e1 e2 -->* EApp e1' e2.
+Proof. induction 1; repeat (done || econstructor). Qed.
+
+Ltac inv_step := repeat
+  match goal with H : ?e --> _ |- _ => assert_fails (is_var e); inv H end.
+
+Lemma step_det e d1 d2 :
+  e --> d1 →
+  e --> d2 →
+  d1 = d2.
+Proof.
+  intros Hred1. revert d2.
+  induction Hred1; intros d2 Hred2; inv Hred2; try by inv_step.
+  f_equal. by apply IHHred1.
+Qed.
+
+End lambda.