From Undecidability.L Require Import DecidableRecognisable InterpreterResults.

Implicit Types s t : term.

Definition enumerable p := exists u, proc u /\ (forall n, u(enc n) ≡ none \/ exists s, u (enc n) ≡ oenc (Some s) /\ p s) /\ forall s, p s -> exists n, u (enc n) ≡ oenc (Some s).

Definition Eq := rho (.\ "Eq", "s", "t"; "s" (.\"n"; "t" (.\"m"; !EqN "n" "m") !(lambda (lambda F)) !(lambda F))
                                           (.\"s1", "s2"; "t" !(lambda F) (.\"t1","t2"; ("Eq" "s1" "t1") ("Eq" "s2" "t2") !F) !(lambda F))
                                           (.\"s1"; "t" !(lambda F) !(lambda (lambda F)) (.\"t1"; "Eq" "s1" "t1")) ).
Hint Unfold Eq : cbv.

Definition term_eq_bool s t := if decision (s = t) then true else false.

Lemma Eq_correct' s t :
  Eq (tenc s) (tenc t) ≡ benc (term_eq_bool s t).
Proof with try solveeq.
  revert t; induction s; intros.
  + destruct t; [ | solveeq..].
    transitivity (EqN (enc n) (enc n0)). solveeq. rewrite EqN_correct.
    unfold term_eq_bool. destruct _. inv e.
    now rewrite <- beq_nat_refl. assert (n <> n0) by firstorder congruence.
    rewrite <- Nat.eqb_neq in H. now rewrite H.
  + destruct t; [ solveeq | | solveeq].
    transitivity ((Eq (tenc s1) (tenc t1)) (Eq (tenc s2) (tenc t2)) F). solveeq.
    rewrite IHs1, IHs2.
    unfold term_eq_bool. destruct *; try congruence; solveeq.
  + destruct t; [ solveeq.. | ].
    transitivity (Eq (tenc s) (tenc t)). solveeq.
    rewrite IHs.
    unfold term_eq_bool. destruct *; try congruence; solveeq.
Qed.

Lemma Eq_correct s t :
      (s = t -> Eq (tenc s) (tenc t) ≡ T )
  /\ ( s <> t -> Eq (tenc s) (tenc t) ≡ F ).
Proof.
  intuition; rewrite Eq_correct';
  unfold term_eq_bool; destruct _; now try congruence.
Qed.

Section Fix_f.

  Variable u : term.
  Hypothesis proc_u : proc u.
  Hypothesis total_u : forall n, u (enc n) ≡ none \/ exists s, u (enc n) ≡ oenc (Some s).

  Definition Re : term := Eval cbv in
        .\ "s"; !C (.\ "n"; !u "n" (.\ "t"; !Eq "s" "t") !F).

  Lemma Re_proc :
    proc Re.
  Proof.
    value.
  Qed.

  Lemma H_rec n s : ((lambda (((u 0) (lambda ((Eq (tenc s)) 0))) F)) (enc n) ≡ u (enc n) (lambda (Eq (tenc s) 0)) F).
  Proof.
    solveeq.
  Qed.

  Lemma H_proc s : proc (.\ "n"; !u "n" (.\ "t"; !Eq !(tenc s) "t") !F).
  Proof.
    value.
  Qed.

  Lemma H_test s : test (.\ "n"; !u "n" (.\ "t"; !Eq !(tenc s) "t") !F).
  Proof.
    intros n. cbn. rewrite H_rec.
    destruct (total_u n) as [ | [] ].
    + rewrite H. right. solveeq.
    + rewrite H, some_correct_r; value.
      assert (lambda (Eq (tenc s) 0) (tenc x) ≡ Eq (tenc s) (tenc x)) by solveeq.
      rewrite H0. decide (s = x).
      * eapply Eq_correct in e. rewrite e. left. econstructor.
      * eapply Eq_correct in n0. rewrite n0. right. econstructor.
  Qed.

  Lemma Re_sound s : eva (Re (tenc s)) -> exists n, u (enc n) ≡ oenc (Some s).
  Proof.
    intros.
    assert (Re (tenc s) ≡ C (lambda (u 0 (lambda (Eq (tenc s) 0)) F))) by solveeq.
    rewrite H0 in H. eapply C_sound in H as [n H]; value.
    - exists n. unfold satis in H. destruct (total_u n) as [ | []].
      + cbn. rewrite H_rec, H1, none_correct in H; value. inv H.
      + rewrite H_rec, H1, some_correct_r in H; value.
        assert (lambda (Eq (tenc s) 0) (tenc x) ≡ Eq (tenc s) (tenc x)) by (clear; solveeq).
        rewrite H2 in H.
        decide (s = x).
        * now subst.
        * eapply Eq_correct in n0. rewrite n0 in H. inv H.
    - intros n. rewrite H_rec. destruct (total_u n) as [ | [] ].
      + rewrite H1. right. solveeq.
      + rewrite H1, some_correct_r; value.
        assert (lambda (Eq (tenc s) 0) (tenc x) ≡ Eq (tenc s) (tenc x)) by solveeq.
        rewrite H2. decide (s = x).
        * eapply Eq_correct in e. rewrite e. left. econstructor.
        * eapply Eq_correct in n0. rewrite n0. right. econstructor.
  Qed.

  Lemma Re_complete n s : u (enc n) ≡ oenc (Some s) -> eva (Re (tenc s)).
  Proof.
    intros. assert (Re (tenc s) ≡ C (lambda (u 0 (lambda (Eq (tenc s) 0)) F))) by solveeq.
    rewrite H0. edestruct (C_complete (n := n) (H_proc s) (H_test s)).
    - unfold satis. cbn. rewrite H_rec, H. eapply evaluates_equiv; split; value.
      transitivity (Eq (tenc s) (tenc s)). solveeq.
      edestruct (Eq_correct). now rewrite H1.
    - destruct H1; eauto.
  Qed.

