proposition: Theorem Diophantine_to_MuRec_computable {k} (R : Vector.t nat k -> nat -> Prop) : functional R -> Diophantine' R -> MuRec_computable R.
proof: Proof. intros HR (k' & P1 & P2 & H). eapply (MuRec_computable_functional_iff _ HR). unshelve eexists. - eapply ra_comp. 1: refine (ra_project (Fin.F1)). 2: exact (ra_dio_poly_find (dio_move P1) (dio_move P2) ## vec_nil). exact k'. - split. + intros v m. specialize (H (Vector.cons _ m _ v)). cbn -[dp_eval Vector.nth] in H. rewrite H. rewrite <- ra_bs_correct, ra_rel_fix_comp. unfold s_comp. intros (vi & H1 & H2). revert H1 H2. eapply (Vector.caseS' vi). clear vi. intros im. refine (Vector.case0 _ _). intros Hproj Hfind. specialize (Hfind Fin.F1). cbn -[ra_dio_poly_find] in Hfind. eapply ra_dio_poly_find_spec_strong1 in Hfind. eapply ra_project_rel in Hproj. clear H. subst. pose (w := (recomp.project (S k') im)). exists (fun j => vec_pos w (Fin.FS j)). generalize (eq_refl w). unfold w at 1. eapply (Vector.caseS' w). clear w. intros x w Hw. rewrite Hw in Hfind. rewrite !dio_move_spec in Hfind. erewrite dp_eval_ext. * rewrite Hfind. eapply dp_eval_ext. -- intros. reflexivity. -- intros. rewrite vec_pos_spec. cbn [vec_pos vec_head]. rewrite Hw. reflexivity. * intros. reflexivity. * intros. cbn [vec_head]. rewrite Hw. unfold vec_pos at 1. cbn [pos_S_inv]. now rewrite vec_pos_spec. + intros v m Hvm. specialize (H (Vector.cons _ m _ v)). cbn -[dp_eval Vector.nth] in H. eapply H in Hvm as [ν Hν]. erewrite dp_eval_ext in Hν at 1. 1: symmetry in Hν. 1: erewrite dp_eval_ext in Hν at 1. 1: symmetry in Hν. 1: erewrite <- !dio_move_spec in Hν. 1: eapply ra_dio_poly_find_spec_strong2 in Hν as [e Hν]. 1: eexists. 1: rewrite <- ra_bs_correct, ra_rel_fix_comp. 1: unfold s_comp. 1: eexists. 1: split. * eapply ra_project_rel. reflexivity. * intros p. eapply (Fin.caseS' p). 2: eapply Fin.case0. rewrite vec_pos_map. instantiate (1 := e ## vec_nil). cbn [vec_pos pos_S_inv]. eassumption. * intros. instantiate (1 := vec_set_pos _). now rewrite vec_pos_set. * intros. now rewrite vec_pos_spec. * intros. now rewrite vec_pos_set. * intros. now rewrite vec_pos_spec. Unshelve. Qed.
imports: List Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_nat) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.H10(Dio.dio_single H10 Diophantine) Undecidability.MuRec.Util(recalg ra_dio_poly MuRec_computable ra_sem_eq ra_recomp)