Library AD

Require Import Por Acceptability.

Theorem AD M : (forall x, M x \/ ~ M x) -> lacc M -> lacc (complement M) -> ldec M.

Proof.

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

  pose (por_u_v := lam (Por ((App (tenc u) (Q #0))) ((App (tenc v) (Q #0))))).

  exists por_u_v.

  split; value.
intros t.

  assert (A : converges (Por (tenc (u (tenc t))) (tenc (v (tenc t))))). {

    eapply Por_correct_1.

    destruct (pdec_M t); firstorder.

  }

  destruct (Por_correct_2 A) as [[B C] | [B C]].

  - left; split; try firstorder 2.

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

  - right; split; try firstorder 2.

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

Qed.