Library Seval
Inductive seval : nat → term → term → Prop :=
| 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)) w → seval (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 t → eval s t.
Lemma seval_S n s t : seval n s t → seval (S n) s t.
Lemma eval_step s s' t n : s >> s' → seval n s' t → seval (S n) s t.
Lemma eval_seval s t : eval s t → ∃ n, seval n s t.
Fixpoint eva (n : nat) (u : term) :=
match u with
| var n ⇒ None
| lam s ⇒ Some (lam s)
| app s t ⇒ match n with
| 0 ⇒ None
| S n ⇒ match eva n s, eva n t with
| Some (lam s), Some t ⇒ eva n (subst s 0 t)
| _ , _ ⇒ None
end
end
end.
Lemma eva_lam n s t : eva n s = Some t → ∃ u, t = lam u.
Lemma eva_seval n s t : eva n s = Some t → seval n s t.
Lemma seval_eva n s t : seval n s t → eva n s = Some t.
Lemma equiv_eva s s' : s == lam s' → ∃ n, eva n s = Some (lam s').
Lemma eva_equiv s s' n : eva n s = Some s' → s == s'.
Lemma eva_n_Sn n s t : eva n s = Some t → eva (S n) s = Some t.
Lemma eva_Sn_n n s : eva (S n) s = None → eva n s = None.
Lemma eproc_equiv s t: eval s (lam t) ↔ s == (lam t).