proposition: Theorem computable_MuRec_to_L {k} (R : Vector.t nat k -> nat -> Prop) : MuRec_computable R -> L_computable R.
proof: Proof. intros [f Hf]. exists (cont_vec k (lam (mu_option (lam (ext evalfun 0 (enc (erase f)) 1))))). intros v. rewrite <- many_app_eq_nat. split. - intros m. rewrite L_facts.eval_iff. assert (lambda (encNatL m)) as [b Hb]. { change (lambda (enc m)). Lproc. } rewrite Hb. rewrite eproc_equiv. rewrite cont_vec_correct. 2: unfold mu_option; Lproc. assert (lam (mu_option (lam (ext evalfun 0 (enc (erase f)) 1))) (enc v) == mu_option (lam (ext evalfun 0 (enc (erase f)) (enc v)))). { unfold mu_option. now Lsimpl. } rewrite H. rewrite <- Hb. change (encNatL m) with (enc m). rewrite mu_option_spec. 2:Lproc. 2:{ intros []; cbv; congruence. } 2:{ intros. eexists. rewrite !enc_vector_eq. Lsimpl. reflexivity. } 1: rewrite Hf. 1: split. + intros [n Hn % erase_correct] % ra_bs_to_c. exists n. rewrite !enc_vector_eq. Lsimpl. unfold evalfun. rewrite <- vec_list_eq. now rewrite Hn. + intros [n Hn]. eapply ra_bs_from_c. eapply erase_correct with (c := n). match goal with [Hn : ?s == ?b |- _ ] => evar (t : term); assert (s == t) end. { rewrite !enc_vector_eq. Lsimpl. subst t. reflexivity. } subst t. rewrite vec_list_eq. rewrite H0 in Hn. eapply enc_extinj in Hn. unfold evalfun in Hn. now destruct eval as [[] | ]; inv Hn. + intros. rewrite enc_vector_eq in *. match type of H0 with ?s == ?b => evar (t : term); assert (s == t) end. 1: Lsimpl. all: subst t. 1: reflexivity. rewrite H2 in H0. clear H2. eapply enc_extinj in H0. Lsimpl. unfold evalfun in *. destruct (eval n) as [ [] | ] eqn:E; inv H0. rewrite <- vec_list_eq in *. eapply eval_mono in E. 1: rewrite E; eauto. lia. - intros v' [H1 H2] % eval_iff. eapply star_equiv_subrelation in H1. rewrite cont_vec_correct in H1. 2: unfold mu_option; Lproc. match goal with [Hn : ?s == ?b |- _ ] => evar (t : term); assert (s == t) end. 1: unfold mu_option. 1: Lsimpl. all: subst t. 1: reflexivity. rewrite H in H1. match type of H1 with ?s == _ => assert (converges s) end. 1: exists v'; split; eassumption. eapply app_converges in H0 as [Hc _]. eapply app_converges in Hc as [Hc _]. eapply app_converges in Hc as [_ Hc]. destruct Hc as [v'' [Hc1 Hc2]]. pose proof (Hc1' := Hc1). eapply mu_sound in Hc1; eauto. + destruct Hc1 as [m [-> []]]. rewrite Hc1' in H1. rewrite enc_vector_eq in H1. destruct (evalfun m (erase f) (Vector.to_list v)) eqn:E. * match type of H1 with ?s == ?b => evar (t : term); assert (s == t) end. 1: Lsimpl. all: subst t. 1: reflexivity. rewrite H4, E in H1. match type of H1 with ?s == ?b => evar (t : term); assert (s == t) end. 1: Lsimpl. all: subst t. 1: reflexivity. rewrite H5 in H1. eapply unique_normal_forms in H1. 2,3: Lproc. subst. exists n. reflexivity. * enough (true = false) by congruence. eapply enc_extinj. rewrite <- H0. rewrite enc_vector_eq. Lsimpl. now rewrite E. + Lproc. + intros n. destruct (evalfun n (erase f) (Vector.to_list v)) eqn:EE; eexists; rewrite enc_vector_eq; Lsimpl; rewrite EE; try Lsimpl; reflexivity. Qed.
imports: Undecidability.H10(H10 dio_single dio_logic) Undecidability.L.Datatypes(LNat LOptions LSum) Undecidability.L(Tactics.LTactics Computability.MuRec Computability.Synthetic Tactics.GenEncode) Undecidability.Shared(DLW.Utils.finite DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec(MuRec recalg ra_sem_eq) Undecidability.L.Reductions.MuRec.MuRec_extract Undecidability.L.Reductions.MuRec.MuRec_extract Undecidability(MuRec_computable LVector) Undecidability.L.Util(NaryApp ClosedLAdmissible) Undecidability(LOptions) Undecidability.L.Reductions.MuRec.MuRec_extract