# Library Seval

Require Export Tactics.

# Definition of evaluation

Definition eval s t := s >* t lambda t.
Hint Unfold eval.

Notation "s '⇓' t" := (eval s t) (at level 51).

# Step indexed evaluation

Inductive seval : nattermtermProp :=
| sevalR n s : seval n (lam s) (lam s)
| sevalS n s t u v w :
seval n s (lam u) → seval n t (lam v) → seval n (subst u 0 (lam v)) wseval (S n) (s t) w.

Notation "s '⇓' n t" := (seval n s t) (at level 51).

Lemma seval_eval n s t : seval n s teval s t.
Proof with eauto using star_trans, star_trans_l, star_trans_r.
intros. induction H as [ | n s t u v w _ [IHe1 _] _ [IHe2 _] _ [IHe3 lam_w]].
- repeat econstructor.
- split...
transitivity ((lam u) t)...
transitivity ((lam u) (lam v))... crush.
Qed.

# Equivalence between step index evaluation and evaluation

Lemma seval_S n s t : seval n s tseval (S n) s t.
Proof.
induction 1; eauto using seval.
Qed.

Lemma eval_step s s' t n : s >> s'seval n s' tseval (S n) s t.
Proof with eauto using seval_S, seval.
intros H; revert n t; induction H; intros n u A...
- inv A...
- inv A...
Qed.

Lemma eval_seval s t : eval s t n, seval n s t.
Proof.
intros [A B]. induction A.
- destruct B. subst. eauto using seval.
- destruct (IHA B) as [k C]. eauto using seval, eval_step.
Grab Existential Variables. exact 0.
Qed.

# Evaluation as a function

Fixpoint eva (n : nat) (u : term) :=
match u with
| var nNone
| lam sSome (lam s)
| app s tmatch n with
| 0 ⇒ None
| S nmatch eva n s, eva n t with
| Some (lam s), Some teva n (subst s 0 t)
| _ , _None
end
end
end.

# Equivalence between the evaluation function and step indexed evaluation

Lemma eva_lam n s t : eva n s = Some t u, t = lam u.
Proof.
revert s t; induction n; intros s t H;
destruct s; try inv H; eauto.
destruct (eva n s1) eqn:Hs1; try now inv H1.
destruct t0; try inv H1.
destruct (eva n s2); try inv H0.
eapply IHn in H1. eassumption.
Qed.

Lemma eva_seval n s t : eva n s = Some tseval n s t.
Proof.
revert s t. induction n; intros s t H;
destruct s; try now inv H; eauto using seval.
destruct (eva n s1) eqn:Hs1; try now (simpl in H; rewrite Hs1 in H; inv H).
destruct t0; try now (simpl in H; rewrite Hs1 in H; inv H).
destruct (eva n s2) eqn:Hs2; try now (simpl in H; rewrite Hs1, Hs2 in H; inv H).
destruct (eva_lam Hs2); subst t1.
econstructor; eauto. eapply IHn. simpl in H. rewrite Hs1, Hs2 in H. eassumption.
Qed.

Lemma seval_eva n s t : seval n s teva n s = Some t.
Proof.
induction 1.
- destruct n; reflexivity.
- simpl. rewrite IHseval1, IHseval2. eassumption.
Qed.

Lemma equiv_eva s s' : s == lam s' n, eva n s = Some (lam s').
Proof.
intros A. cut (eval s (lam s')). intros H.
eapply eval_seval in H. destruct H as [n H]. eapply seval_eva in H.
eauto. eauto using equiv_lambda.
Qed.

Lemma eva_equiv s s' n : eva n s = Some s's == s'.
Proof.
intros H. eapply eva_seval in H. eapply seval_eval in H. destruct H. eapply star_equiv.
eassumption.
Qed.

Lemma eva_n_Sn n s t : eva n s = Some teva (S n) s = Some t.
Proof.
intros H. eapply eva_seval in H. eapply seval_eva.
eapply seval_S. eassumption.
Qed.

Lemma eva_Sn_n n s : eva (S n) s = Noneeva n s = None.
Proof.
intros H; destruct s, n; try reflexivity; try now inv H.
simpl. destruct (eva n s1) eqn:Hs1, (eva n s2) eqn:Hs2.
- destruct t; try reflexivity.
assert (Hs' : eva (S n) s1 = Some (lam t)) by eauto using eva_n_Sn.
assert (Ht' : eva (S n) s2 = Some (t0)) by eauto using eva_n_Sn.
destruct (eva n (subst t 0 t0)) eqn:Ht; try reflexivity.
assert (H' : eva (S n) (subst t 0 t0) = Some t1) by eauto using eva_n_Sn.
rewrite <- H. change (Some t1 = match eva (S n) s1, eva (S n) s2 with
| Some (lam s), Some teva (S n) (subst s 0 t)
| _ , _None
end). rewrite Hs', Ht'. rewrite H'. reflexivity.

- destruct t; reflexivity.
- reflexivity.
- reflexivity.
Qed.

Lemma eproc_equiv s t: eval s (lam t) s == (lam t).
Proof.
split; intros H; eauto using equiv_lambda.
destruct (eval_seval H) as [n A]. destruct H; eauto.
Qed.

# Omega diverges

Lemma Omega_diverges s : ¬ (Omega == lam s).
Proof.
intros H. eapply eproc_equiv in H.
eapply eval_seval in H. destruct H. inv H.
inv H2. inv H4. induction n.
- inv H6.
- inv H6. inv H2. inv H3. simpl in ×.
eapply IHn. eassumption.
Qed.

# If an application converges, both sides converge

Lemma app_converges (s t : term) : (converges (s t)) → converges s converges t.
Proof.
intros H. split;
destruct H as [u H];
eapply eproc_equiv in H; eapply eval_seval in H; destruct H as [n H]; inv H;
[ u0 | v]; eapply eproc_equiv; eapply seval_eval; eassumption.
Qed.