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.