End Fix_f.

Lemma enumerable_recognisable p : enumerable p -> recognisable p.
Proof.
  intros [v [f_cls [f_total f_enum]]].
  pose (u := (lambda (Re v 0))).
  assert (Hu : forall s, u (tenc s) ≡ Re v (tenc s)) by (intros; solveeq).
  exists u.
  split. value. intuition.
  - rewrite Hu. eapply f_enum in H as []. eapply Re_complete.
    + value.
    + firstorder.
    + eauto.
  - rewrite Hu in H. eapply Re_sound in H as [n H].
    destruct (f_total n).
    + rewrite H in H0. replace none with (oenc None) in H0. eapply oenc_inj in H0. inv H0.
      reflexivity.
    + destruct H0 as [? [? ?]]. rewrite H0 in H. eapply oenc_inj in H. inv H. eassumption.
    + value.
    + firstorder.
Qed.

Lemma R_enumerates (R : nat -> option term) (u : term) :
  proc u -> (forall s, exists n, R n = Some s) -> (forall n, u (enc n) ▷ oenc (R n)) ->
  enumerable (fun s => True).
Proof.
  intros Hp HR Hu. exists u. repeat split; eauto; value.
  - intros . destruct (R n) eqn:E.
    + right. exists t. rewrite Hu, E. eauto.
    + left. rewrite Hu, E. reflexivity.
  - intros. destruct (HR s) as [n H0].
    exists n. rewrite (Hu n), H0. eauto.
Qed.

Fixpoint L n :=
  match n with
  | 0 => [ ]
  | S n => L n ++ var n :: map_pro app (L n) (L n) ++ map lambda (L n)
  end.

Lemma length_L n : |L n| >= n.
Proof.
  induction n; cbn.
  - omega.
  - rewrite app_length. cbn. omega.
Qed.

Lemma L_exists n : exists s, nth n (L (S n)) = Some s.
Proof.
  edestruct nth_length with (A := L (S n)) (n := n).
  + eapply length_L.
  + eauto.
Qed.

Lemma L_cum m n : m <= n -> exists A, L n = L m ++ A.
Proof.
  induction 1.
  - exists []. now simpl_list.
  - cbn. destruct IHle as [A ->].
    rewrite <- app_assoc. eauto.
Qed.

Lemma nth_app_l X (x : X) n A B :
  nth n A = Some x -> nth n (A ++ B) = Some x.
Proof.
  revert n.
  induction A as [|y A IH]; cbn; intros k H.
  - destruct k; discriminate H.
  - destruct k as [|k]; cbn in *. exact H.
    apply IH, H.
Qed.

Lemma L_inv m n k s t :
  nth k (L m) = Some s -> nth k (L n) = Some t -> s = t.
Proof.
  intros H1 H2.
  assert (m <= n \/ n <= m) as [H3|H3] by omega.
  - destruct (L_cum H3) as [A ?]. rewrite H in *.
    eapply nth_app_l in H1. rewrite H1 in H2. now inv H2.
  - destruct (L_cum H3) as [A ?]. rewrite H in *.
    eapply nth_app_l in H2. rewrite H2 in H1. now inv H1.
Qed.

