Definition decides u p := forall s, (p s /\ u (tenc s) ▷ T) \/ (~ p s /\ u (tenc s) ▷ F).
Definition decidable p :=
exists u, proc u /\ decides u p.
Lemma decidable_spec u p : decides u p -> forall s, (p s <-> u (tenc s) ▷ T) /\ (~ p s <-> u (tenc s) ▷ F).
Proof.
intros; split; destruct (H s); firstorder;
rewrite H1 in H2; destruct T_equiv_F; now rewrite H2.
Qed.
Definition pi s t := eva (s (tenc t)).
Definition recognisable p :=
exists u, proc u /\ forall s, p s <-> eva (u (tenc s)).
(* * Complement, intersection and union of predicates *)
Definition complement p := fun t => ~ p t.
Definition intersection p q := fun t => p t /\ q t.
Definition union p q := fun t => p t \/ q t.
Definition tcompl (u : term) : term := .\"x"; (!u "x") !F !T.
Definition tintersection u v : term := .\"x"; (!u "x") (!v "x") !F.
Definition tunion u v : term := .\"x"; (!u "x") !T (!v "x").
Lemma decidable_intersection p q : decidable p -> decidable q -> decidable (intersection p q).
Proof.
intros [u [[cls_u lam_u] decp]] [v [[cls_v lam_v] decq]].
exists (tintersection u v). split; unfold tintersection; value.
intros s. destruct (decp s) as [[ps Hu ] | [nps Hu]], (decq s) as [[Qs Hv] | [nQs Hv]]; [left| right..]; firstorder; solvered.
Qed.
Lemma decidable_union p q : decidable p -> decidable q -> decidable (union p q).
Proof.
intros [u [[cls_u lam_u] Hu]] [v [[cls_v lam_v] Hv]].
exists (tunion u v). split; unfold tunion; value.
intros s. destruct (Hu s) as [[A B] | [A B]], (Hv s) as [[C D] | [C D]]; [left .. | right]; firstorder; solvered.
Qed.
Lemma decidable_complement p : decidable p -> decidable (complement p).
Proof.
intros [u [[cls_u lam_u] H]].
exists (tcompl u). split; unfold tcompl; value.
intros s. destruct (H s) as [[ps A] | [nps A]]; [right | left]; intuition; solveeq.
Qed.
Lemma undecidable_russell : ~ decidable (fun s => ~ s (tenc s) ▷ T).
Proof.
intros (u & proc_u & Hu).
destruct (Hu u) as [ | [] ].
- firstorder.
- eapply T_equiv_F. rewrite <- H0. exfalso. eapply H. intros H1.
eapply T_equiv_F. now rewrite <- H0, <- H1.
Qed.
Definition recinter u v := lambda ((lambda (v 1)) (u 0) ).
Hint Unfold recinter : cbv.
Lemma recinter_correct u v s : closed u -> closed v -> eva (recinter u v (tenc s)) <-> eva ( u (tenc s)) /\ eva (v (tenc s)).
Proof.
intros cls_u cls_q.
split.
- intros [x [Hx lx] % evaluates_equiv].
assert (H : eva ((lambda (v (tenc s))) (u (tenc s)))). exists x; eapply evaluates_equiv;split;auto. symmetry. symmetry in Hx. solvered.
destruct (app_eva H) as [_ [y [Hy ly] % evaluates_equiv]]. split.
+ eexists; eapply evaluates_equiv; split;eassumption.
+ exists x; eapply evaluates_equiv; split;auto. rewrite <- Hx. symmetry. clear Hx. solvered.
- intros [[x [Hx ?] % evaluates_equiv] [y [Hy ?] % evaluates_equiv]]. exists y. eapply evaluates_equiv.
split. solvered. value.
Qed.
Lemma recognisable_intersection p q : recognisable p -> recognisable q -> recognisable (intersection p q).
Proof.
intros [u1 [[? ?] Hu1]] [u2 [[? ?] Hu2]].
exists (recinter u1 u2). split. unfold recinter. value.
intros; rewrite recinter_correct; firstorder.
Qed.
Lemma dec_recognisable p : decidable p -> recognisable p.
Proof.
intros [u [[cls_u lam_u] dec_u_p]].
exists (lambda (u 0 I (lambda Omega) I)); split; value.
+ intros t. specialize (dec_u_p t).
split; intros H; destruct dec_u_p; try tauto.
* destruct H0 as [_ u_T]. eexists; eapply evaluates_equiv; split;[|eexists;reflexivity]. solvered.
* destruct H. destruct H0.
assert ((lambda ((((u 0) I) (lambda Omega)) I)) (tenc t) ≡ Omega). clear H. solveeq.
rewrite H2 in H. destruct (eva_Omega). eexists; eauto.
Qed.
Lemma dec_rec p : decidable p -> recognisable p /\ recognisable (complement p).
Proof.
intros decp; split.
- eapply (dec_recognisable decp).
- eapply decidable_complement in decp. eapply (dec_recognisable decp).
Qed.
Theorem SecondFixedPoint (s : term) : closed s -> exists t, closed t /\ s (tenc t) ≡ t.
Proof.
intros cls_s.
pose (C := (.\ "x"; !s (!App "x" (!Q "x"))) : term). cbn in C.
pose (t := C (tenc C)).
exists t. split; [subst t C; value|].
symmetry. unfold t, C.
transitivity (s (App (tenc C) (Q (tenc C)))). solvered.
rewrite Q_correct, App_correct. reflexivity.
Qed.
Theorem Scott p :
(forall s t, closed s -> p s -> closed t -> t ≡ s -> p t) ->
(exists t1, closed t1 /\ p t1) -> (exists t2, closed t2 /\ ~ p t2) ->
~ decidable p.
Proof.
intros p_equiv [s1 [cls_s1 ps1]] [s2 [cls_s2 nps2]] [u [[cls_u lam_u] Hu]].
pose (x := lambda(u 0 (lambda s2) (lambda s1) I)).
destruct (SecondFixedPoint (s := x)) as [t [cls_t H]]; subst x; value.
eapply eqTrans with (s := u (tenc t) (lambda s2) (lambda s1) I) in H.
destruct (Hu t) as [ [pt Ht] | [npt Ht ]].
- eapply nps2, p_equiv; eauto.
rewrite <- H, Ht. symmetry. solvered.
- eapply npt,p_equiv with (s := s1); eauto.
rewrite <- H, Ht; solvered.
-symmetry. now dobeta.
Qed.
Lemma eva_dec : ~ decidable eva.
Proof.
eapply Scott.
- intros s t cls_s [x [Hx lx] % evaluates_equiv] cls_t t_e_s.
exists x; eapply evaluates_equiv; split;[|value]. now rewrite t_e_s.
- exists I. repeat split. exists I; eapply evaluates_equiv;split. reflexivity. value.
- exists Omega. repeat split. eapply eva_Omega.
Qed.
Lemma equiv_spec_decidable : forall t, closed t -> ~ decidable (fun x => x ≡ t).
Proof.
intros t cls_t H.
eapply Scott; try eassumption; cbn.
- intros s t0 cls_s H0 cls_t0 H1. rewrite H1. assumption.
- exists t. repeat split. value. reflexivity.
- destruct H as (? & ? & ?). destruct (H0 I) as [ [? ?] | [ ? ?] ]. exists Omega.
split. value. intros H3. eapply I_neq_Omega.
rewrite H1, H3. reflexivity.
exists I. split. value. eassumption.
Qed.