Library RE
Require Export Pairs Acceptability.
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).
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.
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.
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.