# Library Computability

Require Export Lvw Nat Decidability Size Coq.Logic.ConstructiveEpsilon Encoding Eval Seval.

Lemma dec_pdec P : ldec P -> forall x, P x \/ ~ P x.

Proof.

intros [d [[cls_d lam_d] Hd]].

intros s.

destruct (Hd s); tauto.

Qed.

Lemma eq_term_dec (s t : term) : (s = t) + (s <> t).

Proof.

revert t.
induction s; intros t; destruct t; try(right; intros H; inv H; fail).
- decide (n = n0).
left. congruence. right. congruence.
- destruct (IHs1 t1), (IHs2 t2); try (right; congruence).
left. congruence.
- destruct (IHs t).
left; congruence. right; congruence.
Qed.

Lemma enc_inj m n : enc m == enc n -> m = n.

Proof.

intros H.
eapply enc_injective. destruct (enc_lam m) as [? A], (enc_lam n) as [? B].
rewrite A, B in H.
eapply eq_lam in H. subst; congruence.
Qed.

Lemma dec_dec P u : (forall s, u (tenc s) == true /\ P s \/ u (tenc s) == false /\ ~ P s) -> forall s, dec(P s).

Proof with try tauto; try (eexists; reflexivity).

intros Hu.
intros s. specialize (Hu s).
assert (exists n, eva n (u (tenc s)) = Some (convert true) \/ eva n (u (tenc s)) = Some (convert false)). {

destruct Hu as [[H B] | [H B]].

assert (A : eval (u (tenc s)) true).
split... cbv in H; eapply equiv_lambda in H...
eapply eval_seval in A.
destruct A as [x A]. exists x. left. eapply seval_eva in A...
assert (A : eval (u (tenc s)) false).
split... cbv in H; eapply equiv_lambda in H...
eapply eval_seval in A.
destruct A as [x A]. apply seval_eva in A. exists x. tauto.
}
eapply cChoice in H.
destruct H as [n H].
destruct (eva n (u (tenc s))) as [t|] eqn:Heva.

destruct (eq_term_dec t true) as [eq_t_true | neq_t_true].

- left.
destruct Hu. intuition. destruct H0. cut (u (tenc s) == true). intros C; rewrite C in H0. exfalso; eauto using true_equiv_false.
eapply eva_seval in Heva.
eapply seval_eval in Heva. rewrite eq_t_true in Heva.
eapply star_equiv.
destruct Heva; eassumption.
- right.
destruct Hu.
+ intros A.
eapply eva_seval in Heva. eapply seval_eval in Heva.
destruct Heva.
destruct H0. eapply star_equiv in H1. rewrite H1 in H0.
destruct H as [H | H]; inv H.
tauto. eapply true_equiv_false. now rewrite H0.
+ intuition.

- right.
destruct H as [H | H]; inv H.
- intros n.
destruct (eva n (u (tenc s))).
destruct (eq_term_dec t true) as [Heq | Heq].
left. left. rewrite Heq. reflexivity.
destruct (eq_term_dec t false) as [Heqf | Heqf].
left. right. rewrite Heqf. reflexivity.
right.
intros [A | B]. eapply Heq. inv A. reflexivity.
eapply Heqf.
inv B. reflexivity. right. intros [A | A]; inv A.
Qed.