Require Import DecidableRecognisable InterpreterResults.

Implicit Types s t : term.

Enumerable classes

Definition of enumerable classes

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).

Enumerable classes are recognisable

Equality of encoded terms

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.

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

Search using Choose

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.

  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).

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

  Lemma H_test s : test (.\ "n"; !u "n" (.\ "t"; !Eq !(tenc s) "t") !F).
    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.

  Lemma Re_sound s : eva (Re (tenc s)) -> exists n, u (enc n) oenc (Some s).
    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.

  Lemma Re_complete n s : u (enc n) oenc (Some s) -> eva (Re (tenc s)).
    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.

End Fix_f.

Lemma enumerable_recognisable p : enumerable p -> recognisable p.
  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.
    + destruct H0 as [? [? ?]]. rewrite H0 in H. eapply oenc_inj in H. inv H. eassumption.
    + value.
    + firstorder.

Terms are countable

Notation "A '.[' i ']'" := (elAt A i) (no associativity, at level 50).

Fixpoint appCross A B :=
match A with
| nil => nil
| a :: A => appCross A B ++ map (app a) B

Fixpoint T_enum n :=
match n with
| 0 => [var n]
| S n => let A := T_enum n in A ++ [var (S n)] ++ map lambda A ++ appCross A A

Lemma sublist_T_enum : forall n : nat, exists (x : term) (B : list term), T_enum (S n) = T_enum n ++ x :: B.
  intros n. exists ( (S n)). simpl. eexists; reflexivity.

Lemma T_S s n m : T_enum n .[ m ] = Some s -> T_enum (S n).[ m ] = Some s.
  destruct (sublist_T_enum n) as [x [B H]]. rewrite H. eapply elAt_app.

Lemma T_ge s n1 n2 m : n2 >= n1 -> T_enum n1 .[ m ] = Some s -> T_enum n2 .[ m ] = Some s.
  remember (S n1) as n1'. induction 1; inv Heqn1'; eauto using T_S.

Lemma appCross_correct A B s t : (s el A /\ t el B) <-> (app s t) el appCross A B.
  - induction A; simpl; intuition; subst; eauto using in_map.
  - induction A; simpl; try rewrite in_app_iff in *; intros H; try tauto; destruct H as [H1 | H2]; intuition; rewrite in_map_iff in *; destruct H2; destruct H; [left|]; congruence.

Lemma T_var n : var n el T_enum n.
  destruct n; simpl; auto.

Lemma T_app s t n : s el T_enum n -> t el T_enum n -> s t el T_enum (S n).
  intros; simpl. decide (s t el T_enum n); auto; simpl.
  rewrite in_app_iff; simpl.
  rewrite in_app_iff, <- appCross_correct.

Lemma T_el_ge s n m : n >= m -> s el T_enum m -> s el T_enum n.
  intros A B; destruct (el_elAt B); eapply elAt_el, T_ge; eassumption.

Lemma T_lambda s n : s el T_enum n -> lambda s el T_enum (S n).
  intros; simpl; decide (lambda s el T_enum n); auto.
  rewrite in_app_iff; simpl; rewrite in_app_iff, in_map_iff.
  right. right. eauto.

Lemma T_exhaustive s : {n | s el (T_enum n) }.
Proof with
  simpl; repeat rewrite in_app_iff; repeat rewrite in_filter_iff; try rewrite <- appCross_correct; eauto using in_filter_iff, in_app_iff, appCross_correct, el_elAt, elAt_el, T_ge, in_map.
  induction s as [ | s1 [n1 IHs1] s2 [n2 IHs2] | s [n IHs] ].
  - exists n. destruct n; cbn; auto.
  - exists (S (S (n1 + n2))). eapply T_app; eapply T_el_ge; try eassumption; omega.
  - exists (S n). now eapply T_lambda.

Lemma T_longenough m : |T_enum m| > m.
  induction m.
  - simpl; omega.
  - simpl. rewrite app_length. simpl. omega.

Definition enum n := match elAt (T_enum n) n with None => 0 | Some n => n end.

Require Import Coq.Logic.ConstructiveEpsilon.

Definition surjective A B (f : A -> B) := forall y : B, {x : A | f x = y}.

Lemma surjective_enum : surjective enum.
  intros s. destruct (T_exhaustive s).
  unfold enum. eapply constructive_indefinite_ground_description_nat_Acc.
  intros. decide (enum n = s); firstorder. eapply el_elAt in i as [m A].
  exists m.
  destruct (lt_eq_lt_dec m x) as [[D | D] | D].
  - destruct _ eqn:B. eapply T_ge in B. rewrite B in A. congruence. omega.
    eapply nth_error_none in B. assert (|T_enum m| > m) by eapply T_longenough. omega.
  - subst. now rewrite A.
  - eapply T_ge in A. rewrite A. reflexivity. omega.
  - exact _.

Procedural realisation of enumeration

Some list procedures

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)))

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

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

  Hint Resolve lenc_proc : cbv.

  Lemma Cons_correct a A : Cons (enc a) (lenc A) lenc(a::A).

  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).
    induction A; solveeq.

  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).
    intros [[? ?] ?].
    induction A.
    - solveeq.
    - specialize (H1 a). solveeq.

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

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

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

