Require Export L.
Fixpoint eval (n : nat) (u : term) :=
match u with
| var n => None
| lambda s => Some (lambda s)
| app s t => match n with
| 0 => None
| S n => match eval n s, eval n t with
| Some (lambda s), Some t => eval n (subst s 0 t)
| _ , _ => None
end
end
end.
Lemma eval_S n s t : eval n s = Some t -> eval (S n) s = Some t.
Proof.
revert s t; induction n; intros; cbn in H;
repeat (destruct _ eqn:_; subst; try congruence; eauto).
remember (S n) as n'; cbn; subst.
now rewrite (IHn _ _ E), (IHn _ _ E0), (IHn _ _ H).
Qed.
Lemma eval_step s s' t n : s ≻ s' -> eval n s' = Some t -> eval (S n) s = Some t.
Proof.
revert s s' t; induction n; intros.
- cbn in H0. destruct _; inv H0.
cbn. destruct _; inv H. now rewrite H3.
- cbn in H0. inv H; repeat (destruct _ eqn:_; subst; try congruence).
+ cbn; now rewrite E, E0, E1.
+ cbn; now rewrite E.
+ remember (S n); cbn; subst.
erewrite eval_S, IHn; eauto. now eapply eval_S.
+ remember (S n). cbn. subst.
erewrite IHn, eval_S; eauto. now eapply eval_S.
Qed.
Lemma evaluates_eval s t : evaluates s t -> exists n, eval n s = Some t.
Proof.
intros [A B] % evaluates_equiv. eapply equiv_star_lam in A; eauto. induction A.
- destruct B. subst; now exists 0.
- destruct (IHA B) as [k C]. eauto using eval_step.
Qed.
Lemma eval_evaluates n s t : eval n s = Some t -> evaluates s t.
Proof.
revert s t; induction n; intros.
- inv H. destruct _; try congruence. inv H1. firstorder.
- inv H. repeat (destruct _ eqn:_; subst; try congruence).
eapply IHn in E. eapply IHn in E0. eapply IHn in H1. eauto. inv H1. eauto.
Qed.
Lemma equiv_eval s t : lam t -> s ≡ t -> exists n, eval n s = Some t.
Proof.
intros. eapply evaluates_eval. firstorder using evaluates_equiv.
Qed.
Lemma eval_equiv s s' n : eval n s = Some s' -> s ≡ s'.
Proof.
intros ? % eval_evaluates. firstorder using evaluates_equiv.
Qed.
Lemma eval_lambda n s t : eval n s = Some t -> lam t.
Proof.
intros ? % eval_evaluates. firstorder using evaluates_equiv.
Qed.
Require Import DecidableRecognisable Encodings Coq.Logic.ConstructiveEpsilon.
Definition cChoice := constructive_indefinite_ground_description_nat_Acc.
Lemma computable_eva s : eva s -> { v | s ▷ v }.
Proof.
intros.
assert (exists n v, eval n s = Some v) by (destruct H as (? & ? % evaluates_eval); firstorder).
eapply cChoice in H0 as []. destruct (eval x s) eqn:E.
- exists t. eauto using eval_evaluates.
- exfalso. firstorder congruence.
- intros. destruct (eval n s). eauto.
right. intros []. congruence.
Qed.
Lemma dec_pdec p : decidable p -> forall x, p x \/ ~ p x.
Proof.
firstorder.
Qed.
Lemma decidable_dec p : decidable p -> exists f, forall s, f s = true <-> p s.
Proof with try tauto; try (eexists; reflexivity).
intros (u & proc_u & Hu).
assert (forall s, {v | u (tenc s) ▷ v}). {
intros. eapply computable_eva. destruct (Hu s). exists T. tauto.
exists F; tauto.
}
exists (fun s => let (v, _) := H s in if decision (v = T) then true else false).
intros. destruct _. decide (x = T).
- subst. firstorder. eapply decidable_spec; eauto.
- firstorder. congruence. exfalso. eapply decidable_spec; eauto.
destruct (Hu s) as [ [? [H4 ?] %evaluates_equiv] | []].
destruct T_equiv_F.
assert (x ≡ T) by now rewrite <- e, <- H4. eapply unique_normal_forms in H6. subst. congruence.
eapply evaluates_abst; eauto. value. firstorder using evaluates_equiv.
Qed.