# Library RE

Require Export Pairs Acceptability.

# Definition of Recursive Enumerability

Definition RE P := exists (f : term), closed f /\ (forall n, f(enc n) == none \/ exists s, f (enc n) == some (tenc s) /\ P s) /\ forall s, P s -> exists n, f (enc n) == some (tenc s).

# The Enumeration combinator and its properties

Section Fix_f.

Variable f : term.

Hypothesis cls_f : closed f.

Hypothesis total_f : forall n, f (enc n) == none \/ exists s, f (enc n) == some (tenc s).

Definition Re := R (.\ "Re", "n", "s"; (!f "n") (.\"t"; ( !(lam(Eq #0)) "t" "s" !I (.\ "", ""; "Re" (!Succ "n") "s") !I))
(.\ ""; "Re" (!Succ "n") "s") !I).

Hint Unfold Re : cbv.

Lemma Re_rec_s n t : Re (enc n) (tenc t) >* (f (enc n)) (lam ( (lam(Eq #0)) #0 (tenc t) I (lam(lam ( (lam(Re #0)) (Succ (enc n)) (tenc t)))) I))
(lam ((lam(Re #0)) (Succ (enc n)) (tenc t))) I.

Proof.

crush.

Qed.

Lemma Re_rec n t : Re (enc n) (tenc t) == (f (enc n)) (lam ( (lam(Eq #0)) #0 (tenc t) I (lam(lam ( (lam(Re #0)) (Succ (enc n)) (tenc t)))) I))
(lam ((lam(Re #0)) (Succ (enc n)) (tenc t))) I.

Proof.

eauto using star_equiv, Re_rec_s.

Qed.

Lemma Re_S n s : converges (Re (enc (S n)) (tenc s)) -> converges (Re (enc n) (tenc s)).

Proof.

intros [x Hx].

destruct (total_f n) as [H | [t H]]; rewrite Re_rec, H.

- exists x.
clear H.
transitivity ((Î» (Re) # 0) (Succ (enc n)) (tenc s)).
crush.
rewrite Succ_correct, Eta; value; crush.

- decide (t = s).

+ exists #0.
eapply Eq_correct in e. simpl. crush.
+ exists x.
eapply Eq_correct in n0.
transitivity ((Î» (Re) # 0) (Succ (enc n)) (tenc s)).
crush.
rewrite Succ_correct, Eta; value; crush.

Qed.

Lemma Re_ge n m s : n >= m -> converges (Re (enc n) (tenc s)) -> converges (Re (enc m) (tenc s)).

Proof.

induction 1; eauto using Re_S.

Qed.

Lemma Re_converges n s : converges (Re (enc n) (tenc s)) -> exists n, f (enc n) == oenc (Some s).

Proof.

intros [v H].

eapply equiv_lambda, star_pow in H.
destruct H as [m H].
revert n H.

eapply complete_induction with (x := m).
clear m; intros m IHm n H.
destruct (total_f n) as [Ht | [t Ht]].

- assert (A : exists k, pow step (S k) (Re (enc n) (tenc s)) (Re (enc (S n)) (tenc s))). {

eapply powSk.
reduce.
simpl.
transitivity ((f (enc n)) (lam ( (lam(Eq #0)) #0 (tenc s) I (lam(lam ( (lam(Re #0)) (Succ (enc n)) (tenc s)))) I))
(lam ((lam(Re #0)) (Succ (enc n)) (tenc s))) I).

repeat reduction'.

eapply star_trans.
do 3 eapply star_trans_l. eapply equiv_lambda. eassumption. crush.
}
destruct A as [k A].

destruct (pow_trans_lam H A) as [l [l_lt_m B]].

eapply (IHm l); eassumption.

- decide (t = s) as [E | E].

+ subst; exists n; crush.

+ assert (A : exists k, pow step (S k) (Re (enc n) (tenc s)) (Re (enc (S n)) (tenc s))). {

eapply powSk.
reduce.
simpl.
transitivity ((f (enc n)) (lam ( (lam(Eq #0)) #0 (tenc s) I (lam(lam ( (lam(Re #0)) (Succ (enc n)) (tenc s)))) I))
(lam ((lam(Re #0)) (Succ (enc n)) (tenc s))) I).

repeat reduction'.

eapply star_trans.
do 3 eapply star_trans_l. eapply equiv_lambda. crush.
simpl.
transitivity ( (lam (Eq #0)) (tenc t) (tenc s) I (lam(lam ( (lam(Re #0)) (Succ (enc n)) (tenc s)))) I I). crush.
assert (Eq (tenc t) (tenc s) >* false).
now eapply equiv_lambda, Eq_correct.
transitivity (Eq (tenc t) (tenc s) I (Î» (Î» (Î» Re # 0) (Succ (enc n)) (tenc s))) I I).
crush.
eapply star_trans.
do 4 eapply star_trans_l. eassumption.
crush.

}
destruct A as [k A].

destruct (pow_trans_lam H A) as [l [l_lt_m B]].

eapply (IHm l); eassumption.

Qed.

End Fix_f.

# Recursive Enumerability implies semi decidability

Lemma RE_Acc P : RE P -> lacc P.

Proof.

intros [f [f_cls [f_total f_enum]]].

pose (u := (lam (Re f (enc 0) #0))).

exists u.

split; value.
intros t.
assert (Hu : u (tenc t) == Re f (enc 0) (tenc t)).
unfold u; crush.
split.

- intros H.

eapply f_enum in H.
destruct H as [n H].
assert (converges (Re f (enc n) (tenc t))).
exists #0.
assert (E : Eq (tenc t) (tenc t) == true) by (eapply Eq_correct; reflexivity).

rewrite Re_rec, H.
simpl. crush. firstorder.
unfold pi.

rewrite Hu.
eapply Re_ge. value. firstorder. omega. eassumption.
- intros.
unfold pi in H. rewrite Hu in H.
assert (A : forall n, f (enc n) == none \/ exists s, f (enc n) == some (tenc s)) by firstorder.

destruct (Re_converges f_cls A H) as [n B].
destruct (f_total n) as [C | C].
+ rewrite B in C.
simpl in C. eapply eq_lam in C. inv C.
+ destruct C as [t' C].
assert (t = t'). destruct C as [C1 C2]. rewrite C1 in B.
eapply eqTrans with (s := oenc (Some t')) in B.
simpl in B.
eapply eq_lam in B.
inv B. now eapply tenc_injective.
symmetry; clear B; crush.

subst.
firstorder.
Qed.

# Semi decidability implies recursive enumerability

Require Import bijection EnumInt Enum Seval.

Lemma pi_eval u s : pi u s -> exists v, eval (u (tenc s)) v.

Proof.

intros [v H].
exists (lam v).
split.
now eapply equiv_lambda. value.
Qed.

Theorem Acc_RE P : lacc P -> RE P.

Proof.

intros [u [proc_u Hu]].
unfold RE.

exists (lam (Cn #0 (lam(lam(Eva #1 (App (tenc u) (Q (U #0))) (lam(some (U #1))) none))))).

repeat split; value.

- intros n.

destruct (c n) as [n1 n2] eqn:Hc.
destruct (eva n1 (u (tenc (g_inv n2)))) eqn:He.
+ right.
exists (g_inv n2). split.
* transitivity (Cn (enc n) (Î» (Î» (Eva #1) ((App (tenc u)) (Q (U #0))) (lam(some (U #1))) none))).
crush.
rewrite Cn_correct, Hc.
unfold penc, fst, snd.
transitivity (Eva (enc n1) (App (tenc u) (Q (U (enc n2)))) (lam(some (U (enc n2)))) none).
crush.
rewrite !U_correct at 1.
rewrite Q_correct, App_correct, Eva_correct, He.
assert (U := U_correct n2).
crush.
* rewrite Hu.
destruct (seval_eval (eva_seval He)) as [H [v Hv]]. exists v. subst. now eapply star_equiv.
+ left.

transitivity (Cn (enc n) (Î» (Î» (Eva #1) ((App (tenc u)) (Q (U #0))) (lam(some (U #1))) none))).
crush.
rewrite Cn_correct, Hc.
unfold penc, fst, snd.
transitivity (Eva (enc n1) (App (tenc u) (Q (U (enc n2)))) (lam(some (U (enc n2)))) none).
crush.
rewrite U_correct at 1.
rewrite Q_correct, App_correct, Eva_correct, He. crush.
- intros s H.

rewrite Hu in H.

destruct (pi_eval H) as [v H'].
clear H. destruct (eval_seval H') as [n H].
eapply seval_eva in H.

assert (C : exists m, c m = (n, g s)) by firstorder using c_surj.

destruct C as [m C].

exists m.

transitivity (Cn (enc m) (Î» (Î» (Eva #1) ((App (tenc u)) (Q (U #0))) (lam(some (U #1))) none))).
crush.
rewrite Cn_correct, C.
unfold penc, fst, snd.
transitivity (Eva (enc n) (App (tenc u) (Q (U (enc (g s))))) (lam(some (U (enc (g s))))) none).
crush.
rewrite U_correct at 1.
rewrite Q_correct, App_correct, Eva_correct, g_inv_g, H.
transitivity (some (U (enc (g s)))).
crush.
rewrite U_correct, g_inv_g.
crush.
Qed.