Definition R n := nth n (L (S n)).

Fixpoint beta s :=
  match s with
  | var n => S n
  | app s t => S (beta s + beta t)
  | lambda s => S (beta s)
  end.

Lemma L_el s m n : s el L m -> m <= n -> s el L n.
Proof.
  intros. induction H0.
  - eauto.
  - cbn. eauto.
Qed.

Lemma L_beta s : s el L (beta s).
Proof.
  induction s; cbn.
  - eauto.
  - rewrite !in_app_iff. cbn. rewrite in_app_iff.
    do 2 right. left. eapply map_pro_in. repeat eexists; eauto.
    + eapply L_el; eauto. omega.
    + eapply L_el; eauto. omega.
  - rewrite !in_app_iff. cbn. rewrite in_app_iff.
    do 3 right. eapply in_map_iff. eauto.
Qed.

Lemma R_surjective s : exists n, R n = Some s.
Proof.
  destruct (el_pos _ (L_beta s)) as [n ? % pos_nth].
  unfold R. exists n. destruct (L_exists n) as [? ?].
  rewrite H0. f_equal. eapply L_inv; eauto.
Qed.

Section Fix_X.

  Variable X : Type.
  Variable enc : X -> term.
  Hypothesis enc_proc : (forall x, proc (enc x)).

  Fixpoint lenc (A : list X) :=
    match A with
    | nil => lambda (lambda 1)
    | a::A => lambda(lambda (0 (enc a) (lenc A)))
    end.

  Definition Nil : term := .\ "n", "c"; "n".
  Definition Cons: term := .\ "a", "A", "n", "c"; "c" "a" "A".

  Lemma lenc_proc A : proc (lenc A).
  Proof.
    induction A; value.
  Qed.

  Hint Resolve lenc_proc : cbv.

  Lemma Cons_correct a A : Cons (enc a) (lenc A) ≡ lenc(a::A).
  Proof.
    solveeq.
  Qed.

  Definition Append := rho (.\ "app", "A", "B";
                            "A" "B" (.\"a", "A"; !Cons "a" ("app" "A" "B"))).

  Hint Unfold Append : cbv.

  Lemma Append_correct A B : Append (lenc A) (lenc B) ≡ lenc(A ++ B).
  Proof.
    induction A; solveeq.
  Qed.

  Definition sim (F : term) f := proc F /\ forall x, F (enc x) ≡ (enc (f x)).

  Definition Map := rho (.\ "map", "F", "A";
                         "A" !Nil (.\"a", "A"; !Cons ("F" "a") ("map" "F" "A"))).

  Hint Unfold sim Map : cbv.

  Lemma Map_correct f A F : sim F f ->
                            Map F (lenc A) ≡ lenc(map f A).
  Proof.
    intros [[? ?] ?].
    induction A.
    - solveeq.
    - specialize (H1 a). solveeq.
  Qed.

  Definition sim2 (F : term) f := proc F /\ forall x y, F (enc x) (enc y) ≡ (enc (f x y)).

  Definition Map_pro := rho (.\ "map_pro", "f", "A", "B";
                               "A" !Nil (.\"a", "A"; !Append ("map_pro" "f" "A" "B") (!Map (.\"y" ; "f" "a" "y") "B"))).

  Goal proc Map_pro.
  Proof.
    value.
  Qed.

  Hint Unfold sim2 Map_pro : cbv.

  Lemma Map_pro_correct f A B F : sim2 F f ->
                            Map_pro F (lenc A) (lenc B) ≡ lenc(map_pro f A B).
  Proof.
    intros [[? ?] ?].
    induction A.
    - solveeq.
    - transitivity (Append (Map_pro F (lenc A) (lenc B)) (Map (lambda (F (enc a) 0)) (lenc B))). solvered.
      rewrite IHA, Map_correct with (f := f a), Append_correct. reflexivity.
      split; value. intros. specialize (H1 a x). solveeq.
  Qed.

  Definition Nth := rho (.\ "nth", "n", "A";
                         "n" ("A" !none (.\ "a", "A"; !some "a"))
                             (.\"n"; ("A" !none (.\"a", "A"; "nth" "n" "A"))) ).

  Definition onatenc x := match x with None => none | Some x => (lambda(lambda(1 (enc x)))) end.

  Lemma Nth_correct A n : Nth (Encodings.enc n) (lenc A) ≡ onatenc(nth n A).
  Proof.
    revert A; induction n; intros A.
    - destruct A; solveeq.
    - destruct A.
      + solveeq.
      + cbn. rewrite <- IHn. solveeq.
  Qed.

