%% Lambda calculus and various results on typing and evaluation
%%
%% Even though we use higher-order abstract syntax here, we do not need
%% to define a meta-level context predicate because all contexts are
%% empty in the inductions.
Specification "eval".
%%
%% Determinancy
%%
Theorem eval_det :
forall E V1 V2, {eval E V1} -> {eval E V2} -> V1 = V2.
induction on 1. intros. case H1.
case H2. search.
case H2. apply IH to H3 H5. apply IH to H4 H6. search.
Theorem step_det :
forall E1 E2 E3, {step E1 E2} -> {step E1 E3} -> E2 = E3.
induction on 1. intros. case H1.
case H2.
search.
case H3.
case H2.
case H3.
apply IH to H3 H4. search.
Theorem nstep_det :
forall E R1 R2, {nstep E (abs R1)} -> {nstep E (abs R2)} -> R1 = R2.
induction on 1. intros. case H1.
case H2.
search.
case H3.
case H2.
case H3.
apply step_det to H3 H5. apply IH to H4 H6. search.
%%
%% Equivalence of semantics
%%
Theorem nstep_lemma :
forall M N R V, {nstep M (abs R)} -> {nstep (R N) V} -> {nstep (app M N) V}.
induction on 1. intros. case H1.
search.
apply IH to H4 H2. search.
Theorem eval_nstep :
forall E V, {eval E V} -> {nstep E V}.
induction on 1. intros. case H1.
search.
apply IH to H2. apply IH to H3. apply nstep_lemma to H4 H5. search.
Theorem step_eval_lemma :
forall A B C, {step A B} -> {eval B C} -> {eval A C}.
induction on 1. intros. case H1.
search.
case H2. apply IH to H3 H4. search.
Theorem nstep_eval :
forall E R, {nstep E (abs R)} -> {eval E (abs R)}.
induction on 1. intros. case H1.
search.
apply IH to H3. apply step_eval_lemma to H2 H4. search.
%%
%% Subject reduction
%%
Theorem sr_eval :
forall E V T, {eval E V} -> {of E T} -> {of V T}.
induction on 1. intros. case H1.
search.
case H2. apply IH to H3 H5. case H7. inst H8 with n1 = N.
cut H9 with H6. apply IH to H4 H10. search.
Theorem sr_step :
forall E1 E2 T, {step E1 E2} -> {of E1 T} -> {of E2 T}.
induction on 1. intros. case H1.
case H2. case H3.
inst H5 with n1 = M. cut H6 with H4.
search.
case H2.
apply IH to H3 H4. search.
Theorem sr_nstep :
forall E1 E2 T, {nstep E1 E2} -> {of E1 T} -> {of E2 T}.
induction on 1. intros. case H1.
search.
apply sr_step to H3 H2.
apply IH to H4 H5. search.
%%
%% Misc
%%
% A cut property for typing judgments
Theorem type_subst : forall L E E' T T', nabla x,
{L, of x T' |- of (E x) T} -> {L |- of E' T'} ->
{L |- of (E E') T}.
intros.
inst H1 with n1 = E'.
cut H3 with H2.
search.
% Self application cannot be simply-typed
Theorem of_self_app_absurd : forall T,
{of (abs (x\ app x x)) T} -> false.
intros. case H1. case H2.
case H3. case H6.
case H5. case H4. case H8.
case H7.
case H9.
case H7.
case H4. case H3. case H5.
% The term (lambda x . x x) (lambda x . x x) does not evaluate to a value
Theorem no_eval : forall V,
{eval (app (abs x\ app x x) (abs x\ app x x)) V} -> false.
induction on 1. intros. case H1.
case H2. apply IH to H3.
% We can also define divergence coinductivly to prove that
% (lambda x . x x) (lambda x . x x) diverges
CoDefine diverge : tm -> prop by
diverge (app M N) := diverge M ;
diverge (app M N) := exists R, {eval M (abs R)} /\ diverge (R N).
Theorem omega_diverge :
diverge (app (abs x\ app x x) (abs x\ app x x)).
coinduction. search.
% More generally we can prove that evaluation and divergence are
% mutually exclusive
Theorem eval_diverge_absurd : forall M V,
{eval M V} -> diverge M -> false.
induction on 1. intros. case H1.
case H2.
case H2.
apply IH to H3 H5.
apply eval_det to H3 H5. apply IH to H4 H6.
