From Undecidability.L Require Import Tactics Encodings DecidableRecognisable.
Implicit Type p : term -> Prop.
Implicit Types s t u : term.

(** * Reduction lemma and Rice’s theorem *)

(** ** Closedness is decidable *)

Definition Leb := Eval cbn in
      rho (.\ "leb", "m", "n"; "m" !T (.\ "m'"; "n" !F (.\ "n'"; "leb" "m'" "n'"))).

Hint Unfold Leb: cbv.

Lemma Leb_correct m n : Leb (enc m) (enc n) ≡ benc (leb m n).
Proof.
(* Goal: equiv (app (app Leb (enc (S m))) (enc (S n))) (benc (Nat.leb (S m) (S n))) *)
  destruct m.
  - solveeq.
  - revert m; induction n; intros m.
(* Goal: evaluates (app (lambda I) (tenc H)) I *)
    + solveeq.
(* Goal: equiv (app (app Leb (enc (S m))) (enc (S n))) (benc (Nat.leb (S m) (S n))) *)
    + destruct m. solveeq. specialize (IHn m). solveeq.
Qed.

Hint Rewrite Leb_correct : Lcorrect.

Definition Lt : term := .\ "m", "n"; !Leb (!Succ "m") "n".

Lemma Lt_correct n k : Lt (enc n) (enc k) ≡ benc (Nat.ltb n k).
Proof.
  unfold Nat.ltb. rewrite <- Leb_correct.
(* Goal: evaluates (app (lambda I) (tenc H)) I *)
  transitivity (Leb (Succ (enc n)) (enc k)). solveeq.
(* Goal: equiv (app (app Leb (app Succ (enc n))) (enc k)) (app (app Leb (enc (S n))) (enc k)) *)
  now rewrite Succ_correct.
Qed.

Definition Bound := Eval cbn in
      rho (.\ "d", "k", "t";
           "t" (.\ "n"; !Lt "n" "k")
               (.\ "s", "t"; ("d" "k" "s") ("d" "k" "t") !F)
               (.\ "s"; "d" (!Succ "k") "s")).

Lemma Bound_correct k s : Bound (enc k) (tenc s) ≡ benc (bound k s).
Proof.
(* Goal: equiv (app (app Bound (enc k)) (tenc s)) (benc (bound k s)) *)
  revert k; induction s; intros k.
  - transitivity (Lt (enc n) (enc k)). solveeq. rewrite Lt_correct. unfold bound.
(* Goal: equiv (benc (Nat.ltb n k)) (benc (if @decision (lt n k) (nat_le_dec (S n) k) then true else false)) *)
    destruct (Nat.ltb_spec0 n k); decide (n < k); try now omega. reflexivity. reflexivity.
  - transitivity ((Bound (enc k) (tenc s1)) (Bound (enc k) (tenc s2)) F). solveeq.
(* Goal: equiv (app (app (app (app Bound (enc k)) (tenc s1)) (app (app Bound (enc k)) (tenc s2))) F) (benc (bound k (app s1 s2))) *)
    rewrite IHs1, IHs2. cbn.
(* Goal: evaluates (app (lambda I) (tenc H)) I *)
    destruct (bound _ s1), (bound _ s2); solveeq.
  - transitivity (Bound (Succ (enc k)) (tenc s)). solveeq. now rewrite Succ_correct, IHs.
Qed.

Definition Closed := Bound (enc 0).

Lemma decidable_closed : decidable closed.
Proof.
(* Goal: decidable closed *)
  exists (lambda (Closed 0)). split; value.
(* Goal: forall s : term, iff (and (closed s) (not (eva (app s (tenc s))))) (eva (app w (tenc s))) *)
  intros s.
(* Goal: or (and (closed s) (evaluates (app (lambda (app Closed (var O))) (tenc s)) T)) (and (not (closed s)) (evaluates (app (lambda (app Closed (var O))) (tenc s)) F)) *)
  assert ((lambda (Closed 0)) (tenc s) ≡ benc (bound 0 s)). 
(* Goal: evaluates (app (lambda I) (tenc H)) I *)
  transitivity (Bound (enc 0) (tenc s)). solveeq. now rewrite Bound_correct.
(* Goal: or (and (closed s) (evaluates (app (lambda (app Closed (var O))) (tenc s)) T)) (and (not (closed s)) (evaluates (app (lambda (app Closed (var O))) (tenc s)) F)) *)
  rewrite H.
  
(* Goal: or (and (closed s) (evaluates (benc (bound O s)) T)) (and (not (closed s)) (evaluates (benc (bound O s)) F)) *)
  destruct (bound 0 s) eqn:E.
  - firstorder econstructor.
  - right. split. intros C. congruence. econstructor.
