Girard's proof of strong normalization of the simply-typed lambda-calculus

Executable Specification

[View stlc-strong-norm.sig] [View stlc-strong-norm.mod]
sig stlc-strong-norm.

kind    tm, ty      type.

type    c           tm.
type    app         tm -> tm -> tm.
type    abs         ty -> (tm -> tm) -> tm.

type    top         ty.
type    arrow       ty -> ty -> ty.

type    ty          ty -> o.
type    of          tm -> ty -> o.
type    step        tm -> tm -> o.

module stlc-strong-norm.

ty top.
ty (arrow A B) :- ty A, ty B.

of (app M N) B :- of M (arrow A B), of N A.
of (abs A R) (arrow A B) :- ty A, pi x\ (of x A => of (R x) B).

% We add this since Girard's proof assumes we can always find
% at least one element in the reducability relation
of c A :- ty A.

step (app M N) (app M' N) :- step M M'.
step (app M N) (app M N') :- step N N'.
step (app (abs A R) M) (R M).
step (abs A R) (abs A R') :- pi x\ step (R x) (R' x).

Reasoning

[View stlc-strong-norm.thm]

Click on a command or tactic to see a detailed view of its use.

%%
%% 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}.

% 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}.

Theorem ty_ignores_ctx : forall L A,
  ctx L -> {L |- ty A} -> {ty A}.

% 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}.

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}.

% 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}.

Theorem of_step : forall M N A,
  {of M A} -> {step M N} -> {of N A}.

Theorem sn_step : forall M N,
  sn M -> {step M N} -> sn N.

% CR2
Theorem reduce_step : forall M N A,
  reduce M A -> {step M N} -> reduce N A.

Theorem sn_app_c : forall M,
  sn (app M c) -> sn M.

% 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).

% CR1
Theorem reduce_sn : forall A M,
  {ty A} -> reduce M A -> sn M.

% 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.

Theorem of_ty_ext : forall L M A,
  ctx L -> {L |- of M A} -> {ty A}.

Theorem of_ty : forall M A,
  {of M A} -> {ty A}.

Theorem reduce_const : forall C,
  {ty C} -> reduce c C.

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.


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).

%% 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 E, nabla (x:tm),
  member (E x) L -> exists F, E = y\F.

% 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.

% Closed terms cannot contain any nominal constants
Theorem prune_closed : forall R, nabla (x:tm),
  closed (R x) -> exists M, R = y\M.

Theorem reduce_closed : forall M A, reduce M A -> closed M.

Theorem prune_reduce : forall R A, nabla (x:tm),
  reduce (R x) A -> exists M, R = y\M.

%% 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.

Theorem subst_const : forall L M,
  subst L c M -> M = c.

Theorem subst_var : forall L M N A,
  ctx L -> member (of M A) L -> subst L M N -> reduce N A.

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.

% 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)).

Theorem subst_preserves_ty : forall L M N A,
  ctx L -> subst L M N -> {L |- of M A} -> {of N A}.

Theorem strong_norm_ext : forall L M R A,
  ctx L -> {L |- of M A} -> subst L M R -> reduce R A.

Theorem strong_norm : forall M A, {of M A} -> sn M.