sig stlc-weak-norm. kind tm, ty type. type app tm -> tm -> tm. type abs ty -> (tm -> tm) -> tm. type top ty. type arrow ty -> ty -> ty. type value tm -> o. type of tm -> ty -> o. type step, steps tm -> tm -> o.

module stlc-weak-norm. value (abs A R). of (app M N) B :- of M (arrow A B), of N A. of (abs A R) (arrow A B) :- pi x\ of x A => of (R x) B. step (app M N) (app M' N) :- step M M'. step (app M N) (app M N') :- value M, step N N'. step (app (abs A R) M) (R M) :- value M. steps M M. steps M N :- step M P, steps P N.

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

%% %% 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. Theorem reduce_of : forall A M, reduce M A -> {of M A}. %% Properties of evaluation Theorem absurd_step_value : forall V M, {step V M} -> {value V} -> false. 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}. % 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}. Theorem steps_app_value : forall M N R, {value M} -> {steps N R} -> {steps (app M N) (app M R)}. Theorem halt_step_forward : forall M N, halts M -> {step M N} -> halts N. Theorem halt_step_backward : forall M N, halts N -> {step M N} -> halts M. 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. 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.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. 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 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. 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. 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.