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.