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

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

## 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
end.

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

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

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

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

Lemma appCross_correct A B s t : (s el A /\ t el B) <-> (app s t) el appCross A B.
Proof.
split.
- 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.
Qed.

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

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

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

Lemma T_lambda s n : s el T_enum n -> lambda s el T_enum (S n).
Proof.
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.
Qed.

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

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

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.
Proof.
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 _.
Qed.

## 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)))
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 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).
Proof.
revert A; induction n; intros A.
- destruct A; solveeq.
- destruct A.
+ solveeq.
+ cbn. rewrite <- IHn. solveeq.
Qed.

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.
Proof.
value.
Qed.

Hint Resolve AppCross_cls : cbv.

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

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

Lemma AppCross_correct A B : AppCross (tlenc A) (tlenc B) tlenc(appCross A B).
Proof.
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.
Qed.

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)))).
Proof.
solveeq.
Qed.

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...
simpl.
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.
Qed.

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

## Recognisable classes are enumerable

Lemma enumerable_all : enumerable (fun s => True).
Proof.
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.
}
split.
- right. exists (enum n). now rewrite H.
- intros. destruct (surjective_enum s) as [n Hn]. exists n. now rewrite H, Hn.
Qed.

Theorem recognisable_enumerable p : recognisable p -> enumerable p.
Proof.
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.
Qed.