End Fix_X.

Hint Resolve lenc_proc : cbv.

Definition AppCross := rho (.\"aC", "A", "B";
  "A" !Nil (.\"a", "A"; !Append ("aC" "A" "B") (!Map (.\"x"; !App "a" "x") "B"))).

Hint Unfold AppCross : cbv.

Lemma AppCross_cls : closed AppCross.

Hint Resolve AppCross_cls : cbv.

Definition tlenc := @lenc term tenc.
Hint Unfold tlenc.

Lemma tlenc_proc B : proc (tlenc B).
  unfold tlenc. value.
Hint Resolve tlenc_proc : cbv.

Lemma AppCross_correct A B : AppCross (tlenc A) (tlenc B) tlenc(appCross A B).
  induction A.
  - solveeq.
  - transitivity (Append (AppCross (tlenc A) (tlenc B)) (Map (lambda (App (tenc a) 0)) (tlenc B))). solveeq.
    rewrite IHA. unfold tlenc; rewrite Map_correct; eauto with cbv.
    + rewrite Append_correct; cbn; eauto with cbv.
    + split; value.
      intros; rewrite <- App_correct. solveeq.

Definition TT := rho (.\ "TT", "n";
  "n" !(tlenc([var 0]))
      (.\"n"; (!Append
              (!Append ("TT" "n") (!Cons (!Var (!Succ "n")) !Nil))
             (!Append (!Map !Lam ("TT" "n"))
                       (!AppCross ("TT" "n") ("TT" "n"))

Lemma TT_S n : TT (enc (S n)) Append (Append (TT (enc n)) (Cons (Var (Succ (enc n))) Nil)) (Append (Map Lam (TT (enc n))) (AppCross (TT (enc n)) (TT (enc n)))).

Lemma TT_correct n : TT (enc n) tlenc(T_enum n).
Proof with (intros; try now value); auto with cbv; unfold tlenc.
  induction n...
  - solveeq.
  - rewrite TT_S. rewrite !IHn.
    rewrite AppCross_correct.
    rewrite (@Map_correct _ tenc tenc_proc lambda)...
    rewrite Append_correct...
    rewrite Succ_correct, Var_correct. change Nil with (lenc tenc nil). rewrite Cons_correct, Append_correct...
    rewrite Append_correct...
    setoid_rewrite <- app_assoc at 1. simpl. reflexivity.
    + split; value.
      intros x. eapply Lam_correct;value.

Definition Enum : term := .\"n";
  (!Nth (!TT "n") "n") !I !(tenc 0).

Hint Unfold Enum : cbv.

Lemma Enum_correct n : Enum (enc n) tenc(enum n).
  transitivity (Nth (TT (enc n)) (enc n) I (tenc 0)). solveeq.
  rewrite TT_correct. unfold tlenc.
  rewrite Nth_correct; value.
  unfold enum, elAt, oenc.
  destruct (nth_error (T_enum n) n); solveeq.
  intros; value.

Recognisable classes are enumerable

Lemma enumerable_all : enumerable (fun s => True).
  exists (lambda (some (Enum 0))). split; value.
  assert (forall n, lambda (some (Enum 0)) (enc n) oenc (Some (enum n))). {
    intros. transitivity (some (Enum (enc n))). solveeq. now rewrite Enum_correct, some_correct.
  - right. exists (enum n). now rewrite H.
  - intros. destruct (surjective_enum s) as [n Hn]. exists n. now rewrite H, Hn.

Theorem recognisable_enumerable p : recognisable p -> enumerable p.
  intros [u [proc_u Hu]]. unfold enumerable.

  pose (v := (.\ "n"; !Enum "n" !(lambda none) (.\ "t", "s"; "t" (.\ "n"; !E "n" (!App !(tenc u) (!Q "s")) (.\ "_"; !some "s") !none) !(lambda (lambda none)) !(lambda none)) !(lambda none)) : term).
  assert (Hv : forall n, v (enc n) Enum (enc n) (lambda none) (lambda (lambda (1 (lambda (E 0 (App (tenc u) (Q 1)) (lambda (some 2)) none)) (lambda (lambda none)) (lambda none)))) (lambda none)) by (intros; solveeq).
  exists v.
  repeat split; value.
  - intros n. destruct (enum n) as [ | ? s | ] eqn:Eq.
    + left. rewrite Hv, Enum_correct, Eq. solveeq.
    + destruct t1 as [ m | |].
      * destruct (eval m (u (tenc s))) eqn:He.
        -- right. exists s. rewrite Hv, Enum_correct, Eq. 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.
        -- left. rewrite Hv, Enum_correct, Eq.
           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.
      * left. rewrite Hv, Enum_correct, Eq. solveeq.
      * left. rewrite Hv, Enum_correct, Eq. solveeq.
    + left. rewrite Hv, Enum_correct, Eq. solveeq.
  - intros s [s' [n H] % evaluates_eval] % Hu.
    destruct (surjective_enum (n s)). exists x.
    rewrite Hv, Enum_correct, e.
    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.