From Undecidability.L Require Import Encodings.

Implicit Types s t u v : term.
Implicit Types p q : term -> Prop.

(** * Decidable and recognisable classes *)
(** ** Definition of decidable classes *)

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 of recognisable classes *)

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.

(** ** Decidable classes are closed under union, intersection and complement *)

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. 
(* Goal: forall (_ : decidable p) (_ : decidable q), decidable (intersection p q) *)
  intros [u [[cls_u lam_u] decp]] [v [[cls_v lam_v] decq]].
(* Goal: decidable (intersection p q) *)
  exists (tintersection u v). split; unfold tintersection; value.
(* Goal: decides (convert (blambda (String (Ascii.Ascii false false false true true true true false) EmptyString) (bapp (bapp (bapp (bter u) (bvar (String (Ascii.Ascii false false false true true true true false) EmptyString))) (bter F)) (bter T)))) (complement p) *)
  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. 
(* Goal: forall (_ : decidable p) (_ : decidable q), decidable (union p q) *)
  intros [u [[cls_u lam_u] Hu]] [v [[cls_v lam_v] Hv]].
(* Goal: decidable (union p q) *)
  exists (tunion u v). split; unfold tunion; value.
(* Goal: decides (convert (blambda (String (Ascii.Ascii false false false true true true true false) EmptyString) (bapp (bapp (bapp (bter u) (bvar (String (Ascii.Ascii false false false true true true true false) EmptyString))) (bter F)) (bter T)))) (complement p) *)
  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.
(* Goal: forall _ : decidable p, decidable (complement p) *)
  intros [u [[cls_u lam_u] H]].
(* Goal: decidable (complement p) *)
  exists (tcompl u). split; unfold tcompl; value.
(* Goal: decides (convert (blambda (String (Ascii.Ascii false false false true true true true false) EmptyString) (bapp (bapp (bapp (bter u) (bvar (String (Ascii.Ascii false false false true true true true false) EmptyString))) (bter F)) (bter T)))) (complement p) *)
  intros s. destruct (H s) as [[ps A] | [nps A]];  [right | left]; intuition; solveeq.
Qed.

(** ** There is an undecidable class *)

Lemma undecidable_russell : ~ decidable (fun s => ~ s (tenc s) ▷ T).
Proof.
(* Goal: not (decidable (fun s : term => not (evaluates (app s (tenc s)) T))) *)
  intros (u & proc_u & Hu).
(* Goal: False *)
  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.

(** ** Recognisable classes are closed under intersection *)

Definition recinter u v : term := .\"x"; !F (!u "x") (!v "x").
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.
(* Goal: forall (_ : closed u) (_ : closed v), iff (eva (app (recinter u v) (tenc s))) (and (eva (app u (tenc s))) (eva (app v (tenc s)))) *)
  intros cls_u cls_q.
(* Goal: and (closed I) (not (equiv I t)) *)
  split.
  - intros H.
(* Goal: and (eva (app u (tenc s))) (eva (app v (tenc s))) *)
    assert (recinter u v (tenc s) ≡ F (u (tenc s)) (v (tenc s))) by solvered. rewrite H0 in H.
(* Goal: and (eva (app u (tenc s))) (eva (app v (tenc s))) *)
    now eapply app_eva in H as [[] % app_eva ].
  - intros [[x [Hx ?] % evaluates_equiv] [y [Hy ?] % evaluates_equiv]]. exists y. eapply evaluates_equiv.
(* Goal: and (closed I) (not (equiv I t)) *)
    split. solvered. value.
Qed.

Lemma recognisable_intersection p q : recognisable p -> recognisable q -> recognisable (intersection p q).
Proof.
(* Goal: forall (_ : recognisable p) (_ : recognisable q), recognisable (intersection p q) *)
  intros [u1 [[? ?] Hu1]] [u2 [[? ?] Hu2]].
(* Goal: and (closed I) (not (equiv I t)) *)
  exists (recinter u1 u2). split. unfold recinter. value.
(* Goal: False *)
  intros; rewrite recinter_correct; firstorder.
Qed.

(** ** Decidable classes are recognisable and coregnisable *)

Lemma dec_recognisable p : decidable p -> recognisable p.
Proof.
  intros [u [[cls_u lam_u] dec_u_p]].
