Initialize repository

1 files changed, 154 insertions, 0 deletions

diff --git a/theories/dynlang/equiv.v b/theories/dynlang/equiv.v
new file mode 100644
index 0000000..aa0b7f3
--- /dev/null
+++ b/theories/dynlang/equiv.v
@@ -0,0 +1,154 @@
+From mininix Require Export lambda.interp_proofs dynlang.interp_proofs.
+From stdpp Require Import options.
+
+Class Lift A B := lift : A → B.
+Global Hint Mode Lift ! - : typeclass_instances.
+Arguments lift {_ _ _} !_ /.
+Notation "⌜ x ⌝" := (lift x) (at level 0).
+Notation "⌜* x ⌝" := (fmap lift x) (at level 0).
+
+Module lambda.
+  Global Instance lambda_expr_lift : Lift lambda.expr dynlang.expr :=
+    fix go e := let _ : Lift _ _ := go in
+    match e with
+    | lambda.EString s => dynlang.EString s
+    | lambda.EId x => dynlang.EId ∅ (dynlang.EString x)
+    | lambda.EAbs x e => dynlang.EAbs (dynlang.EString x) ⌜e⌝
+    | lambda.EApp e1 e2 => dynlang.EApp ⌜e1⌝ ⌜e2⌝
+    end.
+
+  Global Instance lambda_thunk_lift : Lift lambda.thunk dynlang.thunk :=
+    fix go t := let _ : Lift _ _ := go in
+    dynlang.Thunk ⌜*lambda.thunk_env t⌝ ⌜lambda.thunk_expr t⌝.
+
+  Global Instance lambda_val_lift : Lift lambda.val dynlang.val := λ v,
+    match v with
+    | lambda.VString s => dynlang.VString s
+    | lambda.VClo x E e => dynlang.VClo x ⌜*E⌝ ⌜e⌝
+    end.
+End lambda.
+
+Lemma interp_open_lambda_dynlang E e mv n :
+  lambda.closed_env E → lambda.closed (dom E) e →
+  lambda.interp n E e = Res mv →
+  ∃ m, dynlang.interp m ⌜*E⌝ ⌜e⌝ = Res ⌜*mv⌝.
+Proof.
+  revert E e mv. induction n as [|n IH]; [done|]; intros E e mv HE He Hinterp.
+  rewrite lambda.interp_S in Hinterp. destruct e as [s|z|ex e|e1 e2]; simplify_res.
+  - (* EString *) by exists 1.
+  - (* EId *)
+    apply elem_of_dom in He as [[Et et] Hz]. rewrite Hz /= in Hinterp.
+    apply lambda.closed_env_lookup in Hz as He; last done.
+    rewrite lambda.closed_thunk_eq/= in He. destruct He as [HEtclosed Hetclosed].
+    apply IH in Hinterp as [m Hinterp]; [|done..].
+    exists (S (S m)). rewrite !dynlang.interp_S /= -dynlang.interp_S.
+    rewrite lookup_empty /= right_id_L lookup_fmap Hz /=.
+    eauto using dynlang.interp_le with lia.
+  - (* EAbs *) by exists 2.
+  - (* EApp *)
+    destruct He as [He1 He2].
+    destruct (lambda.interp _ _ e1) as [mw|] eqn:Hinterp1; simplify_res.
+    pose proof Hinterp1 as Hinterp1'.
+    apply lambda.interp_closed in Hinterp1' as Hmw; [|done..].
+    eapply IH in Hinterp1 as [m1 Hinterp1]; [|done..].
+    destruct mw as [w|]; simplify_res; last first.
+    { exists (S m1). by rewrite dynlang.interp_S /= Hinterp1. }
+    destruct (maybe3 lambda.VClo w) eqn:?; simplify_res; last first.
+    { exists (S m1). rewrite dynlang.interp_S /= Hinterp1 /=. by destruct w. }
+    destruct w; simplify_res.
+    apply IH in Hinterp as [m2 Hinterp2].
+    + exists (S (m1 + m2)). rewrite dynlang.interp_S /=.
+      rewrite (dynlang.interp_le Hinterp1) /=; last lia.
+      rewrite fmap_insert /= in Hinterp2.
+      rewrite (dynlang.interp_le Hinterp2) /=; last lia. done.
+    + apply lambda.closed_env_insert; [by split|naive_solver].
+    + rewrite dom_insert_L. set_solver.
+Qed.
+Lemma interp_lambda_dynlang e mv n :
+  lambda.closed ∅ e →
+  lambda.interp n ∅ e = Res mv →
+  ∃ m, dynlang.interp m ∅ ⌜e⌝ = Res ⌜*mv⌝.
+Proof. intro. by apply interp_open_lambda_dynlang. Qed.
+
+Lemma interp_open_dynlang_lambda E e mv n :
+  lambda.closed_env E → lambda.closed (dom E) e →
+  dynlang.interp n ⌜*E⌝ ⌜e⌝ = Res mv →
+  ∃ mw, lambda.interp n E e = Res mw ∧ mv = ⌜*mw⌝.
+Proof.
+  revert E e mv. induction n as [|n IH]; [done|]; intros E e mv HE He Hinterp.
+  rewrite dynlang.interp_S in Hinterp. destruct e as [s|z|ex e|e1 e2]; simplify_res.
+  - (* EString *) rewrite lambda.interp_S /=. by eexists.
+  - (* EId *)
+    destruct n as [|n]; [done|].
+    rewrite dynlang.interp_S /= -dynlang.interp_S in Hinterp.
+    apply elem_of_dom in He as [[Et et] Hz].
+    pose proof (f_equal (fmap lift) Hz) as Hz'.
+    rewrite -lookup_fmap /= in Hz'. rewrite Hz' lookup_empty /= {Hz'} in Hinterp.
+    pose proof Hz as Hz'.
+    apply lambda.closed_env_lookup in Hz' as [HEt Het]; simpl in *; last done.
+    apply IH in Hinterp as (mw & Hinterp & ->); [|done..].
+    exists mw. rewrite lambda.interp_S /= Hz /=. done.
+  - (* EAbs *)
+    destruct n as [|n]; [done|].
+    rewrite dynlang.interp_S /= in Hinterp; simplify_res.
+    rewrite lambda.interp_S /=. by eexists.
+  - (* EApp *)
+    destruct He as [He1 He2].
+    destruct (dynlang.interp _ _ _) as [mw1|] eqn:Hinterp1; simplify_res.
+    eapply IH in Hinterp1 as (mv1 & Hinterp1 & ->); [|done..].
+    destruct mv1 as [v1|]; simplify_res; last first.
+    { exists None. by rewrite lambda.interp_S /= Hinterp1. }
+    destruct (maybe3 dynlang.VClo _) eqn:?; simplify_res; last first.
+    { exists None. rewrite lambda.interp_S /= Hinterp1 /=. by destruct v1. }
+    destruct v1; simplify_res.
+    change (dynlang.Thunk ⌜*E⌝ ⌜e2⌝) with ⌜lambda.Thunk E e2⌝ in Hinterp.
+    rewrite -fmap_insert in Hinterp.
+    apply lambda.interp_closed in Hinterp1 as Hmw; [|done..].
+    apply IH in Hinterp as (mv2 & Hinterp2 & ->).
+    + exists mv2. rewrite lambda.interp_S /= Hinterp1 /=. done.
+    + apply lambda.closed_env_insert; [by split|]. naive_solver.
+    + rewrite dom_insert_L. set_solver.
+Qed.
+Lemma interp_dynlang_lambda e mv n :
+  lambda.closed ∅ e →
+  dynlang.interp n ∅ ⌜e⌝ = Res mv →
+  ∃ mw, lambda.interp n ∅ e = Res mw ∧ mv = ⌜*mw⌝.
+Proof. intros. by apply interp_open_dynlang_lambda. Qed.
+
+(* The following equivalences about the semantics trivially follow: *)
+
+Theorem interp_equiv_ret_string e s :
+  lambda.closed ∅ e →
+  rtc lambda.step e (lambda.EString s)
+  ↔ rtc dynlang.step ⌜e⌝ (dynlang.EString s).
+Proof.
+  intros. rewrite -lambda.interp_sound_complete_ret_string //.
+  rewrite -dynlang.interp_sound_complete_ret_string. split; intros [n Hinterp].
+  + by apply interp_lambda_dynlang in Hinterp.
+  + apply interp_dynlang_lambda in Hinterp as ([[]|] & ?); naive_solver.
+Qed.
+
+Theorem interp_equiv_fail e :
+  lambda.closed ∅ e →
+  (∃ e', rtc lambda.step e e' ∧ lambda.stuck e')
+  ↔ (∃ e', rtc dynlang.step ⌜e⌝ e' ∧ dynlang.stuck e').
+Proof.
+  intros. rewrite -lambda.interp_sound_complete_fail //.
+  rewrite -dynlang.interp_sound_complete_fail. split; intros [n Hinterp].
+  + by apply interp_lambda_dynlang in Hinterp.
+  + apply interp_dynlang_lambda in Hinterp as ([] & ?); naive_solver.
+Qed.
+
+Theorem interp_equiv_no_fuel e :
+  lambda.closed ∅ e →
+  all_loop lambda.step e ↔ all_loop dynlang.step ⌜e⌝.
+Proof.
+  intros He. rewrite -lambda.interp_sound_complete_no_fuel; last done.
+  rewrite -dynlang.interp_sound_complete_no_fuel. split; intros Hnofuel n.
+  - destruct (dynlang.interp n ∅ _) as [mv|] eqn:Hinterp; [|done].
+    apply interp_dynlang_lambda in Hinterp as (? & Hinterp & _); [|done].
+    by rewrite Hnofuel in Hinterp.
+  - destruct (lambda.interp n ∅ _) as [mv|] eqn:Hinterp; [|done].
+    apply interp_lambda_dynlang in Hinterp as [m Hinterp]; [|done..].
+    by rewrite Hnofuel in Hinterp.
+Qed.