# Library Acceptability

Require Export Por Decidability.

# Definition of L-acceptability

Definition pi s t := converges (s (tenc t)).

Definition lacc (P : term -> Prop) :=
exists u, proc u /\ forall t, P t <-> pi u t.

# Properties of acceptance

Goal forall s1 s2 t, s1 == s2 -> (pi s1 t <-> pi s2 t).

Proof.

intros s1 s2 t H; intuition; unfold pi; [now rewrite <- H | now rewrite H].

Qed.

# L-acceptable predicates are closed under conjunction and disjunction

Definition acc_conj (p q : term) := lam ((lam (q #1)) (p #0) ).

Hint Unfold acc_conj : cbv.

Lemma acc_conj_correct p q s : closed p -> closed q -> (pi (acc_conj p q) s <-> pi p s /\ pi q s).

Proof.

intros cls_p cls_q.

split.

- intros [x Hx].

assert (H : converges ((Î» q (tenc s)) (p (tenc s)))).
exists x. symmetry. symmetry in Hx. crush.
destruct (app_converges H) as [_ [y Hy]].
split.
+ eexists; eassumption.

+ exists x.
rewrite <- Hx. symmetry. clear Hx. crush.
- intros [[x Hx] [y Hy]].
exists y. crush.
Qed.

Lemma lacc_conj P Q : lacc P -> lacc Q -> lacc (conj P Q).

Proof.

intros [u1 [proc_u1 Hu1]] [u2 [proc_u2 Hu2]].

exists (acc_conj u1 u2).
split; value.
intros; rewrite acc_conj_correct; firstorder.

Qed.

Lemma lacc_disj M N : lacc M -> lacc N -> lacc (disj M N).

Proof.

intros [u [[lam_u cls_u] Hu]] [v [[lam_v cls_v] Hv]].

unfold lacc, disj.

exists (lam (Por ((App (tenc u) (Q #0))) ((App (tenc v) (Q #0))))).

split; value.
intros t.

rewrite Hu, Hv; unfold pi.

assert (H : (Î» (Por ((App (tenc u)) (Q 0))) ((App (tenc v)) (Q 0))) (tenc t) == Por (tenc (u (tenc t))) (tenc (v (tenc t)))). {

transitivity (((Por ((App (tenc u) ( Q (tenc t))))) ((App (tenc v) (Q (tenc t)))))).
crush.
now rewrite Q_correct, App_correct, App_correct.

}
rewrite H; split.

- intros [A | A].

+ eapply Por_correct_1a in A; eassumption.

+ eapply Por_correct_1b in A; eassumption.

- intros A.
eapply Por_correct_2 in A. firstorder.
Qed.

# L-ecidable predicates are L-acceptable (and their complement too)

Lemma dec_lacc M : ldec M -> lacc M.

Proof.

intros [u [[cls_u lam_u] dec_u_M]].

exists (lam (u #0 I (lam Omega) I)); split; value.

+ intros t.
specialize (dec_u_M t).
split; intros H; destruct dec_u_M; try tauto.

* destruct H0 as [_ u_true].
eexists; crush.
* destruct H.
destruct H0.
assert ((lam ((((u #0) I) (lam Omega)) I)) (tenc t) == Omega).
clear H. crush.
rewrite H2 in H.

destruct (Omega_diverges H).

Qed.

Lemma dec_acc : forall M, ldec M -> lacc M /\ lacc (complement M).

Proof.

intros M decM; split.

- eapply (dec_lacc decM).

- eapply ldec_complement in decM.
eapply (dec_lacc decM).
Qed.