Library Scott
Require Export Fixpoints Decidability Proc Seval.
Theorem Scott (M : term -> Prop) : M <=1 closed ->
(forall s t, M s -> closed t -> t == s -> M t) ->
(exists t1, closed t1 /\ M t1) -> (exists t2, closed t2 /\ ~ M t2) ->
~ ldec M.
Proof.
intros M_cl M_equiv [s1 [cls_s1 Ms1]] [s2 [cls_s2 nMs2]] [u [[cls_u lam_u] Hu]].
pose (x := lam(u #0 (lam s2) (lam s1) I)).
destruct (SecondFixedPoint (s := x)) as [t [cls_t H]]; value.
eapply eqTrans with (s := u (tenc t) (lam s2) (lam s1) I) in H.
destruct (Hu t) as [ [Mt Ht] | [nMt Ht ]].
- eapply nMs2, M_equiv; eauto.
rewrite <- H, Ht. symmetry. crush.
- eapply nMt,M_equiv; eauto.
rewrite <- H, Ht; crush.
- symmetry. unfold x. crush.
Qed.
Goal ~ ldec (fun x => closed x /\ converges x).
Proof.
eapply Scott.
- tauto.
- intros s t [cls_s [x Hx]] cls_t t_e_s; split.
+ eassumption.
+ exists x. rewrite t_e_s. rewrite Hx. reflexivity.
- exists I. repeat split. exists #0. reflexivity.
- exists Omega. repeat split. intros [_ [x Hx]]. eapply Omega_diverges. eassumption.
Qed.
Lemma I_neq_Omega : ~ I == Omega.
Proof.
intros H. eapply Omega_diverges. rewrite <- H. unfold I. cbv; reflexivity.
Qed.
Lemma C27 : forall t, closed t -> ~ ldec (fun x => closed x /\ x == t).
Proof.
intros t cls_t H. cut (ldec (fun x : term => closed x /\ x == t)).
eapply Scott.
- tauto.
- intros s t0 [cls_s H0] cls_t0 H1. split. assumption. rewrite H1. assumption.
- exists t. repeat split. assumption. assumption. reflexivity.
- destruct H. destruct H. destruct (H0 I). exists Omega.
split. intros k r. simpl. reflexivity. intros [_ H2]. eapply I_neq_Omega.
rewrite H2. tauto.
exists I. split. intros k r. simpl. reflexivity. tauto.
- eassumption.
Qed.
Lemma C27_proc : forall t, proc t -> ~ ldec (fun x => x == t).
Proof.
intros t proc_t H. eapply C27; eauto using ldec_conj, ldec_closed; value.
Qed.
Lemma Eq_ldec : ~ ldec (fun x => exists (s t : term), x = tenc(s t) /\ s == t).
Proof.
intros [u [[cls_u lam_u] Hu]].
pose (t := I).
eapply (C27_proc (t := t)). value.
pose (v := (lam(u (Q (App #0 (tenc t)))))).
exists v. split; value.
intros s. destruct (Hu (tenc (s t))) as [ [[s' [t' [B Hst]]] H] | [H1 H2]].
- left. repeat split.
+ eapply tenc_injective in B. inv B. rewrite H2. eassumption.
+ unfold v. transitivity (u (Q ((App (tenc s)) (tenc t)))). crush.
rewrite App_correct, Q_correct. eassumption.
- right. repeat split.
+ intros H. eapply H1. exists s, t. tauto.
+ transitivity (u (Q ((App (tenc s)) (tenc t)))). unfold v. crush.
rewrite App_correct, Q_correct. eassumption.
Qed.