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

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.
  destruct m.
  - solveeq.
  - revert m; induction n; intros m.
    + solveeq.
    + 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.
  transitivity (Leb (Succ (enc n)) (enc k)). solveeq.
  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.
  revert k; induction s; intros k.
  - transitivity (Lt (enc n) (enc k)). solveeq. rewrite Lt_correct. unfold bound.
    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.
    rewrite IHs1, IHs2. cbn.
    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.
  exists (lambda (Closed 0)). split; value.
  intros s.
  assert ((lambda (Closed 0)) (tenc s) ≡ benc (bound 0 s)).
  transitivity (Bound (enc 0) (tenc s)). solveeq. now rewrite Bound_correct.
  rewrite H.

  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.
  destruct s.
  + right. split. solveeq. intros [x H]; inv H.
  + right. split. solveeq. intros [x H]; inv H.
  + left. split. solveeq. value.
Qed.

Lemma decidable_lam : decidable lam.
Proof.
  exists Lambda. split; value. intros s.
  assert (H := Lambda_correct s). firstorder.
Qed.

Lemma decidable_proc : decidable proc.
Proof.
  eapply decidable_intersection.
  - eapply decidable_closed.
  - eapply decidable_lam.
Qed.

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.
  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.
  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).
  assert (recognisable closed) as (C & proc_C & HC). {
    eapply dec_recognisable. eapply decidable_closed. }
  pose (w := lambda (F (C 0) (u (v 0)))).
  eapply unrecognisable_russell. exists w; split; value. intros s.

  assert (w (tenc s) ≡ F (C (tenc s)) (u (tenc (f s)))). {
    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.

Lemma D_pi u : pi D u <-> False.
Proof.
  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.
      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.
      * 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.
  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.
  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.
  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.
  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.
  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.
  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.