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.
Definition cChoice := constructive_indefinite_ground_description_nat_Acc.
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.
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.
Definition cChoice := constructive_indefinite_ground_description_nat_Acc.
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.