 # stlc-weak-norm.thm

%% Tait's logical relations argument for weak normalization of STLC %% %% This is based on the presentation in Types and Programming %% Languages by Pierce. Specification "stlc-weak-norm". Close tm, ty. %% Conventions: %% Types: A, B, C %% Terms: M, N, P, R %% Values (Terms): V %% Contexts: L Define halts : tm -> prop by halts M := exists V, {steps M V} /\ {value V}. %% 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} /\ halts M ; reduce M (arrow A B) := {of M (arrow A B)} /\ halts M /\ (forall N, reduce N A -> reduce (app M N) B). Theorem reduce_halts : forall A M, reduce M A -> halts M. intros. case H1. search. search. Theorem reduce_of : forall A M, reduce M A -> {of M A}. intros. case H1. search. search. %% Properties of evaluation Theorem absurd_step_value : forall V M, {step V M} -> {value V} -> false. intros. case H2. case H1. Theorem step_det : forall M N P, {step M N} -> {step M P} -> N = P. induction on 1. intros. case H1. case H2. apply IH to H3 H4. search. apply absurd_step_value to H3 H4. case H3. case H2. apply absurd_step_value to H5 H3. apply IH to H4 H6. search. apply absurd_step_value to H4 H5. case H2. case H4. apply absurd_step_value to H5 H3. search. Theorem step_follows_steps : forall M N V, {step M N} -> {steps M V} -> {value V} -> {steps N V}. intros. case H2. apply absurd_step_value to H1 H3. apply step_det to H1 H4. search. % steps is defined by left recursion on step, so this lemma tells us % that it acts right recursively as well Theorem steps_right : forall M N R, {steps M N} -> {step N R} -> {steps M R}. induction on 1. intros. case H1. search. apply IH to H4 H2. search. Theorem steps_app_value : forall M N R, {value M} -> {steps N R} -> {steps (app M N) (app M R)}. induction on 2. intros. case H2. search. apply IH to H1 H4. search. Theorem halt_step_forward : forall M N, halts M -> {step M N} -> halts N. intros. case H1. apply step_follows_steps to H2 H3 H4. search. Theorem halt_step_backward : forall M N, halts N -> {step M N} -> halts M. intros. case H1. search. Theorem of_step_forward : forall M N A, {of M A} -> {step M N} -> {of N A}. induction on 2. intros. case H2. case H1. apply IH to H4 H3. search. case H1. apply IH to H6 H4. search. case H1. case H4. inst H6 with n1 = M1. cut H7 with H5. search. Theorem reduce_step_forward : forall M N A, reduce M A -> {step M N} -> reduce N A. induction on 1. intros. case H1. apply of_step_forward to H3 H2. apply halt_step_forward to H4 H2. search. unfold. apply of_step_forward to H3 H2. search. apply halt_step_forward to H4 H2. search. intros. apply H5 to H6. apply IH to H7 _. search. Theorem reduce_steps_forward : forall M N A, reduce M A -> {steps M N} -> reduce N A. induction on 2. intros. case H2. search. apply reduce_step_forward to H1 H3. apply IH to H5 H4. search. Theorem reduce_step_backward : forall M N A, reduce N A -> {step M N} -> {of M A} -> reduce M A. induction on 1. intros. case H1. apply halt_step_backward to H5 H2. search. unfold. search. apply halt_step_backward to H5 H2. search. intros. apply H6 to H7. apply reduce_of to H7. apply IH to H8 _ _. search. Theorem reduce_steps_backward : forall M N A, reduce N A -> {steps M N} -> {of M A} -> reduce M A. induction on 2. intros. case H2. search. apply of_step_forward to H3 H4. apply IH to H1 H5 H6. apply reduce_step_backward to H7 H4 H3. search. %% Properties about nominal constants, e.g. where they can and cannot occur. %% Also properties about the contexts of judgments. Define ctx : olist -> prop by ctx nil ; nabla x, ctx (of x A :: L) := ctx L. % 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}. Define name : tm -> prop by nabla x, name x. Theorem ctx_member : forall L E, ctx L -> member E L -> exists X A, E = of X A /\ name X. induction on 1. intros. case H1. case H2. case H2. search. apply IH to H3 H4. search. 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 IH to _ H3. search. apply ctx_member to H1 H4. case H3. apply member_prune to H4. 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 values 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 V, reduce V A /\ {value V} /\ subst L (R V) 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 H5. 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 H5. apply closed_subst to H8 H7. search. case H3. apply member_prune to H5. apply IH to H4 H5 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 H3 H6. search. Theorem subst_abs : forall L M R A, ctx L -> subst L (abs A M) R -> exists MR, R = abs A MR /\ (forall V, reduce V A -> {value V} -> nabla x, subst (of x A :: L) (M x) (MR V)). induction on 1. intros. case H1. case H2. exists M. split. search. intros. search. case H2. apply IH to H3 H6. exists MR. split. search. intros. apply prune_reduce to H8. apply H7 to H8 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 H5. inst H3 with n1 = V. cut H9 with H8. apply IH to H4 H7 H10. search. Theorem weak_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 H12 to H9. search. apply subst_abs to H1 H3. apply subst_preserves_ty to H1 H3 H2. unfold. search. search. intros. % The rest is one single case apply reduce_halts to H7. case H8. apply reduce_steps_forward to H7 H9. apply H5 to H11 H10. apply IH to _ H4 H12. apply steps_app_value to _ H9 with M = abs A1 MR. apply steps_right to H14 _ with R = MR V. apply reduce_of to H7. apply reduce_steps_backward to H13 H15 _. search. apply ctx_member to H1 H5. case H6. case H4. apply subst_var to H1 H5 H3. search. Theorem weak_norm : forall M A, {of M A} -> halts M. intros. apply weak_norm_ext to _ H1 _. apply reduce_halts to H2. search.