From ba61dfd69504ec6263a9dee9931d93adeb6f3142 Mon Sep 17 00:00:00 2001 From: Rutger Broekhoff Date: Mon, 7 Jul 2025 21:52:08 +0200 Subject: Initialize repository --- theories/dynlang/equiv.v | 154 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 154 insertions(+) create mode 100644 theories/dynlang/equiv.v (limited to 'theories/dynlang/equiv.v') 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. -- cgit v1.2.3