%% Girard's proof of strong normalization of the simply-typed lambda-calculus
%%
%% This is based on the presentation in Girard's Proofs and Types.
Specification "stlc-strong-norm".
Close tm, ty.
%% Conventions:
%% Types: A, B, C
%% Terms: M, N, P, R, U, V
%% Contexts: L, K
Define sn : tm -> prop by
sn M := forall N, {step M N} -> sn N.
Define neutral : tm -> prop by
neutral M := forall A R, M = abs A R -> false.
%% Reduce is the logical relation used to prove normalization.
%%
%% This definition uses itself recursively in a negative context (the
%% left side of an implication). In order to guarantee consistency of
%% the system we must ensure this definition is stratified. Note the
%% second argument to reduce is strictly smaller in the (negative)
%% recursive occurrence, thus the definition is indeed stratified.
Define reduce : tm -> ty -> prop by
reduce M top := {of M top} /\ sn M ;
reduce M (arrow A B) :=
{of M (arrow A B)} /\
(forall U, reduce U A -> reduce (app M U) B).
Theorem reduce_of : forall A M, reduce M A -> {of M A}.
intros. case H1.
search.
search.
% ctx defines the context of "of M A" judgments. The judgment {ty A}
% ensures that all types in the context are well-formed, e.g. they do
% not contain nominal constants.
Define ctx : olist -> prop by
ctx nil ;
nabla x, ctx (of x A :: L) := {ty A} /\ ctx L.
Define name : tm -> prop by
nabla x, name x.
Theorem ctx_member : forall E L,
ctx L -> member E L -> exists X A, E = of X A /\ name X /\ {ty A}.
induction on 1. intros. case H1.
case H2.
case H2.
search.
apply IH to H4 H5. search.
Theorem ty_ignores_ctx : forall L A,
ctx L -> {L |- ty A} -> {ty A}.
induction on 2. intros. case H2.
search.
apply IH to H1 H3. apply IH to H1 H4. search.
apply ctx_member to H1 H4. case H3.
% Some nice inversion lemmas for typing judgements in a non-empty context
Theorem case_of_app : forall L M N B,
ctx L -> {L |- of (app M N) B} ->
exists A, {L |- of M (arrow A B)} /\ {L |- of N A}.
intros. case H2.
search.
apply ctx_member to H1 H4. case H5. case H3.
Theorem case_of_abs : forall L M A B,
ctx L -> {L |- of (abs A M) B} ->
exists C, B = arrow A C /\ {ty A} /\ nabla x, {L, of x A |- of (M x) C}.
intros. case H2.
apply ty_ignores_ctx to H1 H3. search.
apply ctx_member to H1 H4. case H5. case H3.
% Subject reduction - generalized version
Theorem of_step_ext : forall L M N A,
ctx L -> {L |- of M A} -> {step M N} -> {L |- of N A}.
induction on 3. intros. case H3.
apply case_of_app to H1 H2. apply IH to H1 H5 H4. search.
apply case_of_app to H1 H2. apply IH to H1 H6 H4. search.
apply case_of_app to H1 H2. apply case_of_abs to H1 H4.
inst H7 with n1 = M1. cut H8 with H5. search.
apply case_of_abs to H1 H2. apply IH to _ H6 H4. search.
Theorem of_step : forall M N A,
{of M A} -> {step M N} -> {of N A}.
intros. apply of_step_ext to _ H1 H2. search.
Theorem sn_step : forall M N,
sn M -> {step M N} -> sn N.
intros. case H1. apply H3 to H2. search.
% CR2
Theorem reduce_step : forall M N A,
reduce M A -> {step M N} -> reduce N A.
induction on 1. intros. case H1.
apply of_step to H3 H2. apply sn_step to H4 H2. search.
unfold.
apply of_step to H3 H2. search.
intros. apply H4 to H5. apply IH to H6 _. search.
Theorem sn_app_c : forall M,
sn (app M c) -> sn M.
induction on 1. intros. case H1.
unfold. intros.
assert {step (app M c) (app N c)}.
apply H2 to H4. apply IH to H5. search.
% CR1 and CR3 are mutually recursive,
Theorem cr1_cr3 : forall A,
{ty A} ->
(forall M, reduce M A -> sn M)
/\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) ->
reduce M A).
induction on 1. intros. split*.
% CR1
intros. case H2.
% Atomic case
search.
% Arrow case
case H1.
assert 0 (neutral c).
unfold. intros. case H7.
assert {of c A1}.
assert 0 (forall P, {step c P} -> reduce P A1).
intros. case H9.
apply IH to H5.
apply H11 to H7 H8 H9.
apply H4 to H12.
apply IH to H6.
apply H14 to H13.
apply sn_app_c to H16. search.
% CR3
intros. case H1.
% Atomic type
unfold.
search.
unfold. intros.
apply H5 to H6. apply H2 to H7. search.
% Arrow type
unfold.
search.
intros.
apply IH to H6.
apply H9 to H8.
% We want to induct on (sn U) so we have to abstract the
% variable U out entirely.
assert forall U, sn U -> reduce U A1 -> reduce (app M U) B.
induction on 1. intros. case H12.
assert forall P, {step (app M U1) P} -> reduce P B.
intros. case H15.
apply H5 to H16. case H17.
apply H19 to H13. search.
apply H14 to H16. apply reduce_step to H13 H16.
apply IH1 to H17 H18. search.
case H3. apply H16 to _.
assert 0 neutral (app M U1).
unfold. intros. case H16.
assert {of (app M U1) B}.
apply reduce_of to H13. search.
apply IH to H7.
apply H19 to H16 H17 H15. search.
apply H12 to H11 H8. search.
% CR1
Theorem reduce_sn : forall A M,
{ty A} -> reduce M A -> sn M.
intros. apply cr1_cr3 to H1. apply H3 to H2. search.
% CR3
Theorem neutral_step_reduce : forall A M,
neutral M -> {of M A} -> {ty A} ->
(forall P, {step M P} -> reduce P A) ->
reduce M A.
intros. apply cr1_cr3 to H3. apply H6 to H1 H2 H4. search.
Theorem of_ty_ext : forall L M A,
ctx L -> {L |- of M A} -> {ty A}.
induction on 2. intros. case H2.
apply IH to H1 H3. case H5. search.
apply ty_ignores_ctx to H1 H3. apply IH to _ H4. search.
apply ty_ignores_ctx to H1 H3. search.
apply ctx_member to H1 H4. case H5. case H3. search.
Theorem of_ty : forall M A,
{of M A} -> {ty A}.
intros. apply of_ty_ext to _ H1. search.
Theorem reduce_const : forall C,
{ty C} -> reduce c C.
intros.
assert 0 (neutral c).
unfold. intros. case H2.
assert (forall P, {step c P} -> reduce P C).
intros. case H3.
apply neutral_step_reduce to H2 _ H1 H3. search.
Theorem abs_step_reduce_lemma : forall U M A B,
sn U -> sn (M c) -> reduce U A ->
(forall V, reduce V A -> reduce (M V) B) ->
{of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B.
induction on 1. induction on 2. intros.
assert (forall P, {step (app (abs A M) U) P} -> reduce P B).
intros. case H6.
% Case 1: (app (abs A M) U) -> (app M' U)
case H7. inst H8 with n1 = c.
case H2. apply H10 to H9.
apply IH1 to H1 H11 H3 _ _ with M = R', B = B.
apply of_step to H5 _. search.
intros. apply H4 to H12.
inst H8 with n1 = V.
apply reduce_step to H13 H14. search.
search.
% Case 2: (app (abs A M) U) -> (app (abs A M) N')
case H1. apply H8 to H7.
apply reduce_step to H3 H7.
apply IH to H9 H2 H10 H4 H5 with M = M. search.
% Case 3: (app (abs A M) U) -> (M U)
apply H4 to H3. search.
assert 0 neutral (app (abs A M) U).
unfold. intros. case H7.
assert {of (app (abs A M) U) B}.
apply reduce_of to H3. search.
apply of_ty to H8.
apply neutral_step_reduce to H7 H8 H9 H6. search.
Theorem abs_step_reduce : forall M A B,
{of (abs A M) (arrow A B)} ->
(forall V, reduce V A -> reduce (M V) B) ->
reduce (abs A M) (arrow A B).
intros. unfold.
search.
intros.
apply of_ty to H1. case H4.
apply reduce_const to H5.
apply H2 to H7.
apply reduce_sn to H5 H3.
apply reduce_sn to H6 H8.
apply abs_step_reduce_lemma to H9 H10 H3 H2 H1 with M = M.
search.
%% Properties about nominal constants, e.g. where they can and cannot occur.
% A term is closed if it can be typed in the empty context
Define closed : tm -> prop by
closed M := exists A, {of M A}.
Theorem member_prune : forall (L:olist) E, nabla (x:tm),
member (E x) L -> exists F, E = y\F.
induction on 1. intros. case H1.
search.
apply IH to H2. search.
% A term cannot contain a nominal variable which does not appear in
% its typing context L.
Theorem prune_of : forall L R A, nabla (x:tm),
ctx L -> {L |- of (R x) A} -> exists M, R = y\M.
induction on 2. intros. case H2.
apply IH to H1 H3. apply IH to H1 H4. search.
apply ty_ignores_ctx to H1 H3.
apply IH to _ H4. search.
search.
apply member_prune to H4.
apply ctx_member to H1 H4. case H5. case H3. search.
% Closed terms cannot contain any nominal constants
Theorem prune_closed : forall R, nabla (x:tm),
closed (R x) -> exists M, R = y\M.
intros. case H1. apply prune_of to _ H2. search.
Theorem reduce_closed : forall M A, reduce M A -> closed M.
intros. apply reduce_of to H1. search.
Theorem prune_reduce : forall R A, nabla (x:tm),
reduce (R x) A -> exists M, R = y\M.
intros. apply reduce_closed to H1. apply prune_closed to H2. search.
%% Now we need to state the generalize theorem. This will require reasoning
%% about all possible closed instantiations of an open term.
% Suppose that {L |- of M A} is true. Then M is an open term with nominal
% constants that are listed in L. The judgment "subst L M N" holds for all
% instantiations N of the nominal constants in M with terms that satisfy
% the reduce relation for their respective types. The key to defining this
% judgment is the use of nabla in the head of a definition which extracts
% a nominal constant from L and M. The definition of subst then substitutes
% for this nominal constant and continues processing the list L.
Define subst : olist -> tm -> tm -> prop by
subst nil M M ;
nabla x, subst (of x A :: L) (R x) M :=
exists U, reduce U A /\ subst L (R U) M.
% Subst on a closed term has no effect
Theorem closed_subst : forall L M N,
closed M -> subst L M N -> M = N.
induction on 2. intros. case H2.
search.
apply prune_closed to H1.
apply IH to H1 H4. search.
Theorem subst_const : forall L M,
subst L c M -> M = c.
induction on 1. intros. case H1.
search.
apply IH to H3. search.
Theorem subst_var : forall L M N A,
ctx L -> member (of M A) L -> subst L M N -> reduce N A.
induction on 1. intros. case H1.
case H2.
case H2.
case H3. apply reduce_closed to H6.
apply closed_subst to H8 H7. search.
case H3. apply member_prune to H6.
apply IH to H5 H6 H8. search.
Theorem subst_app : forall L M N R,
ctx L -> subst L (app M N) R ->
exists MR NR, R = app MR NR /\ subst L M MR /\ subst L N NR.
induction on 1. intros. case H1.
case H2. search.
case H2. apply IH to H4 H6. search.
% This theorem has a {ty A} hypothesis to ensure that no nominal variables
% can appear in A and thus substitutions do not affect A
Theorem subst_abs : forall L M R A,
ctx L -> subst L (abs A M) R -> {ty A} ->
exists MR, R = abs A MR /\
(forall U, reduce U A ->
nabla x, subst (of x A :: L) (M x) (MR U)).
induction on 1. intros. case H1.
case H2. exists M. split.
search.
intros. search.
case H2.
apply IH to H5 H7 H3.
exists MR. split.
search.
intros. apply prune_reduce to H9.
apply H8 to H9. case H10. search.
Theorem subst_preserves_ty : forall L M N A,
ctx L -> subst L M N -> {L |- of M A} -> {of N A}.
induction on 1. intros. case H1.
case H2. search.
case H2.
apply reduce_of to H6. inst H3 with n1 = U. cut H9 with H8.
apply of_ty_ext to _ H3.
apply IH to H5 H7 H10. search.
Theorem strong_norm_ext : forall L M R A,
ctx L -> {L |- of M A} -> subst L M R -> reduce R A.
induction on 2. intros. case H2 (keep).
apply subst_app to H1 H3.
apply IH to H1 H4 H6.
apply IH to H1 H5 H7.
case H8. apply H11 to H9. search.
apply ty_ignores_ctx to H1 H4.
apply subst_abs to H1 H3 H6.
apply subst_preserves_ty to H1 H3 H2.
apply abs_step_reduce to H8 _. intros.
apply ty_ignores_ctx to H1 H4.
apply H7 to H9.
apply IH to _ H5 H11. search.
search.
apply subst_const to H3.
apply ty_ignores_ctx to H1 H4.
apply reduce_const to H5. search.
apply ctx_member to H1 H5. case H6. case H4.
apply subst_var to H1 H5 H3. search.
Theorem strong_norm : forall M A, {of M A} -> sn M.
intros. apply strong_norm_ext to _ H1 _.
apply of_ty to H1.
apply reduce_sn to _ H2. search.
