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.