(* Goal: closed I *)
(* Goal: not (equiv I t) *)
  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. 
(* Goal: equiv (app (app (app T (lambda s2)) (lambda s1)) I) s2 *)
      * 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.
(* Goal: and (closed I) (not (equiv I t)) *)
  intros decp; split.
  - eapply (dec_recognisable decp).
  - eapply decidable_complement in decp. eapply (dec_recognisable decp).
Qed.

(** ** Scott's theorem *)

Theorem SecondFixedPoint (s : term) : closed s -> exists t, closed t /\ s (tenc t) ≡ t.
Proof.
(* Goal: forall _ : closed s, @ex term (fun t : term => and (closed t) (equiv (app s (tenc t)) t)) *)
  intros cls_s.
(* Goal: @ex term (fun t : term => and (closed t) (equiv (app s (tenc t)) t)) *)
  pose (C := (.\ "x"; !s (!App "x" (!Q "x"))) : term). cbn in C.
(* Goal: @ex term (fun t : term => and (closed t) (equiv (app s (tenc t)) t)) *)
  pose (t := C (tenc C)).
(* Goal: @ex term (fun t1 : term => and (closed t1) (equiv t1 t)) *)
  exists t. split; [subst t C; value|].
(* Goal: equiv (app (app (app (app u (tenc t)) (lambda s2)) (lambda s1)) I) (app (lambda (app (app (app (app u (var O)) (lambda s2)) (lambda s1)) I)) (tenc t)) *)
  symmetry. unfold t, C.
(* Goal: equiv (app (app (app T (lambda s2)) (lambda s1)) I) s2 *)
  transitivity (s (App (tenc C) (Q (tenc C)))). solvered.
(* Goal: equiv (app s (app (app App (tenc C)) (app Q (tenc C)))) (app s (tenc (app (lambda (app s (app (app (lambda (lambda (lambda (lambda (lambda (app (app (var (S O)) (var (S (S (S (S O)))))) (var (S (S (S O)))))))))) (var O)) (app Q (var O))))) (tenc (lambda (app s (app (app (lambda (lambda (lambda (lambda (lambda (app (app (var (S O)) (var (S (S (S (S O)))))) (var (S (S (S O)))))))))) (var O)) (app Q (var O))))))))) *)
  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.
(* Goal: forall (_ : forall (s t : term) (_ : closed s) (_ : p s) (_ : closed t) (_ : equiv t s), p t) (_ : @ex term (fun t1 : term => and (closed t1) (p t1))) (_ : @ex term (fun t2 : term => and (closed t2) (not (p t2)))), not (decidable p) *)
  intros p_equiv [s1 [cls_s1 ps1]] [s2 [cls_s2 nps2]] [u [[cls_u lam_u] Hu]].
(* Goal: False *)
  pose (x := lambda(u 0 (lambda s2) (lambda s1) I)).
(* Goal: closed I *)
(* Goal: not (equiv I t) *)
  destruct (SecondFixedPoint (s := x)) as [t [cls_t H]]; subst x; value.
(* Goal: False *)
  eapply eqTrans with (s := u (tenc t) (lambda s2) (lambda s1) I) in H.
(* Goal: False *)
(* Goal: equiv (app (app (app (app u (tenc t)) (lambda s2)) (lambda s1)) I) (app (lambda (app (app (app (app u (var O)) (lambda s2)) (lambda s1)) I)) (tenc t)) *)
  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.
(* Goal: not (decidable eva) *)
  eapply Scott.
  - intros s t cls_s [x [Hx lx] % evaluates_equiv] cls_t t_e_s.
(* Goal: eva t *)
    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. 
(* Goal: forall (t : term) (_ : closed t), not (decidable (fun x : term => equiv x t)) *)
  intros t cls_t H.
(* Goal: False *)
  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.
(* Goal: and (closed I) (not (equiv I t)) *)
    split. value. intros H3. eapply I_neq_Omega.
(* Goal: equiv t t *)
(* Goal: @ex term (fun t2 : term => and (closed t2) (not (equiv t2 t))) *)
    rewrite H1, H3. reflexivity.
(* Goal: and (closed I) (not (equiv I t)) *)
    exists I. split. value. eassumption.
Qed.
    