Qed.

Definition Lambda := lambda (0 (lambda F) (lambda (lambda F)) (lambda T)).

Hint Unfold Lambda : cbv.

Lemma Lambda_correct s : Lambda (tenc s) ▷ T /\ lam s \/
                         Lambda (tenc s) ▷ F /\ ~ lam s.
Proof.
(* Goal: or (and (evaluates (app Lambda (tenc s)) T) (lam s)) (and (evaluates (app Lambda (tenc s)) F) (not (lam s))) *)
  destruct s.
(* Goal: evaluates (app (lambda I) (tenc H)) I *)
  + right. split. solveeq. intros [x H]; inv H.
(* Goal: evaluates (app (lambda I) (tenc H)) I *)
  + right. split. solveeq. intros [x H]; inv H.
(* Goal: evaluates (app (lambda I) (tenc H)) I *)
  + left. split. solveeq. value.
Qed.

Lemma decidable_lam : decidable lam.
Proof.
(* Goal: and (proc (lambda Omega)) (not (forall t : term, pi (lambda Omega) t)) *)
  exists Lambda. split; value. intros s.
(* Goal: or (and (lam s) (evaluates (app Lambda (tenc s)) T)) (and (not (lam s)) (evaluates (app Lambda (tenc s)) F)) *)
  assert (H := Lambda_correct s). firstorder.
Qed.

Lemma decidable_proc : decidable proc.
Proof.
(* Goal: decidable proc *)
  eapply decidable_intersection.
  - eapply decidable_closed.
  - eapply decidable_lam.
Qed.

(** ** Reduction lemma *)

Notation "s '≈' t" := (forall u v, t (tenc u) ▷ v <-> s (tenc u) ▷ v) (at level 50).

Lemma equiv_semantic s t : s ≡ t -> s ≈ t.
Proof.
(* Goal: or (and (closed s) (evaluates (app (lambda (app Closed (var O))) (tenc s)) T)) (and (not (closed s)) (evaluates (app (lambda (app Closed (var O))) (tenc s)) F)) *)
  intros H ? ?; now rewrite H.
Qed.

Definition closed_under_proc R p := forall s t , proc s -> proc t -> p s -> R s t -> p t.
Definition semantic p := closed_under_proc (fun s t => s ≈ t) p.

Lemma unrecognisable_russell : ~ recognisable (fun s => closed s /\ ~ eva (s (tenc s))).
Proof.
(* Goal: not (recognisable (fun s : term => and (closed s) (not (eva (app s (tenc s)))))) *)
  intros [u [[cls_u lam_u] H]]. specialize (H u). tauto.
Qed.

Lemma Reduction p f v :
  proc v ->
  (forall s, closed s -> p (f s) <-> ~ eva (s (tenc s))) ->
  (forall s, v (tenc s) ≡ tenc (f s)) ->
  ~ recognisable p.
Proof.
  intros proc_v  spec_f spec_v (u & proc_u & Hu).
(* Goal: False *)
  assert (recognisable closed) as (C & proc_C & HC). {
(* Goal: decidable closed *)
    eapply dec_recognisable. eapply decidable_closed. }
(* Goal: False *)
  pose (w := lambda (F (C 0) (u (v 0)))).
(* Goal: and (proc (lambda Omega)) (not (forall t : term, pi (lambda Omega) t)) *)
  eapply unrecognisable_russell. exists w; split; value. intros s.
  
(* Goal: equiv (app w (tenc s)) (app (app F (app C (tenc s))) (app u (tenc (f s)))) *)
(* Goal: iff (and (closed s) (not (eva (app s (tenc s))))) (eva (app w (tenc s))) *)
  assert (w (tenc s) ≡ F (C (tenc s)) (u (tenc (f s)))). {
(* Goal: evaluates (app (lambda I) (tenc H)) I *)
    transitivity (F (C (tenc s)) (u (v (tenc s)))). solveeq. now rewrite spec_v. }
   intuition; [ | rewrite H, F_eva, <- HC, <- Hu, spec_f in H0; tauto..].
  rewrite H, F_eva, <- HC, <- Hu, spec_f; eauto.
Qed.

(** ** Rice's lemma and Rice's theorem *)

Lemma D_pi u : pi D u <-> False.
Proof.
(* Goal: iff (pi D u) False *)
  unfold pi. firstorder using eva_D.
Qed.

Lemma Rice p N :
  semantic p ->
  proc N -> ~ p N ->
  p D ->
  ~ recognisable p.
