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


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


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


  intros cls_p cls_q.


  - 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]].
    + eexists; eassumption.

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

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


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

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


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


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

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

Lemma dec_lacc M : ldec M -> lacc M.


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


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


  intros M decM; split.

  - eapply (dec_lacc decM).

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