Library Scott

Require Export Fixpoints Decidability Proc Seval.

Scott's Theorem

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.

Applications of Scott's Theorem

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.