Proof with eauto; try now intuition.
  intros p_sem proc_N pN pD [u [[cls_u lam_u] Hu]].
  pose (f := fun s => lambda (F (s (tenc s)) N 0)).
  pose (v := lambda (Lam (App (App (App (tenc F) (App 0 (Q 0))) (tenc N)) (tenc 0)))).

  eapply Reduction with (p := p) (f := f) (v := v).
  - value.    
  - intros. assert (Hf : forall t, f s (tenc t) ≡ F (s (tenc s)) N (tenc t)) by (intros; solvered).
    intuition.
    + eapply p_sem in H0; value. eapply pN, H0. intros t t'. rewrite Hf.
(* Goal: lam (lambda s) *)
      destruct H1 as (s' & [] % evaluates_equiv). rewrite H1, F_correct; value. tauto.
    + eapply p_sem with (s := D); value. eauto. intros t t'. rewrite Hf.
      intuition.
(* Goal: pi D I *)
      * destruct H0. eapply F_eva with (t := N). eapply app_eva with (t := tenc t). firstorder.
      * exfalso. eapply D_pi. exists t'. eassumption.
  - intros. transitivity (Lam ((App ((App ((App (tenc F)) ((App (tenc s)) (Q (tenc s))))) (tenc N))) (tenc 0))). solveeq.
    now rewrite Q_correct, !App_correct, Lam_correct.
  - exists u. firstorder.
Qed.

Lemma Rice_pi p :
  closed_under_proc (fun s t => (forall u, pi s u <-> pi t u)) p ->
 (exists u, proc u /\ ~ p u) -> 
 p (lambda Omega) -> ~ recognisable p.
Proof with eauto; try now intuition.
(* Goal: forall t : term, pi s t *)
  intros. destruct H0 as [u [H0 H0']]. eapply Rice.
  - intros. hnf. intuition. eapply H. exact H2. eauto. eauto. split; intros (? & ?); exists x; firstorder.
  - eauto.
  - eauto.
  - firstorder.
Qed.

Lemma rec_total : ~ recognisable (fun s => ~forall t, pi s t).
Proof.
(* Goal: not (recognisable (fun s : term => and (proc s) (not (forall t : term, pi s t)))) *)
  eapply Rice_pi.
  - hnf; intuition. eapply H1. intros. rewrite H2. eauto.
  - exists (lambda I). repeat split; value. intros H. eapply H. intros t. exists I. solveeq.
  - intros A. eapply (D_pi I); eauto.  
Qed.

Lemma rec_total_cls : ~ recognisable (fun s => closed s /\ ~forall t, pi s t).
Proof.
(* Goal: not (recognisable (fun s : term => and (proc s) (not (forall t : term, pi s t)))) *)
  eapply Rice_pi.
  - hnf; intuition. eapply H4. intros. rewrite H2. eauto.
  - exists (lambda I). repeat split; value. intros H. eapply H. intros t. exists I. solveeq.
  - split; value. intros A. eapply (D_pi I); eauto.  
Qed.

Lemma rec_total_proc : ~ recognisable (fun s => proc s /\ ~forall t, pi s t).
Proof.
(* Goal: not (recognisable (fun s : term => and (proc s) (not (forall t : term, pi s t)))) *)
  eapply Rice_pi.
  - hnf; intuition. eapply H4. intros. rewrite H2. eauto.
  - exists (lambda I). repeat split; value. intros H. eapply H. intros t. exists I. solveeq. 
  - split; value. intros A. eapply (D_pi I); eauto.  
Qed.


Theorem Rice_Theorem p :
  closed_under_proc (fun s t => s ≈ t) p ->
 (exists u, proc u /\ ~ p u) -> (exists u, proc u /\ p u) ->
  ~ decidable p.
Proof.
(* Goal: forall t : term, pi s t *)
  intros. intros A. assert (B : decidable p) by eassumption. destruct A as [u [proc_u Hu]].
  destruct H0 as (? & ? & ?), H1 as (? & ? & ?).
  destruct (Hu D).
  - eapply Rice. exact H. exact H0. tauto. firstorder. eapply dec_recognisable. exists u; tauto.
  - eapply Rice with (p := complement p).
    + unfold complement. hnf. intuition. eapply H8.  eapply H; eauto. intuition; now eapply H9.
    + exact H1.
    + firstorder.
    + firstorder.
    + now eapply dec_recognisable, decidable_complement.
Qed.

Lemma dec_total : ~ decidable (fun s => proc s /\ forall t, pi s t).
Proof.
(* Goal: not (decidable (fun s : term => and (proc s) (forall t : term, pi s t))) *)
  eapply Rice_Theorem.
  - hnf; intuition. destruct (H4 t0). firstorder.
  - exists D. repeat split; value. intros A. eapply (D_pi I); eauto.  firstorder.
  - exists (lambda I). repeat split; value. intros H. exists I. solveeq. 
Qed.
