Library Eval
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.
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.
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.