From Undecidability Require Import TM.TMEncoding TM.TMinL TM.Util.TM_facts.
From Undecidability.L Require Import Computability.MuRec.
Require Import Undecidability.Synthetic.Definitions.
Lemma TM_eval_halts Σ n (M : TM Σ n) q t q' t' :
TM.eval M q t q' t' -> halt M q' = true.
Proof.
induction 1; eauto.
Qed.
Theorem HaltMTM_to_HaltL :
HaltMTM ⪯ HaltL.
Proof.
eexists (fun '(existT2 (Sigma, n) M tp) =>
(L.app mu (@ext _ _ _ (term_test (mk_mconfig (start M) tp))))).
intros [ [Sigma n] M tp ]. cbn.
unfold HaltL. setoid_rewrite eval_iff.
split.
- intros H.
epose proof (Halt_red (mk_mconfig (start M) tp)) as [[v [H1 H2]] _].
+ destruct H as (? & ? & ?). eexists (mk_mconfig _ _).
rewrite <- TM_eval_iff. split. 2:eassumption.
eapply TM_eval_halts. eassumption.
+ exists v. split; eauto.
eapply equiv_lambda. eassumption. eassumption.
- intros [t [H1 H2]].
epose proof (Halt_red (mk_mconfig (start M) tp)) as [_ [[q' t']]].
+ eexists. eauto.
+ exists q', t'. eapply TM_eval_iff. eapply H.
Qed.
From Undecidability.L Require Import Computability.MuRec.
Require Import Undecidability.Synthetic.Definitions.
Lemma TM_eval_halts Σ n (M : TM Σ n) q t q' t' :
TM.eval M q t q' t' -> halt M q' = true.
Proof.
induction 1; eauto.
Qed.
Theorem HaltMTM_to_HaltL :
HaltMTM ⪯ HaltL.
Proof.
eexists (fun '(existT2 (Sigma, n) M tp) =>
(L.app mu (@ext _ _ _ (term_test (mk_mconfig (start M) tp))))).
intros [ [Sigma n] M tp ]. cbn.
unfold HaltL. setoid_rewrite eval_iff.
split.
- intros H.
epose proof (Halt_red (mk_mconfig (start M) tp)) as [[v [H1 H2]] _].
+ destruct H as (? & ? & ?). eexists (mk_mconfig _ _).
rewrite <- TM_eval_iff. split. 2:eassumption.
eapply TM_eval_halts. eassumption.
+ exists v. split; eauto.
eapply equiv_lambda. eassumption. eassumption.
- intros [t [H1 H2]].
epose proof (Halt_red (mk_mconfig (start M) tp)) as [_ [[q' t']]].
+ eexists. eauto.
+ exists q', t'. eapply TM_eval_iff. eapply H.
Qed.