Library Eval

Require Export Subst Options Seval Partial.

Internalized Evaluation Function

Definition Eva := R (.\ "Eva","n","u";"u" (.\"";!none)
(.\"s","t"; "n" !none
(.\"n"; "Eva" "n" "s"
(.\"s"; "Eva" "n" "t"
(.\"t"; "s"
(.\""; !none)
(.\"",""; !none)
(.\"s"; "Eva" "n" (!Subst "s" !Zero "t")))
!none)
!none))
(.\"s"; !some (!Lam "s"))).

Hint Unfold Eva : cbv.

Correctness of the internalized evaluation function

Lemma Eva_rec_var k n : Eva (enc k) (tenc (# n)) == none.

Proof.
crush. Qed.

Lemma Eva_rec_lam k s : Eva (enc k) (tenc (lam s)) == some (Lam (tenc s)).

Proof.
crush. Qed.

Lemma Eva_rec_app_0 s t : Eva Zero (tenc (app s t)) == none.

Proof.
crush. Qed.

Lemma Eva_rec_app_Sn s t n :
Eva (enc (S n)) (tenc (app s t)) == Eva (enc n) (tenc s) (lam ((lam (Eva #0)) (enc n) (tenc t) (lam (
#1 (lam none)
(lam (lam none))
(lam ((lam (Eva #0)) (enc n) (Subst #0 Zero #1))))) none )) none.

Proof.
crush. Qed.

Definition cLam s := lam(lam(lam(#0 s))).

Hint Unfold cLam : cbv.

Lemma Eva_rec_app_Sn_1 s t n s1 t1 :
proc s1 ->
proc t1 ->
Eva (enc n) (tenc s) == some (cLam s1) ->
Eva (enc n) (tenc t) == some (cLam t1) ->
Eva (enc (S n)) (tenc (app s t)) == Eva (enc n) (Subst s1 Zero (cLam t1)).

Proof.

intros [clsS1 lamS1] [clsT1 lamT1] someS someT.

rewrite Eva_rec_app_Sn.
crush.
Qed.

Lemma Eva_rec_app_Sn_2 s t n : Eva (enc n) (tenc s) == none -> Eva (enc (S n)) (tenc (s t)) == none.

Proof.

intros H.
rewrite Eva_rec_app_Sn; crush.
Qed.

Lemma Eva_rec_app_Sn_3 s t n s1 t1 : proc s1
-> proc t1
-> Eva (enc n) (tenc s) == some (cLam t1)
-> Eva (enc n) (tenc t) == none
-> Eva (enc (S n)) (tenc (s t)) == none.

Proof.

intros [clsS1 lamS1] [clsT1 lamT1] Hs Ht.

rewrite Eva_rec_app_Sn; crush.

Qed.

Hint Unfold cLam : cbv.

Lemma Eva_correct k s : Eva (enc k) (tenc s) == oenc (eva k s).

Proof.

revert s; induction k; intros s.

- destruct s; [crush.. | idtac].

now rewrite Eva_rec_lam, Lam_correct, some_correct_enc.

- destruct s.

+ crush.

+ destruct (eva k s1) eqn:Hs1.

* destruct (eva_lam Hs1); subst t. {
destruct (eva k s2) eqn:Hs2.

- destruct (eva_lam Hs2); subst t.

eapply eqTrans.

eapply Eva_rec_app_Sn_1 with (s1 := tenc x) (t1 := tenc ( x0));
eauto with cbv...

rewrite IHk, Hs1.
symmetry. crush.
rewrite IHk, Hs2.
symmetry. crush.
assert (Subst (tenc x) Zero (tenc (lam x0)) == tenc (subst x 0 (lam x0))).

change Zero with (enc 0).
eapply Subst_correct.
rewrite H, IHk.
simpl. now rewrite Hs1, Hs2.
- rewrite Eva_rec_app_Sn_3 with (t1 := tenc x); eauto with cbv...

simpl.
rewrite Hs1, Hs2. reflexivity.
rewrite IHk.
rewrite Hs1. symmetry. crush.
rewrite IHk.
rewrite Hs2. symmetry. crush.
}
* simpl.
rewrite Hs1. eapply Eva_rec_app_Sn_2.
change none with (oenc (None)).
rewrite <- Hs1. eapply IHk.
+ now rewrite Eva_rec_lam, (Lam_correct s), some_correct_enc.

Grab Existential Variables.
exact #0.
Qed.

Internalized Evaluation

Definition Eval := Se (.\"x"; !Eva "x").

Hint Unfold Eval : cbv.

Hint Resolve star_equiv : cbv.

Hint Unfold convert convert'.

Lemma Eval_correct s v : proc v -> (Eval (tenc s) == v <-> exists n, Eva (enc n) (tenc s) == some v).

Proof.

intros cls_v.

unfold Eval.
rewrite Se_correct; value.
- split; intros [n H]; exists n; rewrite <- H; clear H; [symmetry | ]; crush.

- intros.
destruct (eva n t) eqn:A.
+ left.
exists (tenc t0). unfold convert, convert'; simpl. rewrite Eta...
split...
rewrite Eva_correct, A... cbv; symmetry; crush. value. value. value.
+ right.
cbv. rewrite Eta, Eva_correct, A... crush. value. value.
- intros ? ? ?.
repeat autounfold. simpl. change (Î» (Î» O (enc n))) with (enc (S n)).
rewrite !Eta, !Eva_correct; value.
destruct (eva n t) eqn:A, (eva (S n) t) eqn:B; intros.
+ rewrite <- H.
eapply eva_n_Sn in A. rewrite A in B. now inv B.
+ rewrite (eva_n_Sn A) in B.
inv B.
+ eapply eqTrans with (s := none) in H.
now destruct none_equiv_some with (v := v0). symmetry; crush.
+ eapply eqTrans with (s := none) in H.
now destruct none_equiv_some with (v := v0). symmetry; crush.
Qed.

Lemma seval_Eval n s t: seval n s t -> Eval (tenc s) == (tenc t).

Proof.

intros.
eapply seval_eva in H.
rewrite Eval_correct; value.
exists n. rewrite Eva_correct, H. symmetry; crush.
Qed.

Lemma eval_Eval s t : eval s t -> Eval (tenc s) == (tenc t).

Proof.

intros H.
eapply eval_seval in H. destruct H. eapply seval_Eval. eassumption.
Qed.

Lemma equiv_lambda' s t : lambda t -> s == t -> s >* t.

Proof.

intros.
destruct H; subst. eauto using equiv_lambda.
Qed.

Lemma Eval_eval (s t : term) : Eval (tenc s) == tenc t -> eval s t.

Proof with value.

intros H.
rewrite Eval_correct in H. destruct H as [n H].
rewrite Eva_correct in H.
destruct (eva n s) eqn:E.
eapply oenc_correct_some in H.
eapply tenc_inj in H. subst. eapply seval_eval, eva_seval. eassumption.
value.
now eapply none_equiv_some in H. value.
Qed.

Lemma eval_converges s : converges s -> exists t, eval s t.

Proof.

intros [x Hx].
exists (lam x). eauto using equiv_lambda.
Qed.

Lemma Eval_converges s : converges s <-> converges (Eval (tenc s)).

Proof with eauto.

split; intros H.

- destruct (eval_converges H) as [t Ht].

assert (He := eval_Eval Ht).

destruct (tenc_lam t).
rewrite He, H0. eexists; reflexivity.
- destruct H.
rewrite Eval_correct in H.
+ destruct H as [n H].
rewrite Eva_correct in H.
destruct (eva n s) eqn:E.
eapply oenc_correct_some in H.
subst.
destruct (eva_lam E). exists x0. eapply eva_seval in E. eapply seval_eval in E.
subst.
now eapply eproc_equiv.
eapply oenc_correct_some in H.
value. value. destruct (none_equiv_some H).
+ { value; eapply Se_converges in H...
value.
+ intros.
destruct (eva n t) eqn:A.
* left.
exists (tenc t0). unfold convert, convert' ; simpl. rewrite Eta; value.
split...
rewrite Eva_correct, A... symmetry; crush. value.
* right.
unfold convert, convert' ; simpl. rewrite Eta; value. rewrite Eva_correct, A... reflexivity.
+ intros ? ? ?.
repeat autounfold. simpl. change (Î» (Î» O (enc n))) with (enc (S n)).
rewrite !Eta; value.
rewrite !Eva_correct. destruct (eva n t) eqn:A, (eva (S n) t) eqn:B; intros.
* rewrite <- H0.
eapply eva_n_Sn in A. rewrite A in B. now inv B.
* rewrite (eva_n_Sn A) in B.
inv B.
* now destruct none_equiv_some with (v := v).

* now destruct none_equiv_some with (v := v).

}
Qed.