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