End Fix_X.

Definition L_term := rho (.\ "L", "n";
                            "n" !Nil (.\ "n"; !Append ("L" "n") (!Cons (!Var "n") (!Append (!Map_pro !App ("L" "n") ("L" "n")) (!Map !Lam ("L" "n")))))).

Lemma L_term_correct n : L_term (enc n) ≡ lenc tenc (L n).
Proof.
  induction n.
  - solvered.
  - transitivity (Append (L_term (enc n)) (Cons (Var (enc n)) (Append (Map_pro App (L_term (enc n)) (L_term (enc n))) (Map Lam (L_term (enc n)))))). solvered.
    rewrite IHn, Map_correct with (f := lambda), Map_pro_correct with (f := app), Append_correct, Var_correct, Cons_correct, Append_correct;
      intros; value.
    + reflexivity.
    + split. value. exact App_correct.
    + split. value. exact Lam_correct.
Qed.

Definition OfNat : term := .\ "n" ; !Nth "n" (!L_term (!Succ ("n"))).

Lemma OfNat_correct n : OfNat (enc n) ≡ oenc (R n).
Proof.
  transitivity (Nth (enc n) (L_term (Succ (enc n)))). solveeq.
  rewrite Succ_correct, L_term_correct, Nth_correct. reflexivity.
  intros; value.
Qed.

Lemma enumerable_all : enumerable (fun s => True).
Proof.
  eapply R_enumerates with (u := OfNat).
  - value.
  - eapply R_surjective.
  - intros. rewrite OfNat_correct. eapply evaluates_equiv; split; now value.
Qed.

Theorem recognisable_enumerable p : recognisable p -> enumerable p.
Proof.
  destruct enumerable_all as (Enum & pE & TE & HE).
  intros [u [proc_u Hu]].

  pose (v := (.\ "n"; !Enum "n" (.\ "u"; "u" !(lambda none) (.\ "t", "s"; "t" (.\ "n"; !E "n" (!App !(tenc u) (!Q "s")) (.\ "_"; !some "s") !none) !(lambda (lambda none)) !(lambda none)) !(lambda none)) !none) : term).
  cbn -[none App Q some] in v.
  assert (Hv : forall n, v (enc n) ≡ Enum (enc n) (.\ "u"; "u" !(lambda none) (.\ "t", "s"; "t" (.\ "n"; !E "n" (!App !(tenc u) (!Q "s")) (.\ "_"; !some "s") !none) !(lambda (lambda none)) !(lambda none)) !(lambda none)) !none) by (intros; solvered).
  exists v.
  repeat split; value.
  - intros n. destruct (TE n) as [ | H]; try destruct H as ([ | t1 s | ] & H & _).
    + left. rewrite Hv, H. solveeq.
    + left. rewrite Hv, H. solveeq.
    + destruct t1 as [ m | |].
      * destruct (eval m (u (tenc s))) eqn:He.
        -- right. exists s. rewrite Hv, H, some_correct_r. split.
           transitivity (E (enc m) (App (tenc u) (Q (tenc s))) (lambda (some (tenc s))) none). solveeq.
           rewrite Q_correct, App_correct, E_correct, He. transitivity (some (tenc s)). solveeq.
           now rewrite some_correct.
           eapply Hu. eapply eval_evaluates in He. firstorder. value. now value.
        -- left. rewrite Hv, H, some_correct_r.
           transitivity (E (enc m) (App (tenc u) (Q (tenc s))) (lambda (some (tenc s))) none). solveeq.
           rewrite Q_correct, App_correct, E_correct, He. solveeq. value. now value.
      * left. rewrite Hv, H. solveeq.
      * left. rewrite Hv, H. solveeq.
    + left. rewrite Hv, H. solveeq.
  - intros s [s' [n H] % evaluates_eval] % Hu.
    destruct (HE (n s)). eauto. exists x.
    rewrite Hv, H0.
    transitivity (E (enc n) (App (tenc u) (Q (tenc s))) (lambda (some (tenc s))) none). solveeq.
    rewrite Q_correct, App_correct, E_correct, H. solveeq.
Qed.

Lemma recognisable_range_total f u : proc u -> (forall n, u (enc n) ▷ tenc (f n)) -> recognisable (fun t => exists n, f n = t).
Proof.
  intros. eapply enumerable_recognisable.
  exists (lambda (some (u 0))). repeat split; value.
  - intros n. right. exists (f n); split; eauto.
    specialize (H0 n). solveeq.
  - intros s [n]. exists n. specialize (H0 n). subst. solveeq.
Qed.