Library DA

Require Export Decidability Acceptability Enum EnumInt.

Definition Ex := R (lam (lam (lam (
   #0 #1 (lam I) (lam (#3 (Succ #2) #1)) I)))).

Lemma Ex_rec u n : proc u -> Ex (enc n) u == u (enc n) (lam I) (lam ((lam (Ex #0)) (Succ (enc n)) u)) I.
Proof.
  intros [cls_u lam_u]. crush.
Qed.

Lemma Ex_correct_1 (u : term) n : proc u -> u (enc n) == true -> converges (Ex (enc n) u).
Proof.
  intros proc_u H.
  exists #0.
  now rewrite Ex_rec, H; crush.
Qed.

Definition n_decider u := proc u /\ forall n, u (enc n) == true \/ u (enc n) == false.

Lemma Ex_correct_3a (u : term) n : n_decider u -> converges ( Ex (enc (S n)) u ) -> converges ( Ex (enc n) u ).
Proof.
  intros [proc_u dec_u] H.
  rewrite Ex_rec. destruct (dec_u n).
  - rewrite H0. cut (converges I). eapply converges_equiv.
    crush. now exists #0.
  - rewrite H0. revert H. eapply converges_equiv. crush.
  - eassumption.
Qed.

Lemma Ex_correct_3 (u : term) n m : n_decider u -> n >= m -> converges ( Ex (enc n) u ) -> converges ( Ex (enc m) u ).
Proof.
  induction 2; eauto using Ex_correct_3a.
Qed.

Lemma Ex_correct_2 (u : term) n : n_decider u -> converges (Ex (enc n) u) -> exists n, u (enc n) == true.
Proof.
  intros [proc_u dec_u] H. destruct H as [v H].
  eapply equiv_lambda, star_pow in H. destruct H as [m H].
  revert n H.
  eapply complete_induction with (x := m). clear m; intros m IHm n H'.
  destruct (dec_u n).
  - now exists n.
  - assert (A : exists k, pow step (S k) (Ex (enc n) u) (Ex (enc (S n)) u)). {
      eapply powSk. reduce.
      simpl. transitivity (u (enc n) (lam I) (lam ((lam (Ex #0)) (Succ (enc n)) u )) I). repeat reduction'.
      cbv in H; eapply equiv_lambda in H. eapply star_trans.
      do 3 eapply star_trans_l. eassumption. crush.
   }
   destruct A as [k A].
   destruct (pow_trans_lam H' A) as [l [l_lt_m B]].
   eapply (IHm l); eassumption.
Qed.

Definition n_ldec P := exists u : term ,
  proc u /\
  (forall s : nat, P s /\ u (enc s) == true \/ ~ P s /\ u (enc s) == false ).

Lemma DA_nat M :
  n_ldec M -> lacc (fun _ => exists n, M n).
Proof.
  intros [u [[lam_u cls_u] Hu]].
  exists (lam (Ex (enc 0) u)).
  split; value.
  intros t.
  split; intros H.
  - unfold pi.
    assert (converges (Ex (enc 0) u)).
    destruct H as [n H].
    eapply Ex_correct_3 with (n := n). split; value. intros k; destruct (Hu k); intuition. omega.
    eapply Ex_correct_1. now value.
    destruct (Hu n); intuition.
    revert H0. eapply converges_equiv. crush.
  - unfold pi in H.
    assert (converges (Ex (enc 0) u)).
    revert H. eapply converges_equiv. symmetry. crush.
    eapply Ex_correct_2 in H0. destruct H0. exists x.
    destruct (Hu x). intuition. rewrite H0 in H1. exfalso. eapply true_equiv_false. intuition. econstructor.
    now value.
    intros n; destruct (Hu n); intuition.
Qed.

Theorem DA M :
  ldec M -> lacc (fun _ => exists t, M t).
Proof.
  intros [u [[lam_u cls_u] Hu]].
  assert (n_ldec (fun x => M (g_inv x))). {
    exists (lam (u (U #0))).
    split; value.
    intros n.
    destruct (Hu (g_inv n)); assert (U := U_correct n); [left | right]; intuition; crush.
  }
  eapply DA_nat in H.
  destruct H as [v [[lam_v cls_v] Hv]].
  exists v; split; value; intuition.
  - destruct H as [s Hs].
    eapply Hv. exists (g s). now rewrite g_inv_g.
  - eapply Hv in H. destruct H as [n H]. now exists (g_inv n).
Qed.